Curious kind-checking failure with GHC 9.2.1 and visible dependent quantification

While porting some code over to GHC 9.2.1 recently, I noticed an unusual quirk in the way kind inference interacts with visible dependent quantification. Consider these two modules:

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module A where

import Data.Kind

type T1 :: Type -> Type
data T1 a = MkT1

t1FunA :: (forall a. T1 a -> r) -> r
t1FunA g = g MkT1

t1FunB :: T1 a -> T1 a -> ()
t1FunB _ _ = ()

type T2 :: forall (a :: Type) -> Type
data T2 a = MkT2

t2FunA :: (forall a. T2 a -> r) -> r
t2FunA g = g MkT2

t2FunB :: T2 a -> T2 a -> ()
t2FunB _ _ = ()

{-# LANGUAGE NoPolyKinds #-}
module B where

import A

g1 :: ()
g1 = t1FunA $ \x ->
     let y = MkT1
     in t1FunB x y

g2 :: ()
g2 = t2FunA $ \x ->
     let y = MkT2
     in t2FunB x y

The A module defines two data types, T1 and T2, as well as some functions which use them. The only difference between T1 and T2 is that the latter uses visible dependent quantification while the former does not. The B module uses these functions in a relatively straightforward way. Note that B does not enable PolyKinds (I distilled this from a cabal project which uses Haskell2010).

What's curious about this is that while both g1 and g2 will typecheck on GHC 9.0.2, only g1 typechecks on GHC 9.2.1. On the other hand, g2 will fail to typecheck in GHC 9.2.1:

$ ghc-9.2.1 B.hs
[1 of 2] Compiling A                ( A.hs, A.o )
[2 of 2] Compiling B                ( B.hs, B.o )

B.hs:14:18: error:
    • Couldn't match type ‘a’ with ‘*’
      Expected: T2 a
        Actual: T2 (*)
      ‘a’ is a rigid type variable bound by
        a type expected by the context:
          forall a. T2 a -> ()
        at B.hs:(12,15)-(14,18)
    • In the second argument of ‘t2FunB’, namely ‘y’
      In the expression: t2FunB x y
      In the expression: let y = MkT2 in t2FunB x y
    • Relevant bindings include x :: T2 a (bound at B.hs:12:16)
   |
14 |      in t2FunB x y
   |                  ^

I'm not confident enough to claim with 100% certainty that this is a regression, since the use of NoPolyKinds might be throwing a wrench into things. Indeed, enabling PolyKinds is enough to make the program accepted again. Still, the fact that this only fails if the data type uses visible dependent quantification (and only with GHC 9.2.1) is rather strange, so I wanted to file an issue to ask people more knowledgeable in this space than I am.