From: Anders <mortberg@chalmers.se>
Date: Fri, 8 May 2015 13:28:49 +0000 (+0200)
Subject: Change order in checkPathSystem
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7b53932993d55c2de354416b9acd2dbd5b9655f1;p=cubicaltt.git

Change order in checkPathSystem
---

diff --git a/TypeChecker.hs b/TypeChecker.hs
index e55ff67..b8fa058 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -356,14 +356,15 @@ checkPath v t = do
 checkPathSystem :: Ter -> Val -> System Ter -> Typing (System Val)
 checkPathSystem t0 va ps = do
   rho <- asks env
-  checkCompSystem (evalSystem rho ps)
-  T.sequence $ mapWithKey (\alpha pAlpha ->
+  v <- T.sequence $ mapWithKey (\alpha pAlpha ->
     local (faceEnv alpha) $ do
       rhoAlpha <- asks env
       (a0,a1)  <- checkPath (constPath (va `face` alpha)) pAlpha
       unlessM (a0 === eval rhoAlpha t0) $
         throwError $ "Incompatible system with " ++ show t0
       return a1) ps
+  checkCompSystem (evalSystem rho ps)
+  return v
 
 checks :: (Tele,Env) -> [Ter] -> Typing ()
 checks _              []     = return ()