Antiquotation types silently ignore tokens

[gebner]

import Lean open Lean
@[defaultInstance] instance : MonadQuotation Elab.TermElabM := inferInstance

syntax "👉" (ident <|> "_") : term
#eval `(👉 $_)

The last underscore has type TSyntax `ident, which suggests that only identifiers are valid to insert here.

This just majorly confused me in leanprover-community/mathport#152.

To clarify: I would expect a type like TSyntax [`ident, `token.«_»].

Versions

Nightly from July 2, as well as the relaxed antiquotations branch.

[gebner]

I'm not sure what the takeaway here is:

1. Never use nested <|>.
2. Add antiquotations for <|>.
3. Add antiquotations for symbols.
4. Add a leading_parser to def binderIdent.

[Kha]

This comes back to the old issue of tokens being ignored in syntax patterns. How about something like the following:

• We introduce a new parser alias tokenWithAntiquot(str) that introduces both an antiquotation as well as a surrounding syntax node so that it is not ignored in syntax patterns anymore
• We come up with sensible heuristics for when to default to tokenWithAntiquot in syntax, say whenever str is not used in a sequence. Thus "simp" ("!" <|> "?") ... would make only the latter two tokens pattern-relevant.

[gebner]

say whenever str is not used in a sequence

More conservatively, we could also say whenever str is used directly in a <|>. The difference between the heuristics would be with "+"+ or "?"?, where we don't really need nodes or antiquotations.

The same should presumably also apply to unicode symbols.

[Kha]

Yes, that would probably be a better heuristic!