@@ -59,6 +59,11 @@ prove ctxt lit n ty
59 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
59 let tree = simpleCase False True CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]
60 logLvl 3 (show tree)
60 logLvl 3 (show tree)
61 (ptm, pty) <- recheckC (FC "proof" 0) [] tm
61 (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
66+ Error e -> ierror (CantUnify False ty pty e [] 0)
62 ptm' <- applyOpts ptm
67 ptm' <- applyOpts ptm
63 updateContext (addCasedef n True False True False
68 updateContext (addCasedef n True False True False
64 [Right (P Ref n ty, ptm)]
69 [Right (P Ref n ty, ptm)]