git.iko.soy/Idris-dev
on master help sign in
Extra info for errors in advanced mode

When showing error context information, display the difference between unification and conversion errors. This is convenient when debugging Elab scripts.

commitd741a30ed58463931b525cb9d4ba51d37fab9b77 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 20 Aug 2015, 22:37 (11 years ago) parent1c87b5e
1 file changed+4−2
compare with master
unifiedsplit
src/Idris/Delaborate.hs+4−2
src/Idris/Delaborate.hs+4−2
@@ -289,7 +289,9 @@ pprintErr' i (CantUnify _ (x_in, xprov) (y_in, yprov) e sc s) =
289289 CantUnify _ (x_in', _) (y_in',_) _ _ _ | x_in == x_in' && y_in == y_in' -> empty
290290 _ -> line <> line <> text "Specifically:" <>
291291 indented (pprintErr' i e) <>
292− if (opt_errContext (idris_options i)) then showSc i sc else empty
292+ if (opt_errContext (idris_options i))
293+ then text "Unification failure" <$> showSc i sc
294+ else empty
293295pprintErr' i (CantConvert x_in y_in env) =
294296 let (x_ns, y_ns, nms) = renameMNs x_in y_in
295297 (x, y) = addImplicitDiffs (delabSugared i (flagUnique x_ns))
@@ -300,7 +302,7 @@ pprintErr' i (CantConvert x_in y_in env) =
300302 text "and" <>
301303 indented (annTm y_ns (pprintTerm' i (map (\ (n, b) -> (n, False)) env)
302304 y)) <>
303− if (opt_errContext (idris_options i)) then line <> showSc i env else empty
305+ if (opt_errContext (idris_options i)) then line <> text "Conversion failure" <$> showSc i env else empty
304306 where flagUnique (Bind n (Pi i t k@(UType u)) sc)
305307 = App Complete (P Ref (sUN (show u)) Erased)
306308 (Bind n (Pi i (flagUnique t) k) (flagUnique sc))