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

 I have another use case for dysfunctional dependencies. While I agree that
 the problem could be solved "just with type annotations", the burden would
 be quite high:

 {{{#!haskell

 {-# LANGUAGE RebindableSyntax, MultiParamTypeClasses, FlexibleInstances,
              AllowAmbiguousTypes, FunctionalDependencies #-}

 module PolyMonad where

 import Prelude hiding (Monad(..))

   -- normal, "monomorphic" monads
 class Monad m where
   return :: a -> m a
   bind   :: m a -> (a -> m b) -> m b
   fail   :: String -> m a

   -- Morph m1 m2 means that we can lift results in m1 to results in m2
 class Morph m1 m2 where
   morph :: m1 a -> m2 a

   -- Three monads form a polymonad when we can define this kind of
   -- bind operation. The functional dependency is very much meant to
   -- be *dys*functional, in that GHC should use it only when it has
   -- no other means to determine m3.
 class PolyMonad m1 m2 m3 | m1 m2 -> m3 where
   (>>=) :: m1 a -> (a -> m2 b) -> m3 b

 -- This is my desired instance, rejected (quite rightly) by the coverage
 -- condition:

 -- instance (Morph m1 m3, Morph m2 m3, Monad m3) => PolyMonad m1 m2 m3
 where
 --   ma >>= fmb = bind (morph ma) (morph . fmb)

 -- an example of this in action:
 newtype Id a = Id a
 instance Monad Id where
   return = Id
   bind (Id x) f = f x
   fail = error

 instance Morph m m where
   morph = id

 -- Without the fundep on PolyMonad, `f` cannot type-check,
 -- even with a top-level type signature, because of inherent
 -- ambiguity.
 f x y z = do a <- x
              b <- y a
              z b

 }}}

 Instead of using fancy rebindable syntax, I could write out my definition
 for `f`, put in lots of type annotations with lots of scoped type
 variables, and get away with it all. But that's quite a dissatisfying
 answer here. One of the key reasons why I'm OK with dysfunctionality here
 is that there is an (unenforced) expectation of coherence among `Morph`
 instances. That is, if we have `Morph m1 m2` and `Morph m2 m3`, I expect
 also to have `Morph m1 m3` such that `morph == morph . morph`, if you
 follow my meaning. Without this coherence, the dysfunctionality is indeed
 disastrous... but, I believe that `Morph` coherence would allow the code
 above to work nicely.

 This is why I've always seen dysfunctional dependencies to be quite like
 incoherent instances. We're asking GHC to care less about consistency so
 that we, the programmer, can care more.

 Following this further, I disagree with Martin in comment:33 saying that
 we insist on consistency. He gives the following example:

 {{{#!haskell
 class C a b | a -> b
 instance C Int Bool
 instance C Int Char
 }}}

 In a dysfunctional world, what's wrong with this? It absolutely does mean
 that if GHC has to satisfy `C Int x`, an arbitrary and fragile choice will
 be made. But it also means that GHC can satisfy both `C Int Bool` and `C
 Int Char` if it needs to. It's up to the programmer to ensure that the
 implementations of the instances obey some set of properties so that the
 program's behavior is not fragile. This seems like a reasonable burden to
 me.

 danilo2, does my example above work with your `DysfunctionalDependencies`,
 with the instance put in?

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