Egg #1: Error Reflection

Status

This has been merged.

Motivation

Many embedded languages struggle with the problem of readable error messages for users who don't know about how the types work with the embedding under the hood. Error reflection is intended to give EDSL authors the ability to customize compiler errors so that they match the user's domain.

User-level description

This feature will add a new language extension, ErrorReflection, that is available from the command line or from the %language directive. When this feature is enabled, it will be possible to define custom error handlers. These error handlers will be available even in modules that do not enable the extension, because there's no need for embedded language users to have to type it. For debugging, it might be wise to add a command line option to completely disable it however.

When the extension is enabled, functions with type List (TTName, TT) -> List TT -> Err -> Maybe ErrorReport defined with the modifier %error_handler will be registered as error handlers. Then, when emitting an error, the Idris compiler will attempt to call all such errors with a reflected version of the global context, the local environment, and a reflected representation of the error in question. The results returned will use constructors of ErrorReport to determine whether the original message should be suppressed or amended, and provide a rich representation to allow, eg, use of the compiler's pretty printer.

Implementation

Steps:

1. Refactor the Idris monad to an ErrorT - this ensures that all errors have the same type. Done, but needs debugging and polish.
2. Add a way to register functions as handlers. Done.
3. Actually call the functions with reflected errors. Remains to be done.
4. Consider performance.