[Haskell-cafe] I'm afraid of OverloadedLabels.

[Alexis King]

> On Jul 10, 2017, at 2:38 PM, Ertugrul Söylemez <esz at posteo.de> wrote:
> 
> ... type inference would have to be done multiple times, once for each
> matching identifier in scope.  Do each of them independently, then see
> which ones turn out to be well-typed (no ambiguity, no missing
> instances, no mismatch, etc.).  If there is exactly one, take it,
> otherwise give up with a type error.

This would make type inference go exponential *extremely* quickly. This
sort of approach is a non-starter, since it would imply typechecking a
module 2^n times for n ambiguities where only 2 of the same identifiers
are in scope; it would be even worse when there are more than 2. Due to
the way Haskell’s type inference works, it would be very difficult
(impossible?) in general to limit the duplicate work the typechecker
would need to perform if you want to run it multiple times to see which
binding would typecheck. GHC does no backtracking in the typechecker,
and this would be even worse than backtracking, since it would always
need to run multiple times.

The only workable approach I can imagine for TDNR is something like the
following:

  1. If an identifier is unambiguous, don’t do anything differently from
     what already happens now.

  2. If an identifier is ambiguous, ignore the bindings’ types entirely
     and assign the identifier a fresh type variable. (If the binding
     is in function application position, it can be assigned the type
     (a -> b -> c -> ...), depending on the number of expressions it is
     applied to, but this doesn’t fundamentally change anything.)

  3. Typecheck the program using that information alone. Defer name
     resolution to the constraint solver. If the program typechecks, try
     to find an unambiguous substitution during constraint solving via
     subsumption. If one can be found, use it. Otherwise, bail with an
     appropriate error message.

In my head, this seems less invasive than trying to typecheck the
program multiple times and less wishful thinking than trying to divine
the proper binding during the bulk of the typechecking process. However,
I am not familiar with the details of GHC’s particularly advanced and
complex typechecker, and it’s entirely possible that even the heavily
constrained approach I just outlined is an enormous amount of work or
even impossible.

Even if it were possible to implement the above approach, it would still
be limited. It’s possible it would need to be restricted to imported and
top-level bindings (excluding local bindings), and it would probably
sometimes fail to typecheck even when one of the bindings would
successfully typecheck (when higher-rank types are involved, for
example). I’d personally be quite happy with the feature even with those
limitations, but I can’t make any claims to its practicality or
possibility, since I have never touched GHC’s source at all, much less
the typechecker.