Reification of out-of-scope variables?

[Boespflug, Mathieu]

Hi Richard,

Facundo and I had a chat about this offline. Facundo noticed that
there /is/ a form of splicing that runs during type checking, and
therefore has access to the type environment: namely typed splices,
which return a TExp rather than an Exp. Turns out the example from my
first email does work if you adapt it to use typed splices:

f :: Int -> Int
f x = $$(do let {name = mkName x}; info <- reify name; runIO (print
info) [|| x ||])

Running reify still doesn't work inside addModFinalizer, but at least
we do have access to x's type from within the typed splice, so we can
record it for use in the foreign code generation phase later.

The issue is, typed splices run afoul of the very same issue that
caused GHC HQ to move splice expansion out of the type checker and
into the renamer: namely that type inference becomes observable, as
documented here:

https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/BlogPostChanges

In particular,

f x = $$(... same splice as above...) `asTypeOf` True

yields a type error, while

f :: Bool -> Bool
f x = $$(... same splice as above...)

does not.

So let's discuss what the next actions are:

* Should we consider it a bug (and file a ticket) that reification in
typed splices is able to observe the order of type checking, just like
reify used to do in untyped splices?
* While Richard's proposed addGroupFinalizer might not work with
untyped splices, perhaps it can be made to work with typed splices,
since these run in the type checker?
* If part of the solution here is to use typed splices, how do we get
quasiquotation to be syntactic sugar for a *typed* splice? Do we want
to be introducing a typed quasiquotation syntax, just like Geoff did
for much of the rest of Template Haskell?

Facundo and I think that something like Richard's addGroupFinalizer is
still interesting to have, because while reification during type
checking sounds dubious, reification /after/ the declaration group is
fully type checked is perfectly safe.

Best,
--
Mathieu Boespflug
Founder at http://tweag.io.


On 13 April 2016 at 04:25, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> On Apr 12, 2016, at 5:35 PM, Facundo Domínguez <facundo.dominguez at tweag.io> wrote:
>
>> Hello Richard,
>>
>>> TH will offer a new function `addGroupFinalizer :: Q () -> Q ()` that runs its argument in the local typing environment available when addGroupFinalizer is called.
>>
>> When considering this approach, how could one capture the local typing
>> environment given that the untyped splices are run in the renamer
>> where no such environment is populated yet?
>>
>
> Ah. Excellent point. I hadn't quite thought it through. Not sure, off the top of my head, how to get around this.
>
> Richard
>