From 97588301e16a00b287f75936bf7529332218a973 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 18 Jun 2024 01:21:14 +0200
Subject: [PATCH] fix: `deprecated` warning position at `simp` arguments
 (#4484)

closes #4452
---
 src/Lean/Elab/Term.lean           |  4 ++--
 tests/lean/4452.lean              | 29 +++++++++++++++++++++++++++++
 tests/lean/4452.lean.expected.out |  2 ++
 3 files changed, 33 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/4452.lean
 create mode 100644 tests/lean/4452.lean.expected.out

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 8844e312d2..81dfec93a9 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1836,9 +1836,9 @@ def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? :
       return (c, ids.head!, ids.tail!)
   | _ => throwError "identifier expected"
 
-def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) :=
+def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := withRef stx do
   match stx with
-  | .ident _ _ val preresolved => do
+  | .ident _ _ val preresolved =>
     let rs ← try resolveName stx val preresolved [] catch _ => pure []
     let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty
     let fs := rs.map fun (f, _) => f
diff --git a/tests/lean/4452.lean b/tests/lean/4452.lean
new file mode 100644
index 0000000000..4e7191a822
--- /dev/null
+++ b/tests/lean/4452.lean
@@ -0,0 +1,29 @@
+def a := 1
+
+@[deprecated]
+theorem hi : a = 1 := rfl
+
+attribute [simp] hi
+
+example (h : 1 = b) : a = b := by
+  simp
+  guard_target =ₛ 1 = b
+  exact h
+
+set_option linter.all true
+
+example (h : 1 = b) : a = b := by
+  simp[
+    hi
+  ]
+  guard_target =ₛ 1 = b
+  exact h
+
+@[deprecated]
+theorem hi' : True := .intro
+
+example : True := by
+  -- the warning is on `simp`
+  simp [
+    hi'  -- warning should be logged here
+  ]
diff --git a/tests/lean/4452.lean.expected.out b/tests/lean/4452.lean.expected.out
new file mode 100644
index 0000000000..b23f7d3f53
--- /dev/null
+++ b/tests/lean/4452.lean.expected.out
@@ -0,0 +1,2 @@
+4452.lean:17:4-17:6: warning: `hi` has been deprecated
+4452.lean:28:4-28:7: warning: `hi'` has been deprecated