Bugfix for type checking glueElems by Fabian Ruch

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