edcef51434
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`.
113 lines
3.1 KiB
Text
113 lines
3.1 KiB
Text
/-!
|
||
# Invalid field notation on expressions of function type
|
||
|
||
Ensure we produce correct field notation error messages for expressions of function type and not the
|
||
fallback "type is not of the form `C ...`" message.
|
||
-/
|
||
|
||
set_option pp.mvars false
|
||
|
||
def foo : α → α := id
|
||
|
||
/--
|
||
@ +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`, so it is not possible to project the field `foo` from an expression
|
||
fun x => x
|
||
of type `?_ → ?_`
|
||
-/
|
||
#guard_msgs in
|
||
example (f : α → α) := (fun x => x).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
|
||
of type `α → α`
|
||
-/
|
||
#guard_msgs (positions := true) in
|
||
example (f : α → α) := f.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
|
||
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 `α` 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`, so it is not possible to project the field `foo` from an expression
|
||
f x
|
||
of type `α → α`
|
||
-/
|
||
#guard_msgs in
|
||
example (f : α → α → α) (x : α) := (f x).foo
|
||
|
||
/--
|
||
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.
|
||
-/
|
||
#guard_msgs in
|
||
example (x : α) := (foo x).foo
|
||
|
||
def foo.bar := 32
|
||
|
||
/--
|
||
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
|
||
of type `α → α`
|
||
-/
|
||
#guard_msgs in
|
||
example (foo : α → α) := foo.bar
|
||
|
||
/--
|
||
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
|
||
of type `?_ → ?_`
|
||
-/
|
||
#guard_msgs in
|
||
example := (let x := id; x).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
|
||
?_
|
||
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`, so it is not possible to project the field `foo` from an expression
|
||
n
|
||
of type `Nat`
|
||
-/
|
||
#guard_msgs in
|
||
example (n : Nat) := n.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
|
||
[]
|
||
of type `List Nat`
|
||
-/
|
||
#guard_msgs in
|
||
example (n : Nat) := (@List.nil Nat).foo
|
||
|
||
#check Nat.add.uncurry
|