feat: suggestions for ambiguous dotted identifiers (#11555)

This PR scans the environment for viable replacements for a dotted
identifier (like `.zero`) and suggests concrete alternatives as
replacements.

## Example

```
#example .zero
```

Error message:
```
Invalid dotted identifier notation: The expected type of `.cons` could not be determined
```

Additional hint added by this PR:
```
Hint: Using one of these would be unambiguous:
  [apply] `BitVec.cons`
  [apply] `List.cons`
  [apply] `List.Lex.cons`
  [apply] `List.Pairwise.cons`
  [apply] `List.Perm.cons`
  [apply] `List.Sublist.cons`
  [apply] `List.Lex.below.cons`
  [apply] `List.Pairwise.below.cons`
  [apply] `List.Perm.below.cons`
  [apply] `List.Sublist.below.cons`
  [apply] `Lean.Grind.AC.Seq.cons`
```

## Additional changes

This PR also brings several related error message descriptions and code
actions more in line with each other, changing several "Suggested
replacement: " code actions to the more common "Change to " wording, and
sorts suggestions obtained from searching the context by the default
sort for Names (which prefers names with fewer segments).

Author: robsimmons

src/Lean/Elab/App.lean

@@ -1314,6 +1314,16 @@ where
     | none => 0
     | some (_, p2) => prodArity p2 + 1
 
+/--
+For a fieldname `fieldName`, locate all the environment constants with that name
+-/
+private def reverseFieldLookup (env : Environment) (fieldName : String) :=
+  env.constants.fold (init := #[]) (fun accum name _ =>
+      match name with
+      | .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
+      | _ => accum)
+    |>.qsort (lt := Name.lt)
+
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
   match eType.getAppFn, lval with
   | .const structName _, LVal.fieldIdx ref idx =>
@@ -1379,11 +1389,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       has function type{inlineExprTrailing eType}"
 
   | .mvar .., .fieldName _ fieldName _ _ =>
-    let possibleConstants := (← getEnv).constants.fold (fun accum name _ =>
-      match name with
-      | .str _ s => if s = fieldName && !name.isInternal then accum.push name else accum
-      | _ => accum) #[]
-    let hint := match possibleConstants with
+    let hint := match reverseFieldLookup (← getEnv) fieldName with
       | #[] => MessageData.nil
       | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`."
       | opts => .hint' m!"Consider replacing the field projection with a call to one of the following:\
@@ -1428,16 +1434,15 @@ where
           (suggestions.map fun suggestion => {
             preInfo? := .some s!"{e}.",
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Suggested replacement: {e}.{·}"),
+            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
             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!"Suggested replacement: {e}.{·}"),
-            diffGranularity := .all,
+            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
             messageData? := .some m!"`{.ofConstName suggestion}`: {e}.{suggestion.getString!}",
           })
 
@@ -1765,8 +1770,17 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedT
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
-  throwNoExpectedType :=
-    throwNamedError lean.invalidDottedIdent "Invalid dotted identifier notation: The expected type of `.{id}` could not be determined"
+  throwNoExpectedType := do
+    let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with
+      | #[] => pure MessageData.nil
+      | suggestions =>
+        let oneOfThese := if h : suggestions.size = 1 then m!"`{.ofConstName suggestions[0]}" else m!"one of these"
+        m!"Using {oneOfThese} would be unambiguous:".hint (suggestions.map fun suggestion => {
+          suggestion := mkIdent suggestion
+          toCodeActionTitle? := .some (s!"Change to {·}")
+          messageData? := .some m!"`{.ofConstName suggestion}`",
+        })
+    throwNamedError lean.invalidDottedIdent (m!"Invalid dotted identifier notation: The expected type of `.{id}` could not be determined" ++ hint)
   /-- A weak version of forallTelescopeReducing that only uses whnfCore, to avoid unfolding definitions except by `unfoldDefinition?` below. -/
   withForallBody {α} (type : Expr) (k : Expr → TermElabM α) : TermElabM α := do
     let type ← whnfCoreUnfoldingAnnotations type

src/Lean/Elab/PatternVar.lean

@@ -67,35 +67,13 @@ private def throwCtorExpected {α} (ident : Option Syntax) : M α := do
 
   if candidates.size = 0 then
     throwError message
-  else if h : candidates.size = 1 then
-    throwError message ++ .hint' m!"`{candidates[0]}` is similar"
-  else
-    let sorted := candidates.qsort (·.toString < ·.toString)
-    let diff :=
-      if candidates.size > 10 then [m!" (or {candidates.size - 10} others)"]
-      else []
-    let suggestions : MessageData := .group <|
-      .joinSep ((sorted.extract 0 10 |>.toList |>.map (showName env)) ++ diff)
-        ("," ++ Format.line)
-    throwError message ++ .group (.hint' ("These are similar:" ++ .nestD (Format.line ++ suggestions)))
-where
-  -- Create some `MessageData` for a name that shows it without an `@`, but with the metadata that
-  -- makes infoview hovers and the like work. This technique only works because the names are known
-  -- to be global constants, so we don't need the local context.
-  showName (env : Environment) (n : Name) : MessageData :=
-    let params :=
-      env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-    .ofFormatWithInfos {
-      fmt := "'" ++ .tag 0 (format n) ++ "'",
-      infos :=
-        .ofList [(0, .ofTermInfo {
-          lctx := .empty,
-          expr := .const n params,
-          stx := .ident .none (toString n).toRawSubstring n [.decl n []],
-          elaborator := `Delab,
-          expectedType? := none
-        })] _
-    }
+  let oneOfThese := if h : candidates.size = 1 then m!"`{candidates[0]}`" else m!"one of these"
+  let hint ← m!"Using {oneOfThese} would be valid:".hint (ref? := idStx) (candidates.map fun candidate => {
+    suggestion := mkIdent candidate
+    toCodeActionTitle? := .some (s!"Change to {·}")
+    messageData? := .some m!"`{.ofConstName candidate}`",
+  })
+  throwError message ++ hint
 
 private def throwInvalidPattern {α} : M α :=
   throwError "Invalid pattern"

src/Lean/IdentifierSuggestion.lean

@@ -90,8 +90,7 @@ public def throwUnknownConstantWithSuggestions (constName : Name) : CoreM α :=
         let modified := modifySuggestion suggestion
         {
           suggestion := s!"{modified}",
-          toCodeActionTitle? := .some (s!"Suggested replacement: {·}"),
-          diffGranularity := .all,
-          -- messageData? := .some m!"replace `{.ofName rawId}` with `{.ofName modified}`",
+          toCodeActionTitle? := .some (s!"Change to {·}"),
+          messageData? := .some m!"`{.ofConstName suggestion}`",
         }) ref
   throwUnknownIdentifierAt (declHint := constName) ref (m!"Unknown constant `{.ofConstName constName}`" ++ hint)

tests/lean/10488.lean

@@ -51,3 +51,10 @@ structure Foo where
 def bar : Foo := {}
 #check bar.x.2.snd
 #eval { bar with x.2.snd := 1 }
+
+inductive Nope where
+  | succ : Nope -> Nope -> Nope
+  | leaf : Nope
+
+example := (match · with
+  | succ x y => 4)

tests/lean/10488.lean.expected.out

@@ -30,6 +30,12 @@ foo 31 : ?m → Unit
 foo 31 : ?m → Unit
 10488.lean:33:15-33:16: error: unexpected token '('; expected command
 10488.lean:34:14-34:19: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.succ` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `succ`
+  [apply] `Fin.succ`
+  [apply] `Nat.succ`
+  [apply] `Std.PRange.succ`
 foo 31 sorry : Unit
 foo 31. succ : Unit
 11 : Nat
@@ -41,3 +47,8 @@ foo 31. succ : Unit
 10488.lean:41:13-41:17: error: unexpected identifier; expected ')', ',' or ':'
 bar.x.snd.snd : Nat
 { x := (2, 4, 1) }
+10488.lean:60:4-60:12: error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
+
+Hint: Using one of these would be valid:
+  [apply] `Nat.succ`
+  [apply] `Nope.succ`

tests/lean/1719.lean.expected.out

@@ -1 +1,8 @@
 1719.lean:2:8-2:12: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.inl` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `Or.inl`
+  [apply] `PSum.inl`
+  [apply] `Sum.inl`
+  [apply] `Sum.Lex.inl`
+  [apply] `Sum.LiftRel.inl`

tests/lean/coeM.lean

@@ -26,6 +26,10 @@ It was checking that `Eq (some true)` and `Eq _` were defeq monads. The defeq ch
 -/
 /--
 error: Invalid dotted identifier notation: The expected type of `.some` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `some`
+  [apply] `Option.Rel.some`
 -/
 #guard_msgs in
 example : some true = (some true).map id := by

tests/lean/emptyTypeAscription.lean.expected.out

@@ -1,5 +1,25 @@
 emptyTypeAscription.lean:3:19-3:24: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.zero` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `BitVec.zero`
+  [apply] `Dyadic.zero`
+  [apply] `Nat.zero`
+  [apply] `Vector.zero`
+  [apply] `Zero.zero`
+  [apply] `System.Uri.UriEscape.zero`
+  [apply] `Lean.Grind.IntModule.OfNatModule.zero`
+  [apply] `Lean.Grind.Linarith.Expr.zero`
 emptyTypeAscription.lean:4:29-4:34: error(lean.invalidDottedIdent): Invalid dotted identifier notation: The expected type of `.zero` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `BitVec.zero`
+  [apply] `Dyadic.zero`
+  [apply] `Nat.zero`
+  [apply] `Vector.zero`
+  [apply] `Zero.zero`
+  [apply] `System.Uri.UriEscape.zero`
+  [apply] `Lean.Grind.IntModule.OfNatModule.zero`
+  [apply] `Lean.Grind.Linarith.Expr.zero`
 emptyTypeAscription.lean:9:63-9:70: error: invalid `▸` notation, expected result type of cast is 
   w = add x y
 however, the equality 

tests/lean/run/change.lean

@@ -139,6 +139,10 @@ Fails, type hint can't hint enough since `.some _` is postponed.
 -/
 /--
 error: Invalid dotted identifier notation: The expected type of `.some` could not be determined
+
+Hint: Using one of these would be unambiguous:
+  [apply] `some`
+  [apply] `Option.Rel.some`
 -/
 #guard_msgs in example : some true = (some true).map id := by
   change _ = .some _

tests/lean/run/coinductive_syntax.lean

@@ -24,12 +24,12 @@ theorem casesOnTest (r : α → α → Prop) (a : α) : infSeq α r a → ∃ b,
 /--
 error: Invalid pattern: Expected a constructor or constant marked with `[match_pattern]`
 
-Hint: These are similar:
-  'Lean.Order.iterates.below.step',
-  'Lean.Order.iterates.step',
-  'Nat.le.below.step',
-  'Nat.le.step',
-  'infSeq._functor.step'
+Hint: Using one of these would be valid:
+  [apply] `Nat.le.step`
+  [apply] `Nat.le.below.step`
+  [apply] `Lean.Order.iterates.below.step`
+  [apply] `Lean.Order.iterates.step`
+  [apply] `infSeq._functor.step`
 ---
 error: Case tag `rhs` not found.