GitLab

(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 into HsExpanded $(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. See Note [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 have

  type 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 make splitHsApps 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.