[GHC] #14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a class alias

[GHC]

#14879: QuantifiedConstraints: Big error message + can't substitute (=>) with a
class alias
-------------------------------------+-------------------------------------
        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):

 Iceland Jack!  You are torturing me.  Here is what is happening.

 To deal with `yo` we want to solve
 {{{
 [W] Implies (Yo a b) (Implies a b)
 }}}
 We proceed as follows
 {{{
      [W] Implies (Yo a b) (Implies a b)

 ===> (apply instance)
      [W] (forall {}. Yo a b => Implies a b)     -- A quantified constraint

 ===> build implication constraint
      forall {}. [G] Yo a b
              => [W] Implies a b
 }}}
 So we have a Given constraint `[G] Yo a b`.  So we expand its superclasss
 giving
 {{{
     [G] (forall xx. Implies (Implies b xx) (Implies a xx))
 }}}
 and try solving
 {{{
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
              => [W] Implies a b
 }}}
 Ok... now we return attention to that Wanted and try to solve it.  Use the
 top level instance!  Gives us
 {{{
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
              => [W] Implies a b

 ===> (top level instance)
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
              => [W] (a => b)

 ===> (build implication constraint)
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
              => forall {}. [G] a
                         => [W] b

 }}}
 Now we seem to be stuck so we expand another layer of superclasses.
 We can take the superclasses of that quantified constraint (as in
 [https://github.com/Gertjan423/ghc-proposals/blob/quantified-
 constraints/proposals/0000-quantified-constraints.rst Section 3.4 of the
 proposal]) giving us
 {{{
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
                 [G] (forall xx. Implies b xx => Implies a xx)
 --- Next superclass
              => forall {}. [G] a
                         => [W] b
 }}}
 We are still stuck, so expand sueprclasses again:
 {{{
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies (Implies b xx) (Implies a xx))
                 [G] (forall xx. Implies b xx => Implies a xx)
                 [G] (forall xx. Implies b xx => a => xx)            ---
 Next superclass
              => forall {}. [G] a
                         => [W] b
 }}}
 And now we are in a very bad place.  We have a Given quantified constraint
 that lets us solve ANY constraint `xx` (for any `xx`!).  But in solving
 it, we just get another bigger problem to solve.  So solving diverges.

 I hvae no idea what you are trying to do, but GHC seems to be behaving
 quite reasonably.

 Why does it "work" you have `=>` instead of `Implies` in the superclass
 for `Yo`?   (The instance for `Yo` is irrelevant; just delete it.)  By a
 fluke.  We get as before
 {{{
      forall {}. [G] Yo a b
              => [W] Implies a b
 }}}
 But we expand the given superclasses layer by layer, so before trying to
 solve the Wanted we get
 {{{
      forall {}. [G] Yo a b
                 [G] (forall xx. Implies b xx => Implies a xx)    --
 Superclass!
              => [W] Implies a b
 }}}
 Now it just happens that the wanted matches the quantified constraint, we
 can apply that local instance decl giving `[W] Implies b b` which we can
 solve.

 ----------------
 There are several difficulties here.

 * First, your setup is weird.  If you expand superclasses enough, you get
 to prove any constraint whatsoever, and that is plainly stupid.

 * I don't like flukes.  Maybe we should not make use the local instance
 (quantified constraint) if the constraint we are solving also matches a
 global instance.  Curerntly we make the local ones "shadow" the global
 ones.

 * The superclass expansion is a bit less aggressive than I expected; I'm
 not sure why. If we expanded more vigorously, the fluke would happen both
 times.  I'm not sure how hard to work on this.

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