feat: hint alternatives when field-projecting from an unknown type (#11482)

This PR gives suggestions based on the currently-available constants
when projecting from an unknown type.

## Example: single suggestion in namespace

This was the originally motivating example, as the string refactor led
to a number of anonymous-lambda-expressions with `Char` functions that
were no longer recognized as such.

```lean4
example := (·.isWhitespace)
```
Before:
```
Invalid field notation: Type of
  x✝
is not known; cannot resolve field `isWhitespace`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
```

## Example: single suggestion in namespace

```lean4
example := fun n => n.succ
```
Before:
```
Invalid field notation: Type of
  n
is not known; cannot resolve field `succ`
```
The message is unchanged, but this PR adds a hint:
```
Hint: Consider replacing the field projection with a call to one of the following:
  • `Fin.succ`
  • `Nat.succ`
  • `Std.PRange.succ`
```

Author: robsimmons

src/Lean/Elab/App.lean

@@ -1376,8 +1376,17 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       has function type{inlineExprTrailing eType}"
 
   | .mvar .., .fieldName _ fieldName _ _ =>
-    throwNamedError lean.invalidField m!"Invalid field notation: Type of{indentExpr e}\nis not \
-      known; cannot resolve field `{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
+      | #[] => 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:\
+          {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}"
+    throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \
+      known; cannot resolve field `{fieldName}`" ++ hint)
   | .mvar .., .fieldIdx _ i  =>
     throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
       projection `{i}`"

tests/lean/run/invalid_field_notation_mvar.lean

@@ -9,30 +9,48 @@ def Foo.f5 (f : Foo) : Nat := f.n
 error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `n`
+
+Hint: Consider replacing the field projection with a call to one of the following:
+  • `BitVec.DivModArgs.n`
+  • `Foo.n`
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `n`
+
+Hint: Consider replacing the field projection with a call to one of the following:
+  • `BitVec.DivModArgs.n`
+  • `Foo.n`
 ---
 error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `f1`
+
+Hint: Consider replacing the field projection `.f1` with a call to the function `Foo.f1`.
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `f2`
+
+Hint: Consider replacing the field projection `.f2` with a call to the function `Foo.f2`.
 ---
 error: Invalid field notation: Type of
   h
 is not known; cannot resolve field `f3`
+
+Hint: Consider replacing the field projection `.f3` with a call to the function `Foo.f3`.
 ---
 error: Invalid field notation: Type of
   f
 is not known; cannot resolve field `f4`
+
+Hint: Consider replacing the field projection `.f4` with a call to the function `Foo.f4`.
 ---
 error: Invalid field notation: Type of
   g
 is not known; cannot resolve field `f5`
+
+Hint: Consider replacing the field projection `.f5` with a call to the function `Foo.f5`.
 ---
 error: Invalid field notation: Type of
   h
@@ -51,3 +69,26 @@ is not known; cannot resolve field `foo`
 -/
 #guard_msgs in
 example := fun x => (id x).foo
+
+/--
+error: Invalid field notation: Type of
+  x✝
+is not known; cannot resolve field `isWhitespace`
+
+Hint: Consider replacing the field projection `.isWhitespace` with a call to the function `Char.isWhitespace`.
+-/
+#guard_msgs in
+example := (·.isWhitespace)
+
+/--
+error: Invalid field notation: Type of
+  x
+is not known; cannot resolve field `succ`
+
+Hint: Consider replacing the field projection with a call to one of the following:
+  • `Fin.succ`
+  • `Nat.succ`
+  • `Std.PRange.succ`
+-/
+#guard_msgs in
+example := fun x => x.succ