@@ -59,6 +59,11 @@ prove ctxt lit n ty
5959 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
6060 logLvl 3 (show tree)
6161 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
62+ logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++
63+ "Expected type:" ++ show ty)
64+ case converts ctxt [] ty pty of
65+ OK _ -> return ()
66+ Error e -> ierror (CantUnify False ty pty e [] 0)
6267 ptm' <- applyOpts ptm
6368 updateContext (addCasedef n True False True False
6469 [Right (P Ref n ty, ptm)]