3 files changed, 16 insertions, 7 deletions

diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index fb14b4e3..e83eb0ea 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -265,6 +265,7 @@ data SExp' a
     | SBind_  SI Binder (SData SIName){-parameter name-} (SExp' a) (SExp' a)
     | SVar_   (SData SIName) !Int
     | SLet_   SI (SData SIName) (SExp' a) (SExp' a)    -- let x = e in f   -->  SLet e f{-x is Var 0-}
+    | SLHS    SIName (SExp' a)
     | STyped  a
   deriving (Eq)
 
@@ -378,6 +379,7 @@ instance SourceInfo (SExp' a) where
         SLet_ si _ _ _    -> si
         SVar sn _         -> sourceInfo sn
         SLit si _         -> si
+        SLHS n x          -> sourceInfo x
         STyped _          -> mempty
 
 instance SetSourceInfo SExp where
@@ -388,6 +390,7 @@ instance SetSourceInfo SExp where
         SVar sn i        -> SVar (setSI si sn) i
         SGlobal sn       -> SGlobal (setSI si sn)
         SLit _ l         -> SLit si l
+        SLHS n x         -> SLHS n $ setSI si x
         STyped v         -> elimVoid v
 
 foldS
@@ -407,6 +410,7 @@ foldS h g f = fs
         SVar sn j -> f sn j i
         SGlobal sn -> g sn i
         x@SLit{} -> mempty
+        SLHS _ x -> fs i x
         STyped x -> h i x
 
 foldName f = foldS (\_ -> elimVoid) (\sn _ -> f sn) mempty 0
@@ -428,6 +432,7 @@ mapS hh gg f2 = g where
         SBind_ si k si' a b -> SBind_ si k si' (g i a) (g (i+1) b)
         SVar sn j -> f2 sn j i
         SGlobal sn -> gg sn i
+        SLHS n x -> SLHS n $ g i x
         STyped x -> hh i x
         x@SLit{} -> x
 
@@ -453,6 +458,7 @@ trSExp f = g where
         SVar sn j -> SVar sn j
         SGlobal sn -> SGlobal sn
         SLit si l -> SLit si l
+        SLHS n x -> SLHS n (g x)
         STyped a -> STyped $ f a
 
 trSExp' :: SExp -> SExp' a
@@ -471,6 +477,7 @@ instance (HasFreeVars a, PShow a) => PShow (SExp' a) where
         SBind_ _ h _ SType b -> shLam_ (usedVar 0 b) h Nothing (pShow b)
         SBind_ _ h _ a b -> shLam (usedVar 0 b) h (pShow a) (pShow b)
         SLet _ a b      -> shLet_ (pShow a) (pShow b)
+        SLHS n x        -> "_lhs" `DApp` pShow n `DApp` pShow x
         STyped a        -> pShow a
         SVar _ i        -> shVar i
         SLit _ l        -> pShow l
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index 3eaae43b..444dd1b9 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -238,6 +238,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
         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
@@ -268,6 +269,7 @@ 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
         | 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
 --            tellType e t
diff --git a/src/LambdaCube/Compiler/Statements.hs b/src/LambdaCube/Compiler/Statements.hs
index 1ce2beb6..178e5505 100644
--- a/src/LambdaCube/Compiler/Statements.hs
+++ b/src/LambdaCube/Compiler/Statements.hs
@@ -96,11 +96,11 @@ compileStmt compilegt ds = \case
             | (m, t) <- ms
 --            , let ts = fst $ getParamsS $ up1 t
             , let as = [ funAlt m p $ noGuards {- -$ SLam Hidden (Wildcard SType) $ up1 -} $ SLet m' e $ sVar "cst" 0
-                      | Instance n' i cstrs alts <- ds, n' == n
-                      , StLet m' ~Nothing e <- alts, m' == m
-                      , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")]
+                       | Instance n' i cstrs alts <- ds, n' == n
+                       , StLet m' ~Nothing e <- alts, m' == m
+                       , let p = zip ((,) Hidden <$> ps) i ++ [((Hidden, Wildcard SType), PVarSimp $ dummyName "cst2")]
         --              , let ic = patVars i
-                      ]
+                       ]
             ]
         return $ cd ++ concat cds
     [TypeAnn n t] -> return [Primitive n t | n `notElem` [n' | FunAlt n' _ _ <- ds]]
@@ -113,7 +113,7 @@ compileStmt compilegt ds = \case
           | 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]) cf]
+            return [StLet n (listToMaybe [t | TypeAnn n' t <- ds, n' == n]) $ SLHS 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,7 +134,7 @@ desugarValueDef p e = sequence
     dns = reverse $ getPVars p
     n = mangleNames dns
 
-getLet (StLet x Nothing (SRHS dx)) = Just (x, dx)
+getLet (StLet x Nothing (SLHS _ (SRHS dx))) = Just (x, dx)
 getLet _ = Nothing
 
 fst' (x, _) = x -- TODO
@@ -144,7 +144,7 @@ desugarMutual [x] = [x]
 desugarMutual (traverse getLet -> Just (unzip -> (ns, ds))) = fst' $ runWriter $ do
     ss <- compileStmt' =<< desugarValueDef (foldr cHCons cHNil $ PVarSimp <$> ns) (SGlobal xy)
     return $
-        StLet xy Nothing (addFix xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
+        StLet xy Nothing (addFix xy $ SLHS xy $ SRHS $ mkLets' SLet ss $ foldr HCons HNil ds) : ss
   where
     xy = mangleNames ns
 desugarMutual xs = error "desugarMutual"