From f88e503f3d21cee457b264398b24f62f352e711b Mon Sep 17 00:00:00 2001
From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com>
Date: Wed, 10 Dec 2025 17:50:45 -0500
Subject: [PATCH] feat: `@[suggest_for]` annotations for prompting easy-to-miss
 names (#11554)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds `@[suggest_for]` annotations to Lean, allowing lean to
provide corrections for `.every` or `.some` methods in place of `.all`
or `.any` methods for most default-imported types (arrays, lists,
strings, substrings, and subarrays, and vectors).

Due to the need for stage0 updates for new annotations, the
`suggest_for` annotation itself was introduced in previous PRs: #11367,
#11529, and #11590.

## Example
```
example := "abc".every (! ·.isWhitespace)
```

Error message:
```
Invalid field `every`: The environment does not contain `String.every`, so it is not possible to project the field `every` from an expression
  "abc"
of type `String`

Hint: Perhaps you meant `String.all` in place of `String.every`:
  .e̵v̵e̵r̵y̵a̲l̲l̲
```

(the hint is added by this PR)

## Additional changes

Adds suggestions that are not currently active but that can be used to
generate autocompletion suggestions in the reference manual:
 - `Either` -> `Except` and `Sum`
 - `Exception` -> `Except`
 - `ℕ` -> `Nat`
 - `Nullable` -> `Option`
 - `Maybe` -> `Option`
 - `Optional` -> `Option`
 - `Result` -> `Except`
---
 src/Init/Core.lean                      |   1 +
 src/Init/Data/Array/Basic.lean          |   4 +-
 src/Init/Data/Array/Subarray.lean       |   4 +-
 src/Init/Data/List/Basic.lean           |   2 +
 src/Init/Data/String/Search.lean        |   5 +-
 src/Init/Data/String/Slice.lean         |   2 +-
 src/Init/Data/String/Substring.lean     |   4 +-
 src/Init/Data/Vector/Basic.lean         |   4 +-
 src/Init/Prelude.lean                   |   3 +
 tests/lean/run/idSuggestEvery.lean      | 110 ++++++++++++++++++++++++
 tests/lean/run/idSuggestStandalone.lean |  13 +++
 11 files changed, 141 insertions(+), 11 deletions(-)
 create mode 100644 tests/lean/run/idSuggestEvery.lean

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 919797cdc5..a08aef2cb4 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -201,6 +201,7 @@ An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : 
 indication of which of the two types was chosen. The union of a singleton set with itself contains
 one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
 -/
+@[suggest_for Either]
 inductive Sum (α : Type u) (β : Type v) where
   /-- Left injection into the sum type `α ⊕ β`. -/
   | inl (val : α) : Sum α β
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 5805456fcb..f33fedb991 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -1348,7 +1348,7 @@ Examples:
 * `#[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `#[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
-@[inline, expose]
+@[inline, expose, suggest_for Array.some]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.anyM (pure <| p ·) start stop
 
@@ -1366,7 +1366,7 @@ Examples:
 * `#[2, 4, 6].all (· % 2 = 0) = true`
 * `#[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
-@[inline]
+@[inline, suggest_for Array.every]
 def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
   Id.run <| as.allM (pure <| p ·) start stop
 
diff --git a/src/Init/Data/Array/Subarray.lean b/src/Init/Data/Array/Subarray.lean
index 50772392ba..48bb946a92 100644
--- a/src/Init/Data/Array/Subarray.lean
+++ b/src/Init/Data/Array/Subarray.lean
@@ -280,7 +280,7 @@ Checks whether any of the elements in a subarray satisfy a Boolean predicate.
 The elements are tested starting at the lowest index and moving up. The search terminates as soon as
 an element that satisfies the predicate is found.
 -/
-@[inline]
+@[inline, suggest_for Subarray.some]
 def any {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
   Id.run <| as.anyM (pure <| p ·)
 
@@ -290,7 +290,7 @@ Checks whether all of the elements in a subarray satisfy a Boolean predicate.
 The elements are tested starting at the lowest index and moving up. The search terminates as soon as
 an element that does not satisfy the predicate is found.
 -/
-@[inline]
+@[inline, suggest_for Subarray.every]
 def all {α : Type u} (p : α → Bool) (as : Subarray α) : Bool :=
   Id.run <| as.allM (pure <| p ·)
 
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 8e830152a8..afa2e5f691 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -1847,6 +1847,7 @@ Examples:
 * `[2, 4, 5, 6].any (· % 2 = 0) = true`
 * `[2, 4, 5, 6].any (· % 2 = 1) = true`
 -/
+@[suggest_for List.some]
 def any : (l : List α) → (p : α → Bool) → Bool
   | [], _ => false
   | h :: t, p => p h || any t p
@@ -1866,6 +1867,7 @@ Examples:
 * `[2, 4, 6].all (· % 2 = 0) = true`
 * `[2, 4, 5, 6].all (· % 2 = 0) = false`
 -/
+@[suggest_for List.every]
 def all : List α → (α → Bool) → Bool
   | [], _ => true
   | h :: t, p => p h && all t p
diff --git a/src/Init/Data/String/Search.lean b/src/Init/Data/String/Search.lean
index 258710d585..d0383ad2d2 100644
--- a/src/Init/Data/String/Search.lean
+++ b/src/Init/Data/String/Search.lean
@@ -324,7 +324,8 @@ Examples:
  * {lean}`"tea".contains (fun (c : Char) => c == 'X') = false`
  * {lean}`"coffee tea water".contains "tea" = true`
 -/
-@[inline] def contains (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
+@[inline, suggest_for String.some]
+def contains (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
   s.toSlice.contains pat
 
 @[export lean_string_contains]
@@ -352,7 +353,7 @@ Examples:
  * {lean}`"aaaaaa".all "aa" = true`
  * {lean}`"aaaaaaa".all "aa" = false`
 -/
-@[inline] def all (s : String) (pat : ρ) [ForwardPattern pat] : Bool :=
+@[inline, suggest_for String.every] def all (s : String) (pat : ρ) [ForwardPattern pat] : Bool :=
   s.toSlice.all pat
 
 /--
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index e206284b6b..6e518e313b 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -505,7 +505,7 @@ Examples:
  * {lean}`"tea".toSlice.contains (fun (c : Char) => c == 'X') = false`
  * {lean}`"coffee tea water".toSlice.contains "tea" = true`
 -/
-@[specialize pat]
+@[specialize pat, suggest_for String.Slice.some]
 def contains (s : Slice) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
   let searcher := ToForwardSearcher.toSearcher pat s
   searcher.any (· matches .matched ..)
diff --git a/src/Init/Data/String/Substring.lean b/src/Init/Data/String/Substring.lean
index 0f7df7c0b2..038a733d8b 100644
--- a/src/Init/Data/String/Substring.lean
+++ b/src/Init/Data/String/Substring.lean
@@ -274,7 +274,7 @@ Checks whether the Boolean predicate `p` returns `true` for any character in a s
 
 Short-circuits at the first character for which `p` returns `true`.
 -/
-@[inline] def any (s : Substring.Raw) (p : Char → Bool) : Bool :=
+@[inline, suggest_for Substring.Raw.some] def any (s : Substring.Raw) (p : Char → Bool) : Bool :=
   s.toSlice?.get!.any p
 
 /--
@@ -282,7 +282,7 @@ Checks whether the Boolean predicate `p` returns `true` for every character in a
 
 Short-circuits at the first character for which `p` returns `false`.
 -/
-@[inline] def all (s : Substring.Raw) (p : Char → Bool) : Bool :=
+@[inline, suggest_for Substring.Raw.every] def all (s : Substring.Raw) (p : Char → Bool) : Bool :=
   s.toSlice?.get!.all p
 
 @[export lean_substring_all]
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 8755e112fc..d6283267b1 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -474,11 +474,11 @@ to avoid having to have the predicate live in `p : α → m (ULift Bool)`.
   xs.toArray.allM p
 
 /-- Returns `true` if `p` returns `true` for any element of the vector. -/
-@[inline, expose] def any (xs : Vector α n) (p : α → Bool) : Bool :=
+@[inline, expose, suggest_for Vector.some] def any (xs : Vector α n) (p : α → Bool) : Bool :=
   xs.toArray.any p
 
 /-- Returns `true` if `p` returns `true` for all elements of the vector. -/
-@[inline, expose] def all (xs : Vector α n) (p : α → Bool) : Bool :=
+@[inline, expose, suggest_for Vector.every] def all (xs : Vector α n) (p : α → Bool) : Bool :=
   xs.toArray.all p
 
 /-- Count the number of elements of a vector that satisfy the predicate `p`. -/
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 2d8528e799..bc15d995e2 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1197,6 +1197,7 @@ This type is special-cased by both the kernel and the compiler, and overridden w
 implementation. Both use a fast arbitrary-precision arithmetic library (usually
 [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
 -/
+@[suggest_for ℕ]
 inductive Nat where
   /--
   Zero, the smallest natural number.
@@ -2856,6 +2857,7 @@ Optional values, which are either `some` around a value from the underlying type
 `Option` can represent nullable types or computations that might fail. In the codomain of a function
 type, it can also represent partiality.
 -/
+@[suggest_for Maybe, suggest_for Optional, suggest_for Nullable]
 inductive Option (α : Type u) where
   /-- No value. -/
   | none : Option α
@@ -3939,6 +3941,7 @@ value of type `α`.
 the `pure` operation is `Except.ok` and the `bind` operation returns the first encountered
 `Except.error`.
 -/
+@[suggest_for Result, suggest_for Exception, suggest_for Either]
 inductive Except (ε : Type u) (α : Type v) where
   /-- A failure value of type `ε` -/
   | error : ε → Except ε α
diff --git a/tests/lean/run/idSuggestEvery.lean b/tests/lean/run/idSuggestEvery.lean
new file mode 100644
index 0000000000..51f20ab8c3
--- /dev/null
+++ b/tests/lean/run/idSuggestEvery.lean
@@ -0,0 +1,110 @@
+-- test every/all replacements in default imports
+
+/-
+Expected replacements for `Subarray.any` and `Subarray.all` do not work as suggestion annotations
+when using generalized field notation: Subarray is an abbreviation and so the underlying `Std.Slice`
+type, which does not have a corresponding `.any`/`.all` function.
+-/
+
+/--
+error: Invalid field `every`: The environment does not contain `Std.Slice.every`, so it is not possible to project the field `every` from an expression
+  x
+of type
+  Std.Slice (Std.Slice.Internal.SubarrayData Nat)
+-/
+#guard_msgs in example (x : Subarray Nat) := x.every fun _ => true
+#guard_msgs in example (x : Subarray Nat) := x.all fun _ => true
+
+/--
+error: Unknown constant `Subarray.every`
+
+Hint: Perhaps you meant `Subarray.all` in place of `Subarray.every`:
+  [apply] `Subarray.all`
+-/
+#guard_msgs in example := (@Subarray.every Nat (fun _ => true) ·)
+#guard_msgs in example := (@Subarray.all Nat (fun _ => true) ·)
+
+/--
+error: Unknown constant `Subarray.some`
+
+Hint: Perhaps you meant `Subarray.any` in place of `Subarray.some`:
+  [apply] `Subarray.any`
+-/
+#guard_msgs in example := (@Subarray.some Nat (fun _ => true) ·)
+#guard_msgs in example := (@Subarray.any Nat (fun _ => true) ·)
+
+/--
+error: Invalid field `every`: The environment does not contain `String.every`, so it is not possible to project the field `every` from an expression
+  x
+of type `String`
+
+Hint: Perhaps you meant `String.all` in place of `String.every`:
+  .e̵v̵e̵r̵y̵a̲l̲l̲
+-/
+#guard_msgs in example (x : String) := x.every fun _ => true
+#guard_msgs in example (x : String) := x.all fun _ => true
+/--
+error: Invalid field `some`: The environment does not contain `String.some`, so it is not possible to project the field `some` from an expression
+  x
+of type `String`
+
+Hint: Perhaps you meant `String.contains` in place of `String.some`:
+  .s̵o̵m̵e̵c̲o̲n̲t̲a̲i̲n̲s̲
+-/
+#guard_msgs in example (x : String) := x.some fun _ => true
+#guard_msgs in example (x : String) := x.contains fun _ => true
+
+
+/--
+error: Invalid field `every`: The environment does not contain `Array.every`, so it is not possible to project the field `every` from an expression
+  x
+of type `Array Nat`
+
+Hint: Perhaps you meant `Array.all` in place of `Array.every`:
+  .e̵v̵e̵r̵y̵a̲l̲l̲
+-/
+#guard_msgs in example (x : Array Nat) := x.every fun _ => true
+#guard_msgs in example (x : Array Nat) := x.all fun _ => true
+/--
+error: Invalid field `some`: The environment does not contain `Array.some`, so it is not possible to project the field `some` from an expression
+  x
+of type `Array Nat`
+
+Hint: Perhaps you meant `Array.any` in place of `Array.some`:
+  .s̵o̵m̵e̵a̲n̲y̲
+-/
+#guard_msgs in example (x : Array Nat) := x.some fun _ => true
+#guard_msgs in example (x : Array Nat) := x.all fun _ => true
+
+/--
+error: Invalid field `every`: The environment does not contain `List.every`, so it is not possible to project the field `every` from an expression
+  x
+of type `List Nat`
+
+Hint: Perhaps you meant `List.all` in place of `List.every`:
+  .e̵v̵e̵r̵y̵a̲l̲l̲
+-/
+#guard_msgs in example (x : List Nat) := x.every fun _ => true
+#guard_msgs in example (x : List Nat) := x.all fun _ => true
+/--
+error: Invalid field `some`: The environment does not contain `List.some`, so it is not possible to project the field `some` from an expression
+  x
+of type `List Nat`
+
+Hint: Perhaps you meant `List.any` in place of `List.some`:
+  .s̵o̵m̵e̵a̲n̲y̲
+-/
+#guard_msgs in example (x : List Nat) := x.some fun _ => true
+#guard_msgs in example (x : List Nat) := x.all fun _ => true
+
+/--
+@ +1:17...22
+error: Invalid field `every`: The environment does not contain `List.every`, so it is not possible to project the field `every` from an expression
+  [1, 2, 3]
+of type `List ?m.10`
+
+Hint: Perhaps you meant `List.all` in place of `List.every`:
+  .e̵v̵e̵r̵y̵a̲l̲l̲
+-/
+#guard_msgs (positions := true) in
+#check [1, 2, 3].every
diff --git a/tests/lean/run/idSuggestStandalone.lean b/tests/lean/run/idSuggestStandalone.lean
index d046824007..b8b667eff2 100644
--- a/tests/lean/run/idSuggestStandalone.lean
+++ b/tests/lean/run/idSuggestStandalone.lean
@@ -1,3 +1,5 @@
+-- test suggest_for independently of any library annotations
+
 @[suggest_for String.test0 String.test1 String.test2]
 public def String.foo (x: String) := x.length + 1
 
@@ -37,6 +39,17 @@ Hint: Perhaps you meant `String.foo` in place of `String.test0`:
 #guard_msgs in
 #check String.test0
 
+/--
+error: Unknown constant `String.test0`
+
+Hint: Perhaps you meant `String.foo` in place of `String.test0`:
+  [apply] `String.foo`
+---
+info: fun x1 x2 x3 => sorry : (x1 : ?m.1) → (x2 : ?m.5 x1) → (x3 : ?m.6 x1 x2) → ?m.7 x1 x2 x3
+-/
+#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