syntax quotation with cases

Stream: lean4

[Floris van Doorn]

This is a question about syntax quotations. In the example below, I'm wondering why the line cases $t fails without syntax category annotation, even though I've already specified t:term. I was just struggling with @Sven Manthe for while to get cases $t to parse in a similar example.

import Lean

syntax "example" atomic(ident " : ")? term : tactic

macro "example_without_ident" t:term : tactic =>
  `(tactic|example $t) -- this succeeds

macro "cases_without_ident" t:term : tactic =>
  `(tactic|cases $t) -- this fails
  -- `(tactic|cases $t:term) -- this succeeds

#check Lean.Parser.Tactic.cases -- for reference

[Eric Wieser]

I think the ambiguity here is caused by cases h : x notation existing

[Eric Wieser]

But agreed that I'd expect the annotation in t:term to suffice

[Floris van Doorn]

Eric Wieser said:

I think the ambiguity here is caused by cases h : x notation existing

I tried to simulate that with the example syntax, where I don't have to specify the syntax category of $t. But cases does have a bit more complicated arguments, which probably causes the difference.

[Sebastian Ullrich]

The disambiguation of antiquotations is done at parse time, other information about t cannot be taken into account. Though now I'm wondering whether that could be delayed until elaboration time by producing choice nodes instead...

[Floris van Doorn]

I see, the error has nothing to do with optional arguments, just the fact that there is a different syntax category.

syntax myTerm := term

syntax (name := myCases) "mycases " myTerm : tactic

macro "cases_without_ident" t:term : tactic =>
  `(tactic|mycases $t) -- this fails
  -- `(tactic|mycases $t:term) -- this succeeds

I think it's something that is easy to get wrong, but can be solved by giving more information. I am not experienced enough with syntax quotations to always know where/how to give more information.

[Patrick Massot]

It is the golden rule of quotation and antiquotation: in case of mysterious errors, add annotations before trying anything else.