Overlapping tactic syntax hides error messages

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Certain tactics, including at least apply and exact, hide error messages when there is another elaborator for the same syntax.

For example, Mathlib defines an applyWith tactic using optConfig. Since optConfig allows the configuration to be absent, apply t can be both parsed as built-in apply and Mathlib's applyWith. When there is such overlapping syntax, and an error happens (this error would occur in the built-in apply and in Mathlib's applyWith), this error is silently ignored and a sorry is inserted.

module

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

public meta section

open Lean Parser Meta Elab Tactic Term

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"

Context

Found in Mathlib for applyWith, which now has a workaround consisting of a custom parser that can't be ambiguous with builtin apply. Discussed on Zulip here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/optConfig.20causes.20tactics.20to.20be.20ignored

Steps to Reproduce

1. Declare new syntax for apply that overlaps with existing apply syntax.
2. Write an erroring use of apply, for example try to close the goal with a term of the wrong type.
3. Receive no visible error.

Expected behavior: One error message is displayed, for example a type mismatch.

Actual behavior: No error message is displayed, the goal is closed with a sorry.

Versions

v4.28.0-rc1, nightly Lean 4.29.0-nightly-2026-02-09

Additional Information

n/a

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Run the minimal reproduction with the imports Lean.Elab.Eval and Lean.Elab.Tactic.ElabTerm, then inspect how overlapping apply syntax and optConfig elaborators handle errors. Compare the built-in apply path with the overlapping elaborator. Done means the type-mismatch error is displayed and no sorry is inserted.