#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