From 97c1fb49dd36e19e795e4faf9d05c13d1f7b282e Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Thu, 23 Apr 2015 14:57:28 +0200
Subject: [PATCH] bugix: take the border of the system where is=js

---
 TypeChecker.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 08e75b0..93557f4 100644
--- 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
       js'  = map Atom js
       vts  = evalSystem (subs (upds nu us) (zip is js')) ts
-      vfts = intersectionWith app (border g ts) vts
+      vfts = intersectionWith app (border g vts) vts
   local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do
     check (app f (VPCon c va vus js')) e
     ve  <- evalTyping e -- TODO: combine with next line?
-    unlessM (border ve ts === vfts) $
+    unlessM (border ve vts === vfts) $
       throwError $ "Faces of branch don't match"
 
 checkFormula :: Formula -> Typing ()
-- 
2.34.1