Fix bug in type checker for HITs

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 407f7af4e3d3b492348c49fafae833b05f96f91f..4d85f3b7141249e2dc8d90562c82c541f1af1610 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -92,7 +92,7 @@ faceEnv alpha tenv = tenv{env=env tenv `face` alpha}
 getLblType :: LIdent -> Val -> Typing (Tele, Env)\r
 getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of\r
   Just as -> return (as,r)\r
-  Nothing -> throwError ("getLblType: " ++ show c)\r
+  Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)\r
 getLblType c u = throwError ("expected a data type for the constructor "\r
                              ++ c ++ " but got " ++ show u)\r
 \r
@@ -212,8 +212,9 @@ checkDecls d = do
   let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
   trace ("Checking: " ++ unwords idents)\r
   checkTele tele\r
-  rho <- asks env\r
-  localM (addTele tele) $ checks (tele,rho) ters\r
+  local (addDecls d) $ do\r
+    rho <- asks env\r
+    checks (tele,rho) ters\r
 \r
 -- Check a telescope\r
 checkTele :: Tele -> Typing ()\r