From what I can tell, there was no reason for the matching (instead of unifying) behavior to begin with; it was just "how type class matching worked", back in 1996. E.g. page 12 of https://courses.cs.washington.edu/courses/cse590p/06sp/multi.pdf mentions
* //no matter what other (legal) instance declarations are added//,
This issue is a rather small, dark corner of the language, so few have
#12240: Common Sense for Type Classes -------------------------------------+------------------------------------- Reporter: Mathnerd314 | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by adamgundry): that matching uses one-way unification, but gives no explanation of why two-way unification was not chosen. Then on page 13 they state that constraints can be improved if they unify with a unique instance, but just say "it is not yet clear if it would improve enough useful programs to be worth the extra effort." I believe the reason is the open world assumption, i.e. allowing for instances to be added later without changing the solver behaviour. Also, it's not clear to me whether any theoretical properties have been studied for the type system with unification in place of matching. Note one of the conditions regarding Decision 8 on page 13 of the paper you cite (my emphasis): there is only one instance declaration that the constraint can be made to match in this way. This is much more restrictive than your proposal, and would indeed not apply to many programs (if any), so it indeed hardly seems worth it. the patience to discuss it. I respectfully disagree. You are suggesting a rather significant change to the type system, and I for one think it is very interesting to discuss its implications. Thank you for bringing it up! Please take all these comments in a spirit of constructive debate, and apologies if my previous comment was too blunt.
Furthermore, I have not really elaborated on my proposal, because I don't know enough of GHC internals to describe it accurately, so it is hard to actively support a nebulous concept. At least a patch can be judged on its merits.
Most people won't judge a patch at all, I'm afraid. ;-) We really need a clear specification of the feature, articulated independently of the details of the implementation. A wiki page is a good place to put this, and can link to this ticket and other discussions. A specification should outline the motivation for the feature, describe the changes to the type system (not just the type inference algorithm, although that may be helpful too), give plenty of examples, and mention potential problems with the extension. On a different tangent, consider this module: {{{#!hs class C a where foo :: a instance C Int where foo = 42 f _ = foo }}} What is the inferred type of `f`? Previously it would have been `C a => b -> a` but under your proposal it would be `b -> Int`, right? This means that enabling the extension might cause existing programs to cease to type-check. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12240#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler