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

 Several points

  * Your script in comment:37 typechecks just fine if you use
 `-XScopedTypeVariables`.  You need the 's' in the body of `tst` to be the
 same as the one in the type signature.

  * Interestingly in this example, unlike earlier ones, the instances for
 `Property` really do morally satisfy the (liberal) Coverage condition: the
 first parameter determines the second. And GHC knows this.  For example,
 this is accepted right now (with `UndecidableInstances` so that we get the
 liberal coverage condition):
 {{{
 class Property a b | a -> b  where   -- Note the fundep
    property :: a -> b

 instance (y ~ Y) => Property X y where   -- Suppose this was accepted
     property _ = Y
 }}}
  And now you don't need the `:: s` signature in the body of `tst`

  * It's also worth remembering that ALL fundeps do in GHC is guide the
 type inference engine.  And you can offer the same guidance via type
 signatures.  So you should be alle to fix your 600-module system by adding
 some type signatures.

  * Martin's excellent example, explained in detail in comment:30, is a
 pretty convincing reason for not rushing ahead with lifting the coverage
 condition altogether, especially given that there is another workaround
 (type signatures).

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