Reification of out-of-scope variables?

[Facundo Domínguez]

An implementation for untyped splices could be:
* Have a map from internal names to the local typing environments.
* When the renamer runs addGroupFinalizer it generates an internal
name and annotates the AST with the internal name at the location of
the splice.
* When the type checker finds the annotation it inserts the local
typing environment in the map.
* When the finalizer runs, it looks up its local typing environment in the map.

It is not as simple as running the splice in the typechecker, but
would you still be happy merging a solution like this?

Facundo


On Wed, Apr 13, 2016 at 6:09 AM, Boespflug, Mathieu <m at tweag.io> wrote:
> 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
>>