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

 Here's a brief summary of my current understanding:

 At all times we demand (the) Consistency (Condition). For instance, the
 following example violates the Consistency Condition.

 class C a b | a -> b
 instance C Int Bool
 instance C Int Char

 The Consistency Condition is the minimal requirement to guarantee type
 safety.

 (1) The Coverage Condition guarantees termination and confluence for all
 programs. Recall confluence means that we find unique answers.

 (2) The Weak Coverage Condition guarantees (local) confluence assuming
 that we can establish (local) termination. That is, if the type inferencer
 terminates for some constraint arising from some program text (aka goal
 constraint) then we know the answer is unique.

 (3) So what happens if we drop coverage (but of course still demand
 consistency)? Then we can neither guarantee termination nor confluence
 (which is obviously bad for predictable type inference). The example I
 gave still enjoys termination but in general we encounter non-confluence.
 danilo2 mentions some specific application scenario where for the specific
 constraints arising out of the program text we seem to find unique
 answers.

 I agree that the naming of GHC flags (UndecidableInstances,
 DysfunctionalDependencies) connected to (2) and (3) is not very helpful
 and rather confusing.

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