4 files changed, 18 insertions, 36 deletions

diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 9397245b..fe17cfa4 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -1153,7 +1153,7 @@ handleStmt defs = \case
   Let n mf mt ar t_ -> do
         af <- addF
         let t__ = maybe id (flip SAnn . af) mt t_
-        (x, t) <- inferTerm (snd n) tr id $ trSExp' $ fromMaybe (SBuiltin "primFix" `SAppV` SLamV t__) $ downS 0 t__
+        (x, t) <- inferTerm (snd n) tr id $ trSExp' $ if usedS n t__ then SBuiltin "primFix" `SAppV` SLamV (substSG0 n t__) else t__
         tellStmtType (fst n) t
         addToEnv n (mkELet (True, n, SData mf, ar) x t, t)
   PrecDef{} -> return ()
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 0ec5e83e..67dbe5fc 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -248,6 +248,8 @@ foldS h g f = fs
 
 freeS = nub . foldS (\_ _ _ -> error "freeS") (\sn _ -> [sn]) mempty 0
 
+usedS n = getAny . foldS (\_ _ _ -> error "usedS") (\sn _ -> Any $ n == sn) mempty 0
+
 mapS' = mapS__ (\_ _ _ -> error "mapS'") (const . SGlobal)
 mapS__ hh gg f2 h = g where
     g i = \case
@@ -261,7 +263,7 @@ mapS__ hh gg f2 h = g where
 
 rearrangeS :: (Int -> Int) -> SExp -> SExp
 rearrangeS f = mapS' (\sn j i -> SVar sn $ if j < i then j else i + f (j - i)) (+1) 0
-
+{-
 substS'' :: Int -> Int -> SExp' a -> SExp' a
 substS'' j' x = mapS' f2 (+1) j'
   where
@@ -269,12 +271,12 @@ substS'' j' x = mapS' f2 (+1) j'
         | j < i = SVar sn j
         | j == i = SVar sn $ x + (j - j')
         | j > i = SVar sn $ j - 1
-
+-}
 substSG j = mapS__ (\_ _ _ -> error "substSG") (\sn x -> if sn == j then SVar sn x else SGlobal sn) (\sn j -> const $ SVar sn j) (+1)
 substSG0 n = substSG n 0 . up1
 
-downS t x | used t x = Nothing
-          | otherwise = Just $ substS'' t (error "impossible") x
+downS n x | usedS n x = Nothing
+          | otherwise = Just x -- $ substS'' t (error "impossible") x
 
 instance Up Void where
     up_ n i = error "up_ @Void"
@@ -744,7 +746,7 @@ data Stmt
     | Class SIName [SExp]{-parameters-} [(SIName, SExp)]{-method names and types-}
     | Instance SIName [Pat]{-parameter patterns-} [SExp]{-constraints-} [Stmt]{-method definitions-}
     | TypeAnn SIName SExp            -- intermediate
-    | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)] SExp)
+    | FunAlt SIName [((Visibility, SExp), Pat)] (Either [(SExp, SExp)]{-guards-} SExp{-no guards-})
     deriving (Show)
 
 pattern Primitive n mf t <- Let n mf (Just t) _ (SBuiltin "undefined") where Primitive n mf t = Let n mf (Just t) (map fst $ fst $ getParamsS t) $ SBuiltin "undefined"
@@ -814,7 +816,7 @@ parseDef =
       where
         mkProj (cn, (Just fs, _))
           = [ Let fn Nothing Nothing [Visible]
-            $ up1{-non-rec-} $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i
+            $ patLam SLabelEnd ge (PCon cn $ replicate (length fs) $ ParPat [PVar (fst cn, "generated_name1")]) $ SVar (fst cn, ".proj") i
             | (i, fn) <- zip [0..] fs]
         mkProj _ = []
 
@@ -844,7 +846,7 @@ funAltDef parseName = do   -- todo: use ns to determine parseName
                 n <- parseSIName parseName
                 localIndentation Gt $ (,) n <$> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|")
     checkPattern fee
-    FunAlt n (map (second $ upP 0 1{-todo: replace n with Var 0-}) tss) <$> parseRHS (dbf' $ fee ++ [n]) "="
+    FunAlt n tss <$> parseRHS (dbf' fee) "="
 
 valueDef :: P Stmt
 valueDef = do
@@ -867,9 +869,9 @@ parseSomeGuards f = do
 
 mkLets :: Bool -> DesugarInfo -> [Stmt]{-where block-} -> SExp{-main expression-} -> SExp{-big let with lambdas; replaces global names with de bruijn indices-}
 mkLets _ _ [] e = e
-mkLets False ge (Let n _ mt ar (downS 0 -> Just x): ds) e
+mkLets False ge (Let n _ mt ar x: ds) e | not $ usedS n x
     = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets False ge ds e)
-mkLets True ge (Let n _ mt ar (downS 0 -> Just x): ds) e
+mkLets True ge (Let n _ mt ar x: ds) e | not $ usedS n x
     = SLet (False, n, SData Nothing, ar) (maybe id (flip SAnn . addForalls {-todo-}[] []) mt x) (substSG0 n $ mkLets True ge ds e)
 mkLets le ge (ValueDef p x: ds) e = patLam id ge p (dbff (getPVars p) $ mkLets le ge ds e) `SAppV` x    -- (p = e; f) -->  (\p -> f) e
 mkLets _ _ (x: ds) e = error $ "mkLets: " ++ show x
@@ -906,7 +908,7 @@ compileFunAlts par ulend lend ds xs = dsInfo >>= \ge -> case xs of
          ++ [ FunAlt n (replicate (length ps) (noTA $ PVar (debugSI "compileFunAlts1", "generated_name0"))) $ Right $ SBuiltin "'Empty" `SAppV` sLit (LString $ "no instance of " ++ snd n ++ " on ???")]
          ++ concat
             [ TypeAnn m (addParamsS (map ((,) Hidden) ps) $ SPi Hidden (foldl SAppV (SGlobal n) $ downToS 0 $ length ps) $ up1 t)
-            : [ FunAlt m p $ Right $ {- SLam Hidden (Wildcard SType) $ up1 $ -} substS'' 0 ic $ up1_ (ic+1) e
+            : [ FunAlt m p $ Right {- $ SLam Hidden (Wildcard SType) $ up1 -} e
               | Instance n' i cstrs alts <- ds, n' == n
               , Let m' ~Nothing ~Nothing ar e <- alts, m' == m
               , let p = zip ((,) Hidden <$> ps) i  -- ++ ((Hidden, Wildcard SType), PVar): []
diff --git a/testdata/typeclass.lc b/testdata/typeclass.lc
index a0ba8068..1ec4ba73 100644
--- a/testdata/typeclass.lc
+++ b/testdata/typeclass.lc
@@ -24,12 +24,12 @@ a /= b = not (a == b)
 instance Eq Bool where
     True == a = a
     False == a = not a
-
+{- todo
 instance Eq t => Eq [t] where
     []   == []   = True
-    (==) (a:as) (b:bs) = a == b -- && as == bs
-    -- TODO  a:as == b:bs = a == b && as == bs
+    a:as == b:bs = a == b && as == bs
     _    == _    = False
+-}
 {-
 Ord = \a -> Eq a & Ord' a       -- so this is an alias, always subst.
 
diff --git a/testdata/typeclass.out b/testdata/typeclass.out
index 43360117..3b1d788d 100644
--- a/testdata/typeclass.out
+++ b/testdata/typeclass.out
@@ -29,7 +29,6 @@ testdata/typeclass.lc 16:14-17:17  Bool->Bool
 testdata/typeclass.lc 17:13-17:17  Bool
 testdata/typeclass.lc 19:7-19:9  Type->Type
 testdata/typeclass.lc 19:7-20:27  Type
-testdata/typeclass.lc 19:7-32:25  V0->V1 | {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 20:5-20:9  {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 20:13-20:14  Type
 testdata/typeclass.lc 20:13-20:27  Type
@@ -44,10 +43,8 @@ testdata/typeclass.lc 22:15-22:16  V5
 testdata/typeclass.lc 22:15-22:19  V4->Bool
 testdata/typeclass.lc 22:17-22:19  {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 22:20-22:21  V2
-testdata/typeclass.lc 24:13-24:17  Type
-testdata/typeclass.lc 24:13-26:23  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
-testdata/typeclass.lc 24:13-28:23  Type | Type->Type | V0->V1
-testdata/typeclass.lc 24:13-32:25  {a : Eq V0} -> V1 -> V2->Bool | {a} -> {b : Eq a} -> a -> a->Bool
+testdata/typeclass.lc 24:13-24:17  Type | Type->Type
+testdata/typeclass.lc 24:13-26:23  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool | {a} -> {b : Eq a} -> a -> a->Bool
 testdata/typeclass.lc 25:5-25:9  Bool
 testdata/typeclass.lc 25:5-26:23  Bool | Bool -> Bool->Bool | Bool->Bool
 testdata/typeclass.lc 25:17-25:18  Bool
@@ -55,20 +52,3 @@ testdata/typeclass.lc 25:17-26:23  Bool->Bool
 testdata/typeclass.lc 26:18-26:21  Bool->Bool
 testdata/typeclass.lc 26:18-26:23  Bool
 testdata/typeclass.lc 26:22-26:23  Bool
-testdata/typeclass.lc 28:10-28:12  Type->Type
-testdata/typeclass.lc 28:10-28:14  Type | Type->Type
-testdata/typeclass.lc 28:10-28:23  Type->Type
-testdata/typeclass.lc 28:13-28:14  Type
-testdata/typeclass.lc 28:22-28:23  Type
-testdata/typeclass.lc 28:22-32:25  ({a : Eq V0} -> V1 -> V2->Bool) -> {e : Eq V1} -> V2 -> V3->Bool
-testdata/typeclass.lc 29:20-29:24  Bool
-testdata/typeclass.lc 29:20-32:25  Bool | List V0 -> Bool | List V1 -> List V2 -> Bool | List V2 -> Bool | a:Type -> {b : Eq a} -> List a -> List a -> Bool
-testdata/typeclass.lc 30:18-30:22  List V7
-testdata/typeclass.lc 30:18-32:25  Bool | List V1 -> Bool | V0 -> List V1 -> Bool
-testdata/typeclass.lc 30:26-30:27  V7
-testdata/typeclass.lc 30:26-30:30  V6->Bool
-testdata/typeclass.lc 30:26-30:32  Bool | List V1 -> Bool | V0 -> List V1 -> Bool
-testdata/typeclass.lc 30:26-32:25  List V3 -> Bool
-testdata/typeclass.lc 30:28-30:30  {a} -> {b : Eq a} -> a -> a->Bool
-testdata/typeclass.lc 30:31-30:32  V3
-testdata/typeclass.lc 32:20-32:25  Bool | List V1 -> Bool | V0 -> List V1 -> Bool