From 95afe82d2c6231071ef3e5ea7842480c93ff75bb Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 14 Jan 2016 18:21:50 -0500 Subject: [PATCH] minor changes --- TypeChecker.hs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.34.1