From 7b1dbe31c6e993221495eb660f213a154d74ea61 Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 15 Apr 2015 11:47:06 +0200 Subject: [PATCH] Fix bug in type checker for HITs --- TypeChecker.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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 () -- 2.34.1