[GHC] #12240: Common Sense for Type Classes

[GHC]

#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):

 > 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
 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):

 > * //no matter what other (legal) instance declarations are added//,
 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.

 > This issue is a rather small, dark corner of the language, so few have
 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