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

@@ -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

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