RequiredTypeArguments doesn't interact with DeepSubsumption

While experimenting with RequiredTypeArguments in GHC 9.10.1-alpha3, I discovered a surprising quirk that feels like a bug, although I'm not entirely sure. For context, suppose you have this program:

{-# LANGUAGE GHC2024 #-}
{-# LANGUAGE DeepSubsumption #-}
{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE TypeAbstractions #-}
module Foo where

f1 :: () -> forall a. Eq a => a -> a -> Bool
f1 () @a = (==) @a

f2 :: () -> forall a. Ord a => a -> a -> Bool
f2 = f1

Note that f2 only typechecks due to DeepSubsumption being enabled.

I decided to see what would happen if I turned the invisible forall a.s to visible forall ->s:

g1 :: () -> forall a -> Eq a => a -> a -> Bool
g1 () a = (==) @a

g2 :: () -> forall a -> Ord a => a -> a -> Bool
g2 = g1

Surprisingly, this doesn't typecheck:

$ ghc-9.10.0.20240413 Foo.hs
[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

Foo.hs:17:6: error: [GHC-83865]
    • Couldn't match type: Eq a
                     with: Ord a
      Expected: forall a -> Ord a => a -> a -> Bool
        Actual: forall a -> Eq a => a -> a -> Bool
    • In the expression: g1
      In an equation for ‘g2’: g2 = g1
   |
17 | g2 = g1
   |      ^^

I would have expected DeepSubsumption to allow g2 to typecheck, much in the same way that f2 typechecks. Note that g2 u = g1 u also does not typecheck.