Opened 4 years ago

Last modified 17 months ago

#10572 new bug

Type signatures are not implicitly quantified over TH type variables

Reported by: spinda Owned by:
Priority: normal Milestone:
Component: Template Haskell Version: 7.10.1
Keywords: Cc: mgsloan, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by spinda)

Consider this simple quasiquoter producing a type variable:

tv :: QuasiQuoter
tv = QuasiQuoter { quoteType = varT . mkName }

If a type variable is introduced elsewhere in a type signature, it is implicitly quantified as normal and the TH name resolves properly:

id' :: a -> [tv|a|]
id' x = x

But if the type variable is not mentioned elsewhere in the type, an error results:

const' :: a -> [tv|b|] -> a
const' x _ = x
Not in scope: type variable ‘b’

One would expect the type variable introduced by the TH splice to be included in the implicit quantification of the type signature.

In fact, there is no way to introduce a new type variable in this context, apart from using Rank(2/N)Types with an explicit forall. But this prevents the type variable from being referred to elsewhere in the type, eg:

const'' :: [tv|a|] -> b -> [tv|a|]
const'' x _ = x

Change History (7)

comment:1 Changed 4 years ago by spinda

Description: modified (diff)

comment:2 Changed 4 years ago by spinda

Summary: Template Haskell does not implicitly quantify typesType signatures are not implicitly quantified over TH type variables

comment:3 Changed 4 years ago by goldfire

Quite right. Should be easy enough to fix. I'm not going to put the newcomer tag on this one, because renaming and scoping and such has tended to be a little challenging, but my guess is that this is straightforward.

comment:4 Changed 4 years ago by mgsloan

Cc: mgsloan added

comment:5 Changed 17 months ago by sighingnow

Differential Rev(s): Phab:D4641
Status: newpatch
Test Case: tests/th/T10572a, tests/th/T10572a

comment:6 Changed 17 months ago by simonpj

Cc: goldfire added

Thanks for the patch. I've had a look, and I really wonder whether the gain is worth the pain.

The pain is significant: a whole extra usually-wasted pass trySpliceTy over every HsType to expand any splices, before renaming. And I'm not even certain that will work; what about

f :: $(g 'a) -> a

Here g 'a might expand to some type involving a; but it does require a to be in scope already.

In the examples, wouldn't it all be clearer if we had an explicit forall? Thus

const'' :: forall a. [tv|a|] -> b -> [tv|a|]

Overall, I feel unsure about this.

Richard, you are TH supremo, and you wrote the still-rather-cyptic note

Note [rnSplicePat]
~~~~~~~~~~~~~~~~~~
Renaming a pattern splice is a bit tricky, because we need the variables
bound in the pattern to be in scope in the RHS of the pattern. This scope
management is effectively done by using continuation-passing style in
RnPat, through the CpsRn monad. We don't wish to be in that monad here
(it would create import cycles and generally conflict with renaming other
splices), so we really want to return a (Pat RdrName) -- the result of
running the splice -- which can then be further renamed in RnPat, in
the CpsRn monad.

The problem is that if we're renaming a splice within a bracket, we
*don't* want to run the splice now. We really do just want to rename
it to an HsSplice Name. Of course, then we can't know what variables
are bound within the splice. So we accept any unbound variables and
rename them again when the bracket is spliced in.  If a variable is brought
into scope by a pattern splice all is fine.  If it is not then an error is
reported.

In any case, when we're done in rnSplicePat, we'll either have a
Pat RdrName (the result of running a top-level splice) or a Pat Name
(the renamed nested splice). Thus, the awkward return type of
rnSplicePat.

(NB: the pattern situation is much less bad than the propose solution for types, because it doesn't require a whole extra pass.)

comment:7 Changed 17 months ago by sighingnow

Differential Rev(s): Phab:D4641
Status: patchnew
Test Case: tests/th/T10572a, tests/th/T10572a

I have realized that my previous patch couldn't remedy the situation. I have mark my previous patch as abandoned.

For

f :: $(g 'a) -> a

This patch doesn't work. Sorry for the noise.

Note: See TracTickets for help on using tickets.