#15989: Adding extra quantified constraints leads to resolution failure -------------------------------------+------------------------------------- Reporter: eror | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.3 Component: Compiler (Type | Version: 8.6.2 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by eror: Old description:
{{{ {-# 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` fail 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
New description: {{{ {-# 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 -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15989#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler