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 |