optConfig causes tactics to be ignored

Stream: lean4

[Eric Wieser]

Something fishy is going on here (minimized from #new members > Wall of warnings of `unreachableTactic`/`unusedTactic` to be Mathlib free):

module

public meta import Lean.Elab.Eval
public meta import Lean.Elab.Tactic.ElabTerm

public meta section

open Lean Parser Meta Elab Tactic Term

/-- Elaborator for the configuration in `apply (config := cfg)` syntax. -/
declare_config_elab elabApplyConfig ApplyConfig

@[tactic_alt Lean.Parser.Tactic.apply]
elab (name := applyWith) "apply" cfg:optConfig ppSpace e:term : tactic => do
  let cfg ← elabApplyConfig cfg
  evalApplyLikeTactic (·.apply · cfg) e


def MyProp (n : Nat) : Prop := n = n

theorem MyProp.mk (n : Nat) : MyProp n := by rw [MyProp]

-- this emits a warning that sorry was used, but no errors
theorem foo : MyProp 1337 := by
  apply MyProp.mk "foo"
  exact "qed"

[Anne Baanen]

I don't think it's optConfig that causes the issue: replacing cfg with {} still results in an error about sorry, while replacing evalApplyLikeTactic with throwErrorAt e "error'd" does show an error in the infobar.

[Anne Baanen]

In fact, replacing the applyWith code with an identical copy of the original apply code results in the same:

module

public meta import Lean.Elab.Eval
public meta import Lean.Elab.Tactic.ElabTerm

public meta section

open Lean Parser Meta Elab Tactic Term

/-- Elaborator for the configuration in `apply (config := cfg)` syntax. -/
declare_config_elab elabApplyConfig ApplyConfig

elab "apply" t:term : tactic => do
  evalApplyLikeTactic (fun g e => g.apply e (term? := some m!"`{e}`")) t

def MyProp (n : Nat) : Prop := n = n

theorem MyProp.mk (n : Nat) : MyProp n := by rw [MyProp]

-- this emits a warning that sorry was used, but no errors
theorem foo : MyProp 1337 := by
  apply MyProp.mk "foo"
  exact "qed"

[Anne Baanen]

I suspect this is caused by the two variants having overlapping parsers: I don't know exactly how this works but I recall if multiple parses apply to the same tactic syntax, they are each tried in turn until one succeeds. (And apparently there is no error reporting done upon failure?)

[Thomas Murrills]

Interestingly, if you look at the infotrees, only the original syntax is ever actually elaborated. I guess it’s “succeeding” via errToSorry when it shouldn’t; maybe there’s a missing withoutErrToSorry near the backtracking logic used for choice nodes (like observing?)?

[Anne Baanen]

Indeed if I make the syntax non-overlapping the expected error occurs. So let's use that as the fix in Mathlib for now:

module

public meta import Lean.Elab.Eval
public meta import Lean.Elab.Tactic.ElabTerm

public meta section

open Lean Parser Meta Elab Tactic Term

/-- Elaborator for the configuration in `apply (config := cfg)` syntax. -/
declare_config_elab elabApplyConfig ApplyConfig

/-- At least one configuration option for tactics.

`optConfig` allows zero or more, `manyConfig` requires at least one.
 -/
syntax manyConfig := (colGt configItem)+

@[tactic_alt Lean.Parser.Tactic.apply]
elab (name := applyWith) "apply" cfg:manyConfig ppSpace e:term : tactic => do
  let cfg ← elabApplyConfig cfg
  evalApplyLikeTactic (·.apply · cfg) e

def MyProp (n : Nat) : Prop := n = n

theorem MyProp.mk (n : Nat) : MyProp n := by rw [MyProp]

/--
error: Application type mismatch: The argument
  "foo"
has type
  String
but is expected to have type
  Nat
in the application
  MyProp.mk "foo"
-/
#guard_msgs in
theorem foo : MyProp 1337 := by
  apply MyProp.mk "foo"
  exact "qed"

[Anne Baanen]

Workaround in #34721.

[Anne Baanen]

I reported the lack of error message as a Lean bug: lean4#12394