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

On Jul 10, 2017, at 2:38 PM, Ertugrul Söylemez 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.