From 2eca5ca6e48d4996859b71fd7f125b8671e873cf Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Tue, 2 Dec 2025 18:53:50 +1100
Subject: [PATCH] fix: `getEqnsFor?` should not panic on matchers (#11463)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a panic in `getEqnsFor?` when called on matchers generated
from match expressions in theorem types.

When a theorem's type contains a match expression (e.g., `theorem bar :
(match ... with ...) = 0`), the compiler generates a matcher like
`bar.match_1`. Calling `getEqnsFor?` on this matcher would panic with:

```
PANIC: duplicate normalized declaration name bar.match_1.eq_1 vs. _private...bar.match_1.eq_1
```

This also affected the `try?` tactic, which internally uses
`getEqnsFor?`.

We make `shouldGenerateEqnThms` return `false` for matchers, since their
equations are already generated separately by
`Lean.Meta.Match.MatchEqs`. This prevents the equation generation
machinery from attempting to create duplicate equation theorems.

Closes #11461
Closes #10390


🤖 Prepared with Claude Code

Co-authored-by: Claude <noreply@anthropic.com>
---
 src/Lean/Meta/Eqns.lean       |  6 +++++-
 tests/lean/run/try_panic.lean | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/try_panic.lean

diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean
index c9c7a2e09d..0f0aac19d2 100644
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -150,9 +150,13 @@ def registerGetEqnsFn (f : GetEqnsFn) : IO Unit := do
     throw (IO.userError "failed to register equation getter, this kind of extension can only be registered during initialization")
   getEqnsFnsRef.modify (f :: ·)
 
-/-- Returns `true` iff `declName` is a definition and its type is not a proposition. -/
+/-- Returns `true` iff `declName` is a definition and its type is not a proposition.
+    Returns `false` for matchers since their equations are handled by `Lean.Meta.Match.MatchEqs`. -/
 private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
   if let some { kind := .defn, sig, .. } := (← getEnv).findAsync? declName then
+    -- Matcher equations are handled separately in Lean.Meta.Match.MatchEqs
+    if isMatcherCore (← getEnv) declName then
+      return false
     return !(← isProp sig.get.type)
   else
     return false
diff --git a/tests/lean/run/try_panic.lean b/tests/lean/run/try_panic.lean
new file mode 100644
index 0000000000..38a694735a
--- /dev/null
+++ b/tests/lean/run/try_panic.lean
@@ -0,0 +1,35 @@
+import Lean
+
+/-!
+# Regression test: getEqnsFor? should not panic on matchers
+
+Previously, when a theorem had a match expression in its type (e.g. `bar.match_1`),
+calling `getEqnsFor?` on the matcher would panic with "duplicate normalized declaration name".
+
+This was fixed by making `shouldGenerateEqnThms` return `false` for matchers, since
+matcher equations are handled separately by `Lean.Meta.Match.MatchEqs`.
+-/
+
+-- A theorem with a match expression in its type creates a matcher `bar.match_1`
+theorem bar : (match (0 : Nat) with | 0 => 0 | _ => 1) = 0 := by native_decide
+
+-- getEqnsFor? on a matcher should return none (not panic)
+/-- info: eqns: none -/
+#guard_msgs in
+#eval do
+  let eqns ← Lean.Meta.getEqnsFor? `bar.match_1
+  IO.println s!"eqns: {eqns}"
+
+-- try? should not panic when encountering matchers in the goal
+-- (it may fail to find suggestions, but should not panic)
+/--
+info: Try these:
+  [apply] rfl
+  [apply] simp
+  [apply] simp only
+  [apply] grind
+  [apply] grind only
+  [apply] simp_all
+-/
+#guard_msgs in
+theorem bar' : (match (0 : Nat) with | 0 => 0 | _ => 1) = 0 := by try?