From: Anders <mortberg@chalmers.se>
Date: Wed, 15 Apr 2015 09:47:06 +0000 (+0200)
Subject: Fix bug in type checker for HITs
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7b1dbe31c6e993221495eb660f213a154d74ea61;p=cubicaltt.git

Fix bug in type checker for HITs
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 407f7af..4d85f3b 100644
--- 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)
 getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel c cas of
   Just as -> return (as,r)
-  Nothing -> throwError ("getLblType: " ++ show c)
+  Nothing -> throwError ("getLblType: " ++ show c ++ " in " ++ show cas)
 getLblType c u = throwError ("expected a data type for the constructor "
                              ++ c ++ " but got " ++ show u)
 
@@ -212,8 +212,9 @@ checkDecls d = do
   let (idents,tele,ters) = (declIdents d,declTele d,declTers d)
   trace ("Checking: " ++ unwords idents)
   checkTele tele
-  rho <- asks env
-  localM (addTele tele) $ checks (tele,rho) ters
+  local (addDecls d) $ do
+    rho <- asks env
+    checks (tele,rho) ters
 
 -- Check a telescope
 checkTele :: Tele -> Typing ()