fix: getEqnsFor? should not panic on matchers (#11463)

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 <[email protected]>

Author: kim-em

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

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?