TH doesn't preserve `forall`

I think there are several bugs in the way TH currently deals with type variable quantification.

• *Background**

GHC uses the "forall-or-nothing" rule. This means that, if there is a top-level forall in a type signature, that forall must bind all variables being brought into scope in that signature. Examples:

f1 :: a -> a
f1 x = x    -- OK, no forall

f2 :: forall . a -> a
f2 x = x    -- rejected

f3 :: forall a. a -> a
f3 x = x    -- OK, forall binds all variables

f4 :: forall a. a -> a
f4 x = helper x
  where helper :: a -> a        -- OK; this uses a already in scope
        helper _ = x

f5 :: forall a. a -> a
f5 x = helper x
  where helper :: forall . a -> a   -- OK; a is already in scope
        helper _ = x

f6 :: forall a. a -> a
f6 x = helper x
  where helper :: forall a. a -> a   -- this is a new variable `a`
        helper _ = x     -- rejected; the two `a`s are different

Upshot: the existence of forall matters.

• *Strangeness 1**

foo1 :: $([t| a -> a |])
foo1 x = x

is rejected, because a is not in scope. This is incongruent with the treatment of f1. One could argue, though, that all type variables used in quotes should be in scope. I would disagree with such an argument (that's not what we do these days in terms), but it's not silly.

• *Strangeness 2**

foo2 :: $([t| $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo2 x = x

is rejected because a is not in scope. This behavior seems just wrong.

• *Strangeness 3**

foo3 :: $([t| forall . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo3 x = x

is rejected in the same way as foo2. While this should be rejected (it's f2), -ddump-splices says that the splice evaluates to a -> a; note: no forall. So it's rejected under false pretenses.

• *Strangeness 4**

foo4 :: $([t| forall a . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
foo4 x = x

This one is accepted (as it should be), but it produces a warning!

Scratch.hs:51:21: warning: [-Wunused-foralls]
    Unused quantified type variable ‘a’
    In the type ‘forall a.
                 $(varT (mkName "a")) -> $(varT (mkName "a"))’
   |
51 | foo :: $([t| forall a . $(varT (mkName "a")) -> $(varT (mkName "a")) |])
   |                  

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Template Haskell
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture