{-# LANGUAGE KindSignatures, QuantifiedConstraints, UndecidableInstances #-}

Consider the following datatype and two classes:

data X (f :: * -> *)

class A a
class A a => B a

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

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:

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

instance A (f (X f)) => A (X f)

or even just

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.