_ -> 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
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