[GHC] #14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'

[GHC]

#14877: QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      Resolution:                    |             Keywords:
                                     |  QuantifiedConstraints, wipT2893
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Consider the quantified constraint (QC) in
 {{{
 instance (forall xx. (xx => a) => Implies xx b)
       => F a b
 }}}
 It serves as a local instance declaration.  To construct the dictionary
 for `(F a b)` I may need to to solve a constraint `(Implies xx b)`.  The
 QC says "if you want to solve `Implies xx b`, then it suffices to prove
 `xx => a`".  And to prove `xx => a`, the built-in rules assume `xx` and
 try to prove `a`.

 It's quite different to say
 {{{
 instance (forall xx. (xx => a) => (xx => b)
       => F a b
 }}}
 That is precisely equivalant to
 {{{
 instance (forall xx. (xx => a, xx) => b)
       => F a b
 }}}
 Now the QC says "if you want to solve the goal `b`, then conjure up some
 constraint `xx`, and prove `(xx => a, xx)`.  But how can we guess `xx`?

 Each QC has an instance "head", usually headed by a type constructor,
 sometimes by a type variable.  That head is the pattern the QC can solve.
 `Implies xx b` is a good instance head: it matches things of that form.
 Plain `b` is not a good instance head!

 In short, I see nothing wrong here.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14877#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler