[GHC] #15974: QuantifiedConstraints: Spurious error involving superclass constraints

[GHC]

#15974: QuantifiedConstraints: Spurious error involving superclass constraints
-------------------------------------+-------------------------------------
        Reporter:  lexi.lambda       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.3
       Component:  Compiler          |              Version:  8.6.2
      Resolution:  invalid           |             Keywords:
                                     |  QuantifiedConstraints
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:                    |
-------------------------------------+-------------------------------------
Changes (by lexi.lambda):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 I discovered #14831, which is superficially related to this ticket, but I
 think the issues are actually distinct. The issue in that ticket is that
 GHC has //two different// options for solving a constraint, and it picks
 the wrong one. After reading some of the discussion there, however, I
 think I understand what’s going on in this ticket, and I don’t think it’s
 an issue with GHC making the wrong choice, but rather GHC having only one
 choice to make.

 In the program in the ticket, GHC is performing the following steps:

 1. GHC attempts to solve the superclass constraint `A (X f)` when
 declaring the `B (X f)` instance.

 2. Since the only way to get there is through the instance declaration for
 `A (X f)`, it then tries to solve the (quantified) instance context,
 `forall a. A a => A (f a)`.

 3. GHC then attempts to solve `A (f a)`, assuming it has `A a`, and it
 only has one path to get there, which is through `B (f a)` (via the
 superclass relationship).

 4. It then tries to solve `B a`, since that is the quantified context of
 `B (f a)`, and it gets stuck.

 This suggests a fix: add `forall a. A a => A (f a)` to the instance
 context for `B (X f)`. And indeed, the following declaration is accepted!

 {{{#!hs
 instance (forall a. A a => A (f a), forall a. B a => B (f a)) => B (X f)
 }}}

 This is unintuitive to me, since when I write, say, `Eq` and `Ord`
 instance on a datatype, I merely write them like

 {{{#!hs
 instance Eq a => Eq (List a)
 instance Ord a => Ord (List a)
 }}}

 not like

 {{{#!hs
 instance Eq a => Eq (List a)
 instance (Eq a, Ord a) => Ord (List a)
 }}}

 …but this works out only because `Ord a` entails `Eq a`. In this case,
 `forall a. B a => B (f a)` does **not** actually entail `forall a. A a =>
 A (f a)`, so I guess this is not actually a bug.

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