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

 Replying to [comment:41 goldfire]:
 It deos not, but from simple reason. Your instance for PolyMonad does not
 specify what is the `m3` in any sense. I mean - you are using `(morph ma)`
 and `(morph . fmb)`. According to open world assumption, anybody can
 create any instance for `Morph` class, which is NOT injective, so we get
 here disambigous types:

 {{{#!haskell
     Could not deduce (Monad m20)
       arising from the ambiguity check for ‘f’
     from the context (Monad m3,
                       Monad m2,
                       Morph m5 m2,
                       Morph m4 m2,
                       Morph m2 m3,
                       Morph m1 m3)
       bound by the inferred type for ‘f’:
                  (Monad m3, Monad m2, Morph m5 m2, Morph m4 m2, Morph m2
 m3,
                   Morph m1 m3) =>
                  m1 t -> (t -> m4 t1) -> (t1 -> m5 b) -> m3 b
       at Tmp.hs:(44,1)-(46,16)
     The type variable ‘m20’ is ambiguous
     When checking that ‘f’ has the inferred type
       f :: forall t
                   (m1 :: * -> *)
                   (m2 :: * -> *)
                   (m3 :: * -> *)
                   b
                   t1
                   (m4 :: * -> *)
                   (m5 :: * -> *).
            (Monad m3, Monad m2, Morph m5 m2, Morph m4 m2, Morph m2 m3,
             Morph m1 m3) =>
            m1 t -> (t -> m4 t1) -> (t1 -> m5 b) -> m3 b
     Probable cause: the inferred type is ambiguous
 }}}

 But your example can be easly fixed by defining any hints and NOT using
 `-XDysfunctionalDependencies` like this:

 {{{#!haskell
 {-# LANGUAGE RebindableSyntax, MultiParamTypeClasses, FlexibleInstances,
              AllowAmbiguousTypes, FunctionalDependencies,
              NoMonomorphismRestriction, ScopedTypeVariables,
 UndecidableInstances #-}

 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:

 class (Monad m1, Monad m2, Monad m3) => MatchMonad m1 m2 m3 | m1 m2 -> m3


 instance (Morph m1 m3, Morph m2 m3, Monad m3, MatchMonad m1 m2 m3) =>
 PolyMonad m1 m2 m3 where
   ma >>= fmb = bind (morph ma) (morph . fmb)
   -- ma >>= fmb = bind (matchMonad (morph ma) (undefined:: )) (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 a
 }}}

 Still, I completely agree with all the things you stated in your post.

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