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).