GHC 9.2.1 typechecking regression with RankNTypes, TemplateHaskell, and compound expressions
(Originally spun off from #21038 (comment 407457))
The crux-llvm
library (specifically, this code) typechecks on GHC 9.0.2 and earlier, but fails to typecheck with GHC 9.2.1. I made an attempt to minimize the issue in #21038 (closed), but after trying again with that patch, I discovered that crux-llvm
still does not typecheck. It turns out that my minimization of the issue was a bit too minimal. Here is an example that better illustrates what is going on:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}
module Bug where
data Foo = MkFoo () (forall a. a -> a)
worksOnAllGHCs1 :: Foo
worksOnAllGHCs1 = MkFoo () (\x -> x)
worksOnAllGHCs2 :: Foo
worksOnAllGHCs2 = MkFoo () $ \x -> x
worksOnAllGHCs42 :: Foo
worksOnAllGHCs42 = (MkFoo ()) $ \x -> x
doesn'tWorkOnGHC9'2 :: Foo
doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
As the names suggest, all of the things functions will typecheck on GHC 9.0.2 and earlier. The worksOnAllGHCs{1,2,3}
functions will typecheck on GHC 9.2.1, but doesn'tWorkOnGHC9'2
will not:
$ ghc-9.2.1 Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o, Bug.dyn_o )
Bug.hs:17:24: error:
• Couldn't match type: forall a. a -> a
with: p0 -> p0
Expected: (p0 -> p0) -> Foo
Actual: (forall a. a -> a) -> Foo
• In the first argument of ‘($)’, namely ‘(MkFoo ())’
In the expression: (MkFoo ()) $ \ x -> x
In an equation for ‘doesn'tWorkOnGHC9'2’:
doesn'tWorkOnGHC9'2 = (MkFoo ()) $ \ x -> x
|
17 | doesn'tWorkOnGHC9'2 = $([| MkFoo () |]) $ \x -> x
| ^^^^^^^^^^^^^^^^
The commit which introduced this regression is 9632f413 (Implement Quick Look impredicativity
).
Note that unlike the example in #21038 (closed), the expression being spliced isn't a simple identifier (i.e., a "head", to use Quick Look terminology), but rather a compound expression. @simonpj suggests the following fix:
Ah yes. Hmm. Reflecting on this, I think the Right Thing is to treat a splice that is run in the renamer (i.e. an untyped TH splice) as using the "HsExpansion" mechanism. See
Note [Handling overloaded and rebindable constructs]
in GHC.Tc.Rename.Expr.That is, the splice
$(expr)
turns intoHsExpanded $(expr) <result-of-running-splice>
. After all, it really is an expansion! Then the stuff in the type checker will deal smoothly with application chains. SeeNote [Looking through HsExpanded]
in GHC.Tc.Gen.Head.In principle that should be pretty easy. But
Note [Delaying modFinalizers in untyped splices]
in GHC.Rename.Splice is a painful wart that will hurt us here.
Where might we store these modFinalizdrs in the HsExpanded? Maybe in the first (original expression) field?
Actually I think I favour separating them out entirely into a new extension constructor for
HsExpr GhcRn
. Currenlty we havetype instance XXExpr GhcRn = HsExpansion (HsExpr GhcRn) (HsExpr GhcRn) type instance XXExpr GhcTc = XXExprGhcTc
We could instead have
type instance XXExpr GhcRn = XXExprGhcRn data XXExprGhcRn = ExpansionRn (HsExpansion (HsExpr GhcRn) (HsExpr GhcRn)) | AddModFinalizedrs ThModFinalizers (HsExpr GhcRn)
In exchange we can get rid of
HsSpliced
altogether.We still need to call
addModFinalizersWithLclEnv
on those finalisers; so it looks as if we'd need to makesplitHsApps
monadic. That's a pain, but not actually difficult.I'm not certain of this. But something along these lines seems like the right solution.