This looks to me like the fix to #15244 (closed) not properly generalizing to constraints with different forall
s that actually mean the same thing.
(Why do I want to use a constraint like this in the first place? I discovered this while trying to write something like
( forall x x'. x ~ x' => MonadReader (Env x) (m x')
, forall x. MonadWriter Log (m x)
)
where the two type variables and equality constraint are there to work around #15351.)
( forall x x'. Monad (m x), forall x. Traversable (m x) )
and ( forall x x'. Traversable (m x), forall x. Monad (m x) )
both fail on fmap
but not pure
, which makes it look like the problem is in resolving classes that are superclasses of more than one of the constraints.( forall x. Monad (m x), Monad (m y) )
compiles.{# LANGUAGE QuantifiedConstraints, FlexibleContexts #}
import Control.Monad.Reader
data T x = T
ok :: ( forall x x'. MonadReader (T x) (m x') )
=> m y Bool
ok = fmap not (pure True)
bad :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Monad (m x) )
=> m y Bool
bad = fmap not (pure True)
better :: ( forall x x'. MonadReader (T x) (m x')
, forall x. Applicative (m x)
, forall x. Functor (m x) )
=> m y Bool
better = fmap not (pure True)
ok
and better
compile, but bad
fails to resolve, despite having strictly more in the context than ok
:
BadQC.hs:15:7: error:
• Could not deduce (Functor (m y)) arising from a use of ‘fmap’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^^^^^^^^^^^^
BadQC.hs:15:17: error:
• Could not deduce (Applicative (m y)) arising from a use of ‘pure’
from the context: (forall x x'. MonadReader (T x) (m x'),
forall x. Monad (m x))
bound by the type signature for:
bad :: forall (m :: * > * > *) y.
(forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
m y Bool
at BadQC.hs:(12,1)(14,15)
• In the second argument of ‘fmap’, namely ‘(pure True)’
In the expression: fmap not (pure True)
In an equation for ‘bad’: bad = fmap not (pure True)

15  bad = fmap not (pure True)
 ^^^^^^^^^
Failed, no modules loaded.
Also:
( forall x. MonadReader (T x) (m x), forall x. Monad (m x) )
compiles — the error seems to require two quantified type variables( forall x x'. Monad (m x), forall x. Monad (m x) )
reports an ambiguity error on the constraint, which makes sense; if I turn on AllowAmbiguousTypes
, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that x'
is unused( forall x x'. Foldable (m x), forall x. Monad (m x) )
and ( forall x x'. Monad (m x), forall x. Foldable (m x) )
compile — being in the same class hierarchy matters( forall x x'. Applicative (m x), forall x. Monad (m x) )
fails on fmap
(but not pure
) — which is the superclass doesn't seem to matter