[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                |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Provoked by this ticket, and other recent ones (#9227, #9103) I’ve taken
 another look.  Here are my preliminary conclusions.

  * #1241 has the best overall discussion, and the paper
 “[http://research.microsoft.com/en-us/um/people/simonpj/papers/fd-chr/
 Understanding functional dependencies using constraint handling rules]”

  * The [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-
 class-extensions.html#instance-rules user manual section] that claims
 “Both the Paterson Conditions and the Coverage Condition are lifted if you
 give the `-XUndecidableInstances` flag” is plain wrong.

  * What actually happens is that `-XUndecideableInstances` weakens the
 Coverage Condition to the Liberal Coverage condition.  See `Note [Coverage
 conditions]` in `FunDeps.lhs`.  (Actually, looking at the paper, what is
 called “Liberal Coverage Condition” here and in the code is the “Refined
 Weak Coverage Condition” in the paper, Definition 15.

  * Even this looks bogus.  Looking at #1241 comment 15, we see that to get
 good behaviour (termination, confluence) we need “full fundeps” and
 “S(tvsright) are all type variables”, neither of which are checked by GHC.

  * I disagree with Richard's comment above (comment 11).  There is no way
 that fundeps can cause a program to pass the type checker but fail Core
 Lint.  All that fundeps do is cause extra “derived” type equalities to be
 added to the constraint solver’s pile.  That can cause type errors, and
 perhaps confusing ones, but it cannot cause unsoundness.

  * The worst that can happen is
     1. Non-termination of the type inference engine.  This can definitely
 happen, but is acceptable; c.f. `-XUndecideableInstances`.
     2. Non-confluence of type inference.  The paper goes on about this at
 length.  I think it amounts to incompleteness.  Maybe type inference will
 succeed one day, but fail the next because of some random variation in the
 order in which the constraint solver tackles its constraints.  I do not
 have an example that shows this behaviour, but it would be a Bad Thing.

 I see no good reason to stop programmers getting perhaps-strange behaviour
 if they ask for it.  So I would be OK with doing this (which is exactly
 what https://phabricator.haskell.org/D69 proposes this behaviour for the
 Coverage Condition (see
 [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-
 extensions.html#instance-rules user manual])
  * No flags: Coverage Condition enforced
  * `-XUndecidableInstances`: changes Coverage Condition to Liberal
 Coverage Condition.  This risks non-termination.  I’m still uneasy about
 the consequences of not checking  for “full” fundeps (see comment 15 of
 #1241) but it’s what happens right now.
  * `-XDysFunctionalDependencies`: removes the Coverage Condition
 altogether, with somewhat unknown consequences.

 So this is a long-winded way of saying I’m ok with the D69 proposal.

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