#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: | -------------------------------------+------------------------------------- Comment (by eror): (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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15989#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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: | -------------------------------------+------------------------------------- Comment (by simonpj): I agree that it is confusing that adding extra quantified constraints leads to failure. And yet it is [https://downloads.haskell.org/~ghc/8.6.2/docs/html/users_guide/glasgow_exts.... documented in the user manual]. The issue described there is that two quantified constraints may both claim to prove a constraint, but have different contexts, so picking one over the other would yield unpredictable behaviour. In your particular case, however, the available 'Givens' look like this {{{ [G] df_a2ra {0}:: forall x. Functor (m_a2aR[sk:1] x) [G] df_a2r9 {0}:: forall x. Applicative (m_a2aR[sk:1] x) [G] df_a2aV {0}:: forall x. Monad (m_a2aR[sk:1] x) [G] df_a2r8 {0}:: forall x x'. Functor (m_a2aR[sk:1] x') [G] df_a2r7 {0}:: forall x x'. Applicative (m_a2aR[sk:1] x') [G] df_a2r6 {0}:: forall x x'. Monad (m_a2aR[sk:1] x') [G] df_a2aU {0}:: forall x x'. MonadReader (T x) (m_a2aR[sk:1] x') }}} So there are two ways to prove `Functor (m y)` from `df_a2ra` and `df_a2r8`. So GHC takes neither. In this particular case, picking one would ''not'' get stuck, since they both have an empty context. In general, if one has a subset of the context of the other, we could pick that one. This additional check would save the day in this case. But is it sufficiently general to be worth it? The fix in #15244 (See `Note [Do not add duplicate quantified instances]` in `TcSMonad`) is indeed a special case. It looks for ''identical'' givens, and (as you can see above) they aren't quite identical. Perhaps I could prune the quantified variables (you can see that `x` is redundant); and that would solve this particular example. Note that the identical-given idea works on the ''givens themselves'', when adding them to the inert set, rather the ''matching instances'' following a lookup. For example, consider {{{ f :: ( forall a. D a Int , forall b c. D [b] c) => blah }}} These are not identical. But if we seek `D [ty] Int` it'll match both; but since both have an empty context we could pick eitehr. The empty context is easy but it's probably more often like this: {{{ g :: ( forall a. Eq a => D a Int , forall b. Eq b => D [b] c) => blah }}} Now if we wanted to solve `D [ty] Int`, we'll need `Eq [ty]` for the first one, and `Eq ty` for the second. We know that these are equivalent, but it's more of a stretch for GHC to figure that out during instance selection. I'm not sure how clever to try to be here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15989#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler