From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 14 Jan 2016 23:21:50 +0000 (-0500)
Subject: minor changes
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=95afe82d2c6231071ef3e5ea7842480c93ff75bb;p=cubicaltt.git

minor changes
---

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