feat: `Quote` + related syntax improvements

[tydeu]

This PR does a few syntax-related things:

• Adds the ability to pass SourceInfo to syntax constructed via Quote.
• Exposes the Name to NameLit conversion originally embedded inside the Quote Name instance as Name.toNameLit?
• Makes the kind parameter of Quote an outParam, which seems logical and helps with type inference.
• Adds some missing literal TSyntax helpers (e.g., getName for name literals)

I have split most of these changes into separate commits in case you wish to cherry-pick some subset of the changes. I am proposing this PR now because I feel it fits well with other Syntax changes being made (i.e., TSyntax).

[tydeu]

@Kha, I appear to have hit a weird bug in the Linux (non-release) and Nix CI builds when linking the executables. It is for some reason looking in libleanshared for the old name of some symbols I renamed (e.g., quoteNameMk and getEscapedNameParts). Is this a caching or staging issue or what?

[Kha]

Makes the kind parameter of Quote an outParam, which seems logical and helps with type inference.

Mmh, I started with this signature, but apart from potential instances into multiple kinds as mentioned in https://github.com/leanprover/lean4/commit/ffdf7ae665c05bf581f733f06539ac57f4a3aaed, I think the main issue was that outParams do not play well with coercions. I don't know if it works for you because you still have the [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' instance, but that is a very suspicious instance with outParams since we usually assume that the mapping from in-params to out-params is injective.

[Kha]

@Kha, I appear to have hit a weird bug in the Linux (non-release) and Nix CI builds when linking the executables. It is for some reason looking in libleanshared for the old name of some symbols I renamed (e.g., quoteNameMk and getEscapedNameParts). Is this a caching or staging issue or what?

You can try purging the ccache cache as in https://github.com/Kha/lean4/commit/524ae5abf72e25287b753382b267519e4e43870d. If it's really that, it's starting to get annoying...

[tydeu]

@Kha

I think the main issue was that outParams do not play well with coercions. I don't know if it works for you because you still have the [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' instance, but that is a very suspicious instance with outParams since we usually assume that the mapping from in-params to out-params is injective.

The MonadReader, MonadState, etc. instances use a similar approach in their instance which derives from MonadReaderOf, MonadStateOf, etc. Their mapping to out-params is thus similarly not injective. The idea, as I understand it, is to get smart inference through the outParam (i.e., get a reasonable default for the metavariable) while still being compatible with cases where the type is already fixed.

Mmh, I started with this signature, but apart from potential instances into multiple kinds as mentioned in ffdf7ae,

Ah, sorry, I didn't see that. While I agree that the ability to support multiple kinds is nice, I think the smarter type inference is a more valuable feature in most common use cases. One way to address both, if we desire to do so, would to do a QuoteOf / Quote split similar to what is done with above-mentioned monad classes. I would be happy to add that to the PR if desired.

[tydeu]

@Kha

You can try purging the ccache cache as in Kha@524ae5a. If it's really that, it's starting to get annoying...'

Good new, ccache is not at fault! Bad news, I have no clue what is then.

[tydeu]

Bad news, I have no clue what is then.

Actually, I think it is some kind of staging issue. One of the errors references the register_parser_alias expansion and that expansion uses quote here: https://github.com/leanprover/lean4/blob/0896180f1282547b4e49b0ea860f0906a8efd42a/src/Lean/Parser/Extra.lean#L178

So, I think there is a mismatch between the (builtin?) quote for Name which uses the old symbols and the new quote which uses the new symbols. The question that bugs me, though, is why does this only happen on Nix and non-release Linux builds. Do you have any ideas, @Kha?

~~Also, should I do a stage0 update to fix this?~~ EDIT: Apparently, I can't do that from my Windows machine because it produces code the CI doesn't like.

[tydeu]

Okay, so restoring the old names worked. That worries me. I feel like I am just papering over a bigger linking bug in the Nix and non-release Linux CI. Thoughts, @Kha?

[tydeu]

All the tests now pass, so I think this PR is now all set for a merge from my end.

@Kha, what is your verdict on the PR? I know you said you have some objections to the outParam change. I gave my reasoning, but I do not know if it was persuasive, If not, confining the PR to just the quote w/ SourceInfo feature (and possibly the helpers) would be still useful.

Also, please note, I am not trying to rush you. I just wanted to make sure I had everything done on my end so that when/if you have time to review this, there is not still work I need to do that blocks it.

[Kha]

@tydeu It doesn't look like your outParam is doing anything, since it is wrapped in optParam. Which would explain why it did not break the stdlib.

def f (s : String) := quote s

typeclass instance problem is stuck, it is often due to metavariables
  Quote ?m.8 ?m.9

[Kha]

I'm not sure what to think of the quote SourceInfo change, compared to directly moving to quote [MonadQuotation m] : A -> m A (and ditching all the Unhygiene.runs). Invoking monadic functions is a little more onerous, but it would make sure we can't forget passing the relevant source info. See also discussion about potentially moving to monadic TSyntax coercions in, err, a different issue? @gebner Thoughts?

[gebner]

I'm not sure what to think of the quote SourceInfo change, compared to directly moving to quote [MonadQuotation m] : A -> m A (and ditching all the Unhygiene.runs).

The manual SourceInfo param seems to be the worst option here, I agree. It's very easy to just ignore the argument (like all of the Unhygienic.run instances in this PR do).

I'm not sure how much I like the ∀ {M} [MonadQuotation M], A → M (TSyntax k) solution. I'm a bit concerned that this will lead to code explosion in the compiler due to monomorphization, and then there's the usual universe issues (Quote gets bumped up one level).

An alternative could be to use quote : A → Unhygienic (TSyntax k).

See also discussion about potentially moving to monadic TSyntax coercions in, err, a different issue?

For reference: https://github.com/leanprover/lean4/pull/1272#discussion_r912104150

To be honest, the auto-coercion in quote is too magic for my taste. The nonidentity coercions are already a bit iffy due to the diamonds (e.g. there's str→term vs. str→json→term). And then Quote adds another level of nondeterminism on top (e.g. Quote Name `ident seems reasonable and useful but obviously causes issues). It doesn't help that Quote doesn't have a clear specification either (see e.g. the questionable Quote Term instance).

[tydeu]

@Kha

The manual SourceInfo param seems to be the worst option here, I agree. It's very easy to just ignore the argument (like all of the Unhygienic.run instances in this PR do).

@gebner

[I]t would make sure we can't forget passing the relevant source info.

I see that both of you are viewing SourceInfo more as a requirement. In making in this change, I was merely wishing to add the option to provide SourceInfo (which was hitherto impossible).

EDIT: Also, if you want the monadic approach, why not just use quoteFromRef? In my view, I think a type class should always rely on minimum abstraction needed to achieve its goal (i.e, in this case, SourceInfo). Richer interfaces can be provided by other definitions which use the type class (e.g., quoteFrom, quoteFromRef).

[tydeu]

@tydeu It doesn't look like your outParam is doing anything, since it is wrapped in optParam. Which would explain why it did not break the stdlib.

Ah, didn't realize optParam had that effect. 😞

[Kha]

@tydeu For macro programming, it is important we propagate source info as well as possible for accurate positions in error messages. As such, having both quote and quoteFromRef might not be a good idea if using the former is too convenient such that people just default to it. And yes, neither the current quote nor other function like mkIdent(FromRef) currently adhere to this design principle.

[tydeu]

@Kha

For macro programming, it is important we propagate source info as well as possible for accurate positions in error messages.

I fully agree that this is ideal. However, as you pointed out, this is currently not adhere to by most of the Syntax constructors. Thus, I think following the current style is appropriate for the moment until a more principled solution can be applied to the codebase. As the saying goes, don't let the perfect be the enemy of the good. Being able to provide SourceInfo to quote at least some of the time, while not perfect, is certainly better than the current state of affairs where such a thing is impossible.

[Kha]

Ok, I'm fine with merging the proposed quote/quoteFromRef signatures due to this consistency with other current signatures. But for the implementation of Quote instances (i.e. the signature of Lean.Quote.quote, which we could let diverge from Lean.quote) I would prefer @gebner's Unhygienic (TSyntax k) proposal, as it makes forwarding the ref both less of a hassle and (as pointed out) harder to forget, and removes the need for Unhygienic.run in any non-trivial instance.

[Kha]

I've cherry-picked the uncontroversial commit for now

[leodemoura]

PR is stuck. Closing soon.

[leodemoura]

We can reopen the PR in the future when we can move it forward.