this works

Author: nomeata

src/Lean/Elab/App.lean

@@ -1602,7 +1602,7 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
       let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable!
       if isInaccessiblePrivateName (← getEnv) 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 }
@@ -1612,7 +1612,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/run/issue10821.lean

@@ -8,7 +8,7 @@ def Nat.inc (n : Nat) : Nat := n + 1
 def Nat.inc' (n : Nat) : Nat := n + 1
 
 /--
-@ +2:2...+3:9
+@ +3:5...9
 warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
 -/
 #guard_msgs (positions := true) in
@@ -17,23 +17,23 @@ example (n : Nat) : Nat :=
   |>.inc'
 
 /--
-@ +2:2...11
+@ +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:2...10
+@ +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:2...8
+@ +2:4...8
 warning: `Nat.inc'` has been deprecated: Use `Nat.inc` instead
 -/
 #guard_msgs (positions := true) in