fix: deprecation warning location with field notation (leanprover#10826)

This PR fixes the location of the “deprecated constant” and similar
error messages on field notation (`e.f`, `(e).f`, `e |>. f`). Fixes
leanprover#10821.

Author: nomeata

src/Lean/Elab/App.lean

@@ -1340,7 +1340,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     throwErrorAt ref m!"{msg}{.nil}"
   if eType.isForall then
     match lval with
-    | LVal.fieldName _ fieldName suffix? fullRef =>
+    | LVal.fieldName ref fieldName suffix? _fullRef =>
       let fullName := Name.str `Function fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
@@ -1349,7 +1349,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
            been a field in the `Function` namespace, so we needn't wait to check if this is actually
            a constant. If `suffix?` is non-`none`, we prefer to throw the "unknown constant" error
            (because of monad namespaces like `IO` and auxiliary declarations like `mutual_induct`) -/
-        throwInvalidFieldAt fullRef fieldName fullName
+        throwInvalidFieldAt ref fieldName fullName
     | .fieldIdx .. =>
       throwLValError e eType "Invalid projection: Projections cannot be used on functions"
   else if eType.getAppFn.isMVar then
@@ -1386,7 +1386,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
         throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}"
           ++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}"
           ++ tupleHint
-  | some structName, LVal.fieldName _ fieldName _ fullRef =>
+  | some structName, LVal.fieldName ref fieldName _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1402,15 +1402,15 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     -- Then search the environment
     if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then
       return LValResolution.const baseStructName structName fullName
-    throwInvalidFieldAt fullRef fieldName fullName
+    throwInvalidFieldAt ref fieldName fullName
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
-  | none, LVal.fieldName _ _ (some suffix) fullRef =>
+  | none, LVal.fieldName ref _ (some suffix) _fullRef =>
     -- This may be a function constant whose implicit arguments have already been filled in:
     let c := e.getAppFn
     if c.isConst then
-      throwUnknownConstantAt fullRef (c.constName! ++ suffix)
+      throwUnknownConstantAt ref (c.constName! ++ suffix)
     else
       throwInvalidFieldNotation e eType
   | _, _ => throwInvalidFieldNotation e eType
@@ -1619,7 +1619,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if (← isInaccessiblePrivateName info.projFn) then
         throwError "Field `{fieldName}` from structure `{structName}` is private"
-      let projFn ← mkConst info.projFn
+      let projFn ← withRef lval.getRef <| mkConst info.projFn
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
@@ -1629,7 +1629,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
         loop f lvals
     | LValResolution.const baseStructName structName constName =>
       let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f
-      let projFn ← mkConst constName
+      let projFn ← withRef lval.getRef <| mkConst constName
       let projFn ← addProjTermInfo lval.getRef projFn
       if lvals.isEmpty then
         let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit

tests/lean/1038.lean.expected.out

@@ -1 +1 @@
-1038.lean:1:7-1:21: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`
+1038.lean:1:10-1:12: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`

tests/lean/346.lean.expected.out

@@ -1,5 +1,5 @@
-346.lean:10:6-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
-346.lean:13:2-13:5: error: Invalid field `z`: The environment does not contain `Nat.z`
+346.lean:10:15-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
+346.lean:13:4-13:5: error: Invalid field `z`: The environment does not contain `Nat.z`
   x
 has type
   Nat

tests/lean/funind_errors.lean.expected.out

@@ -1,5 +1,5 @@
 funind_errors.lean:4:7-4:26: error(lean.unknownIdentifier): Unknown identifier `doesNotExist.induct`
-funind_errors.lean:22:7-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
+funind_errors.lean:22:17-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
@@ -10,5 +10,5 @@ takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (mo
       have a := as[i];
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
-funind_errors.lean:38:7-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
-funind_errors.lean:45:7-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`
+funind_errors.lean:38:14-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
+funind_errors.lean:45:13-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`

tests/lean/run/issue10821.lean

@@ -0,0 +1,65 @@
+set_option linter.deprecated true
+
+/-!
+Checks that deprecated names in projection notation cause just
+the name to be marked, not the whole expression.
+-/
+def Nat.inc (n : Nat) : Nat := n + 1
+
+@[deprecated inc (since := "2025-10-17")]
+def Nat.inc' (n : Nat) : Nat := n + 1
+
+/--
+@ +3:5...9
+warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  n
+  |>.inc'
+
+/--
+@ +2:7...11
+warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  n |>.inc'
+
+/--
+@ +2:6...10
+warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  (n).inc'
+
+/--
+@ +2:4...8
+warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  n.inc'
+
+/--
+@ +2:4...8
+error: Invalid field `incc`: The environment does not contain `Nat.incc`
+  n
+has type
+  Nat
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  n.incc
+
+/--
+@ +2:4...8
+error: Invalid field `incc`: The environment does not contain `Nat.incc`
+  n
+has type
+  Nat
+-/
+#guard_msgs (positions := true) in
+example (n : Nat) : Nat :=
+  n.incc.foo