chore: switch the association of stored suggestions (#11590)

robsimmons · web-flow · commit 9e875603768b · 2025-12-10T21:42:05.000Z
This PR switches the way olean files store identifier suggestions. The ordering introduced in #11367 and #11529 made sense if we were only storing incorrect -> correct mappings, but for the reference manual we want to store the correct -> incorrect mappings as well, and so it is more sensible to store just the correct -> incorrect mapping that mimics the author-generated data better. Also tweaks error messages further in preparation for public-facing @[suggest_for] annotations and forbids suggestions on non-public names. Does not make generally-visible changes as there are no introduced uses of @[suggest_for] annotations yet.
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
@@ -1375,13 +1375,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
 
-  | .forallE .., LVal.fieldName ref fieldName suffix? _fullRef =>
+  | .forallE .., LVal.fieldName ref fieldName suffix? fullRef =>
     let fullName := Name.str `Function fieldName
     if (← getEnv).contains fullName then
       return LValResolution.const `Function `Function fullName
     match e.getAppFn, suffix? with
     | Expr.const c _, some suffix =>
-      throwUnknownConstantWithSuggestions (c ++ suffix)
+      throwUnknownConstantWithSuggestions (ref? := fullRef) (c ++ suffix)
     | _, _ =>
       throwInvalidFieldAt ref fieldName fullName
   | .forallE .., .fieldIdx .. =>
@@ -1402,8 +1402,8 @@ 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 (c ++ suffix)
+    | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef =>
+      throwUnknownConstantWithSuggestions (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 \
@@ -1424,26 +1424,26 @@ where
           type{inlineExprTrailing eType}"
 
     -- Possible alternatives provided with `@[suggest_for]` annotations
-    let suggestions := (← Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix)
+    let suggestions := (← Lean.getSuggestions fullName).filter (·.getPrefix = fullName.getPrefix) |>.toArray
     let suggestForHint ←
       if h : suggestions.size = 0 then
         pure .nil
       else if suggestions.size = 1 then
         MessageData.hint (ref? := ref)
           m!"Perhaps you meant `{.ofConstName suggestions[0]}` in place of `{fullName}`:"
           (suggestions.map fun suggestion => {
-            preInfo? := .some s!"{e}.",
+            preInfo? := .some s!".",
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
+            toCodeActionTitle? := .some (s!"Change to .{·}"),
             diffGranularity := .all,
           })
       else
         MessageData.hint (ref? := ref)
           m!"Perhaps you meant one of these in place of `{fullName}`:"
           (suggestions.map fun suggestion => {
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
-            messageData? := .some m!"`{.ofConstName suggestion}`: {e}.{suggestion.getString!}",
+            toCodeActionTitle? := .some (s!"Change to .{·}"),
+            messageData? := .some m!"`{.ofConstName suggestion}`",
           })
 
     -- By using `mkUnknownIdentifierMessage`, the tag `Lean.unknownIdentifierMessageTag` is
diff --git a/src/Lean/IdentifierSuggestion.lean b/src/Lean/IdentifierSuggestion.lean
@@ -17,23 +17,35 @@ namespace Lean
 
 set_option doc.verso true
 
+public structure IdentSuggestion where
+  existingToIncorrect : NameMap NameSet := {}
+  incorrectToExisting : NameMap NameSet := {}
+deriving Inhabited
+
+def IdentSuggestion.add (table : IdentSuggestion) (trueName : Name) (altNames : Array Name) : IdentSuggestion :=
+  { existingToIncorrect :=
+      table.existingToIncorrect.alter trueName fun old =>
+        altNames.foldl (β := NameSet) (init := old.getD {}) fun accum altName =>
+          accum.insert altName
+    incorrectToExisting :=
+      altNames.foldl (init := table.incorrectToExisting) fun accum altName =>
+        accum.alter altName fun old =>
+          old.getD {} |>.insert trueName
+  }
 
 builtin_initialize identifierSuggestionForAttr : PersistentEnvExtension
-    (Name × Array Name) /- *Store* mappings from incorrect names to corrections (identifiers that exist) -/
-    (Name × Array Name) /- *Add* mappings from existing functions to possible incorrect namings -/
-    (NameMap NameSet) /- *Use* mapping from incorrect names to corrections (identifiers that exist) -/ ←
+    (Name × Array Name) /- Mapping from existing constant to potential incorrect alternative names -/
+    (Name × Array Name) /- Mapping from existing constant to potential incorrect alternative names -/
+    IdentSuggestion /- Two directional mapping between existing identifier and alternative incorrect mappings -/ ←
   let ext ← registerPersistentEnvExtension {
     mkInitial := pure {},
     addImportedFn := fun modules => pure <|
-      modules.foldl (init := {}) fun accum entries =>
-        entries.foldl (init := accum) fun accum (altName, trueNames) =>
-          accum.alter altName (fun old => trueNames.foldl (β := NameSet) (init := old.getD ∅) fun accum trueName =>
-            accum.insert trueName),
-    addEntryFn := fun table (trueName, altNames) =>
-      altNames.foldl (init := table) fun accum alt =>
-        accum.alter alt (·.getD {} |>.insert trueName)
-    exportEntriesFn table := table.toArray.map fun (altName, trueNames) =>
-      (altName, trueNames.toArray)
+      (modules.foldl (init := {}) fun accum entries =>
+        entries.foldl (init := accum) fun accum (trueName, altNames) =>
+          accum.add trueName altNames),
+    addEntryFn := fun table (trueName, altNames) => table.add trueName altNames
+    exportEntriesFn table := table.existingToIncorrect.toArray.map fun (trueName, altNames) =>
+      (trueName, altNames.toArray)
   }
 
   registerBuiltinAttribute {
@@ -47,32 +59,48 @@ builtin_initialize identifierSuggestionForAttr : PersistentEnvExtension
         | -- Attributes parsed _before the suggest_for notation is added
           .node _ ``Parser.Attr.simple #[.ident _ _ `suggest_for [], .node _ `null #[id]] => pure #[id]
         | _ => throwError "Invalid `[suggest_for]` attribute syntax {repr stx}"
+      if isPrivateName decl then
+        throwError "Cannot make suggestions for private names"
       modifyEnv (ext.addEntry · (decl, altSyntaxIds.map (·.getId)))
   }
 
   return ext
 
-public def getSuggestions [Monad m] [MonadEnv m] (fullName : Name) : m (Array Name) := do
+/--
+Given a name, find all the stored correct, existing identifiers that mention that name in a
+{lit}`suggest_for` annotation.
+-/
+public def getSuggestions [Monad m] [MonadEnv m] (incorrectName : Name) : m NameSet := do
+  return identifierSuggestionForAttr.getState (← getEnv)
+    |>.incorrectToExisting
+    |>.find? incorrectName
+    |>.getD {}
+
+/--
+Given a (presumably existing) identifier, find all the {lit}`suggest_for` annotations that were given
+for that identifier.
+-/
+public def getStoredSuggestions [Monad m] [MonadEnv m] (trueName : Name) : m NameSet := do
   return identifierSuggestionForAttr.getState (← getEnv)
-    |>.find? fullName
+    |>.existingToIncorrect
+    |>.find? trueName
     |>.getD {}
-    |>.toArray
 
 /--
 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
+public def throwUnknownConstantWithSuggestions (constName : Name) (ref? : Option Syntax := .none) : CoreM α := do
+  let suggestions := (← getSuggestions constName).toArray
+  let ref := ref?.getD (← 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 rawId := ref.getId
       let env ← getEnv
       let ns ← getCurrNamespace
       let openDecls ← getOpenDecls
@@ -86,7 +114,8 @@ public def throwUnknownConstantWithSuggestions (constName : Name) : CoreM α :=
               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 inPlaceOfThis := if rawId.isAnonymous then .nil else m!" in place of `{.ofName rawId}`"
+      m!"Perhaps you meant {alternative}{inPlaceOfThis}:".hint (suggestions.map fun suggestion =>
         let modified := modifySuggestion suggestion
         {
           suggestion := s!"{modified}",
diff --git a/tests/lean/run/idSuggestStandalone.lean b/tests/lean/run/idSuggestStandalone.lean
@@ -23,7 +23,7 @@ error: Invalid field `test0`: The environment does not contain `String.test0`, s
 of type `String`
 
 Hint: Perhaps you meant `String.foo` in place of `String.test0`:
-  "abc".t̵e̵s̵t̵0̵f̲o̲o̲
+  .t̵e̵s̵t̵0̵f̲o̲o̲
 -/
 #guard_msgs in
 #check "abc".test0
@@ -44,8 +44,8 @@ error: Invalid field `test1`: The environment does not contain `String.test1`, s
 of type `String`
 
 Hint: Perhaps you meant one of these in place of `String.test1`:
-  [apply] `String.foo`: "abc".foo
-  [apply] `String.baz`: "abc".baz
+  [apply] `String.foo`
+  [apply] `String.baz`
 -/
 #guard_msgs in
 #check "abc".test1
@@ -67,9 +67,9 @@ error: Invalid field `test2`: The environment does not contain `String.test2`, s
 of type `String`
 
 Hint: Perhaps you meant one of these in place of `String.test2`:
-  [apply] `String.foo`: "abc".foo
-  [apply] `String.baz`: "abc".baz
-  [apply] `String.bar`: "abc".bar
+  [apply] `String.foo`
+  [apply] `String.baz`
+  [apply] `String.bar`
 -/
 #guard_msgs in
 #check "abc".test2
@@ -119,7 +119,7 @@ error: Invalid field `toNum`: The environment does not contain `Foo.Bar.toNum`,
 of type `Foo.Bar`
 
 Hint: Perhaps you meant `Foo.Bar.toNat` in place of `Foo.Bar.toNum`:
-  Foo.Bar.three.t̵o̵N̵u̵m̵t̲o̲N̲a̲t̲
+  .t̵o̵N̵u̵m̵t̲o̲N̲a̲t̲
 -/
 #guard_msgs in
 #eval Foo.Bar.three.toNum
@@ -130,7 +130,7 @@ error: Invalid field `toStr`: The environment does not contain `Foo.Bar.toStr`,
 of type `Foo.Bar`
 
 Hint: Perhaps you meant `Foo.Bar.toString` in place of `Foo.Bar.toStr`:
-  Foo.Bar.two.t̵o̵S̵t̵r̵t̲o̲S̲t̲r̲i̲n̲g̲
+  .t̵o̵S̵t̵r̵t̲o̲S̲t̲r̲i̲n̲g̲
 -/
 #guard_msgs in
 #eval Foo.Bar.two.toStr
@@ -274,7 +274,35 @@ error: Invalid field `not`: The environment does not contain `MyBool.not`, so it
 of type `MyBool`
 
 Hint: Perhaps you meant `MyBool.swap` in place of `MyBool.not`:
-  MyBool.tt.n̵o̵t̵s̲w̲a̲p̲
+  .n̵o̵t̵s̲w̲a̲p̲
 -/
 #guard_msgs in
 example := MyBool.tt.not
+
+/--
+error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
+  (fun x => if x < 3 then MyBool.tt else MyBool.ff) 4
+of type `MyBool`
+
+Hint: Perhaps you meant `MyBool.swap` in place of `MyBool.not`:
+  .n̵o̵t̵s̲w̲a̲p̲
+-/
+#guard_msgs in
+example := ((fun x => if x < 3 then MyBool.tt else .ff) 4).not
+
+
+@[suggest_for MyBool.not]
+def MyBool.justFalse : MyBool → MyBool
+  | _ => ff
+
+/--
+error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
+  (fun x => if x < 3 then MyBool.tt else MyBool.ff) 4
+of type `MyBool`
+
+Hint: Perhaps you meant one of these in place of `MyBool.not`:
+  [apply] `MyBool.justFalse`
+  [apply] `MyBool.swap`
+-/
+#guard_msgs in
+example := ((fun x => if x < 3 then MyBool.tt else .ff) 4).not
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
@@ -510,3 +510,17 @@ public meta def delab : Lean.PrettyPrinter.Delaborator.Delab :=
 
 public def noMetaDelab : Lean.PrettyPrinter.Delaborator.Delab :=
   default
+
+/-- error: Cannot make suggestions for private names -/
+#guard_msgs in
+@[suggest_for Bar1]
+def FooBar1 := 4
+
+/-- error: Cannot make suggestions for private names -/
+#guard_msgs in
+@[suggest_for Bar2]
+meta def FooBar2 := 4
+
+#guard_msgs in
+@[suggest_for Bar3 FooBar1 FooBar2]
+public def FooBar3 := 4
