feat: improve error messages for invalid field access #11456
Merged
+351
−183
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…ess error explination (draft)
robsimmons
changed the title
robsimmons
changed the title
robsimmons
commented
Dec 2, 2025
Contributor
Author
robsimmons
left a comment
robsimmons
left a comment
There was a problem hiding this comment.
@Kha can I request a spot-check on my use of the module system for non-exported error functionality here?
Comment on lines
+6
to
+17
| 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 |
Contributor
Author
There was a problem hiding this comment.
Lean.Elab.ErrorUtils has no public sections, so all its definitions default private
| public import Lean.Meta.Tactic.ElimInfo | ||
| public import Lean.Elab.Binders | ||
| public import Lean.Elab.RecAppSyntax | ||
| import all Lean.Elab.ErrorUtils |
Contributor
Author
There was a problem hiding this comment.
I'm using the error utils with import all
Comment on lines
+5
to
+7
| /-- error: Unknown constant `Nat.toOrdinal` -/ | ||
| #guard_msgs in | ||
| #check Nat.toOrdinal |
Contributor
Author
There was a problem hiding this comment.
...and then I'm checking after the fact that I didn't accidentally add them to the Lean import
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
Contributor
Author
|
Discussed the question I had for @Kha synchronously — the answer is that it's probably not a great idea in general to be doing the namespace polluting additions I'm doing in the current ErrorUtils, if I'm going to do them the private export + |
alok
reviewed
Dec 2, 2025
| 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 |
Contributor
There was a problem hiding this comment.
typo in url? structure-fiel(d)s
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
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`.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
indentExprand the type is giveninlineExprtreatment. This is something of a workaround for the fact that theFormattype is awkward for embedding possibly-linebreaking expressions in not-linebreaking text, which may be a separate issue worth addressing.String.parse, and therefore you can't project.parsefrom aString.Some specific examples:
No such projection function
before:
after:
Type does not have the correct form
before:
after:
Refactoring
Includes some refactoring changes as well:
resolveLValAuxinLean.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 onfoo.bar, but field projection errors should appear only on thebarpart offoo.bar.