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

 Some brief comments regarding the various conditions/flags.

 * Paterson Conditions and the Coverage Condition (plus the FD Consistency
 Condition)

    The above guarantee sound and decidable type inference. In CHR speak,
 termination and confluence. Confluence effectively means that we find
 unique answers. Hence, confluence implies consistency. Hence, we also
 obtain type safety.

 * Dropping the Coverage Condition

    There are numerous examples which violate this condition. Naively
 dropping this condition potentially threatens decidable type inference
 (due to non-termination) and type safety (due to non-confluence).

 * Weak (aka refined) Coverage Condition

    Guarantees local confluence (critical pairs are joinable). Assuming
 that instances are terminating we obtain confluence (by Newman's Lemma).

     The bad news is that typical examples which violate the coverage but
 satisfy the weak coverage condition are non-terminating.
      Consider the classic example

    class F a b | a -> b
    instance F a b => F [a] [b]

    where for constraint F [a] a the type inferencer will not terminate

    The good news is that in "On Termination, Confluence and Consistent
 CHR-based Type Inference", ICLP'14, we show that (under some modest extra
 conditions) for terminating type inference goals we find unique answers.
 In essence, we're happy to achieve local confluence under the assumption
 that we have local termination.

 * XUndecidableInstances

   Enforces the weak coverage condition but gives up on (global)
 termination. Assuming that the GHC type inference terminates nothing bad
 will happen though (cause we find unique answers, see above)

 * DysfunctionalDependencies

    I can only guess what this means as I couldn't find any concrete
 definition. My impression is to drop the weak coverage condition?

    Bad idea! We no longer have local confluence. We might be lucky enough
 that GHC always applies type inference rules (FD improvement, instances)
 in a fixed order and thus 'unique' answers are guarantees. Sounds rather
 brittle to me.

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