feat: @[suggest_for] attribute to inform replacements (#11367)

This PR introduces a new annotation that allows definitions to describe
plausible-but-wrong name variants for the purpose of improving error
messages.

This PR just adds the notation and extra functionality; a stage0 update
will allow standard Lean functions to have suggestion annotations.
(Hence the changelog-no tag: this should go in the changelog when some
preliminary annotations are actually added.)

## Example

```lean4
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
```

Author: robsimmons

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 .. =>
@@ -1394,7 +1395,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 \
@@ -1413,10 +1414,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)