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

 Hi Richard, I think we're already (at GHC 7.10/8.0) pretty close to being
 able to write your `class Terrible`.
 >
 > {{{
 > class Terrible a b | a -> b
 > instance Terrible Int Bool
 > instance Terrible Int Char
 > }}}

 See Iavor's example comment:12:ticket:10675. Or this
 https://mail.haskell.org/pipermail/glasgow-haskell-
 users/2017-April/026507.html .

 Both examples rely on `UndecidableInstances` and overlaps. Not necessrily
 `OverlappingInstances`: in Iavor's example, the FunDeps are non-full.

 >
 > {{{
 > 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.

 In those examples I cited, GHC does make a predictable choice (so not
 entirely on a whim). But it's inconsistent between the FunDeps, so very
 sensitive to subtle changes in (apparently) unrelated parts of the
 program/some distant module. For example, merely adding a type signature
 could trigger selecting a different instance.

 > ... Much like with `IncoherentInstances`, it's up to the user not to
 shoot themselves in the foot.
 >

 With a great deal of hindsight, what `Undecidable` means in these cases
 is:

 * The type specified in the instance head isn't mechanically derivable
 from the other type parameters. So the programmer is saying "trust me, at
 any use site, you'll be able to figure out the right type".
 * GHC can't follow the trail of instance constraints/instantiation --
 especially because it might need looking at other modules and/or a very
 long chain.
 * So `Undecidable` means GHC can't/won't decide whether any given FunDep
 is instantiated consistently across all the instances.

 I'm not sure that's abundantly well explained in the docos. OTOH, there's
 some type-level programming that deliberately exploits that inconsistency
 -- such as anything that despatches on a type-level type-equality
 condition (the whole of the HList library, as originally developed).
 Closed type families is nowadays a much more hygienic mechanism.

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