Adding extra quantified constraints leads to resolution failure
{-# 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 onAllowAmbiguousTypes
, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter thatx'
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 onfmap
(but notpure
) — which is the superclass doesn't seem to matter