minor changes

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 17fcb668e486f0d9cfb205ba7902b0f7749c45c6..c04b91ca7028f2886b357a6e34554a1ade9363c7 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -182,6 +182,7 @@ check a t = case (a,t) of
       throwError $ "check: lam types don't match"\r
         ++ "\nlambda type annotation: " ++ show a'\r
         ++ "\ndomain of Pi: " ++ show a\r
+        ++ "\nnormal form of type: " ++ show (normal ns a)\r
     let var = mkVarNice ns x a\r
     local (addTypeVal (x,a)) $ check (app f var) t\r
   (VSigma a f, Pair t1 t2) -> do\r
@@ -376,7 +377,10 @@ checkPathSystem t0 va ps = do
       unlessM (a0 === eval rhoAlpha t0) $\r
         throwError $ "Incompatible system " ++ showSystem ps ++\r
                      ", component\n " ++ show pAlpha ++\r
-                     "\nincompatible with\n " ++ show t0\r
+                     "\nincompatible with\n " ++ show t0 ++\r
+                     "\na0 = " ++ show a0 ++\r
+                     "\nt0alpha = " ++ show (eval rhoAlpha t0) ++\r
+                     "\nva = " ++ show va\r
       return a1) ps\r
   checkCompSystem (evalSystem rho ps)\r
   return v\r