5 files changed, 34 insertions, 21 deletions

diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 0685f45c..273791a7 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -82,6 +82,9 @@ upDB x (MaxDB i) = MaxDB $ ad x i where
   ad n i = Su $ ad (n-1) i
 -}
 
+setMaxDB db = \case
+    Neut (Fun_ _ a b c) -> Neut $ Fun_ db a b c
+
 class HasMaxDB a where
     maxDB_ :: a -> MaxDB
 
@@ -152,6 +155,7 @@ data Neutral
     | CaseFun__   !MaxDB CaseFunName   [Exp] Neutral
     | TyCaseFun__ !MaxDB TyCaseFunName [Exp] Neutral
     | Fun_        !MaxDB FunName [Exp]{-given parameters, reversed-} Exp{-unfolded expression, in hnf-}
+--    | Let_        !MaxDB
 
 -------------------------------------------------------------------------------- auxiliary functions and patterns
 
diff --git a/src/LambdaCube/Compiler/DesugaredSource.hs b/src/LambdaCube/Compiler/DesugaredSource.hs
index 264912ca..d47726d0 100644
--- a/src/LambdaCube/Compiler/DesugaredSource.hs
+++ b/src/LambdaCube/Compiler/DesugaredSource.hs
@@ -276,9 +276,20 @@ data Binder
     | BMeta      -- a metavariable is like a floating hidden lambda
   deriving (Eq)
 
+instance PShow Binder where
+    pShow = \case
+        BPi v -> "BPi" `DApp` pShow v
+        BLam v -> "BLam" `DApp` pShow v
+        BMeta -> "BMeta"
+
 data Visibility = Hidden | Visible
   deriving (Eq)
 
+instance PShow Visibility where
+    pShow = \case
+        Hidden -> "Hidden"
+        Visible -> "Visible"
+
 dummyName s = SIName (debugSI s) ("v_" ++ s)
 dummyName' = SData . dummyName
 sVar = SVar . dummyName
diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index cd484897..3b8bdd5a 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -54,7 +54,7 @@ mkELet n x xt env = term
     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
+    term = {-setMaxDB (mconcat (maxDB_ . Var <$> vs)) $ -} mkFun fn (Var <$> reverse vs) $ getFix x 0
 
     getFix (Lam z) i = Lam $ getFix z (i+1)
     getFix (DFun FprimFix _ [t, Lam f]) i = subst 0 (foldl app_ term (downTo 0 i)) f
@@ -71,7 +71,7 @@ mkELet n x xt env = term
         acc' = s <> acc
         s' = mconcat (free . snd . flip (varType "mkELet2") env <$> Set.toList s)
 
-instance PShow (CEnv Exp) where
+instance MkDoc a => PShow (CEnv a) where
     pShow = mkDoc (False, False)
 
 instance PShow Env where
@@ -104,14 +104,11 @@ envDoc x m = case x of
     ERHS ts             -> envDoc ts $ shApp Visible (text "rhs") m
     x   -> error $ "envDoc: " ++ ppShow x
 
-instance MkDoc (CEnv Exp) where
-    mkDoc pr e = green $ f e
-      where
-        f :: CEnv Exp -> Doc
-        f = \case
-            MEnd a          -> mkDoc pr a
-            Meta a b        -> shLam True BMeta (mkDoc pr a) (f b)
-            Assign i (ET x _) e -> shLet i (mkDoc pr x) (f e)
+instance MkDoc a => MkDoc (CEnv a) where
+    mkDoc pr = \case
+        MEnd a          -> mkDoc pr a
+        Meta a b        -> shLam True BMeta (mkDoc pr a) (mkDoc pr b)
+        Assign i (ET x _) e -> shLet i (mkDoc pr x) (mkDoc pr e)
 
 -------------------------------------------------------------------------------- constraints env
 
@@ -121,11 +118,6 @@ data CEnv a
     | Assign !Int ExpType (CEnv a)       -- De Bruijn index decreasing assign reservedOp, only for metavariables (non-recursive)
   deriving (Functor)
 
-instance (Subst Exp a, Up a) => Up (CEnv a) where
-    usedVar i a = error "usedVar @(CEnv _)"
-    foldVar _ _ _ = error "foldVar @(CEnv _)"
---    maxDB_ _ = error "maxDB_ @(CEnv _)"
-
 instance (Subst Exp a, Rearrange a) => Rearrange (CEnv a) where
     rearrange l f = \case
             MEnd a -> MEnd $ rearrange l f a
@@ -415,7 +407,9 @@ inferN_ tellTrace = infer  where
         EGlobal{} -> return eet
         _ -> case eet of
             MEnd x -> throwError' $ ErrorMsg $ "focus todo:" <+> pShow x
-            _ -> throwError' $ ErrorMsg $ "focus checkMetas:" <+> pShow env <$$> pShow (expr <$> eet)
+            _ -> 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'
         refocus_ _ e (MEnd at) = focus_ e at
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs
index cd118768..f4ea8489 100644
--- a/src/LambdaCube/Compiler/Parser.hs
+++ b/src/LambdaCube/Compiler/Parser.hs
@@ -421,7 +421,7 @@ parseDef =
             return $ pure $ Class x (map snd ts) cs
  <|> do reserved "instance" *> do
           typeNS $ do
-            constraints <- option [] $ try_ "constraint" $ map SCW . getTTuple <$> setR parseTermOp <* reservedOp "=>"
+            constraints <- option [] $ try_ "constraint" $ getTTuple <$> setR parseTermOp <* reservedOp "=>"
             x <- upperCase
             (nps, args) <- telescopePat
             cs <- expNS $ option [] $ reserved "where" *> identation False ({-deBruijnify nps <$> -} funAltDef (Just lhsOperator) varId)
diff --git a/testdata/typesig.reject.out b/testdata/typesig.reject.out
index e69bd9cc..60f0c6c8 100644
--- a/testdata/typesig.reject.out
+++ b/testdata/typesig.reject.out
@@ -1,14 +1,18 @@
-focus checkMetas: \(a :: Type) -> ((\b -> primFix a b) :: (a -> a) -> a)
+focus checkMetas:
+\(a :: Type) -> ((\b -> primFix a b) :: (a -> a) -> a)
   let a = Type in \(c :: Type) -> <<HERE>>
-\(a :: CW (Type ~ _a)) (b :: CW (_a ~ X)) -> typeAnn _a (_rhs X)
+---
+\(a :: CW (Type ~ _a)) (b :: CW (_a ~ X)) -> typeAnn _a (_rhs X) :: _a
 ------------ trace
 'X :: Type
 X :: X
 case'X :: forall (a :: X -> Type) -> a 'X -> forall (b :: X) -> a b
 match'X :: forall (a :: Type -> Type) -> a X -> forall b -> a b -> a b
-!focus checkMetas: \(a :: Type) -> ((\b -> primFix a b) :: (a -> a) -> a)
+!focus checkMetas:
+\(a :: Type) -> ((\b -> primFix a b) :: (a -> a) -> a)
   let a = Type in \(c :: Type) -> <<HERE>>
-\(a :: CW (Type ~ _a)) (b :: CW (_a ~ X)) -> typeAnn _a (_rhs X)
+---
+\(a :: CW (Type ~ _a)) (b :: CW (_a ~ X)) -> typeAnn _a (_rhs X) :: _a
 ------------ tooltips
 testdata/typesig.reject.lc 4:6-4:7
     Type | Type | Type | Type | Type