Commas are used to have multiple attributes, so attributes shouldn't contain commas

src/Init/Notation.lean

@@ -633,6 +633,20 @@ existing code. It may be removed in a future version of the library.
 syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
     (" (" &"since" " := " str ")")? : attr
 
+/--
+The attribute `@[suggest_for]` on a declaration suggests likely ways in which
+someone might **incorrectly** refer to a definition.
+
+* `@[suggest_for String.endPos]` on the definition of `String.rawEndPos` suggests that `"str".endPos` might be correctable to `"str".rawEndPos`.
+* `@[suggest_for Either Result]` on the definition of `Except` suggests that `Either Nat String` might be correctable to `Except Nat String`.
+
+The namespace of the suggestions is always relative to the root namespace. In the namespace `X.Y`,
+adding an annotation `@[suggest_for Z.bar]` to `def Z.foo` will suggest `X.Y.Z.foo` only as a
+replacement for `Z.foo`. If your intent is to suggest `X.Y.Z.foo` as a replacement for
+`X.Y.Z.bar`, you must instead use the annotation `@[suggest_for X.Y.Z.bar]`.
+-/
+syntax (name := suggest_for) "suggest_for" (ppSpace ident)+ : attr
+
 /--
 The `@[coe]` attribute on a function (which should also appear in a
 `instance : Coe A B := ⟨myFn⟩` declaration) allows the delaborator to show

src/Lean/Elab/App.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Tactic.ElimInfo
 public import Lean.Elab.Binders
 public import Lean.Elab.RecAppSyntax
+public import Lean.IdentifierSuggestion
 import all Lean.Elab.ErrorUtils
 
 public section
@@ -1368,7 +1369,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 =>
-      throwUnknownConstant (c ++ suffix)
+      throwUnknownConstantWithSuggestions (c ++ suffix)
     | _, _ =>
       throwInvalidFieldAt ref fieldName fullName
   | .forallE .., .fieldIdx .. =>
@@ -1385,7 +1386,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 =>
-      throwUnknownConstant (c ++ suffix)
+      throwUnknownConstantWithSuggestions (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 \
@@ -1404,10 +1405,24 @@ where
         m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`, so it is not \
           possible to project the field `{fieldName}` from an expression{indentExpr e}\nof \
           type{inlineExprTrailing eType}"
+
+    -- Possible alternatives provided with `@[suggest_for]` annotations
+    let suggestions := (← Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix)
+    let suggestForHint ←
+      if suggestions.size = 0 then
+        pure .nil
+      else
+        m!"Perhaps you meant one of these in place of `{fullName}`:".hint (suggestions.map fun suggestion => {
+          suggestion := suggestion.getString!,
+          toCodeActionTitle? := .some (s!"Suggested replacement: {e}.{·}"),
+          diffGranularity := .all,
+          messageData? := .some m!"`{.ofConstName suggestion}`: {e}.{suggestion.getString!}",
+        }) ref
+
     -- By using `mkUnknownIdentifierMessage`, the tag `Lean.unknownIdentifierMessageTag` is
     -- incorporated within the message, as required for the "import unknown identifier" code action.
     -- The "outermost" lean.invalidField name is the only one that triggers an error explanation.
-    throwNamedErrorAt ref lean.invalidField msg
+    throwNamedErrorAt ref lean.invalidField (msg ++ suggestForHint)
 
 
 /-- whnfCore + implicit consumption.

src/Lean/Expr.lean

@@ -952,18 +952,30 @@ def isCharLit : Expr → Bool
   | app (const c _) a => c == ``Char.ofNat && a.isRawNatLit
   | _                 => false
 
+/--
+If the expression is a constant, return that name.
+Otherwise panic.
+-/
 def constName! : Expr → Name
   | const n _ => n
   | _         => panic! "constant expected"
 
+/--
+If the expression is a constant, return that name.
+Otherwise return `Option.none`.
+-/
 def constName? : Expr → Option Name
   | const n _ => some n
   | _         => none
 
-/-- If the expression is a constant, return that name. Otherwise return `Name.anonymous`. -/
+/--
+If the expression is a constant, return that name.
+Otherwise return `Name.anonymous`.
+-/
 def constName (e : Expr) : Name :=
   e.constName?.getD Name.anonymous
 
+
 def constLevels! : Expr → List Level
   | const _ ls => ls
   | _          => panic! "constant expected"

src/Lean/IdentifierSuggestion.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2025 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rob Simmons
+-/
+module
+
+prelude
+public import Lean.Attributes
+public import Lean.Exception
+public import Lean.Meta.Hint
+public import Lean.Elab.DeclModifiers
+public import Lean.ResolveName
+import all Lean.Elab.ErrorUtils
+
+namespace Lean
+
+set_option doc.verso true
+
+builtin_initialize identifierSuggestionForAttr : ParametricAttribute (Name × Array Name) ←
+  registerParametricAttribute {
+    name := `suggest_for,
+    descr := "suggest other (incorrect, not-existing) identifiers that someone might use when they actually want this definition",
+    getParam := fun trueDeclName stx => do
+      let `(attr| suggest_for $altNames:ident*) := stx
+        | throwError "Invalid `[suggest_for]` attribute syntax"
+      let ns := trueDeclName.getPrefix
+      return (trueDeclName, altNames.map (·.getId))
+    }
+
+public def getSuggestions [Monad m] [MonadEnv m] (fullName : Name) : m (Array Name) := do
+  let mut possibleReplacements := #[]
+  let (_, allSuggestions) := identifierSuggestionForAttr.ext.getState (← getEnv)
+  for (_, trueName, suggestions) in allSuggestions do
+    for suggestion in suggestions do
+      if fullName = suggestion then
+        possibleReplacements := possibleReplacements.push trueName
+  return possibleReplacements.qsort (lt := lt)
+where
+  -- Ensure the result of getSuggestions is stable (if arbitrary)
+  lt : Name -> Name -> Bool
+    | .anonymous, _ => false
+    | .str _ _, .anonymous => true
+    | .num _ _, .anonymous => true
+    | .str _ _, .num _ _ => true
+    | .num _ _, .str _ _ => false
+    | .num a n, .num b m => n < m || n == m && lt a b
+    | .str a s1, .str b s2 => s1 < s2 || s1 == s2 && lt a b
+
+/--
+Throw an unknown constant error message, potentially suggesting alternatives using
+{name}`suggest_for` attributes. (Like {name}`throwUnknownConstantAt` but with suggestions.)
+
+The "Unknown constant `<id>`" message will fully qualify the name, whereas the
+-/
+public def throwUnknownConstantWithSuggestions (constName : Name) : CoreM α := do
+  let suggestions ← getSuggestions constName
+  let ref ← getRef
+  let hint ← if suggestions.size = 0 then
+      pure MessageData.nil
+    else
+      -- Modify suggestions to have the same structure as the user-provided identifier, but only
+      -- if that doesn't cause ambiguity.
+      let rawId := (← getRef).getId
+      let env ← getEnv
+      let ns ← getCurrNamespace
+      let openDecls ← getOpenDecls
+      let modifySuggestion := match constName.eraseSuffix? rawId with
+        | .none => id
+        | .some prefixName => fun (suggestion : Name) =>
+            let candidate := suggestion.replacePrefix prefixName .anonymous
+            if (ResolveName.resolveGlobalName env {} ns openDecls candidate |>.length) != 1 then
+              suggestion
+            else
+              candidate
+
+      let alternative := if h : suggestions.size = 1 then m!"`{.ofConstName suggestions[0]}`" else m!"one of these"
+      m!"Perhaps you meant {alternative} in place of `{.ofName rawId}`:".hint (suggestions.map fun suggestion =>
+        let modified := modifySuggestion suggestion
+        {
+          suggestion := s!"{modified}",
+          toCodeActionTitle? := .some (s!"Suggested replacement: {·}"),
+          diffGranularity := .all,
+          -- messageData? := .some m!"replace `{.ofName rawId}` with `{.ofName modified}`",
+        }) ref
+  throwUnknownIdentifierAt (declHint := constName) ref (m!"Unknown constant `{.ofConstName constName}`" ++ hint)

tests/lean/run/identifierSuggestions.lean

@@ -0,0 +1,280 @@
+@[suggest_for String.test0 String.test1 String.test2]
+public def String.foo (x: String) := x.length + 1
+
+@[simp, grind, suggest_for test1 String.test2]
+public def String.bar (x: String) := x.length + 1
+
+@[suggest_for String.test1 String.test2, inline]
+public def String.baz (x: String) := x.length + 1
+
+@[suggest_for String.test2, always_inline]
+public def otherFoo (x: String) := x.length + 1
+
+@[suggest_for String.test2]
+public def otherBaz (x: String) := x.length + 1
+
+@[suggest_for _root_.String.test2]
+public def Nat.otherBar (x: String) := x.length + 1
+
+-- Single suggested replacement
+/--
+error: Invalid field `test0`: The environment does not contain `String.test0`, so it is not possible to project the field `test0` from an expression
+  "abc"
+of type `String`
+
+Hint: Perhaps you meant one of these in place of `String.test0`:
+  [apply] `String.foo`: "abc".foo
+-/
+#guard_msgs in
+#check "abc".test0
+
+/--
+error: Unknown constant `String.test0`
+
+Hint: Perhaps you meant `String.foo` in place of `String.test0`:
+  S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵0̵S̲t̲r̲i̲n̲g̲.̲f̲o̲o̲
+-/
+#guard_msgs in
+#check String.test0
+
+-- Two suggested replacements: the bar replacement is for `test1`, which does not apply
+/--
+error: Invalid field `test1`: The environment does not contain `String.test1`, so it is not possible to project the field `test1` from an expression
+  "abc"
+of type `String`
+
+Hint: Perhaps you meant one of these in place of `String.test1`:
+  [apply] `String.baz`: "abc".baz
+  [apply] `String.foo`: "abc".foo
+-/
+#guard_msgs in
+#check "abc".test1
+
+/--
+error: Unknown constant `String.test1`
+
+Hint: Perhaps you meant one of these in place of `String.test1`:
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵1̵S̲t̲r̲i̲n̲g̲.̲b̲a̲z̲
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵1̵S̲t̲r̲i̲n̲g̲.̲f̲o̲o̲
+-/
+#guard_msgs in
+#check String.test1
+
+-- Three suggested replacements (filters the ones with other types)
+/--
+error: Invalid field `test2`: The environment does not contain `String.test2`, so it is not possible to project the field `test2` from an expression
+  "abc"
+of type `String`
+
+Hint: Perhaps you meant one of these in place of `String.test2`:
+  [apply] `String.bar`: "abc".bar
+  [apply] `String.baz`: "abc".baz
+  [apply] `String.foo`: "abc".foo
+-/
+#guard_msgs in
+#check "abc".test2
+
+-- Five suggested replacements: does not filter out non-`String` functions, but `_root_` prefix won't ever match.
+/--
+error: Unknown constant `String.test2`
+
+Hint: Perhaps you meant one of these in place of `String.test2`:
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵2̵S̲t̲r̲i̲n̲g̲.̲b̲a̲r̲
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵2̵S̲t̲r̲i̲n̲g̲.̲b̲a̲z̲
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵2̵S̲t̲r̲i̲n̲g̲.̲f̲o̲o̲
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵2̵o̲t̲h̲e̲r̲B̲a̲z̲
+  • S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵2̵o̲t̲h̲e̲r̲F̲o̲o̲
+-/
+#guard_msgs in
+#check String.test2
+
+
+namespace Foo
+inductive Bar where | one | two | three
+
+attribute [suggest_for Foo.Bar.first] Bar.one
+end Foo
+
+namespace Foo.Bar
+attribute [suggest_for Foo.Bar.second Foo.more] Bar.two
+
+@[suggest_for Foo.Bar.toStr]
+def toString : Foo.Bar → String
+ | .one => "one"
+ | .two => "two"
+ | .three => "three"
+end Foo.Bar
+
+attribute [suggest_for Foo.Bar.third Foo.more] Foo.Bar.three
+
+@[suggest_for Foo.Bar.toNum]
+def Foo.Bar.toNat : Foo.Bar → Nat
+  | .one => 1
+  | .two => 2
+  | .three => 3
+
+/--
+error: Invalid field `toNum`: The environment does not contain `Foo.Bar.toNum`, so it is not possible to project the field `toNum` from an expression
+  Foo.Bar.three
+of type `Foo.Bar`
+
+Hint: Perhaps you meant one of these in place of `Foo.Bar.toNum`:
+  [apply] `Foo.Bar.toNat`: Foo.Bar.three.toNat
+-/
+#guard_msgs in
+#eval Foo.Bar.three.toNum
+
+/--
+error: Invalid field `toStr`: The environment does not contain `Foo.Bar.toStr`, so it is not possible to project the field `toStr` from an expression
+  Foo.Bar.two
+of type `Foo.Bar`
+
+Hint: Perhaps you meant one of these in place of `Foo.Bar.toStr`:
+  [apply] `Foo.Bar.toString`: Foo.Bar.two.toString
+-/
+#guard_msgs in
+#eval Foo.Bar.two.toStr
+
+/- ----- -/
+
+/--
+error: Unknown constant `Foo.Bar.first`
+
+Hint: Perhaps you meant `Foo.Bar.one` in place of `Foo.Bar.first`:
+  F̵o̵o̵.̵B̵a̵r̵.̵f̵i̵r̵s̵t̵F̲o̲o̲.̲B̲a̲r̲.̲o̲n̲e̲
+-/
+#guard_msgs in
+#check Foo.Bar.first
+
+/-- error: Unknown identifier `Bar.second` -/
+#guard_msgs in
+#check Bar.second
+
+/-- error: Unknown identifier `third` -/
+#guard_msgs in
+#check third
+
+/- ----- -/
+
+namespace Foo
+/--
+error: Unknown constant `Foo.Bar.first`
+
+Hint: Perhaps you meant `Bar.one` in place of `Foo.Bar.first`:
+  F̵o̵o̵.̵B̵a̵r̵.̵f̵i̵r̵s̵t̵F̲o̲o̲.̲B̲a̲r̲.̲o̲n̲e̲
+-/
+#guard_msgs in
+#check Foo.Bar.first
+
+/--
+error: Unknown constant `Foo.Bar.second`
+
+Hint: Perhaps you meant `Bar.two` in place of `Bar.second`:
+  B̵a̵r̵.̵s̵e̵c̵o̵n̵d̵B̲a̲r̲.̲t̲w̲o̲
+-/
+#guard_msgs in
+#check Bar.second
+
+/-- error: Unknown identifier `third` -/
+#guard_msgs in
+#check third
+end Foo
+
+/- ----- -/
+
+namespace Foo.Bar
+/--
+error: Unknown constant `Foo.Bar.first`
+
+Hint: Perhaps you meant `one` in place of `Foo.Bar.first`:
+  F̵o̵o̵.̵B̵a̵r̵.̵f̵i̵r̵s̵t̵F̲o̲o̲.̲B̲a̲r̲.̲o̲n̲e̲
+-/
+#guard_msgs in
+#check Foo.Bar.first
+
+/--
+error: Unknown constant `Foo.Bar.second`
+
+Hint: Perhaps you meant `two` in place of `Bar.second`:
+  B̵a̵r̵.̵s̵e̵c̵o̵n̵d̵B̲a̲r̲.̲t̲w̲o̲
+-/
+#guard_msgs in
+#check Bar.second
+
+-- TODO: give a suggestion here!
+/-- error: Unknown identifier `third` -/
+#guard_msgs in
+#check third
+end Foo.Bar
+
+/- ----- -/
+
+-- Don't suggest an ambiguous replacement
+namespace Foo2
+inductive Bar where | one | two | three
+attribute [suggest_for Foo2.Bar.first] Bar.one
+end Foo2
+
+namespace Whatever
+open Foo
+open Foo2
+/--
+error: overloaded, errors ⏎
+  Unknown constant `Foo2.Bar.first`
+  ⏎
+  Hint: Perhaps you meant `Foo2.Bar.one` in place of `Bar.first`:
+    B̵a̵r̵.̵f̵i̵r̵s̵t̵F̲o̲o̲2̲.̲B̲a̲r̲.̲o̲n̲e̲
+  ⏎
+  Unknown constant `Foo.Bar.first`
+  ⏎
+  Hint: Perhaps you meant `Foo.Bar.one` in place of `Bar.first`:
+    B̵a̵r̵.̵f̵i̵r̵s̵t̵F̲o̲o̲.̲B̲a̲r̲.̲o̲n̲e̲
+-/
+#guard_msgs in
+#eval Bar.first
+end Whatever
+
+-- Limitation: we ought to suggest `Foo2.Bar.one` here, but we're relying on the upstream
+-- infrastructure that decides that `Bar.first` means `Foo.Bar.first` in this context.
+namespace Foo
+open Foo2
+/--
+error: Unknown constant `Foo.Bar.first`
+
+Hint: Perhaps you meant `Bar.one` in place of `Bar.first`:
+  B̵a̵r̵.̵f̵i̵r̵s̵t̵B̲a̲r̲.̲o̲n̲e̲
+-/
+#guard_msgs in
+#eval Bar.first
+end Foo
+
+
+inductive MyBool where | tt | ff
+
+attribute [suggest_for MyBool.true] MyBool.tt
+attribute [suggest_for MyBool.false] MyBool.ff
+
+@[suggest_for MyBool.not]
+def MyBool.swap : MyBool → MyBool
+  | tt => ff
+  | ff => tt
+
+/--
+error: Unknown constant `MyBool.true`
+
+Hint: Perhaps you meant `MyBool.tt` in place of `MyBool.true`:
+  M̵y̵B̵o̵o̵l̵.̵t̵r̵u̵e̵M̲y̲B̲o̲o̲l̲.̲t̲t̲
+-/
+#guard_msgs in
+example := MyBool.true
+
+/--
+error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
+  MyBool.tt
+of type `MyBool`
+
+Hint: Perhaps you meant one of these in place of `MyBool.not`:
+  [apply] `MyBool.swap`: MyBool.tt.swap
+-/
+#guard_msgs in
+example := MyBool.tt.not