[GHC] #8634: Relax functional dependency coherence check ("liberal coverage condition")

[GHC]

#8634: Relax functional dependency coherence check ("liberal coverage condition")
-------------------------------------+-------------------------------------
              Reporter:  danilo2     |             Owner:
                  Type:  feature     |            Status:  new
  request                            |         Milestone:  7.10.1
              Priority:  high        |           Version:  7.7
             Component:  Compiler    |          Keywords:
            Resolution:              |  Operating System:  Unknown/Multiple
Differential Revisions:  Phab:D69    |   Type of failure:  None/Unknown
          Architecture:              |         Test Case:
  Unknown/Multiple                   |          Blocking:
            Difficulty:  Unknown     |
            Blocked By:              |
       Related Tickets:  #1241,      |
  #2247, #8356, #9103, #9227         |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 OK, Martin, that's a good example (in comment:26).  Let's see a bit more
 detail.
 We start with
 {{{
   F [a] [b], F [a] c
 }}}
 Now there are two sorts of "improvement" rules which might fire:
   A. '''Between two constraints'''.  Since we have `F [a] [b]` and `F [a]
 c`, we may derive `[b] ~ c`.  After all the class fundep for `F` claims
 that `a -> b`.

   B. '''Between a constraint and an instance declaration'''.  Here we have
      * `instance forall p q.  F q p => F [p] [q]`  (I have alpha-renamed.)
      * `F [a] c`
   Since the `[a]` matches the `[p]` we may conclude that `c ~ [q']`, where
 `q'` is a fresh unification variable, reflecting the fact that the
 instance declaration says the second parameter must be a list but doesn't
 tell you what the element type is.

 So Martin's point is that there are two possible solution paths:
 {{{
   F [a] [b], F [a] c
 ===> Use (A) to combine the two
   F [a] [b], F [a] c, c ~ [b]
 ===> Use the instance declaration to simplify
   F b a, c ~ [b]
 }}}
 Here is the other path:
 {{{
   F [a] [b], F [a] c
 ===> use the instance declaration
   F b a, F [a] c
 ===> use (B) to combine the second constraint with the instance
   F b a, F [a] c, c ~ [q']
 ===> use the instance declaration again
   F b a, F q' a, c ~ [q']
 (stuck)
 }}}
 This is helpful: it's a concrete example that demonstrates how minor
 variations in the way the inference engine works may lead to unpredictable
 failures in type inference.

 One possible reaction is that if you are going to lift the Coverage
 Condition, then (A) yields too many equalities, and you shouldn't use it.
 But (B) is still useful, and is actually what is wanted here.  So maybe we
 want
 {{{
 class C a b | a ~> b
 }}}
 notice `a ~> b` rather than `a -> b`, meaning "`a` specifies the ''shape''
 of `b`", which would make use improvement rule (B) but not (A) for this
 fundep.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8634#comment:30>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler