From 9d363e3541fefd78e2a93f5377e412a24b22986a Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 24 Jun 2025 10:31:57 +0200
Subject: [PATCH] fix: linter.simpUnusedSimpArgs to check syntax kind (#8971)

This PR fixes `linter.simpUnusedSimpArgs` to check the syntax kind, to
not fire on `simp` calls behind macros. Fixes #8969
---
 src/Lean/Linter/UnusedSimpArgs.lean |  7 ++++++-
 tests/lean/run/issue8969.lean       | 13 +++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/issue8969.lean

diff --git a/src/Lean/Linter/UnusedSimpArgs.lean b/src/Lean/Linter/UnusedSimpArgs.lean
index fd5cc5943f..8ed3f2b135 100644
--- a/src/Lean/Linter/UnusedSimpArgs.lean
+++ b/src/Lean/Linter/UnusedSimpArgs.lean
@@ -46,6 +46,11 @@ def unusedSimpArgs : Linter where
             -- reporting about unused simp arguments inside macro, which we do not want to do
             -- (we likely cannot see all uses of the macro, so the warning would be incomplete)
             let some range := info.range? | return
+            let stx := ci.stx
+            -- Check that we have the expected syntax
+            unless stx.isOfKind ``Parser.Tactic.simpAll ||
+                   stx.isOfKind ``Parser.Tactic.simp do return
+
             let maskAcc ←
               if let some (_, maskAcc) := (← masksMap.get)[range]? then
                 unless mask.size = maskAcc.size do
@@ -53,7 +58,7 @@ def unusedSimpArgs : Linter where
                 pure <| Array.zipWith (· || ·) mask maskAcc
               else
                 pure mask
-            masksMap.modify fun m => m.insert range (ci.stx, maskAcc)
+            masksMap.modify fun m => m.insert range (stx, maskAcc)
         | _ => pure ())
 
     -- Sort the outputs by position
diff --git a/tests/lean/run/issue8969.lean b/tests/lean/run/issue8969.lean
new file mode 100644
index 0000000000..e55aa63d59
--- /dev/null
+++ b/tests/lean/run/issue8969.lean
@@ -0,0 +1,13 @@
+import Lean
+
+open Lean Elab Meta Tactic
+
+syntax (name := nontriviality) "nontriviality" Parser.Tactic.simpArg,+ : tactic
+
+@[tactic nontriviality] def elabNontriviality : Tactic := fun stx => do
+  let simpArgs := stx[1].getSepArgs
+  let stx := open TSyntax.Compat in Unhygienic.run `(tactic| simp [$simpArgs,*])
+  let ([], _) ← runTactic (← getMainGoal) stx | failure
+
+example : True ∧ True := by
+  nontriviality id_eq