acae2b44fd
This PR changes elaboration of structure instance notation when used in
patterns (e.g. `s matches { x := 1, y := [] }`) so that the structure's
default values are not used to elaborate the pattern. The motivation is
that default values frequently lead to surprisingly over-specific
patterns. It will now report "field missing" errors. The error can be
suppressed using `{ x := 1, .. }` ellipsis notation, which has the same
behavior as before. The pretty printer is also modified to stay in sync
with this feature. **Breaking change:** patterns using structure
instance notation may need missing fields or a `..` added, as
appropriate.
The rationale for the previous behavior is that with `..` you could
opt-in to not using default values, and now with this PR's behavior you
cannot opt-in. However, default values in structure instance patterns
are very likely to silently cause bugs. There are a couple examples in
this PR of unintentional default values in patterns in core Lean
(luckily these were not triggering bugs). With the new behavior, you can
now tell for sure whether every explicit field in a structure is being
matched explicitly or not, by the absence or presence of `..`.
Closes #10753
46 lines
928 B
Text
46 lines
928 B
Text
/-!
|
|
# Structure instance notation should not use defaults in patterns
|
|
|
|
https://github.com/leanprover/lean4/issues/10753
|
|
-/
|
|
|
|
/-!
|
|
In the following, it used to be that the `{ b := bv }` pattern was matching
|
|
`{ b := bv, a := 0 }`, which was confusing.
|
|
-/
|
|
|
|
structure Test where
|
|
a : Nat := 0
|
|
b : Nat
|
|
|
|
/-- error: Fields missing: `a` -/
|
|
#guard_msgs in
|
|
def test1 (t : Test) : Nat :=
|
|
match t with
|
|
| { b := bv } => bv
|
|
|
|
def test2 (t : Test) : Nat :=
|
|
match t with
|
|
| { b := bv, .. } => bv
|
|
|
|
/-- info: 2 -/
|
|
#guard_msgs in #eval test2 { a := 1, b := 2 }
|
|
|
|
/-!
|
|
Check pretty printing: in a pattern, we can't assume we can omit default values.
|
|
We can of course omit them outside of patterns.
|
|
-/
|
|
|
|
def test3 (t : Test) : Test :=
|
|
match t with
|
|
| { b := bv, a := 0 } => { b := bv }
|
|
| _ => t
|
|
|
|
/--
|
|
info: def test3 : Test → Test :=
|
|
fun t =>
|
|
match t with
|
|
| { a := 0, b := bv } => { b := bv }
|
|
| x => t
|
|
-/
|
|
#guard_msgs in #print test3
|