Scoped type variables in typed quotes lose scope

Consider the following code. I used GHC-9.2.3.

{-# language TemplateHaskell, ScopedTypeVariables #-}
import Language.Haskell.TH

f :: forall a. CodeQ a -> CodeQ a
f x = [|| let y :: a; y = $$x in y ||]

This typechecks, but the following doesn't:

g :: Bool -> Bool
g x = $$(f [||x||])

I get

    • Couldn't match expected type ‘a’ with actual type ‘Bool’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          x_a8Yw :: forall a. a

It looks like the scoped a is transformed into a generalized a after splicing.

Looking at -ddump-simpl -dsuppress-all, it seems that the connection between the scoped forall a. and the a in x :: a is completely lost in the code for f, although GHC does know about it during type checking f's definition. As far as I see, the same thing happens with all scoped variables in quotes.

One solution would be to have quoting for types. In hypothetical syntax:

f :: forall (a : CodeQ Type). CodeQ $$a -> CodeQ $$a
f @a x = [|| let y :: $$a; y = $$x in y ||]

This one seems a rather big change but I'm not sure about other solutions which are perhaps more realistic to integrate to TH (I don't really know how splice processing works).