Adding extra quantified constraints leads to resolution failure

{-# LANGUAGE QuantifiedConstraints, FlexibleContexts #-}

import Control.Monad.Reader

data T x = T


ok :: ( forall x x'. MonadReader (T x) (m x') )
   => m y Bool
ok = fmap not (pure True)

bad :: ( forall x x'. MonadReader (T x) (m x')
       , forall x. Monad (m x) )
    => m y Bool
bad = fmap not (pure True)

better :: ( forall x x'. MonadReader (T x) (m x')
          , forall x. Applicative (m x)
          , forall x. Functor (m x) )
       => m y Bool
better = fmap not (pure True)

ok and better compile, but bad fails to resolve, despite having strictly more in the context than ok:

BadQC.hs:15:7: error:
    • Could not deduce (Functor (m y)) arising from a use of ‘fmap’
      from the context: (forall x x'. MonadReader (T x) (m x'),
                         forall x. Monad (m x))
        bound by the type signature for:
                   bad :: forall (m :: * -> * -> *) y.
                          (forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
                          m y Bool
        at BadQC.hs:(12,1)-(14,15)
    • In the expression: fmap not (pure True)
      In an equation for ‘bad’: bad = fmap not (pure True)
   |
15 | bad = fmap not (pure True)
   |       ^^^^^^^^^^^^^^^^^^^^

BadQC.hs:15:17: error:
    • Could not deduce (Applicative (m y)) arising from a use of ‘pure’
      from the context: (forall x x'. MonadReader (T x) (m x'),
                         forall x. Monad (m x))
        bound by the type signature for:
                   bad :: forall (m :: * -> * -> *) y.
                          (forall x x'. MonadReader (T x) (m x'), forall x. Monad (m x)) =>
                          m y Bool
        at BadQC.hs:(12,1)-(14,15)
    • In the second argument of ‘fmap’, namely ‘(pure True)’
      In the expression: fmap not (pure True)
      In an equation for ‘bad’: bad = fmap not (pure True)
   |
15 | bad = fmap not (pure True)
   |                 ^^^^^^^^^
Failed, no modules loaded.

Also:

• ( forall x. MonadReader (T x) (m x), forall x. Monad (m x) ) compiles — the error seems to require two quantified type variables
• ( forall x x'. Monad (m x), forall x. Monad (m x) ) reports an ambiguity error on the constraint, which makes sense; if I turn on AllowAmbiguousTypes, it fails with the same error as above — the error isn't caused by MPTCs, and it doesn't matter that x' is unused
• ( forall x x'. Foldable (m x), forall x. Monad (m x) ) and ( forall x x'. Monad (m x), forall x. Foldable (m x) ) compile — being in the same class hierarchy matters
• ( forall x x'. Applicative (m x), forall x. Monad (m x) ) fails on fmap (but not pure) — which is the superclass doesn't seem to matter