From 7b53932993d55c2de354416b9acd2dbd5b9655f1 Mon Sep 17 00:00:00 2001
From: Anders <mortberg@chalmers.se>
Date: Fri, 8 May 2015 15:28:49 +0200
Subject: [PATCH] Change order in checkPathSystem

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

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 ()
-- 
2.34.1