improve error message
authorSimon Huber <hubsim@gmail.com>
Wed, 29 Apr 2015 12:19:41 +0000 (14:19 +0200)
committerSimon Huber <hubsim@gmail.com>
Wed, 29 Apr 2015 12:19:41 +0000 (14:19 +0200)
TypeChecker.hs

index 93557f47b4e6b181ed6f8e1583021dd0e318de2d..e11c951e6b88bb7849c8c4078a9fe2c67de1dc84 100644 (file)
@@ -211,7 +211,7 @@ check a t = case (a,t) of
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r
-      throwError $ "check conv: " ++ show v ++ " /= " ++ show a\r
+      throwError $ "check conv:\n" ++ show v ++ "\n/=\n" ++ show a\r
 \r
 -- Check a list of declarations\r
 checkDecls :: [Decl] -> Typing ()\r
@@ -304,12 +304,15 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do
       vus  = map snd us\r
       js'  = map Atom js\r
       vts  = evalSystem (subs (upds nu us) (zip is js')) ts\r
-      vfts = intersectionWith app (border g vts) vts\r
+      vgts = intersectionWith app (border g vts) vts\r
   local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do\r
     check (app f (VPCon c va vus js')) e\r
-    ve  <- evalTyping e -- TODO: combine with next line?\r
-    unlessM (border ve vts === vfts) $\r
-      throwError $ "Faces of branch don't match"\r
+    ve  <- evalTyping e -- TODO: combine with next two lines?\r
+    let veborder = border ve vts\r
+    unlessM (veborder === vgts) $\r
+      throwError $ "Faces in branch for " ++ show c ++ " don't match:"\r
+                   ++ "\ngot\n" ++ show veborder ++ "\nbut expected\n"\r
+                   ++ show vgts\r
 \r
 checkFormula :: Formula -> Typing ()\r
 checkFormula phi = do\r