update module test

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

src/Lean/ErrorExplanations/InvalidField.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rob Simmons
+-/
+module
+
+prelude
+public import Lean.ErrorExplanation
+meta import Lean.ErrorExplanation
+
+/--
+This error indicates that an expression containing a dot followed by an identifier was encountered,
+and that it wasn't possible to understand the identifier as a field.
+
+Lean's field notation is very powerful, but this can also make it confusing: the expression
+`color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution),
+it can be a reference to the [field of a structure](lean-manual://section/structure-fiels), and it
+and be a calling a function on the value `color` with
+[generalized field notation](lean-manual://section/generalized-field-notation).
+
+# Examples
+
+## Incorrect Field Name
+
+```lean broken
+#eval (4 + 2).suc
+```
+```output
+Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression
+  4 + 2
+of type `Nat`
+```
+```lean fixed
+#eval (4 + 1).succ
+```
+
+The simplest reason for an invalid field error is that the function being sought, like `Nat.suc`,
+does not exist.
+
+## Projecting from the Wrong Expression
+
+```lean broken
+#eval '>'.leftpad 10 ['a', 'b', 'c']
+```
+```output
+Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression
+  '>'
+of type `Char`
+```
+```lean fixed
+#eval ['a', 'b', 'c'].leftpad 10 '>'
+```
+
+The type of the expression before the dot entirely determines the function being called by the field
+projection. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized
+field notation is to have the list come before the dot.
+
+## Type is Not Specific
+
+```lean broken
+def double_plus_one {α} [Add α] (x : α) :=
+   (x + x).succ
+```
+```output
+Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
+  x + x
+has type `α` which does not have the necessary form.
+```
+```lean fixed
+def double_plus_one (x : Nat) :=
+   (x + x).succ
+```
+
+The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation
+cannot operate without knowing more about the actual type from which `succ` is being projected.
+
+## Insufficient Type Information
+
+```lean broken
+example := fun (n) => n.succ.succ
+```
+```output
+Invalid field notation: Type of
+  n
+is not known; cannot resolve field `succ`
+```
+```lean fixed
+example := fun (n : Nat) => n.succ.succ
+```
+
+Generalized field notation can only be used when it is possible to determine the type that is being
+projected. Type annotations may need to be added to make generalized field notation work.
+
+-/
+register_error_explanation lean.invalidField {
+  summary := "Dotted identifier notation used without ."
+  sinceVersion := "4.22.0"
+}

src/Lean/Message.lean

@@ -619,18 +619,18 @@ def indentExpr (e : Expr) : MessageData :=
   indentD e
 
 /--
-Returns the character length of the message when rendered.
+Returns the string-formatted version of MessageData.
 
 Note: this is a potentially expensive operation that is only relevant to message data that are
 actually rendered. Consider using this function in lazy message data to avoid unnecessary
 computation for messages that are not displayed.
 -/
-private def MessageData.formatLength (ctx : PPContext) (msg : MessageData) : BaseIO Nat := do
+private def MessageData.formatExpensively (ctx : PPContext) (msg : MessageData) : BaseIO String := do
   let { env, mctx, lctx, opts, currNamespace, openDecls } := ctx
   -- Simulate the naming context that will be added to the actual message
   let msg := MessageData.withNamingContext { currNamespace, openDecls } msg
   let fmt ← msg.format (some { env, mctx, lctx, opts })
-  return fmt.pretty.length
+  return fmt.pretty
 
 
 /--
@@ -645,7 +645,8 @@ def inlineExpr (e : Expr) (maxInlineLength := 30) : MessageData :=
   .lazy
     (fun ctx => do
       let msg := MessageData.ofExpr e
-      if (← msg.formatLength ctx) > maxInlineLength then
+      let render ← msg.formatExpensively ctx
+      if render.length > maxInlineLength || render.any (· == '\n') then
         return indentD msg ++ "\n"
       else
         return " `" ++ msg ++ "` ")
@@ -660,7 +661,8 @@ def inlineExprTrailing (e : Expr) (maxInlineLength := 30) : MessageData :=
   .lazy
     (fun ctx => do
       let msg := MessageData.ofExpr e
-      if (← msg.formatLength ctx) > maxInlineLength then
+      let render ← msg.formatExpensively ctx
+      if render.length > maxInlineLength || render.any (· == '\n') then
         return indentD msg
       else
         return " `" ++ msg ++ "`")

tests/lean/1038.lean.expected.out

@@ -1 +1 @@
-1038.lean:1:10-1:12: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`
+1038.lean:1:7-1:21: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`

tests/lean/346.lean.expected.out

@@ -1,5 +1,4 @@
-346.lean:10:15-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
-346.lean:13:4-13:5: error: Invalid field `z`: The environment does not contain `Nat.z`
+346.lean:10:6-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
+346.lean:13:4-13:5: error(lean.invalidField): Invalid field `z`: The environment does not contain `Nat.z`, so it is not possible to project the field `z` from an expression
   x
-has type
-  Nat
+of type `Nat`

tests/lean/funind_errors.lean.expected.out

@@ -1,5 +1,5 @@
 funind_errors.lean:4:7-4:26: error(lean.unknownIdentifier): Unknown identifier `doesNotExist.induct`
-funind_errors.lean:22:17-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
+funind_errors.lean:22:7-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
@@ -10,5 +10,5 @@ takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (mo
       have a := as[i];
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
-funind_errors.lean:38:14-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
-funind_errors.lean:45:13-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`
+funind_errors.lean:38:7-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
+funind_errors.lean:45:7-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`

tests/lean/run/3031.lean

@@ -66,10 +66,9 @@ def Common.String.parse (_ : String) : List Nat := []
 
 namespace ExOpen1
 /--
-error: Invalid field `parse`: The environment does not contain `String.parse`
+error: Invalid field `parse`: The environment does not contain `String.parse`, so it is not possible to project the field `parse` from an expression
   ""
-has type
-  String
+of type `String`
 -/
 #guard_msgs in #check "".parse
 section

tests/lean/run/9312.lean

@@ -10,10 +10,9 @@ no fields.
 structure MyEmpty where
 
 /--
-error: Invalid projection: Projections are not supported on this type because it has no fields
+error: Invalid projection: Projection operates on structure-like types with fields. The expression
   { }
-has type
-  MyEmpty
+has type `MyEmpty` which has no fields.
 -/
 #guard_msgs in
 #check (MyEmpty.mk).1
@@ -22,10 +21,9 @@ inductive T where
   | a
 
 /--
-error: Invalid projection: Projections are not supported on this type because it has no fields
+error: Invalid projection: Projection operates on structure-like types with fields. The expression
   T.a
-has type
-  T
+has type `T` which has no fields.
 -/
 #guard_msgs in
 #check (T.a).1

tests/lean/run/invalidProjection.lean

@@ -12,36 +12,46 @@ inductive P : Nat → n > 0 → Prop
 /--
 error: Invalid projection: Index `2` is invalid for this structure; the only valid index is 1
 
-Note: The expression `h2` has type `P m h'` which has only 1 field
+Note: The expression
+  h2
+has type `P m h'` which has only 1 field
 -/
 #guard_msgs in
 example (h1 : P n h) (h2 : P m h') := h1.1 = h2.2
 
+/--
+error: Invalid projection: Projection operates on types of the form `C ...` where C is a constant. The expression
+  Nat
+has type `Type` which does not have the necessary form.
+-/
+#guard_msgs in
+#check Nat.3
+
 /--
 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `x` has type `Nat × Nat × Nat` which has only 2 fields
+Note: The expression
+  x
+has type `Nat × Nat × Nat` which has only 2 fields
 
-Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+Hint: n-tuples in Lean are actually nested pairs. To access the third component of this tuple, use the projection `.2.2` instead:
   3̵2̲.̲2̲
 -/
 #guard_msgs in
 example (x : Nat × Nat × Nat) := x.3
 
 /--
-error: Invalid projection: Expected a value whose type is a structure
+error: Invalid projection: Projection operates on structure-like types with fields. The expression
   h
-has type
-  Nat
+has type `Nat` which does not have fields.
 -/
 #guard_msgs in
 example (h : Nat) := h.2
 
 /--
-error: Invalid projection: Projections cannot be used on functions
+error: Invalid projection: Projections cannot be used on functions, and
   f
-has type
-  Nat → Nat
+has function type `Nat → Nat`
 -/
 #guard_msgs in
 example (f : Nat → Nat) := f.1

tests/lean/run/invalidTupleProjHints.lean

@@ -9,9 +9,11 @@ def p : Nat × Nat × Nat := (3, 4, 5)
 /--
 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+Note: The expression
+  p
+has type `Nat × Nat × Nat` which has only 2 fields
 
-Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+Hint: n-tuples in Lean are actually nested pairs. To access the third component of this tuple, use the projection `.2.2` instead:
   3̵2̲.̲2̲
 -/
 #guard_msgs in
@@ -20,7 +22,9 @@ Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of
 /--
 error: Invalid projection: Index `17` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+Note: The expression
+  p
+has type `Nat × Nat × Nat` which has only 2 fields
 
 Hint: 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`.
 -/
@@ -30,9 +34,11 @@ Hint: n-tuples in Lean are actually nested pairs. For example, to access the "th
 /--
 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields
+Note: The expression
+  p
+has type `Nat × Nat × Nat` which has only 2 fields
 
-Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead:
+Hint: n-tuples in Lean are actually nested pairs. To access the third component of this tuple, use the projection `.2.2` instead:
   3̵2̲.̲2̲
 -/
 #guard_msgs in
@@ -48,9 +54,11 @@ def mp : MyProd := (1, 2, 3, 4, 5)
 /--
 error: Invalid projection: Index `4` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `mp` has type `Nat × Nat × Nat × Nat × Nat` which has only 2 fields
+Note: The expression
+  mp
+has type `Nat × Nat × Nat × Nat × Nat` which has only 2 fields
 
-Hint: n-tuples in Lean are actually nested pairs. To access the 4th component of this tuple, use the projection `.2.2.2.1` instead:
+Hint: n-tuples in Lean are actually nested pairs. To access the fourth component of this tuple, use the projection `.2.2.2.1` instead:
   4̵2̲.̲2̲.̲2̲.̲1̲
 -/
 #guard_msgs in
@@ -62,7 +70,9 @@ macro "illegally_project_from_a_tuple" : term => `((true, true, false).3)
 /--
 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2
 
-Note: The expression `(true, true, false)` has type `Bool × Bool × Bool` which has only 2 fields
+Note: The expression
+  (true, true, false)
+has type `Bool × Bool × Bool` which has only 2 fields
 
 Hint: 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`.
 -/

tests/lean/run/invalid_field_notation_function.lean

@@ -9,51 +9,59 @@ set_option pp.mvars false
 
 def foo : α → α := id
 
-/-- error: Unknown constant `foo.bar` -/
-#guard_msgs in
+/--
+@ +1:11...18
+error: Unknown constant `foo.bar`
+-/
+#guard_msgs (positions := true) in
 example := foo.bar
 
 /--
-error: Invalid field `foo`: The environment does not contain `Function.foo`
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
   fun x => x
-has type
-  ?_ → ?_
+of type `?_ → ?_`
 -/
 #guard_msgs in
 example (f : α → α) := (fun x => x).foo
 
 /--
-error: Invalid field `foo`: The environment does not contain `Function.foo`
+@ +1:25...28
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
   f
-has type
-  α → α
+of type `α → α`
 -/
-#guard_msgs in
+#guard_msgs (positions := true) in
 example (f : α → α) := f.foo
 
 /--
-error: Invalid field notation: Type is not of the form `C ...` where C is a constant
+@ +1:25...28
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
+  f
+of type `α → α`
+-/
+#guard_msgs (positions := true) in
+example (f : α → α) := f.foo.bar
+
+/--
+error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
   f x
-has type
-  α
+has type `α` which does not have the necessary form.
 -/
 #guard_msgs in
 example (f : α → α) (x : α) := (f x).foo
 
 /--
-error: Invalid field `foo`: The environment does not contain `Function.foo`
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
   f x
-has type
-  α → α
+of type `α → α`
 -/
 #guard_msgs in
 example (f : α → α → α) (x : α) := (f x).foo
 
 /--
-error: Invalid field notation: Type is not of the form `C ...` where C is a constant
+error: Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression
   foo x
-has type
-  α
+has type `α` which does not have the necessary form.
 -/
 #guard_msgs in
 example (x : α) := (foo x).foo
@@ -61,48 +69,45 @@ example (x : α) := (foo x).foo
 def foo.bar := 32
 
 /--
-error: Invalid field `bar`: The environment does not contain `Function.bar`
+error: Invalid field `bar`: The environment does not contain `Function.bar`, so it is not possible to project the field `bar` from an expression
   foo
-has type
-  α → α
+of type `α → α`
 -/
 #guard_msgs in
 example (foo : α → α) := foo.bar
 
 /--
-error: Invalid field `foo`: The environment does not contain `Function.foo`
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
   let x := id;
   x
-has type
-  ?_ → ?_
+of type `?_ → ?_`
 -/
 #guard_msgs in
 example := (let x := id; x).foo
 
 /--
-error: Invalid field `foo`: The environment does not contain `Function.foo`
+error: Invalid field `foo`: The environment does not contain `Function.foo`, so it is not possible to project the field `foo` from an expression
   ?_
-has type
-  α → α
+of type `α → α`
 -/
 #guard_msgs in
 example {α} := (by intro h; exact h : α → α).foo
 
 /-! Make sure we're not overzealously detecting fvars or implicitly-parameterized values in function position -/
 /--
-error: Invalid field `foo`: The environment does not contain `Nat.foo`
+error: Invalid field `foo`: The environment does not contain `Nat.foo`, so it is not possible to project the field `foo` from an expression
   n
-has type
-  Nat
+of type `Nat`
 -/
 #guard_msgs in
 example (n : Nat) := n.foo
 
 /--
-error: Invalid field `foo`: The environment does not contain `List.foo`
+error: Invalid field `foo`: The environment does not contain `List.foo`, so it is not possible to project the field `foo` from an expression
   []
-has type
-  List Nat
+of type `List Nat`
 -/
 #guard_msgs in
 example (n : Nat) := (@List.nil Nat).foo
+
+#check Nat.add.uncurry

tests/lean/run/issue10821.lean

@@ -44,10 +44,9 @@ example (n : Nat) : Nat :=
 
 /--
 @ +2:4...8
-error: Invalid field `incc`: The environment does not contain `Nat.incc`
+error: Invalid field `incc`: The environment does not contain `Nat.incc`, so it is not possible to project the field `incc` from an expression
   n
-has type
-  Nat
+of type `Nat`
 -/
 #guard_msgs (positions := true) in
 example (n : Nat) : Nat :=
@@ -55,10 +54,9 @@ example (n : Nat) : Nat :=
 
 /--
 @ +2:4...8
-error: Invalid field `incc`: The environment does not contain `Nat.incc`
+error: Invalid field `incc`: The environment does not contain `Nat.incc`, so it is not possible to project the field `incc` from an expression
   n
-has type
-  Nat
+of type `Nat`
 -/
 #guard_msgs (positions := true) in
 example (n : Nat) : Nat :=

tests/lean/run/noErrorUtil.lean

@@ -0,0 +1,15 @@
+import Lean
+
+-- Check that private functionality from Lean.Elab.ErrorUtils isn't exported
+
+/-- error: Unknown constant `Nat.toOrdinal` -/
+#guard_msgs in
+#check Nat.toOrdinal
+
+/--
+error: Invalid field `toOxford`: The environment does not contain `List.toOxford`, so it is not possible to project the field `toOxford` from an expression
+  ["a", "b", "c", "d"]
+of type `List String`
+-/
+#guard_msgs in
+#check ["a", "b", "c", "d"].toOxford

tests/pkg/module/Module/Basic.lean

@@ -487,10 +487,9 @@ public structure S
 def S.s := 1
 
 /--
-error: Invalid field `s`: The environment does not contain `S.s`
+error: Invalid field `s`: The environment does not contain `S.s`, so it is not possible to project the field `s` from an expression
   s
-has type
-  S
+of type `S`
 
 Note: A private declaration `S.s` (from the current module) exists but would need to be public to access here.
 -/

tests/pkg/module/Module/Imported.lean

@@ -90,19 +90,17 @@ example : P fexp := by dsimp only [fexp_trfl']; exact hP1
 example : t = t := by dsimp only [trfl]
 
 /--
-error: Invalid field `eq_def`: The environment does not contain `Nat.eq_def`
+error: Invalid field `eq_def`: The environment does not contain `Nat.eq_def`, so it is not possible to project the field `eq_def` from an expression
   f
-has type
-  Nat
+of type `Nat`
 -/
 #guard_msgs in
 #check f.eq_def
 
 /--
-error: Invalid field `eq_unfold`: The environment does not contain `Nat.eq_unfold`
+error: Invalid field `eq_unfold`: The environment does not contain `Nat.eq_unfold`, so it is not possible to project the field `eq_unfold` from an expression
   f
-has type
-  Nat
+of type `Nat`
 -/
 #guard_msgs in
 #check f.eq_unfold