fix: deprecated warnings for overloaded symbols

closes #4636

src/Lean/Elab/App.lean

@@ -1292,6 +1292,7 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
     funLVals.foldlM (init := acc) fun acc (f, fIdent, fields) => do
       let lvals' := toLVals fields (first := true)
       let s ← observing do
+        checkDeprecated fIdent f
         let f ← addTermInfo fIdent f expectedType?
         let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis
         if overloaded then ensureHasType expectedType? e else return e

src/Lean/Elab/Term.lean

@@ -1827,9 +1827,13 @@ def isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool := do
 /--
   Create an `Expr.const` using the given name and explicit levels.
   Remark: fresh universe metavariables are created if the constant has more universe
-  parameters than `explicitLevels`. -/
-def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
-  Linter.checkDeprecated constName -- TODO: check is occurring too early if there are multiple alternatives. Fix if it is not ok in practice
+  parameters than `explicitLevels`.
+
+  If `checkDeprecated := true`, then `Linter.checkDeprecated` is invoked.
+-/
+def mkConst (constName : Name) (explicitLevels : List Level := []) (checkDeprecated := true) : TermElabM Expr := do
+  if checkDeprecated then
+    Linter.checkDeprecated constName
   let cinfo ← getConstInfo constName
   if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels for '{constName}'"
@@ -1838,10 +1842,21 @@ def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM E
     let us ← mkFreshLevelMVars numMissingLevels
     return Lean.mkConst constName (explicitLevels ++ us)
 
+def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do
+  if let .const declName _ := e.getAppFn then
+    withRef ref do Linter.checkDeprecated declName
+
 private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
   candidates.foldlM (init := []) fun result (declName, projs) => do
     -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail.
-    let const ← mkConst declName explicitLevels
+    /-
+    We disable `checkDeprecated` here because there may be many overloaded symbols.
+    Note that, this method and `resolveName` and `resolveName'` return a list of pairs instead of a list of `TermElabResult`s.
+    We perform the `checkDeprecated` test at `resolveId?` and `elabAppFnId`.
+    At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of
+    `TermElabResult`s.
+    -/
+    let const ← mkConst declName explicitLevels (checkDeprecated := false)
     return (const, projs) :: result
 
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
@@ -1895,11 +1910,11 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (
     | []  => return none
     | [f] =>
       let f ← if withInfo then addTermInfo stx f else pure f
+      checkDeprecated stx f
       return some f
     | _   => throwError "ambiguous {kind}, use fully qualified name, possible interpretations {fs}"
   | _ => throwError "identifier expected"
 
-
 def TermElabM.run (x : TermElabM α) (ctx : Context := {}) (s : State := {}) : MetaM (α × State) :=
   withConfig setElabConfig (x ctx |>.run s)
 

tests/lean/run/4636.lean

@@ -0,0 +1,28 @@
+theorem foo : True := trivial
+
+@[deprecated] def Foo.foo : Nat := 3
+
+set_option warningAsError true
+set_option linter.all true
+open Foo
+
+/--
+-/
+#guard_msgs in
+example : True := foo -- Should not produce warning
+
+/--
+error: `Foo.foo` has been deprecated
+-/
+#guard_msgs in
+example : Nat := Foo.foo
+
+namespace Foo
+
+/--
+error: `Foo.foo` has been deprecated
+-/
+#guard_msgs in
+example : Nat := foo
+
+end Foo