Switch monad and clean up

src/Lean/Elab/App.lean

@@ -1381,7 +1381,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       return LValResolution.const `Function `Function fullName
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
-      throwUnknownConstantWithSuggestions (ref? := fullRef) (c ++ suffix)
+      throwUnknownNameWithSuggestions (idOrConst := "constant")  (ref? := fullRef) (c ++ suffix)
     | _, _ =>
       throwInvalidFieldAt ref fieldName fullName
   | .forallE .., .fieldIdx .. =>
@@ -1403,7 +1403,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | _, _ =>
     match e.getAppFn, lval with
     | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
-      throwUnknownConstantWithSuggestions (ref? := fullRef) (c ++ suffix)
+      throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix)
     | _, .fieldName .. =>
       throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \
         types of the form `C ...` where C is a constant. The expression{indentExpr e}\nhas \
@@ -1748,8 +1748,25 @@ private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals :
     (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool)
     (acc : Array (TermElabResult Expr)) :
     TermElabM (Array (TermElabResult Expr)) := do
-  let fRes ← withRef fIdent <| resolveName' fIdent fExplicitUnivs expectedType?
+  let (n, fRes) ← withRef fIdent <| resolveName' fIdent fExplicitUnivs expectedType?
+  if fRes.isEmpty then throwUnknownIdWithSuggestions n
   elabAppFnResolutions fIdent fRes lvals namedArgs args expectedType? explicit ellipsis overloaded acc
+where
+  throwUnknownIdWithSuggestions (n : Name) := withRef fIdent do
+    let env ← getEnv
+    -- check for scope errors before trying auto implicits
+    if env.isExporting then
+      if let [(npriv, _)] ← withoutExporting <| resolveGlobalName (enableLog := false) n then
+        throwUnknownNameWithSuggestions (declHint := npriv) n
+    if !(← read).autoBoundImplicitForbidden n then
+      if (← read).autoBoundImplicitContext.isSome then
+        let allowed := autoImplicit.get (← getOptions)
+        let relaxed := relaxedAutoImplicit.get (← getOptions)
+        match checkValidAutoBoundImplicitName n (allowed := allowed) (relaxed := relaxed) with
+          | .ok true => throwAutoBoundImplicitLocal n
+          | .ok false => throwUnknownNameWithSuggestions n
+          | .error msg => throwUnknownNameWithSuggestions (extraMsg := msg) n
+    throwUnknownNameWithSuggestions n
 
 /--
 Resolves `(.$id:ident)` using the expected type to infer the namespace for `id`.

src/Lean/Elab/Term/TermElabM.lean

@@ -2081,40 +2081,23 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved
   if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
     return [(e, projs)]  -- section variables should shadow global decls
   if preresolved.isEmpty then
-    process (← realizeGlobalName n)
+    mkConsts (← realizeGlobalName n) explicitLevels
   else
-    process preresolved
-where
-  process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
-    if !candidates.isEmpty then
-      return (← mkConsts candidates explicitLevels)
-    let env ← getEnv
-    -- check for scope errors before trying auto implicits
-    if env.isExporting then
-      if let [(npriv, _)] ← withoutExporting <| resolveGlobalName (enableLog := false) n then
-        throwUnknownIdentifierAt (declHint := npriv) stx m!"Unknown identifier `{.ofConstName n}`"
-    if !(← read).autoBoundImplicitForbidden n then
-      if (← read).autoBoundImplicitContext.isSome then
-        let allowed := autoImplicit.get (← getOptions)
-        let relaxed := relaxedAutoImplicit.get (← getOptions)
-        match checkValidAutoBoundImplicitName n (allowed := allowed) (relaxed := relaxed) with
-          | .ok true => throwAutoBoundImplicitLocal n
-          | .ok false => throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"
-          | .error msg => throwUnknownIdentifierAt (declHint := n) stx (m!"Unknown identifier `{.ofConstName n}`" ++ msg)
-    throwUnknownIdentifierAt (declHint := n) stx m!"Unknown identifier `{.ofConstName n}`"
+    mkConsts preresolved explicitLevels
 
 /--
   Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`.
   Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces
   `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/
-def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax)) := do
-  match ident with
-  | .ident _ _ n preresolved =>
-    let r ← resolveName ident n preresolved explicitLevels expectedType?
-    r.mapM fun (c, fields) => do
-      let ids := ident.identComponents (nFields? := fields.length)
-      return (c, ids.head!, ids.tail!)
-  | _ => throwError "identifier expected"
+def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do
+  let .ident _ _ n preresolved := ident
+    | throwError "identifier expected"
+  let r ← resolveName ident n preresolved explicitLevels expectedType?
+  let rc ← r.mapM fun (c, fields) => do
+    let ids := ident.identComponents (nFields? := fields.length)
+    return (c, ids.head!, ids.tail!)
+  return (n, rc)
+
 
 def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM (Option Expr) := withRef stx do
   match stx with

src/Lean/IdentifierSuggestion.lean

@@ -14,6 +14,7 @@ public import Lean.ResolveName
 import all Lean.Elab.ErrorUtils
 
 namespace Lean
+open Elab.Term
 
 set_option doc.verso true
 
@@ -107,14 +108,14 @@ public def getStoredSuggestions [Monad m] [MonadEnv m] (trueName : Name) : m Nam
     | some (_, extras) => extras.foldl (init := results) fun accum extra => accum.insert extra
 
 /--
-Throw an unknown constant error message, potentially suggesting alternatives using
-{name}`suggest_for` attributes. (Like {name}`throwUnknownConstantAt` but with suggestions.)
+Throw an unknown constant/identifier error message, potentially suggesting alternatives using
+{name}`suggest_for` attributes.
 
 The replacement will mimic the path structure of the original as much as possible if they share a
 path prefix: if there is a suggestion for replacing `Foo.Bar.jazz` with `Foo.Bar.baz`, then
 `Bar.jazz` will be replaced by `Bar.baz` unless the resulting constant is ambiguous.
 -/
-public def throwUnknownConstantWithSuggestions (constName : Name) (ref? : Option Syntax := .none) : CoreM α := do
+public def throwUnknownNameWithSuggestions (constName : Name) (idOrConst := "identifier") (declHint := constName) (ref? : Option Syntax := .none) (extraMsg : MessageData := .nil) : TermElabM α := do
   let suggestions := (← getSuggestions constName).toArray
   let ref := ref?.getD (← getRef)
   let hint ← if suggestions.size = 0 then
@@ -144,4 +145,4 @@ public def throwUnknownConstantWithSuggestions (constName : Name) (ref? : Option
           toCodeActionTitle? := .some (s!"Change to {·}"),
           messageData? := .some m!"`{.ofConstName suggestion}`",
         }) ref
-  throwUnknownIdentifierAt (declHint := constName) ref (m!"Unknown constant `{.ofConstName constName}`" ++ hint)
+  throwUnknownIdentifierAt (declHint := declHint) ref (m!"Unknown {idOrConst} `{.ofConstName constName}`" ++ extraMsg ++ hint)

tests/lean/run/idSuggestShort.lean

@@ -0,0 +1,21 @@
+set_option autoImplicit false
+
+/--
+error: Unknown identifier `ℕ`
+
+Note: It is not possible to treat `ℕ` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+
+Hint: Perhaps you meant `Nat` in place of `ℕ`:
+  [apply] `Nat`
+-/
+#guard_msgs in example : ℕ := 3
+
+/--
+error: Unknown identifier `Result`
+
+Note: It is not possible to treat `Result` as an implicitly bound variable here because the `autoImplicit` option is set to `false`.
+
+Hint: Perhaps you meant `Except` in place of `Result`:
+  [apply] `Except`
+-/
+#guard_msgs in example : Result String Nat := .ok 3