[GHC] #8634: Relax functional dependency coherence check ("liberal coverage condition")

[GHC]

#8634: Relax functional dependency coherence check ("liberal coverage condition")
-------------------------------------+-------------------------------------
        Reporter:  danilo2           |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:  8.4.1
       Component:  Compiler (Type    |              Version:  7.7
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #1241, #2247,     |  Differential Rev(s):  Phab:D69
  #8356, #9103, #9227                |
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by AntC):

 Replying to [comment:63 goldfire]:
 >
 > My understanding of `DysfunctionalDependencies` is much, much simpler:
 just omit the check that takes place at instance declarations. For
 example, the following would be accepted:

 Hereby confirming we can write Richard’s class `Terrible` today [GHC
 8.0.1]. Of course not directly like this:

 >
 > {{{
 > class Terrible a b | a -> b
 > instance Terrible Int Bool
 > instance Terrible Int Char
 > }}}
 >

 “Instances inconsistent with Functional Dependency”. But we can abuse
 GHC’s "bogus consistency check" ticket:10675#comment:15.

 {{{
 {-# LANGUAGE UndecidableInstances, … #-}
 class Terrible2 a b | a -> b
 instance {-# OVERLAPS #-} Terrible2 Int Bool
 instance {-# OVERLAPS #-} (b ~ Char) => Terrible2 Int b
 }}}

 If the usage site gives you wanted `b ~ Bool`, this uses the first
 instance. Otherwise it selects the second instance and improves to `b ~
 Char`.

 >
 > {{{
 > foo :: Terrible a b => a -> b
 > foo = undefined
 > }}}
 >
 > and we call `show (foo (5 :: Int))`. GHC has to figure out what type the
 argument to `show` has so it can supply the right `Show` instance. In this
 case, the type inferred for `foo (5 :: Int)` will either be `Bool` or
 `Char`, depending on the whims of GHC at the moment. They're called
 dysfunctional for a reason!
 >

 Want to choose one of those instances arbitrarily, in the absence of any
 wanted for `b`? Then just change the pragmas to `{-# INCOHERENT #-}`.

 You have more possible instances? Then repeat the trick. Instead of that
 second instance:

 {{{
 instance {-# INCOHERENT #-} (Terrible3 Int b) => Terrible2 Int b

 class Terrible3 a b | a -> b
 instance {-# INCOHERENT #-} Terrible3 Int Char
 instance {-# INCOHERENT #-} (Terrible4 Int b) =>  Terrible3 Int b

 -- context gives you the constructor only? Then you can improve the
 content:

 class Terrible4 a b | a -> b
 instance {-# INCOHERENT #-} (b’ ~ String) => Terrible4 Int (Maybe b’)
 instance {-# INCOHERENT #-} (Terrible5 Int b) => Terrible4 Int b
 }}}

 This is a (verbose) way to achieve a Closed Class. The thing we can’t get
 is per @Danilo’s O.P. with a free type var:

 {{{
 class Terrible5 a b | a -> b
 instance {-# INCOHERENT #-} (out ~ (t1 -> t1)) => Terrible5 Int out
 }}}

 Too liberal even for the Liberal Coverage Conditions.

 Perhaps if there’s a known set of choices for `t1` we could write out a
 class/instance for each? (With a default improvement at the end of the
 chain.)

 It's difficult to see this is any genuine variety of `FunDep`. It just
 evades the error you'd get in `show ( foo (5 :: Int) )` about an ambiguous
 type. I suppose we're lucky GHC has never applied the rule (from the
 original FunDeps paper) that if we have `Terrible Int b1` and `Terrible
 Int b2` then `b1 = b2` (that's identical types, not merely unifiable --
 not that they're even unifiable for `Terrible`).

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