There are likely quite a lot of user programs will break

Really? Like what?

the monotype restriction

Does this proposal really solve that? For example, LiftT (forall a. a -> a) is invalid Haskell today. Furthermore, LiftT Proxy would also go awry, because Proxy's kind is polymorphic.

Does your proposal accept the program in the motivation? Note that this doesn't have a LiftT constraint written.

@RyanGlScott showed me a program with untyped template haskell which had some strange dynamic binding property which I think would be rejected by this proposal. I can't recall the exact definition though. Perhaps a lot is quite an exaggeration.

Constraints containing polytypes are solved fine by my tests once you turn on the impredicativity extension. You can see all the examples that work in the test I added with the patch.

If Proxy :: k -> * and there is a LiftT k constraint then it will be accepted but otherwise it has to be rejected as the kind variable will escape its scope. This is part of the design of the proposal.

No the proposal rejects the program because it doesn't have a LiftT constraint. It accepts the program if you add the LiftT constraint.

@RyanGlScott showed me a program with untyped template haskell which had some strange dynamic binding property which I think would be rejected by this proposal.

Indeed, I think the only programs that would be rejected under this proposal are the ones that are doing illicit things to begin with. Here is one example that comes to mind:

wat :: forall a. Proxy a -> Q Type
wat _ = [t| a |]

Currently, this quotation doesn't do what you think it does—it results in VarT a! This will cause disaster any time you try to splice it in:

λ> :k $(wat (Proxy @Int))

<interactive>:1:3: error:
    • The exact Name ‘a’ is not in scope
        Probable cause: you used a unique Template Haskell name (NameU), 
        perhaps via newName, but did not bind it
        If that's it, then -ddump-splices might be useful
    • In the untyped splice: $(wat (Proxy @Int))

This program will be rejected under this proposal, since there's no LiftT a constraint in scope. And I'd argue that that's a good thing, since whatever it was doing before was just plain unhygienic.

Broadly I think this makes sense, but there are lots of things I don't understand.

1. There are two entirely separate things
   (a) the existence of liftTyCl
   (b) a mechanism for automatically inserting liftTyCl splices.

Here (b) is purely a matter of convenience. Once (a) is sorted, (b) is pretty simple. So let's focus on (a).

2. You use $$ so perhaps you are talking about typed TH? But then you should have a guaranteed the spliced type will fit in the hole, and you give no such guarantee. I think perhaps you are doing untyped TH splicing.

3. The type of liftTyCl looks odd, because it doesn't mention t or k. You could stress that its type is

liftTyCl :: forall {k} (t :: k). LiftT t => Q Type

Also stress that the Type here is not Data.Kind.Type but rather the TH syntax-tree Language.Haskell.TH.Syntax.Type. I was terribly confused.

4. What instances for LiftT do you envisage? Where do they come from?

5. You say that polymorphic types give no problem. Can you give a concrete example? Currently you can't say f @(forall a. blah), and I think you'll want to do just that?

6.Do you have any customers? Anyone who needs this feature?

Thanks Simon, responding to your points below.

2. As all the splices in this proposal are implicit the distinction between untyped and typed is not very important. It only matters if you want to support typed type splices in user programs. The one example of $$ is meant to be indicative of some kind of splice as it's not a valid Haskell program.

3. It would be possible to define a kind-indexed type representation which would be analogous to a type indexed expression representation but I didn't want to pollute the proposal with these details as they are not important unless we also add support for splicing types in typed template haskell.

4. It is explained in the proposal that all types get instance for LiftT and are solved automatically.

5. You can say f @(forall a . blah), I added a test which tries this example and produces the right result.

https://gitlab.haskell.org/ghc/ghc/blob/0fa5339ed8c896dfe6c7263d5e8d68f7af727a4b/testsuite/tests/th/T15437.hs

6. This fixes a soundness bug, I'm not sure there needs to be any more motivation? Anyone who uses type variables in splices needs this or they will produce bad code. The only other option is to remove the ability to quote types completely by removing untyped type quotations, quoting type applications and quoting type signatures.

Another solution to the soundness issue is simply not to allow the use of scoped type variables inside of TH quotes.

Also, I'd like to point out that use of polytypes requires -XImpredicativeTypes, which is essentially a non-feature.

This is a cool idea! It's certainly consistent with the decision to lift values in quotes. In the past I've used a very simple TypeRep -> Q Type function for this purpose. The implementation there is missing most of the cases - no handling of tuples, datakinds, etc.

Something like this makes sense to me:

• A complete implementation of liftTypeRep :: TypeRep -> Q Type added to the TH API.
• A reference to some type variable, a, from outer scope, would desugar to $(liftTypeRep typeRep @a).

Is there anything else blocking this proposal? It is needed to fix a bad bug in Template Haskell.

Thanks for the proposal, but unfortunately I have to tell you that the committee has rejected it, 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 -- we would be more in support. We 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 -- we are uninclined to move forward here.

Also, there’s a simple bug-fix for now: just reject the program. If we get lots of people yelling that they really want such programs, we can tackle it then.

Obviously this is an unsatisfactory conclusion for the user's of typed template haskell.

Obviously this is an unsatisfactory conclusion for the user's of typed template haskell.

Why? I don't mean to be dense, but I'm genuinely not sure how you want this feature to work in typed TH. I do see how it could work in untyped TH, but I don't see how the proposal motivates adding the type-variable feature instead of just rejecting the original program.

Full disclosure: I believe I am the original author of the text Joachim cribbed in his rejection. (Apologies if I've misremembered.) So feel free to respond to those points.

I do think TH (and typed TH) should grow toward being more expressive, but the motivation behind this proposal is not compelling to me given that there is a much easier way to solve the problem. When/if folks come forward with more concrete motivation, then I (for one) would be happy to reconsider this.

One big problem with typed template haskell currently is that you can end up splicing in an expression which fails to type check because of an ambiguous type variable. If you want to resolve the ambiguity by instantiating that variable using type applications then you have to choose a concrete type rather than a polymorphic type which can be annoying. This proposal means that you can resolve the ambiguity but still remain polymorphic which is valuable for code reuse. It's not an ideal solution but a decent enough workaround.

There are more invasive and correct ways to fix this issue but I didn't want to derail the proposal with those. I have a paper in preparation which discusses more complicated problems to do with implicit arguments and a more invasive way to fix it.

I think you don't think this will work because there is no source syntax for splicing types into typed quotations? but you don't need a source syntax. The "splices" are inserted implicitly just like how cross stage persistence works for values.

I'm not worried about the source syntax (though it would be a bit sad not to be able to desugar implicit splices into other source syntax). I'm worried about the fact that TH types are not indexed by their kinds, which would seem necessary to support this in a typed way. But maybe it's OK because we allow only implicit splices, where GHC does know the kind of the type variable in question? It would be helpful to spell all this out. Note that this interpretation is in conflict with Simon's #207 (comment) which observed that implicit splicing was merely a matter of convenience. Again, I suppose that could all work, but I'd want it spelled out to be sure (and not just in a comment: in the proposal).

It would also be very helpful (for me, at least) to have a concrete, practical use-case in the motivation. It's clear that you badly want this: why?

Analyzing GHC#15833 yielded some motivation for this proposal. Here is the problem:

type QTExp a = Q (TExp a)

tenM :: Monoid m => QTExp (IO m) -> QTExp (IO m)
tenM dot = [|| let x 0 = putStr "\n" >> return mempty
                   x i = $$dot >> x (i - 1)
               in x 9 ||]

printDots :: QTExp (IO ())
printDots = tenM (tenM [|| putStr "." ||])

-- in another file
main :: IO ()
main = $$printDots

The first two definitions are accepted without issue. When splicing into main, though, we are greeted with an ambiguous type variable error. This is unfortunate, because typed quotes are always supposed to be spliced without issue.

The first step to understanding this is to look at the code in the quote in tenM. See how it uses $$dot, but then throws away the result. This means that we cannot infer the type of $$dot from the context. This is OK in the definition of tenM, though, because we know from the type signature, that dot :: Q (TExp (IO m)). However, when we expand out dot, we lose this type information, and GHC's inference algorithm is hamstrung.

The solution to the problem appears to be not to just replace $$dot with its contents, but instead to replace it with $dot :: IO m (where $dot is the result of splicing the underlying untyped quotation). However -- and here's where this proposal comes in -- we need m!

Indeed I don't see a way to accept the program above without something resembling this proposal.

However, note that this example does not need users of typed TH to be able to include scoped type variables in their splices -- the need here is all internal. So my worries of #207 (comment) are allayed here.

Nevertheless, I still think this proposal can be significantly simplified, say by using Typeable instead of LiftT. @mpickering, would you mind picking this up again, now that we have a concrete use case?