From: Simon Huber <hubsim@gmail.com>
Date: Tue, 15 Dec 2015 13:53:36 +0000 (+0100)
Subject: Bugfix for type checking glueElems by Fabian Ruch
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7b6927e75468fab90b839beae24466fda7177cf4;p=cubicaltt.git

Bugfix for type checking glueElems by Fabian Ruch
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index c0af283..a342b07 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -262,7 +262,8 @@ checkGlueElem vu ts us = do
   unless (keys ts == keys us)
     (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))
   rho <- asks env
-  checkSystemsWith ts us (\_ vt u -> check (isoDom vt) u)
+  checkSystemsWith ts us
+    (\alpha vt u -> local (faceEnv alpha) $ check (isoDom vt) u)
   let vus = evalSystem rho us
   checkSystemsWith ts vus (\alpha vt vAlpha ->
     unlessM (app (isoFun vt) vAlpha === (vu `face` alpha)) $
@@ -291,10 +292,10 @@ mkIso vb = eval rho $
     Pi (Lam "x" a $ IdP (Path (Name "_") a) (App g (App f x)) x)
   where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"]
         rho = upd ("b",vb) emptyEnv
-        
+
 checkIso :: Val -> Ter -> Typing ()
 checkIso vb iso = check (mkIso vb) iso
-        
+
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
   ns' <- asks names