search

idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.43k stars 644 forks source link

Error reflection breaks highlighting of lexical variables #1997

Open david-christiansen opened 9 years ago

david-christiansen commented 9 years ago

Idris's error message objects carry with them the context in which they arose. This allows lexically bound variables to be highlighted as such in displayed errors. However, that information is lost following error rewriters, so some variables show up without highlighting.

I see two potential solutions:

  1. Manual control, in which error rewriters return a pair of a new message and its context; or
  2. Automatic propagation, where Idris attaches the context from the original error automatically following a rewrite

I'm inclined towards option 2. Option 1 is more flexible and allows DSL authors to "lie" about the context in which the errors arose, which might in fact give a better message. However, it's also tedious, requiring every single rewriter to do the right thing with the context extracted from the reflected errors. I think that, in the vast majority of cases, we actually just want to propagate the context.

I suppose there's a third option, which is to completely decouple the reflection API from the internal compiler error representation (this is really a more radical version of Option 2). Then, error rewriters could return something like:

data ErrorReport = SimpleReport String 
                 | Report (List ErrorReportPart)
                 | ReportWithContext (List ErrorReportPart) (List (Binder TT))

when they rewrite.

Limiting the collection of errors that are rewritable to unification errors, proof search failures, and conversion failures (perhaps one or two more), with some things like recoverability of unification errors stripped form the representation, could also give us a more coherent, testable API as well as lessen the burden of changing the internal errors (because never-used error reflection routines would not need updating except in a few cases).

david-christiansen commented 9 years ago

Once the new tactics are working, it might also be worth looking into whether an error rewriter should be in the new tactics monad instead of Maybe, because then it could do things like suggest alternative names based on the global context.