[GHC] #8634: Relax functional dependency coherence check ("liberal coverage condition")
GHC
ghc-devs at haskell.org
Tue Jul 22 13:31:14 UTC 2014
#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
More information about the ghc-tickets
mailing list