Thanks for writing this up! Since we have discussed it extensively already, needless to say I support the proposed changes.

I still feel the Typed Template Haskell changes should be a separate proposal depending on the original.

I agree that Code should be possible to write without involving Q, but I still don't understand that motivations that we ought to overload typed quotes breaking unwrapped m (TExp a). This is unlike the first part which should really be uncontroversial to everyone.

Static pointers are mentioned for comparision, but the crucial difference is https://hackage.haskell.org/package/base/docs/GHC-StaticPtr.html#t:IsStatic supports the identity instance. If that is to be the inspiration, I rather make it more directly so:

class IsExp p where
   fromExp :: Exp -> p
instance IsExp Exp where
  fromExp = id

class IsTExp p where
   fromTExp :: TExp a -> p a
instance IsTExp TExp where
  fromTExp = id

@int-index's alternative code example (#246 (comment)) is changed to:

data Expr a where
  Leaf :: TExp a -> Expr a
  Int :: Int -> Expr Int
  Add :: Expr Int -> Expr Int -> Expr Int

instance IsTExp Expr where
  fromTExp = Leaf

add :: Applicative m => m (Expr Int) -> ExprGen m (Expr Int) -> m (Expr Int)
add = liftA2 Add

expr = [|| 5 ||] `add` [|| 10 ||]

This doesn't look too verbose to me. If anything now add is hardly needed!

I'm broadly in support, at least of the untyped TH changes.

1. I think we can remove fail from Quote. You say that having numTyLit call error would be a run-time error, but I don't see how that's the case: the error would run at the same stage as the fail does now. The error would just produce (perhaps) a worse error message. But this is such a corner case that I don't think it should drive the overall design.

2. I don't understand specification point (4), which mentions top-level splices. This proposal is all about quotes, so I see no change at all to top-level splices. A nested splice might indeed change the type of the surrounding quote. And I can't extract any meaning from "A quotation which contains splices inherits the constraints on the representation.", I'm afraid.

3. Could I ask you to refactor the typed TH section? The specification should be exactly that; you have some motivation mixed in there as well.

4. The typed TH proposal generalizes along a different axis than the untyped proposal. I don't see why untyped quotes wouldn't similarly benefit from this form of generalization. The class name TypedQuote threw me off, because it is almost unrelated to Quote. It's almost TypedLang, but I don't really like that name either. I almost want the typed TH proposal to be completely separate from the rest of this proposal, as it seems orthogonal. Yet I'm sympathetic to the overhead that proposal-writing causes.

5. What's QuoteT?

6. The example under "Other Effects" suggests that nested splices induce a Quasi constraint instead of setting m ~ Q. Which is it? (I think the Quasi constraint is easier, but maybe I'm missing something.)

7. Should we consider banning hand-written Lift? Are there non-trivial hand-written Lift instances out there? Or, at least, we can explicitly say that Lift will not aim to preserve backward-compatibility: use deriving Lift if you want compatibility.

8. I agree that it's OK to break typed TH.

9. Why do we need the typed TH part of the proposal? Can't you do what you want by just adding a function call on your quote? I don't see why this generalization needs to happen inside TH: it looks like everything would just be done in a post-processor, anyway.

@Ericson2314 I'm also fine with that but I was under the impression that making Q (TExp a newtype was contentious.

@goldfirere

1. That seems correct. I will remove fail.

2. This is the point made by @int-index. If you have c :: C1 m => m Exp and c' :: C2 m => m Exp then the idea is that the quotation has the union of the constraints of the constituent
   parts [| $c $c' |] : (C1 m, C2 m) => m Exp.

3. I will split the section about typed template haskell into another proposal.

4. The reason not to generalise untyped quotations is to retain backwards compatibility.

5. QuoteT is supposed to be TypedQuote. Typo.

6. What the constraint is depends on the type of the nested splice. The point is supposed to be that if
   one of the nested splices is specifically of type Q Exp then the whole quote must also be of that type.

7. There are some hand-written lift instances so I would prefer to not ban it.

8. Thanks :)

9. The reason for the existence of the typed template haskell part of the proposal is that in Make Q (TExp a) into a newtype #195 the proposal was shelved as everyone seemed to agree that this axis of generalisation was better than just making Q (TExp a newtype. I then got confused about these two different axis and so started writing this proposal in order to solve Make Q (TExp a) into a newtype #195 but then realised that the WQ stuff was completely separate. At this point I was getting sick of it so I just ploughed on and hoped for clemency.

It is getting a bit frustrating. I have been trying to make Q (TExp into a new type for many months!
I would be happy at this point if I could just make it into a new type rather than this other generalisation but given that (1) the other commenters believed this generalisation was better and (2) it is already how static pointers work, I thought it was better to try to propose to make it polymorphic.

So I will remove the parts about typed template haskell as I need to write a proposal anyway which completely revamps it. Hopefully by the end of the summer I will have done that.

@goldfirere Also the point about top-level splices is that you still need to use a concrete type at the top-level splice and the maximal type of a quote is Q Exp, therefore a top-level splice expects an argument of type Q Exp.

The "Rendered" link is outdated now, perhaps use https://github.com/mpickering/ghc-proposals/blob/overloaded-proposal/proposals/0000-overloaded-bracket.rst instead of a link to a specific commit?

In the current proposal, I see these definitions:

class Lift a where
   lift :: Quote m => a -> m Exp
   liftT :: Quote m => a -> m (TExp a)

Question: what instances of Lift would make use of Quote m methods? Why can't we have lift and liftT without a monadic/applicative context?

class Lift a where
   lift :: a -> Exp
   liftT :: a -> TExp a

DeriveLift is implemented in terms of quotation brackets, so if we want to do that it's more natural to generalise the type of Lift.

Okay, then why the Quote constraint instead of Applicative or Monad? I'd favor some constraint that could be satisfied by Identity.

Because I think it's more consistent to always always give quotations a Quote m constraint rather than relying on the internal implementation detail of how the quotation is desugared.

The Quote constraint can be implemented purely so I don't think it's any significant difference from Applicative or Monad.

@mpickering wait are you OK with #246 (comment) ? It precludes a newtype combining the syntax and the monad from being an instance of IsTExp. But if so, I'm happy to factor out second half of this proposal according to that design on your behalf.

Because I think it's more consistent to always always give quotations a Quote m constraint rather than relying on the internal implementation detail of how the quotation is desugared.

I think the quote-everywhere is more forwards-compatible too.

Off topic. FWIW In some more dependent future I want to make a Reader + Writer thing based off https://cs.brown.edu/~sk/Publications/Papers/Published/pkw-inf-scope-syn-sugar/paper.pdf where you pass around references to the binding sites in a statically keyed map (as in row-types, or some equivalent). The macro evaluation does it's own name resolution, alpha-equivalent by construction, and custom binding syntax is expressible and enforceable. That's probably a huge breaking change in any event, but it seems slightly smaller one if we don't let there be any free Applicatives today.

@Ericson2314 I am not happy until it's possible to write instances for Code, that's the whole point of the newtype. And looking at your suggestion again, that doesn't seem to be possible.

So no, I'm not actually in favour of it it seems.

@mpickering OK drat, but yeah it makes more sense that you wouldn't be :).

@mpickering

2. Yes, that makes sense. But the proposal still talks about "top-level splices" and so it's not clear to me how the proposal matches your intent.

3. I think the back-compat breakage from generalizing untyped quotes would be minimal. There might be a few ambiguous types, I suppose. In any case, it sounds like this other idea is becoming a separate proposal, so we can debate it there.

4. OK. I think I understand this better. But it still seems that the proposal text is contradictory on this point, between specification point (4) and "Other effects".

5. Could you give a real-world example of a hand-written Lift? Why is it hand-written? And what do you feel about abandoning back-compat for such instances (while still retaining support, perhaps via CPP)?

Also the point about top-level splices is that you still need to use a concrete type at the top-level splice and the maximal type of a quote is Q Exp, therefore a top-level splice expects an argument of type Q Exp.

But this proposal looks, on the surface, that it doesn't touch top-level splices at all. So I'm unsure what to infer from this description about them.

The "Rendered" link is outdated now

I took the liberty to fix this myself.

Thanks for your love and care to TH (and its typed variant). It is much appreciated!

@goldfirere

2. A top-level splice still needs to expect something of type Q Exp. Is that what you are asking?
   Later on in your comment you say that it doesn't touch top-level splices but that is explained in bullet point 4.

A top-level splice instantiates m ~ Q and operates as before.

I also see that I explained this in a previous comment so perhaps you could explain with an example what you think the confusion is? Top-level splices have to instantiate m to Q so that there is a concrete type at the top level. Nested splices don't need to do this.

5. There are some (potentially dubious) hand-written instances in th-lift-instances (http://hackage.haskell.org/package/th-lift-instances-0.1.13/docs/src/Instances.TH.Lift.html). I just don't see a particular reason to make it impossible to define for users, it doesn't present a safety problem like Typeable.

• I'm generally sympathetic to making things more general. But generalisation has a price, and without compelling use-cases I'm wondering if the cost is justified. You say "Detaching quotations from Q makes way for a form of "pure" template haskell which can be fully evaluated on the host without having to run effects on the target." But I don't really understand that; it's far from a concrete use-case. Can you perhaps give a few concrete examples of how useful this feature could be? For example, it gives you access to a pure Haskell parser, doesn't it?

• I think the proposal would be stronger if it explicitly said it was about untyped TH, and explicitly makes no change to typed TH. I spent some time hunting for the answer to "what happens about typed TH?".

• Expression quotes are mentioned but nothing about type, pattern, or declaration quotes. Are they covered? Perhaps the proposal could be explicit, and give examples.

• If it doesn't cover typed TH, why is the type of liftT changed? (Maybe lift and liftT should be in different classes?)

• I think the discussion about typing could readily be resolved simply by giving the typing rules. Can you do that, in the proposal? For example:
  | A top-level splice instantiates m ~ Q and operates as before.
  All you need say is that the typing rule for a top-level splice is 100.00% unchanged:

     G |- e :: Q Exp, C
     runQ e --> e'
     G |- e' :: ty, D
     ------------
     G |- $e :: ty, C u D
  

  That is, in a top-level splice $e we expect that e :: Q Exp. There is no m to instantiate. (There might be if it so happened that e :: forall m, Quote m => m Exp, but there no requirement that it has such a type.

  The rule for nesed splices does change though. Looking at the rules in the original paper I think we need some adjustment; I think we need to carry along which 'm' is beind used for this bracket. Perhaps the "State" in Fig 2 needs to be (B m) rather than just B.

In general, we lack a single place where the typing rules for untyped and typed TH are laid out. (Not your fault, of course.) As we debate this proposal, another about nested quotatations, and perhaps another about overloading typed TH quotes, I acutely feel the lack of such a specification. Matthew: you are absolutely on top of all this -- could you help us along by writing the typing rules? Thanks! (Probably Latex is best for that, rather than markdown. The original paper predates the typed/untyped TH split, and so may need adjustment.)

In general, we lack a single place where the typing rules for untyped and typed TH are laid out.

Yes I can write down a type system which contains both untyped and typed template haskell but probably not until after ICFP. There needs to be some additional care taken to deal with top-level splices but I have thought about how to account for this.

Simon says:

All you need say is that the typing rule for a top-level splice is 100.00% unchanged:

Is that true? Then that answers my question about "instantiating m ~ Q". My problem there is that, if I write $( return (LitE (IntegerL 3)) ), there is no m that I can see. So I don't know what you mean by instantiating.

In any case, I agree with Simon that your specification point (4) is in sore need of a typing rule. I can't really understand it as is. At the risk of seeming rude, I will explain how I can't understand it, trusting that you would want me to: "Refine the rules to do with splicing." This looks simply introductory. The second sentence, if I understand it now, is a no-op, saying that top-level splices don't change. "The use of nested brackets..." Now I'm lost, because the introductory sentence is about splices, but here you're talking about brackets. Maybe this sentence is to avoid readers thinking about quotes here? "A quotation that contains splices..." Now we're getting somewhere, but the sentence refers to the "constraints on the representation" and I don't know what these are. (The representation of what?) It would all be cleared up with a typing rule.

👋 @simonpj, about accepting this .

Thank you Matthew for revising the proposal. I declare it accepted.

Let's try to get #195 revised and accepted to; it would make sense to implement both at once.

Simon

But you still want me to merge this as it is now, right?

But you still want me to merge this as it is now, right?

I believe so. Matthew has already updated it.

Matthew: to double check: do you have any pending changes to this proposal?

Yes no blockers from me.

Tom Sydney Kerckhove (NorfairKing) asks: would the authors of this PR please weigh in on the discussion at commercialhaskell/path#170

In our testing so far we've not found any Lift instances relying on any special methods of Q.

The path library seems to be an example of this, and I would like to ask for some advice on how to proceed over there.

Possibly related: https://gitlab.haskell.org/ghc/ghc/-/issues/17565

I posted a possible solution on that thread.

By the way, as I mentioned there, it would be convenient to add a function that reinterprets a Typeable type as a Template Haskell type, as I couldn't find one, but maybe it already exists?

This caused some breakage in recursion-schemes: recursion-schemes/recursion-schemes#132

Short explanation: that package has a typeclass like this:

class MakeBaseFunctor a where makeBaseFunctor :: a -> DecsQ
instance MakeBaseFunctor a => MakeBaseFunctor [a] where -- ...
instance MakeBaseFunctor a => MakeBaseFunctor (Q a) where -- ...
instance MakeBaseFunctor Name where -- ...
instance MakeBaseFunctor Dec where -- ...

(Note that the implementations all eventually use reify internally, so they all really do need to run in Q.)

Anyway, all of the following used to work:

makeBaseFunctor ''Identity
makeBaseFunctor [''Identity, ''Maybe]
makeBaseFunctor [d| instance Recursive (Identity a) |]
makeBaseFunctor [[d| instance Recursive (Identity a) |], [d| instance Recursive (Maybe a) |]]

But now the latter two fail with an ambiguous type error, since the types of the quotations are inferred to be Quote m => m Decs, which isn't enough information to pick the MakeBaseFunctor (Q a) instance. I'm not sure if there's a way that this can be fixed entirely within recursion-schemes, or if users of it will necessarily have to change their code that calls makeBaseFunctor.

Consider changing

instance MakeBaseFunctor a => MakeBaseFunctor (Q a) where -- ...

to

instance {-# OVERLAPPABLE #-} (m ~ Q, MakeBaseFunctor a) => MakeBaseFunctor (m a) where -- ...

Unfortunately, that doesn't help:

    • Overlapping instances for MakeBaseFunctor
                                  (m0 Language.Haskell.TH.Lib.Internal.Decs)
        arising from a use of ‘makeBaseFunctor’
      Matching instances:
        instance [overlappable] [safe] (q ~ Q, MakeBaseFunctor a) =>
                                       MakeBaseFunctor (q a)
          -- Defined in ‘Data.Functor.Foldable.TH’
        instance [safe] MakeBaseFunctor a => MakeBaseFunctor [a]
          -- Defined in ‘Data.Functor.Foldable.TH’
      (The choice depends on the instantiation of ‘m0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)

Bizarrely, that error persists even if I do turn on IncoherentInstances.

That’s too bad. What we want here is some form of defaulting, so that the ambiguous type variable would be instantiated to Q. But I don’t know if there’s a way to get it. Even a recent accepted GHC proposal #409 seems insufficient to handle this use case.

@blamario What would it take to extend #409 in such a way that it could handle this?

I don't see why #409 would not cover this as-is. Admittedly the motivation and the examples included in the proposal are mostly about solving the IsString ambiguity, but there are also examples like

default Foldable ([])

As section 2.1 states

The types may belong to any kind, but the class must have a single parameter.

there's absolutely nothing preventing a declaration like

default MakeBaseFunctor (Q)

In fact it might be a good idea to recommend

default Quote (Q)

in general.

there's absolutely nothing preventing a declaration like

default MakeBaseFunctor (Q)

But wouldn’t this be ill-kinded? Q isn’t an instance of MakeBaseFunctor, but Q a is.

I retract my previous comment. I'm not sure what I did wrong, but I just tried again and it worked this time.

my previous comment. I'm not sure what I did wrong, but I just tried again and it worked this time.

Now that’s surprising, because the error message you posted makes sense! I think if you got it working, then only thanks to IncoherentInstances (overlappable alone isn’t sufficient here), and that’s a fragile arrangement.

But wouldn’t this be ill-kinded? Q isn’t an instance of MakeBaseFunctor, but Q a is.

You're right, sorry I replied too quickly. I was lead from the class name to think it had the same kind as Functor. Still the other declaration I suggested should work to resolve the ambiguity:

default Quote (Q)

Yes, default Quote (Q) sounds like a great idea.