Change order in checkPathSystem

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