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

29 Nov 2018

      #15974: QuantifiedConstraints: Spurious error involving superclass constraints
-------------------------------------+-------------------------------------
           Reporter:  lexi.lambda    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.3
          Component:  Compiler       |           Version:  8.6.2
           Keywords:                 |  Operating System:  Unknown/Multiple
  QuantifiedConstraints              |
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# LANGUAGE KindSignatures, QuantifiedConstraints, UndecidableInstances
 #-}
 }}}

 Consider the following datatype and two classes:

 {{{#!hs
 data X (f :: * -> *)

 class A a
 class A a => B a
 }}}

 If I create an instance `A (X f)` involving a quantified constraint

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

 then curiously, the following instance declaration for `B (X f)` is
 rejected with the accompanying error message:

 {{{#!hs
 instance (forall a. B a => B (f a)) => B (X f)
 }}}
 {{{
 /tmp/qc.hs:11:10: error:
     • Could not deduce (B a)
         arising from the superclasses of an instance declaration
       from the context: forall a. B a => B (f a)
         bound by the instance declaration at /tmp/qc.hs:11:10-46
       or from: A a bound by a quantified context at /tmp/qc.hs:1:1
       Possible fix: add (B a) to the context of a quantified context
     • In the instance declaration for ‘B (X f)’
    |
 11 | instance (forall a. B a => B (f a)) => B (X f)
    |          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 Notably, if the instance declaration for `A (X f)` is altered to not use a
 quantified constraint, as in

 {{{#!hs
 instance A (f (X f)) => A (X f)
 }}}

 or even just

 {{{#!hs
 instance A (X f)
 }}}

 then the above instance declaration for `B (X f)` is accepted.

 I see no reason that the `B (X f)` declaration should be rejected, even
 with the quantified constraint in the instance context for `A (X f)`. The
 error message complains that the typechecker cannot deduce `B a`, and it
 even suggests adding `B a` to the context of the quantified constraint,
 but `B a` is //already// in that context.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15974
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler