feat: improve error messages for invalid field access (#11456)

This PR refines several error error messages, mostly involving invalid
use of field notation, generalized field notation, and numeric
projection. Provides a new error explanation for field notation.

## Error message changes

In general:
- Uses a slightly different convention for expression-type pairs, where
the expression is always given `indentExpr` and the type is given
`inlineExpr` treatment. This is something of a workaround for the fact
that the `Format` type is awkward for embedding possibly-linebreaking
expressions in not-linebreaking text, which may be a separate issue
worth addressing.
- Tries to give slightly more "why" reasoning — the environment does not
contain `String.parse`, and _therefore you can't project `.parse` from a
`String`_.

Some specific examples:

### No such projection function
```lean4
#check "".parse
```
before:
```
error: Invalid field `parse`: The environment does not contain `String.parse`
  ""
has type
  String
```
after:
```
error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
  ""
of type `String`
```

### Type does not have the correct form
```lean4
example (x : α) := (foo x).foo
```
before:
```
error: Invalid field notation: Type is not of the form `C ...` where C is a constant
  foo x
has type
  α
```
after:
```
error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
  foo x
has type `α` which does not have the necessary form.
```

## Refactoring
Includes some refactoring changes as well:
- factors out multiple uses of number (1, 2, 3, 212, 222) to ordinal
("first", "second", "third", "212th", "222nd") conversion into
Lean.Elab.ErrorUtils
- significant refactoring of `resolveLValAux` in `Lean.Elab.App` — in
place of five helper functions, a special-case function case analysis,
and a case analysis on the projection type and structure, there's now a
single case analysis on the projection type and structure. This allows
several error messages to be more explicit (there were a number of cases
where index projection was being described as field projection in an
error messages) and gave the opportunity to slightly improve positining
for several errors: field *notation* errors should appear on `foo.bar`,
but field *projection* errors should appear only on the `bar` part of
`foo.bar`.

Author: robsimmons

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
+import all Lean.Elab.ErrorUtils
 
 public section
 
@@ -1252,15 +1253,6 @@ inductive LValResolution where
   The `baseName` is the base name of the type to search for in the parameter list. -/
   | localRec (baseName : Name) (fvar : Expr)
 
-private def mkLValError (e : Expr) (eType : Expr) (msg : MessageData) : MessageData :=
-  m!"{msg}{indentExpr e}\nhas type{indentExpr eType}"
-
-private def throwLValErrorAt (ref : Syntax) (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α :=
-  throwErrorAt ref (mkLValError e eType msg)
-
-private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermElabM α := do
-  throwLValErrorAt (← getRef) e eType msg
-
 /--
 `findMethod? S fName` tries the for each namespace `S'` in the resolution order for `S` to resolve the name `S'.fname`.
 If it resolves to `name`, returns `(S', name)`.
@@ -1291,9 +1283,6 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N
         return res
     return none
 
-private def throwInvalidFieldNotation (e eType : Expr) : TermElabM α :=
-  throwLValError e eType "Invalid field notation: Type is not of the form `C ...` where C is a constant"
-
 /--
 If it seems that the user may be attempting to project out the `n`th element of a tuple, or that the
 nesting behavior of n-ary products is otherwise relevant, generates a corresponding hint; otherwise,
@@ -1304,15 +1293,13 @@ private partial def mkTupleHint (eType : Expr) (idx : Nat) (ref : Syntax) : Term
   if arity > 1 then
     let numComps := arity + 1
     if idx ≤ numComps && ref.getHeadInfo matches .original .. then
-      let ordinalSuffix := match idx % 10 with
-        | 1 => "st" | 2 => "nd" | 3 => "rd" | _ => "th"
       let mut projComps := List.replicate (idx - 1) "2"
       if idx < numComps then projComps := projComps ++ ["1"]
       let proj := ".".intercalate projComps
       let sug := { suggestion := proj, span? := ref,
                    toCodeActionTitle? := some (s!"Change projection `{idx}` to `{·}`") }
       MessageData.hint m!"n-tuples in Lean are actually nested pairs. To access the \
-        {idx}{ordinalSuffix} component of this tuple, use the projection `.{proj}` instead:" #[sug]
+        {idx.toOrdinal} component of this tuple, use the projection `.{proj}` instead:" #[sug]
     else
       return MessageData.hint' m!"n-tuples in Lean are actually nested pairs. For example, to access the \
         \"third\" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`."
@@ -1325,45 +1312,15 @@ where
     | some (_, p2) => prodArity p2 + 1
 
 private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do
-  let throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
-      (declHint := Name.anonymous) : TermElabM α := do
-    let msg ←
-      -- ordering: put decl hint, if any, last
-      mkUnknownIdentifierMessage (declHint := declHint)
-        (mkLValError e eType
-          m!"Invalid field `{fieldName}`: The environment does not contain `{fullName}`")
-    -- HACK: Simulate previous embedding of tagged `mkUnknownIdentifierMessage`.
-    -- The "import unknown identifier" code action requires the tag to be present somewhere in the
-    -- message. But if it is at the root, the tag will also be shown to the user even though the
-    -- current help page does not address field notation, which should likely get its own help page
-    -- (if any).
-    throwErrorAt ref m!"{msg}{.nil}"
-  if eType.isForall then
-    match lval with
-    | LVal.fieldName ref fieldName suffix? _fullRef =>
-      let fullName := Name.str `Function fieldName
-      if (← getEnv).contains fullName then
-        return LValResolution.const `Function `Function fullName
-      else if suffix?.isNone || e.getAppFn.isFVar then
-        /- If there's no suffix, or the head is a function-typed free variable, this could only have
-           been a field in the `Function` namespace, so we needn't wait to check if this is actually
-           a constant. If `suffix?` is non-`none`, we prefer to throw the "unknown constant" error
-           (because of monad namespaces like `IO` and auxiliary declarations like `mutual_induct`) -/
-        throwInvalidFieldAt ref fieldName fullName
-    | .fieldIdx .. =>
-      throwLValError e eType "Invalid projection: Projections cannot be used on functions"
-  else if eType.getAppFn.isMVar then
-    let (kind, name) :=
-      match lval with
-      |  .fieldName _ fieldName _ _ => (m!"field notation", m!"field `{fieldName}`")
-      | .fieldIdx _ i => (m!"projection", m!"projection `{i}`")
-    throwError "Invalid {kind}: Type of{indentExpr e}\nis not known; cannot resolve {name}"
-  match eType.getAppFn.constName?, lval with
-  | some structName, LVal.fieldIdx ref idx =>
+  match eType.getAppFn, lval with
+  | .const structName _, LVal.fieldIdx ref idx =>
     if idx == 0 then
       throwError "Invalid projection: Index must be greater than 0"
     let env ← getEnv
-    let failK _ := throwLValError e eType "Invalid projection: Expected a value whose type is a structure"
+    let failK _ := throwError  "Invalid projection: Projection operates on structure-like types \
+      with fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not \
+      have fields."
+
     matchConstStructure eType.getAppFn failK fun _ _ ctorVal => do
       let numFields := ctorVal.numFields
       if idx - 1 < numFields then
@@ -1376,17 +1333,15 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
           return LValResolution.projIdx structName (idx - 1)
       else
         if numFields == 0 then
-          throwLValError e eType m!"Invalid projection: Projections are not supported on this type \
-            because it has no fields"
-        let (fields, bounds) := if numFields == 1 then
-          (m!"field", m!"the only valid index is 1")
-        else
-          (m!"fields", m!"it must be between 1 and {numFields}")
+          throwError  m!"Invalid projection: Projection operates on structure-like types with \
+            fields. The expression{indentExpr e}\nhas type{inlineExpr eType}which has no fields."
         let tupleHint ← mkTupleHint eType idx ref
-        throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}"
-          ++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}"
+        throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; \
+          {numFields.plural "the only valid index is 1" s!"it must be between 1 and {numFields}"}"
+          ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \
+          {numFields} field{numFields.plural}"
           ++ tupleHint
-  | some structName, LVal.fieldName ref fieldName _ _ => withRef ref do
+  | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do
     let env ← getEnv
     if isStructure env structName then
       if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then
@@ -1406,14 +1361,54 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
       -- Suggest a potential unreachable private name as hint. This does not cover structure
       -- inheritance, nor `import all`.
       (declHint := (mkPrivateName env structName).mkStr fieldName)
-  | none, LVal.fieldName ref _ (some suffix) _fullRef =>
-    -- This may be a function constant whose implicit arguments have already been filled in:
-    let c := e.getAppFn
-    if c.isConst then
-      throwUnknownConstantAt ref (c.constName! ++ suffix)
-    else
-      throwInvalidFieldNotation e eType
-  | _, _ => throwInvalidFieldNotation e eType
+
+  | .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 =>
+      throwUnknownConstant (c ++ suffix)
+    | _, _ =>
+      throwInvalidFieldAt ref fieldName fullName
+  | .forallE .., .fieldIdx .. =>
+    throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\
+      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}`"
+  | .mvar .., .fieldIdx _ i  =>
+    throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \
+      projection `{i}`"
+
+  | _, _ =>
+    match e.getAppFn, lval with
+    | Expr.const c _, .fieldName _ref _fieldName (some suffix) _fullRef =>
+      throwUnknownConstant (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 \
+        type{inlineExpr eType}which does not have the necessary form."
+    | _, .fieldIdx .. =>
+      throwError  m!"Invalid projection: Projection operates on types of the form `C ...` where C \
+        is a constant. The expression{indentExpr e}\nhas type{inlineExpr eType}which does not have \
+        the necessary form."
+
+where
+  throwInvalidFieldAt {α : Type} (ref : Syntax) (fieldName : String) (fullName : Name)
+      (declHint := Name.anonymous) : TermElabM α := do
+    let msg ←
+      -- ordering: put decl hint, if any, last
+      mkUnknownIdentifierMessage (declHint := declHint)
+        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}"
+    -- 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
+
 
 /-- whnfCore + implicit consumption.
    Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable. -/

src/Lean/Elab/ErrorUtils.lean

@@ -0,0 +1,66 @@
+/-
+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
+import Init.Notation
+import Init.Data.String
+
+/--
+Translate numbers (1, 2, 3, 212, 322 ...) to ordinals with appropriate English-language names for
+small ordinals (0 through 10 become "zeroth" through "tenth") and postfixes for other numbers
+(212 becomes "212th" and 1292 becomes "1292nd").
+-/
+def _root_.Nat.toOrdinal : Nat -> String
+  | 0 => "zeroth"
+  | 1 => "first"
+  | 2 => "second"
+  | 3 => "third"
+  | 4 => "fourth"
+  | 5 => "fifth"
+  | 6 => "sixth"
+  | 7 => "seventh"
+  | 8 => "eighth"
+  | 9 => "ninth"
+  | 10 => "tenth"
+  | n => if n % 100 > 10 && n % 100 < 20 then
+      s!"{n}th"
+    else if n % 10 == 2 then
+      s!"{n}nd"
+    else if n % 10 == 3 then
+      s!"{n}rd"
+    else
+      s!"{n}th"
+
+/--
+Make an oxford-comma-separated list of strings.
+
+ - `["eats"].toOxford == "eats"`
+ - `["eats", "shoots"].toOxford == "eats and shoots"`
+ - `["eats", "shoots", "leaves"] == "eats, shoots, and leaves"`
+-/
+def _root_.List.toOxford : List String -> String
+  | [] => ""
+  | [a] => a
+  | [a, b] => a ++ " and " ++ b
+  | [a, b, c] => a ++ ", " ++ b  ++ ", and " ++ c
+  | a :: as => a ++ ", " ++ toOxford as
+
+/--
+Give alternative forms of a string if the `count` is 1 or not.
+
+ - `(1).plural == ""`
+ - `(2).plural == "s"`
+ - `(1).plural "wug" == "wug"`
+ - `(2).plural "wug" == "wugs"`
+ - `(1).plural "it" "they" == "it"`
+ - `(2).plural "it" "they" == "they"`
+-/
+def _root_.Nat.plural (count : Nat) (singular : String := "") (plural : String := singular ++ "s") :=
+  if count = 1 then
+    singular
+  else
+    plural

src/Lean/Elab/SyntheticMVars.lean

@@ -12,6 +12,7 @@ public import Lean.Util.OccursCheck
 public import Lean.Elab.Tactic.Basic
 public import Lean.Meta.AbstractNestedProofs
 public import Init.Data.List.Sort.Basic
+import all Lean.Elab.ErrorUtils
 
 public section
 
@@ -209,33 +210,6 @@ private def synthesizeUsingDefault : TermElabM Bool := do
       return true
   return false
 
-/--
-Translate zero-based indexes (0, 1, 2, ...) to ordinals ("first", "second",
-"third", ...). Not appropriate for numbers that could conceivably be larger
-than 19 in real examples.
--/
-private def toOrdinalString : Nat -> String
-  | 0 => "first"
-  | 1 => "second"
-  | 2 => "third"
-  | 3 => "fourth"
-  | 4 => "fifth"
-  | n => s!"{n+1}th"
-
-/-- Make an oxford-comma-separated list of strings. -/
-private def toOxford : List String -> String
-  | [] => ""
-  | [a] => a
-  | [a, b] => a ++ " and " ++ b
-  | [a, b, c] => a ++ ", " ++ b  ++ ", and " ++ c
-  | a :: as => a ++ ", " ++ toOxford as
-
-/- Give alternative forms of a string if the `count` is 1 or not. -/
-private def _root_.Nat.plural (count : Nat) (singular : String) (plural : String) :=
-  if count = 1 then
-    singular
-  else
-    plural
 
 def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option MessageData) := do
 
@@ -296,7 +270,7 @@ def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option M
     if args.length = 1 then
       "the type argument"
     else
-      s!"the {toOxford (stuckArguments.toList.map toOrdinalString)} type {nStuck.plural "argument" "arguments"}"
+      s!"the {(stuckArguments.toList.map (·.succ.toOrdinal)).toOxford} type {nStuck.plural "argument" "arguments"}"
 
   return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {nStuck.plural "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass."
     ++ .hint' m!"Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `{MessageData.ofConstName ``Nat}`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.")

src/Lean/ErrorExplanations.lean

@@ -14,6 +14,7 @@ public import Lean.ErrorExplanations.InductiveParamMissing
 public import Lean.ErrorExplanations.InferBinderTypeFailed
 public import Lean.ErrorExplanations.InferDefTypeFailed
 public import Lean.ErrorExplanations.InvalidDottedIdent
+public import Lean.ErrorExplanations.InvalidField
 public import Lean.ErrorExplanations.ProjNonPropFromProp
 public import Lean.ErrorExplanations.PropRecLargeElim
 public import Lean.ErrorExplanations.RedundantMatchAlt