-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WIP: Type error display improvements #49
base: main
Are you sure you want to change the base?
Conversation
Type errors are improved by doing the following: 1. Normalize types in them as far as possible, so it's not just a TyF around METAs in the error message 2. When the unification error occurs in a nested call to unify, call that out but also save the original types. Show the inner fail in a "Specifically" block as GHC does.
This makes the code easier to understand and improves GHC warnings.
Type errors are now collected within the extent of a call to completely, and aggregated for later display.
Having thought about this for a while, I think I have an idea of how to proceed. First of, we must recognize that macros are the source of all compile-time execution, and free variables in macros always refer to either imports or definitions (rather than e.g. I propose to do that by maintaining a mapping from defined names to their type errors and their dependencies' type errors. When we add a macro to the transformer environment (that is, the handler for This means that modules with type errors at phase 1 or higher may not report all type errors, because a macro failing to run may interrupt expansion of the rest of the module. But I think it's a reasonably simple compromise that's much better than only ever showing one type error at a time! |
While writing
pmatch
, it was often difficult to figure out what Klister meant when giving type errors. Many of them were due to #48, it turned out, but that was made hard to see. This PR doesn't make it good, but it is at least non-terrible now:completely
) and reported as a group.This is not quite ready for review/merge yet, due to one downside: unification failures do not prevent the elaboration of a term that can't type check, but they should. As things stand now, ill-typed macro code could be executed (though not ill-typed phase 0 code). I need to ponder the right design for fixing this - probably, the stuff in Expander.TC should run in a Validation applicative functor with a bit of local state to track the union-find structure, rather than an Error monad with the global expander state. The interface between
Expand
andTC
can then check how many failures occurred and spit out an explicit representation of the error into theCore
that results. Or something like that.Also, the work is done on top of #47, because I don't expect to finish this before that's been merged, and because I have some little local tests that use
pmatch
in examples.