bugix: take the border of the system where is=js

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 08e75b0a2c486512d7a4742dad9c24c819900f4c..93557f47b4e6b181ed6f8e1583021dd0e318de2d 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -304,11 +304,11 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
       vus  = map snd us\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
+      vfts = intersectionWith app (border g vts) vts\r
   local (addSubs (zip js js') . addBranch (zip ns vus) 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
+    unlessM (border ve vts === vfts) $\r
       throwError $ "Faces of branch don't match"\r
 \r
 checkFormula :: Formula -> Typing ()\r