idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.46k stars 369 forks source link

[ re #3314, #34 ] Tighten the location information for implicits #3320

Closed gallais closed 2 weeks ago

gallais commented 2 weeks ago

When implicitly binding a variable, use the location of the head function/constructor that expects it. This way we can differentiate multiple implicits bound on the same LHS.

Note that this does not resolve the issue 34: there the location is then further muddled by the fact that where-bound functions are lifted to the toplevel.