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

 Correct. I'm too pessimistic in my comment.
 For type safety (well-typed programs cannot go wrong) it suffices to have
 consistency.
 Simon, surely the Consistency Condition must hold at least, right?
 I agree then that the Coverage Condition (or variants) can be dropped.
 See Theorem 1 in the above mentioned paper.

 I still find it strange that you want to drop the Coverage Condition (or
 variants of it).
 This clearly leads to non-confluence, hence, unpredictable type inference.

 Consider

 class F a b | a -> b where
    f :: a -> b -> a

 instance F b a => F [a] [b]
 -- Order of 'a' and 'b' swapped!
 -- Hence, (weak) coverage is violated.


 g as bs c = (f as bs, f as c)

 The above gives (roughly) rise to the constraints

  F [a] [b], F[a] c

 Depending on the order type inference rules are applied, the following two
 final constraints may arise

 (1) c = [b], F b a

 (2) c = [b'], F b a, F b' a

 Say we use (1) for some type annotation but the type checker only comes up
 with (2). Urgh!

 To conclude:

 - For type safety we require at least consistency
 - For predictable type inference we require (local) termination and (weak)
 coverage.

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