mutual function definitions

7 files changed, 113 insertions, 66 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 27bd6372..487cc4cc 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -35,7 +35,7 @@ data CaseFunName   = CaseFunName   FName Type Int{-num of parameters-}
 data TyCaseFunName = TyCaseFunName FName Type
 
 data FunDef
-    = DeltaDef !Int{-arity-} ([Exp] -> Exp)
+    = DeltaDef !Int{-arity-} (FreeVars -> [Exp] -> Exp)
     | NoDef
     | ExpDef Exp
 
@@ -245,7 +245,7 @@ mkOrdering x = case x of
 conTypeName :: ConName -> TyConName
 conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n
 
-mkFun_ _ (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f $ reverse as
+mkFun_ md (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f md $ reverse as
 mkFun_ md f xs y = Neut $ Fun_ md f xs $ hnf y
 
 mkFun :: FunName -> [Exp] -> Exp -> Exp
@@ -293,6 +293,7 @@ down t x | usedVar t x = Nothing
          | otherwise = Just $ subst_ t mempty (error $ "impossible: down" ++ ppShow (t,x, getFreeVars x) :: Exp) x
 
 instance Eq Exp where
+    Neut a == Neut a' = a == a'         -- try to compare by structure before reduction
     Reduced a == a' = a == a'
     a == Reduced a' = a == a'
     Lam a == Lam a' = a == a'
@@ -301,12 +302,11 @@ instance Eq Exp where
     TyCon a b == TyCon a' b' = (a, b) == (a', b')
     TType_ f == TType_ f' = f == f'
     ELit l == ELit l' = l == l'
-    Neut a == Neut a' = a == a'
     RHS a == RHS a' = a == a'
     _ == _ = False
 
 instance Eq Neutral where
-    Fun f a _ == Fun f' a' _ = (f, a) == (f', a')
+    Fun f a _ == Fun f' a' _ = (f, a) == (f', a')       -- try to compare by structure before reduction
     ReducedN a == a' = a == Neut a'
     a == ReducedN a' = Neut a == a'
     CaseFun_ a b c == CaseFun_ a' b' c' = (a, b, c) == (a', b', c')
@@ -323,7 +323,7 @@ instance Subst Exp Exp where
             substNeut e | dbGE i e = Neut e
             substNeut e = case e of
                 Var_ k              -> case compare k i of GT -> Var $ k - 1; LT -> Var k; EQ -> up (i - i0) x
-                CaseFun_ s as n     -> evalCaseFun s (f i <$> as) (substNeut n)
+                CaseFun__ fs s as n -> evalCaseFun (adjustDB i fs) s (f i <$> as) (substNeut n)
                 TyCaseFun_ s as n   -> evalTyCaseFun s (f i <$> as) (substNeut n)
                 App_ a b            -> app_ (substNeut a) (f i b)
                 Fun_ md fn xs v     -> mkFun_ (adjustDB i md) fn (f i <$> xs) $ f i v
@@ -426,14 +426,26 @@ showNth n = show n ++ f (n `div` 10 `mod` 10) (n `mod` 10)
     f _ 3 = "rd"
     f _ _ = "th"
 
+pattern FFix f <- Fun (FunName FprimFix _ _ _) [f, _] _
+
+getFixLam (Lam (Neut (Fun s@(FunName _ loc _ _) xs _)))
+    | loc > 0
+    , (h, v) <- splitAt loc $ reverse xs
+    , Neut (Var_ 0) <- last h
+    = Just (s, v)
+getFixLam _ = Nothing
+
 instance MkDoc Neutral where
     mkDoc pr@(reduce, body) = \case
         CstrT' t a b        -> shCstr (mkDoc pr a) (mkDoc pr (ET b t))
-        Fun (FunName _ _ (ExpDef d) _) xs _ | body -> mkDoc (reduce, False) (foldl app_ d xs)
-        Fun (FunName _ _ (DeltaDef _ d) _) xs _ | body -> text "<<builtin>>"
-        Fun (FunName _ _ NoDef _) xs _ | body -> text "<<builtin>>"
+        Fun (FunName _ _ (ExpDef d) _) xs _ | body -> mkDoc (reduce, False) (foldl app_ d $ reverse xs)
+        FFix (getFixLam -> Just (s, xs)) | not body -> foldl DApp (pShow s) $ mkDoc pr <$> xs
+        FFix f {- | body -} -> foldl DApp "primFix" [{-pShow t -}"_", mkDoc pr f]
+        Fun (FunName _ _ (DeltaDef n _) _) _ _ | body -> text $ "<<delta function with arity " ++ show n ++ ">>"
+        Fun (FunName _ _ NoDef _) _ _ | body -> "<<builtin>>"
         ReducedN a | reduce -> mkDoc pr a
-        Fun s xs _          -> foldl DApp (pShow s) (mkDoc pr <$> reverse xs)
+        Fun s@(FunName _ loc _ _) xs _ -> foldl DApp ({-foldl DHApp (-}pShow s{-) h-}) v
+          where (h, v) = splitAt loc $ mkDoc pr <$> reverse xs
         Var_ k              -> shVar k
         App_ a b            -> mkDoc pr a `DApp` mkDoc pr b
         CaseFun_ s@(CaseFunName _ _ p) xs n | body -> text $ "<<case function of a type with " ++ show p ++ " parameters>>"
@@ -441,6 +453,7 @@ instance MkDoc Neutral where
         TyCaseFun_ _ _ _ | body -> text "<<type case function>>"
         TyCaseFun_ s [m, t, f] n  -> foldl DApp (pShow s) (mkDoc pr <$> [m, t, Neut n, f])
         TyCaseFun_ s _ n -> error $ "mkDoc TyCaseFun"
+        _ -> "()"
 
 -------------------------------------------------------------------------------- reduction
 
@@ -455,9 +468,19 @@ instance MkDoc Neutral where
 -}
 
 pattern FunName' a t <- FunName a _ _ t
-  where FunName' a t = fn
-          where
-            fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t)) $ getFunDef t a $ \xs -> Neut $ Fun fn (reverse xs) delta) t
+  where FunName' a t = mkFunDef a t
+
+
+mkFunDef a@(show -> "primFix") t = fn
+  where
+    fn = FunName a 0 (DeltaDef (length $ fst $ getParams t) fx) t
+    fx s xs = Neut $ Fun_ s fn (reverse xs) $ case xs of
+        _: f: _ -> RHS x where x = f `app_` Neut (Fun_ s fn (reverse xs) $ RHS x)
+        _ -> delta
+
+mkFunDef a t = fn
+  where
+    fn = FunName a 0 (maybe NoDef (DeltaDef (length $ fst $ getParams t) . const) $ getFunDef t a $ \xs -> Neut $ Fun fn (reverse xs) delta) t
 
 getFunDef t s f = case show s of
     "'EqCT"             -> Just $ \case (t: a: b: _)   -> cstr t a b
@@ -541,15 +564,17 @@ getFunDef t s f = case show s of
 
     modF x y = x - fromIntegral (floor (x / y)) * y
 
-evalCaseFun a ps (Con n@(ConName _ i _) _ vs)
+evalCaseFun _ a ps (Con n@(ConName _ i _) _ vs)
     | i /= (-1) = foldl app_ (ps !!! (i + 1)) vs
     | otherwise = error "evcf"
   where
     xs !!! i | i >= length xs = error $ "!!! " ++ ppShow a ++ " " ++ show i ++ " " ++ ppShow n ++ "\n" ++ ppShow ps
     xs !!! i = xs !! i
-evalCaseFun a b (Reduced c) = evalCaseFun a b c
-evalCaseFun a b (Neut c) = CaseFun a b c
-evalCaseFun a b x = error $ "evalCaseFun: " ++ ppShow (a, x)
+evalCaseFun fs a b (Reduced c) = evalCaseFun fs a b c
+evalCaseFun fs a b (Neut c) = Neut $ CaseFun__ fs a b c
+evalCaseFun _ a b x = error $ "evalCaseFun: " ++ ppShow (a, x)
+
+evalCaseFun' a b c = evalCaseFun (getFreeVars c <> foldMap getFreeVars b) a b c
 
 evalTyCaseFun a b (Reduced c) = evalTyCaseFun a b c
 evalTyCaseFun a b (Neut c) = TyCaseFun a b c
diff --git a/src/LambdaCube/Compiler/CoreToIR.hs b/src/LambdaCube/Compiler/CoreToIR.hs
index d24a7b11..353560cd 100644
--- a/src/LambdaCube/Compiler/CoreToIR.hs
+++ b/src/LambdaCube/Compiler/CoreToIR.hs
@@ -865,7 +865,7 @@ mkLam _ = Nothing
 
 mkCon (ExpTV (I.Con s n xs) et vs) = Just (untick $ show s, chain vs (I.conType et s) $ I.mkConPars n et ++ xs)
 mkCon (ExpTV (I.TyCon s xs) et vs) = Just (untick $ show s, chain vs (nType s) xs)
-mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ 0 _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, chain vs (nType s) xs)
+mkCon (ExpTV (I.Neut (I.Fun s@(I.FunName _ loc _{-I.DeltaDef{}-} _) (reverse -> xs) def)) et vs) = Just (untick $ show s, drop loc $ chain vs (nType s) xs)
 mkCon (ExpTV (I.CaseFun s xs n) et vs) = Just (untick $ show s, chain vs (nType s) $ makeCaseFunPars' (mkEnv vs) n ++ xs ++ [I.Neut n])
 mkCon (ExpTV (I.TyCaseFun s [m, t, f] n) et vs) = Just (untick $ show s, chain vs (nType s) [m, t, I.Neut n, f])
 mkCon _ = Nothing
@@ -878,15 +878,28 @@ removeRHS 0 (I.RHS x) = Just x
 removeRHS n (I.Lam x) | n > 0 = I.Lam <$> removeRHS (n-1) x
 removeRHS _ _ = Nothing
 
-mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) 0 (I.ExpDef def_) nt) xs I.RHS{})) ty vs)
+mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs)
     | Just def <- removeRHS (length xs) def_
     , all (supType . tyOf) (r: xs') && n `notElem` ["typeAnn"] && all validChar n
     = Just (untick n +++ intercalate "_" (filter (/="TT") $ map (filter isAlphaNum . plainShow) hs), toExp $ I.ET (foldl I.app_ def hs) (foldl I.appTy nt hs), tyOf r, xs')
   where
     a +++ [] = a
     a +++ b = a ++ "_" ++ b
-    (map (expOf . snd) -> hs, map snd -> xs') = span ((==Hidden) . fst) $ chain' vs nt $ reverse xs
+    (map (expOf . snd) -> hs, map snd -> xs') = splitAt loc $ chain' vs nt $ reverse xs
     validChar = isAlphaNum
+{-
+mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs)
+    | Just def <- removeRHS (length xs) def_
+    , all validChar n
+    = tracePShow (text n, reverse xs, supType . tyOf <$> (r: xs')) Nothing
+  where
+    a +++ [] = a
+    a +++ b = a ++ "_" ++ b
+    (map (expOf . snd) -> hs, map snd -> xs') = splitAt loc $ chain' vs nt $ reverse xs
+    validChar = isAlphaNum
+mkFunc r@(ExpTV (I.Neut (I.Fun (I.FunName (show -> n) loc (I.ExpDef def_) nt) xs I.RHS{})) ty vs)
+         = tracePShow (text n, take loc $ reverse xs) Nothing
+-}
 mkFunc _ = Nothing
 
 chain vs t@(I.Pi Hidden at y) (a: as) = chain vs (I.appTy t a) as
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index e83eb0ea..06849849 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -269,6 +269,9 @@ data SExp' a
     | STyped  a
   deriving (Eq)
 
+sLHS _ (SRHS x) = x
+sLHS n x = SLHS n x
+
 type SExp = SExp' Void
 
 data Binder
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 444dd1b9..089392d1 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -36,7 +36,6 @@ import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DeBruijn
 import LambdaCube.Compiler.Pretty hiding (braces, parens)
 import LambdaCube.Compiler.DesugaredSource hiding (getList)
-import LambdaCube.Compiler.Statements (addFix)
 import LambdaCube.Compiler.Core
 import LambdaCube.Compiler.InferMonad
 
@@ -49,20 +48,15 @@ varType err n_ env = f n_ env where
     f n (ELet2 _ (ET x t) es) = if n == 0 then (BLam Visible{-??-}, up 1 t) else second (up 1) $ f (n-1) es
     f n e = either (error $ "varType: " ++ err ++ "\n" ++ show n_ ++ "\n" ++ ppShow env) (f n) $ parent e
 
-mkELet n x xt env = term
+mkELet n x xt env = mkFun fn (Var <$> reverse vs) x
   where
-    vs = nub . concat $ grow [] mempty $ free x <> free xt
     fn = FunName (mkFName n) (length vs) (ExpDef $ foldr addLam x vs) (foldr addPi xt vs)
 
-    term = mkFun fn (Var <$> reverse vs) $ getFix x 0
-
-    getFix (Lam_ db z) i = Lam_ db $ getFix z (i+1)
-    getFix (DFun FprimFix _ [_, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f
-    getFix x _ = x
-
     addLam v x = Lam $ rMove v 0 x
     addPi v x = Pi Visible (snd $ varType "mkELet" v env) $ rMove v 0 x
 
+    vs = nub . concat $ grow [] mempty $ free x <> free xt
+
     -- TODO: avoid infinite loop if variable types refer each-other mutually
     grow accu acc s
         | Set.null s = accu
@@ -101,7 +95,8 @@ envDoc x m = case x of
     CheckIType t ts     -> envDoc ts $ shAnn m (text "??") -- mkDoc ts' t
 --    CheckSame t ts      -> envDoc ts $ shCstr <$> m <*> mkDoc ts' t
     CheckAppType si h t te b -> envDoc (EApp1 si h (CheckType_ (sourceInfo b) t te) b) m
-    ERHS ts             -> envDoc ts $ shApp Visible (text "rhs") m
+    ERHS ts             -> envDoc ts $ shApp Visible "rhs" m
+    ELHS n ts           -> envDoc ts $ shApp Visible ("lhs" `DApp` pShow n) m
     x   -> error $ "envDoc: " ++ ppShow x
 
 instance MkDoc a => MkDoc (CEnv a) where
@@ -162,6 +157,7 @@ data Env
     | ELet2 SIName ExpType Env
     | EGlobal
     | ERHS Env
+    | ELHS SIName Env
 
     | EAssign Int ExpType Env
     | CheckType_ SI Type Env
@@ -185,6 +181,7 @@ parent = \case
 --    CheckSame _ x        -> Right x
     CheckAppType _ _ _ x _ -> Right x
     ERHS x               -> Right x
+    ELHS _ x             -> Right x
     EGlobal              -> Left ()
 
 -------------------------------------------------------------------------------- simple typing
@@ -230,6 +227,8 @@ substTo i x = subst i x . up1_ (i+1)
 mkLet x xt y = subst 0 x y
 --mkLet x xt (ET y yt) = ET (Let (ET x xt) y) yt
 
+ET a at `etApp` e = ET (app_ a e) (appTy at e)
+
 inferN_ :: forall m . Monad m => (forall a . String -> String -> IM m a -> IM m a) -> Env -> SExp2 -> IM m ExpType'
 inferN_ tellTrace = infer  where
 
@@ -238,7 +237,7 @@ inferN_ tellTrace = infer  where
         Parens x        -> infer te x
         SAnn x t        -> checkN (CheckIType x te) t TType
         SRHS x          -> infer (ERHS te) x
-        SLHS n x        -> infer te x
+        SLHS n x        -> infer (ELHS n te) x
         SVar sn i       -> focusTell te exp $ ET (Var i) $ snd $ varType "C2" i te
         SLit si l       -> focusTell te exp $ ET (ELit l) (nType l)
         STyped et       -> focusTell' te exp et
@@ -252,6 +251,9 @@ inferN_ tellTrace = infer  where
 
     checkN_ te (Parens e) t = checkN_ te e t
     checkN_ te e t
+        | SBuiltin "primFix" `SAppV` (SLam Visible _ f) <- e = do
+            pf <- getDef te mempty "primFix"
+            checkN (EBind2 (BLam Visible) t $ EApp2 mempty Visible (pf `etApp` t) te) f $ up 1 t
         | x@(SGlobal (sName -> MatchName n)) `SAppV` SLamV (Wildcard _) `SAppV` a `SAppV` SVar siv v `SAppV` b <- e
             = infer te $ x `SAppV` SLam Visible SType (STyped (ET (subst (v+1) (Var 0) $ up 1 t) TType)) `SAppV` a `SAppV` SVar siv v `SAppV` b
             -- temporal hack
@@ -269,9 +271,9 @@ inferN_ tellTrace = infer  where
             = infer te $ x `SAppV` SLamV (SLamV (STyped (subst (n'+2) (Var 1) $ up1_ (n'+3) $ up 2 t, TType))) `SAppV` a `SAppV` b `SAppV` SVar siv v
 -}
         | SRHS x <- e = checkN (ERHS te) x t
-        | SLHS n x <- e = checkN te x t
+        | SLHS n x <- e = checkN (ELHS n te) x t
         | SApp_ si h a b <- e = infer (CheckAppType si h t te b) a
-        | SLam h a b <- e, Pi h' x y <- t, h == h'  = do
+        | SLam h a b <- e, Pi h' x y <- t, h == h' = do
 --            tellType e t
             let same = checkSame te a x
             if same then checkN (EBind2 (BLam h) x te) b $ hnf y else error $ "checkSame:\n" ++ ppShow a ++ "\nwith\n" ++ showEnvExp te (ET x TType)
@@ -311,6 +313,7 @@ inferN_ tellTrace = infer  where
     focus_ :: Env -> ExpType -> IM m ExpType'
     focus_ env eet@(ET e et) = tellTrace "focus" (showEnvExp env eet) $ case env of
         ERHS te -> focus_ te (ET (RHS $ hnf e) et)
+        ELHS n te -> focus_ te (ET (mkELet n e et te) et)
 --        CheckSame x te -> focus_ (EBind2_ (debugSI "focus_ CheckSame") BMeta (cstr x e) te) $ up 1 eet
         CheckAppType si h t te b   -- App1 h (CheckType t te) b
             | Pi h' x (down 0 -> Just y) <- et, h == h' -> case t of
@@ -325,7 +328,7 @@ inferN_ tellTrace = infer  where
             | otherwise -> infer (CheckType_ (sourceInfo b) (Var 2) $ cstr' h (up 2 et) (Pi Visible (Var 1) (Var 1)) (up 2 e) $ EBind2_ (sourceInfo b) BMeta TType $ EBind2_ (sourceInfo b) BMeta TType te) (up 3 b)
           where
             cstr' h x y e = EApp2 mempty h (ET (evalCoe (up 1 x) (up 1 y) (Var 0) (up 1 e)) (up 1 y)) . EBind2_ (sourceInfo b) BMeta (cstr_ TType x y)
-        ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet (mkELet ln x xt te){-let-} xt eet{-in-}
+        ELet2 ln (ET x{-let-} xt) te -> focus_ te $ mkLet x{-let-} xt eet{-in-}
         CheckIType x te -> checkN te x $ hnf e
         CheckType_ si t te
             | hArgs et > hArgs t
@@ -333,7 +336,7 @@ inferN_ tellTrace = infer  where
             | hArgs et < hArgs t, Pi Hidden t1 t2 <- t
                             -> focus_ (CheckType_ si t2 $ EBind2 (BLam Hidden) t1 te) eet
             | otherwise    -> focus_ (EBind2_ si BMeta (cstr_ TType t et) te) $ up 1 eet
-        EApp2 si h (ET a at) te    -> focusTell te si $ ET (app_ a e) (appTy at e)        --  h??
+        EApp2 si h a te    -> focusTell te si $ a `etApp` e        --  h??
         EBind1 si h te b   -> infer (EBind2_ (sourceInfo b) h e te) b
         EBind2_ si (BLam h) a te -> focus_ te $ lamPi h a eet
         EBind2_ si (BPi h) a te -> focusTell te si $ ET (Pi h a e) TType
@@ -344,6 +347,7 @@ inferN_ tellTrace = infer  where
         ELet1 le te b{-in-} -> infer (ELet2 le (replaceMetas' eet{-let-}) te) b{-in-}
         EBind2_ si BMeta tt_ te
             | ERHS te'   <- te -> refocus (ERHS $ EBind2_ si BMeta tt_ te') eet
+            | ELHS n te' <- te -> refocus (ELHS n $ EBind2_ si BMeta tt_ te') eet
             | Unit <- tt    -> refocus te $ subst 0 TT eet
             | Empty msg <- tt -> throwError' $ ETypeError (text msg) si
             | CW (hnf -> T2 x y) <- tt, let te' = EBind2_ si BMeta (up 1 $ cw y) $ EBind2_ si BMeta (cw x) te
@@ -377,6 +381,7 @@ inferN_ tellTrace = infer  where
 
         EAssign i b te -> case te of
             ERHS te'     -> refocus' (ERHS $ EAssign i b te') eet
+            ELHS n te'   -> refocus' (ELHS n $ EAssign i b te') eet
             EBind2_ si h x te' | i > 0, Just b' <- down 0 b
                               -> refocus' (EBind2_ si h (subst (i-1) (expr b') x) (EAssign (i-1) b' te')) eet
             ELet2 le x te' | i > 0, Just b' <- down 0 b
@@ -413,7 +418,6 @@ inferN_ tellTrace = infer  where
         _ -> case eet of
             MEnd x -> throwError' $ ErrorMsg $ "focus todo:" <+> pShow x
             _ -> case env of
---                EBind2 h _ _ -> throwError' $ ErrorMsg $ "focus checkMetas" <+> pShow h
                 _ -> throwError' $ ErrorMsg $ "focus checkMetas:" <$$> pShow env <$$> "---" <$$> pShow eet
       where
         refocus_ :: (Env -> CEnv ExpType -> IM m ExpType') -> Env -> CEnv ExpType -> IM m ExpType'
@@ -463,7 +467,7 @@ recheck' sn e (ET x xt) = ET (recheck_ "main" (checkEnv e) (ET x xt)) xt
             -> checkApps "a" [] zt (Neut . App__ md a' . head) te at [b]
         ET (Con_ md s n as) zt      -> checkApps (ppShow s) [] zt (Con_ md s n . drop (conParams s)) te (conType zt s) $ mkConPars n zt ++ as
         ET (TyCon_ md s as) zt      -> checkApps (ppShow s) [] zt (TyCon_ md s) te (nType s) as
-        ET (CaseFun s@(CaseFunName _ t pars) as n) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
+        ET (Neut (CaseFun__ fs s@(CaseFunName _ t pars) as n)) zt -> checkApps (ppShow s) [] zt (\xs -> evalCaseFun fs s (init $ drop pars xs) (last xs)) te (nType s) (makeCaseFunPars te n ++ as ++ [Neut n])
         ET (TyCaseFun s [m, t, f] n) zt  -> checkApps (ppShow s) [] zt (\[m, t, n, f] -> evalTyCaseFun s [m, t, f] n) te (nType s) [m, t, Neut n, f]
         ET (Neut (Fun_ md f a x)) zt -> checkApps ("lab-" ++ show f ++ ppShow a ++ "\n" ++ ppShow (nType f)) [] zt (\xs -> Neut $ Fun_ md f (reverse xs) x) te (nType f) $ reverse a   -- TODO: recheck x
         ET (Let (ET x xt) y) zt -> Let (recheck'' "let" te $ ET x xt) $ recheck_ "let_in" te $ ET y (Pi Visible xt $ up1 zt)  -- TODO
@@ -493,9 +497,9 @@ handleStmt = \case
         addToEnv n $ flip ET t $ lamify t $ DFun (mkFName n) t
   StLet n mt t_ -> do
         let t__ = maybe id (flip SAnn) mt t_
-        ET x t <- inferTerm n $ trSExp' $ addFix n t__
+        ET x t <- inferTerm n $ trSExp' t__
         tellType (sourceInfo n) t
-        addToEnv n (ET (mkELet n x t EGlobal) t)
+        addToEnv n (ET x t)
 {-        -- hack
         when (snd (getParams t) == TType) $ do
             let ps' = fst $ getParams t
@@ -551,7 +555,7 @@ handleStmt = \case
             )
         return (e1, es, tcn, cfn, ct, cons)
 
-    e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun cfn (init $ drop (length ps) xs) (last xs)) ct
+    e2 <- addToEnv (SIName (sourceInfo s) $ CaseName (sName s)) $ ET (lamify ct $ \xs -> evalCaseFun' cfn (init $ drop (length ps) xs) (last xs)) ct
     let ps' = fst $ getParams vty
         t =   (TType :~> TType)
           :~> addParams ps' (Var (length ps') `app_` TyCon tcn (downTo 0 $ length ps'))
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index 79975251..7ca3d5cb 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -249,7 +249,7 @@ parseTermProj = level parseTermAtom $ \t ->
 parseTermAtom =
          mkLit <$> try_ "literal" parseLit
      <|> Wildcard (Wildcard SType) <$ reserved "_"
-     <|> mkLets <$ reserved "let" <*> parseDefs <* reserved "in" <*> setR parseTermLam
+     <|> mkLets <$ reserved "let" <*> parseDefs sLHS <* reserved "in" <*> setR parseTermLam
      <|> SGlobal <$> lowerCase
      <|> SGlobal <$> upperCase_
      <|> braces (mkRecord <$> commaSep ((,) <$> lowerCase <* symbol ":" <*> setR parseTermLam))
@@ -434,12 +434,12 @@ parseDef =
                     option {-open type family-}[TypeFamily x $ UncurryS ts t] $ do
                         cs <- (reserved "where" >>) $ identation True $ funAltDef Nothing $ mfilter (== x) upperCase
                         -- closed type family desugared here
-                        runCheck $ fmap Stmt <$> compileStmt (compileGuardTrees id . const Nothing) [TypeAnn x $ UncurryS ts t] cs
+                        runCheck $ fmap Stmt <$> compileStmt SLHS (compileGuardTrees id . const Nothing) [TypeAnn x $ UncurryS ts t] cs
              <|> pure <$ reserved "instance" <*> funAltDef Nothing upperCase
              <|> do x <- upperCase
                     (nps, ts) <- telescope $ Just (Wildcard SType)
                     rhs <- deBruijnify nps <$ reservedOp "=" <*> setR parseTermLam
-                    runCheck $ fmap Stmt <$> compileStmt (compileGuardTrees id . const Nothing)
+                    runCheck $ fmap Stmt <$> compileStmt SLHS (compileGuardTrees id . const Nothing)
                         [{-TypeAnn x $ UncurryS ts $ SType-}{-todo-}]
                         [funAlt' x ts (map PVarSimp $ reverse nps) $ noGuards rhs]
  <|> do try_ "typed ident" $ map (uncurry TypeAnn) <$> typedIds addForalls' []
@@ -465,10 +465,10 @@ parseDef =
 
 parseRHS :: String -> BodyParser GuardTrees
 parseRHS tok = do
-    mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs)
+    mkGuards <$> some (reservedOp "|" *> guard) <*> option [] (reserved "where" *> parseDefs sLHS)
   <|> do
     rhs <- reservedOp tok *> setR parseTermLam
-    f <- option id $ mkLets <$ reserved "where" <*> parseDefs
+    f <- option id $ mkLets <$ reserved "where" <*> parseDefs sLHS
     noGuards <$> trackSI (pure $ f rhs)
   where
     guard = do
@@ -482,7 +482,7 @@ parseRHS tok = do
 
     mkGuards gs wh = mkLets_ lLet wh $ mconcat [foldr (uncurry guardNode') (noGuards e) ge | (ge, e) <- gs]
 
-parseDefs = identation True parseDef >>= runCheck . compileStmt' . concat
+parseDefs lhs = identation True parseDef >>= runCheck . compileStmt'_ lhs SRHS SRHS . concat
 
 funAltDef parseOpName parseName = do
     (n, (fee, tss)) <-
@@ -555,7 +555,7 @@ parseModule = do
         { extensions    = exts
         , moduleImports = [(SIName mempty "Prelude", ImportAllBut []) | NoImplicitPrelude `notElem` exts] ++ idefs
         , moduleExports = join $ snd <$> header
-        , definitions   = \ge -> runParse (parseDefs <* eof) (env { desugarInfo = ge }, st)
+        , definitions   = \ge -> runParse (parseDefs SLHS <* eof) (env { desugarInfo = ge }, st)
         }
 
 parseLC :: FileInfo -> Either ParseError Module
diff --git a/src/LambdaCube/Compiler/Pretty.hs b/src/LambdaCube/Compiler/Pretty.hs
index e2ebb5e4..204e4893 100644
--- a/src/LambdaCube/Compiler/Pretty.hs
+++ b/src/LambdaCube/Compiler/Pretty.hs
@@ -320,6 +320,7 @@ infixl 4 `DApp`
 
 pattern DAt x       = DGlue     (InfixR   20) (DText "@") x
 pattern DApp x y    = DSep      (InfixL   10)  x y
+pattern DHApp x y   = DSep      (InfixL   10)  x (DAt y)
 pattern DSemi x y   = DOp ";"   (InfixR (-19)) x y
 pattern DArr_ s x y = DOp s     (InfixR  (-1)) x y      -- -> => .
 pattern DCstr x y   = DOp "~"   (Infix   (-2)) x y
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 178e5505..9d48ffc2 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -49,17 +49,10 @@ mkLets_ mkLet = mkLets' mkLet . concatMap desugarMutual . sortDefs
 
 mkLets' mkLet = f where
     f [] e = e
-    f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt (addFix n x)) (deBruijnify [n] $ f ds e)
+    f (StLet n mt x: ds) e = mkLet n (maybe id (flip SAnn) mt x) (deBruijnify [n] $ f ds e)
     f (PrecDef{}: ds) e = f ds e
     f (x: ds) e = error $ "mkLets: " ++ ppShow x
 
-addFix n x
-    | usedS n x = SBuiltin "primFix" `SAppV` SLamV (deBruijnify [n] x)
-    | otherwise = x
-
-addFix' (StLet n nt nd) = StLet n nt $ addFix n nd
-addFix' x = x
-
 type DefinedSet = Set.Set SName
 
 addForalls :: DefinedSet -> SExp -> SExp
@@ -75,14 +68,14 @@ addForalls defined x = foldl f x [v | v@(sName -> vh:_) <- reverse $ names x, sN
 
 ------------------------------------------------------------------------
 
-compileStmt' = compileStmt'_ SRHS SRHS
+compileStmt' = compileStmt'_ SLHS SRHS SRHS
 
-compileStmt'_ ulend lend ds = fmap concat . sequence $ map (compileStmt (\si vt -> compileGuardTree ulend lend (Just si) vt . mconcat) ds) $ groupBy h ds where
+compileStmt'_ lhs ulend lend ds = fmap concat . sequence $ map (compileStmt lhs (\si vt -> compileGuardTree ulend lend (Just si) vt . mconcat) ds) $ groupBy h ds where
     h (FunAlt n _ _) (FunAlt m _ _) = m == n
     h _ _ = False
 
-compileStmt :: MonadWriter [ParseCheck] m => (SIName -> [(Visibility, SExp)] -> [GuardTrees] -> m SExp) -> [PreStmt] -> [PreStmt] -> m [Stmt]
-compileStmt compilegt ds = \case
+--compileStmt :: MonadWriter [ParseCheck] m => (SIName -> [(Visibility, SExp)] -> [GuardTrees] -> m SExp) -> [PreStmt] -> [PreStmt] -> m [Stmt]
+compileStmt lhs compilegt ds = \case
     [Instance{}] -> return []
     [Class n ps ms] -> do
         cd <- compileStmt' $
@@ -90,7 +83,7 @@ compileStmt compilegt ds = \case
          ++ [ funAlt n (map noTA ps) $ noGuards $ foldr (SAppV2 $ SBuiltin "'T2") (SBuiltin "'CUnit") cstrs | Instance n' ps cstrs _ <- ds, n == n' ]
          ++ [ funAlt n (replicate (length ps) (noTA $ PVarSimp $ dummyName "cst0")) $ noGuards $ SBuiltin "'CEmpty" `SAppV` sLit (LString $ "no instance of " ++ sName n ++ " on ???"{-TODO-})]
         cds <- sequence
-            [ compileStmt'_ SRHS SRHS{-id-}
+            [ compileStmt'_ SLHS SRHS SRHS{-id-}
             $ TypeAnn m (UncurryS (map ((,) Hidden) ps) $ SPi Hidden (SCW $ foldl SAppV (SGlobal n) $ downToS "a2" 0 $ length ps) $ up1 t)
             : as
             | (m, t) <- ms
@@ -106,14 +99,14 @@ compileStmt compilegt ds = \case
     [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]]
     tf@[TypeFamily n t] -> case [d | d@(FunAlt n' _ _) <- ds, n' == n] of
         [] -> return [Primitive n t]
-        alts -> compileStmt compileGuardTrees' [TypeAnn n t] alts
+        alts -> compileStmt lhs compileGuardTrees' [TypeAnn n t] alts
     fs@(FunAlt n vs _: _) -> case groupBy ((==) `on` fst) [(length vs, n) | FunAlt n vs _ <- fs] of
         [gs@((num, _): _)]
           | num == 0 && length gs > 1 -> fail $ "redefined " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd <$> gs)
           | n `elem` [n' | TypeFamily n' _ <- ds] -> return []
           | otherwise -> do
             cf <- compilegt (SIName_ (mconcat [sourceInfo n | FunAlt n _ _ <- fs]) (nameFixity n) $ sName n) vs [gt | FunAlt _ _ gt <- fs]
-            return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ SLHS n cf]
+            return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ lhs n cf]
         fs -> fail $ "different number of arguments of " ++ sName n ++ ":\n" ++ show (vcat $ pShow . sourceInfo . snd . head <$> fs)
     [Stmt x] -> return [x]
   where
@@ -134,21 +127,29 @@ desugarValueDef p e = sequence
     dns = reverse $ getPVars p
     n = mangleNames dns
 
-getLet (StLet x Nothing (SLHS _ (SRHS dx))) = Just (x, dx)
+getLet (StLet x mt dx) = Just (x, mt, dx)
 getLet _ = Nothing
 
 fst' (x, _) = x -- TODO
 
 desugarMutual :: {-MonadWriter [ParseCheck] m => -} [Stmt] -> [Stmt]
-desugarMutual [x] = [x]
-desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do
-    ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy)
+desugarMutual [x@Primitive{}] = [x]
+desugarMutual [x@Data{}] = [x]
+desugarMutual [x@PrecDef{}] = [x]
+desugarMutual [StLet n nt nd] = [StLet n nt $ addFix n nt nd]
+desugarMutual (traverse getLet -> Just (unzip3 -> (ns, ts, ds))) = fst' $ runWriter $ do
+    ss <- compileStmt'_ sLHS SRHS SRHS =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy)
     return $
-        StLet xy Nothing (addFix xy $ SLHS xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
+        StLet xy ty (addFix xy ty $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
   where
+    ty = Nothing -- TODO:  Just $ HList $ foldr BCons BNil $ const (Wildcard SType) <$> ts
     xy = mangleNames ns
 desugarMutual xs = error "desugarMutual"
 
+addFix n nt x
+    | usedS n x = SBuiltin "primFix" `SAppV` SLam Visible (maybe (Wildcard SType) id nt) (deBruijnify [n] x)
+    | otherwise = x
+
 mangleNames xs = SIName (foldMap sourceInfo xs) $ "_" ++ intercalate "_" (sName <$> xs)