[ghc-steering-committee] #207: Type variables in TH quotes (recommendation: reject)

[Richard Eisenberg]

Hi committee,

Matthew Pickering has proposed #207: Fix the treatment of type variables in quotations. (In contrast to the email from our Most Honored and Appreciated Secretary: Matt wrote the proposal, not me.)

PR: https://github.com/ghc-proposals/ghc-proposals/pull/207 <https://github.com/ghc-proposals/ghc-proposals/pull/207>
Proposal: https://github.com/mpickering/ghc-proposals/blob/csp-types/proposals/0000-csp-types.rst <https://github.com/mpickering/ghc-proposals/blob/csp-types/proposals/0000-csp-types.rst>

The proposal considers code like this:

foo :: forall a. Proxy a -> Q Exp
foo _ = [| let x :: a -> a; ... |]

Note that the type variable `a` is in scope in the quotation. Currently, this quotation is accepted, but then any use of it in a splice leads to an error, because the `a` has a Unique of a variable that has fallen out of scope. This is just plain wrong.

Matt proposes to fix this by introducing a new class LiftT, with one method: liftTyCl :: forall {k} (a :: k). LiftT a => Q Type. This is a type-level equivalent of the existing Lift class, whose `lift` method produces a Q Exp. Instances of LiftT would be automatically provided by GHC at all types, including polytypes. Matt has already implemented the proposal.

I recommend against accepting this proposal in its current form, for the following reasons:
 - While the proposal addresses a specific, real bug in TH, this is far from the simplest solution. Instead, we could just state that no variables brought into scope outside a TH quote remain in scope within the TH quote. The body of `foo` above would be rejected for this reason.
 - There is no motivation for the new feature in the proposal, other than fixing the bug.
 - The example in the proposal is one that, even with this proposal implemented, would not work: it uses *typed* TH, which does not allow type-level splices. So, even if Matt has a genuine need for this feature leading to the example in the proposal, implementing the proposal doesn't actually solve his problem.
 - The proposal mentions the possibility of using Typeable instead of LiftT, but discards this idea because we cannot solve, e.g., Typeable (forall a. a -> a); in contrast, we can solve LiftT instances of that form. However, generating a need for a LiftT instance of that form requires -XImpredicativeTypes, which is a bug, not a feature.
 - Although Matt has kindly already implemented this feature, we all know that the initial implementation of a feature is only the tip of the iceberg in its cost. Adding this feature, as proposed, introduces yet another class that we have to have custom treatment for, along with various other points of complexity.

Perhaps with proper motivation -- and with an implementation based on Typeable -- I would be more in support. I do think this may be useful. But given the fact that the TH bug has existed since the dawn of time and no one has complained until now -- and even now, there is no practical, on the ground motivation -- I'm uninclined to move forward here.

As usual, I will take silence as agreement with this recommendation to reject, but I'd love to hear opposing viewpoints.

Thanks,
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20190307/fda70eca/attachment.html>