QuantifiedConstraints: introducing classes through equality constraints fails

The following doesn't typecheck with the wip/T2893 branch:

{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}

module Subst where

class (forall x. c x => d x) => c ~=> d
instance (forall x. c x => d x) => c ~=> d

foo :: forall c a. c ~=> Monoid => (c a => a) -- ok
foo = mempty

bar :: forall c a m. (m ~ Monoid, c ~=> m) => (c a => a) -- ok
bar = mempty

baz :: forall c a. (forall m. m ~ Monoid => c ~=> m) => (c a => a) -- fails
baz = mempty

Prelude> :reload
[1 of 1] Compiling Subst            ( src/Subst.hs, interpreted )

src/Subst.hs:21:7: error:
    • Could not deduce (Monoid a) arising from a use of ‘mempty’
      from the context: (forall (m :: * -> Constraint).
                         (m ~ Monoid) =>
                         c ~=> m,
                         c a)
        bound by the type signature for:
                   baz :: forall (c :: * -> Constraint) a.
                          (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) =>
                          a
        at src/Subst.hs:20:1-66
      Possible fix:
        add (Monoid a) to the context of
          the type signature for:
            baz :: forall (c :: * -> Constraint) a.
                   (forall (m :: * -> Constraint). (m ~ Monoid) => c ~=> m, c a) =>
                   a
    • In the expression: mempty
      In an equation for ‘baz’: baz = mempty
   |
21 | baz = mempty
   |       ^^^^^^
Failed, no modules loaded.

Shouldn't the equality constraint be "substituted in"?

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	Iceland_jack
Operating system
Architecture