bugfix in PBranches

diff --git a/TypeChecker.hs b/TypeChecker.hs
index d5d180eabbbbaa6a2945f2b49dbb5a216bfd7e7a..06ce964cbef6c37762ea9246bf1e40ae0e8ead2d 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -305,17 +305,15 @@ checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
   local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e\r
 checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
   k <- asks index\r
-  mapM_ checkFresh is\r
+  mapM_ checkFresh js\r
   let us   = mkVars k tele nu\r
       vus  = map snd us\r
-      is'  = map Atom is\r
-      vts  = evalSystem (upds nu us) ts\r
-      vfts = intersectionWith app (border f ts) vts\r
-  local (addBranch (zip ns vus) (tele,nu)) $ do\r
-    local (addSubs (zip is is')) $\r
-      check (app f (VPCon c va vus is')) e\r
-    rho <- asks env\r
-    ve  <- evalTyping e -- TODO: combine with next?\r
+      js'  = map Atom js\r
+      vts  = evalSystem (subs (upds nu us) (zip is js')) ts\r
+      vfts = intersectionWith app (border g ts) vts\r
+  local (addSubs (zip js js') . addBranch (zip ns vus) (tele,nu)) $ do\r
+    check (app f (VPCon c va vus js')) e\r
+    ve  <- evalTyping e -- TODO: combine with next line?\r
     unlessM (border ve ts === vfts) $\r
       throwError $ "Faces of branch don't match"\r
 \r