[GHC] #15989: Adding extra quantified constraints leads to resolution failure

[GHC]

#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.html#overlap
 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