1437033e69
Type mismatch errors have a nice feature where expressions are annotated
with `pp.explicit` to expose differences via `isDefEq` checking.
However, this procedure has side effects since `isDefEq` may assign
metavariables. This PR wraps the procedure with `withoutModifyingState`
to prevent assignments from escaping.
Assignments can lead to confusing behavior. For example, in the
following a higher-order unification fails, but the difference-finding
procedure unifies metavariables in a naive way, producing a baffling
error message:
```lean
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀a, f (g a) = a) :
f (g n) = n := hfg n
example {g2 : ℕ → ℕ} (n2 : ℕ) : (λx => x * 2) (g2 n2) = n2 := by
with_reducible refine test n2 ?_
/-
type mismatch
test n2 ?m.648
has type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
but is expected to have type
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
-/
```
With the change, it now says `has type ?m.153 (?m.154 n2) = n2`.
Note: this uses `withoutModifyingState` instead of `withNewMCtxDepth`
because we want to know something about where `isDefEq` failed — we are
trying to simulate a very basic version of `isDefEq` for function
applications, and we want the state at the point of failure to know
which argument is "at fault".
65 lines
1.3 KiB
Text
65 lines
1.3 KiB
Text
/-!
|
|
# Tests of `addPPExplicitToExposeDiff`
|
|
-/
|
|
set_option pp.mvars false
|
|
|
|
/-!
|
|
Basic example.
|
|
-/
|
|
/--
|
|
error: type mismatch
|
|
rfl
|
|
has type
|
|
?_ = ?_ : Prop
|
|
but is expected to have type
|
|
1 = 2 : Prop
|
|
-/
|
|
#guard_msgs in example : 1 = 2 := by
|
|
exact rfl
|
|
|
|
|
|
/-!
|
|
Error message shouldn't fake a higher-order unification. This next one used to give
|
|
```
|
|
type mismatch
|
|
test n2 ?_
|
|
has type
|
|
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
|
|
but is expected to have type
|
|
(fun x ↦ x * 2) (g2 n2) = n2 : Prop
|
|
```
|
|
It now doesn't for the stronger reason that we don't let `addPPExplicitToExposeDiff` have side effects,
|
|
but still it avoids doing incorrect higher-order unifications in its reasoning.
|
|
-/
|
|
|
|
theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :
|
|
f (g n) = n := hfg n
|
|
|
|
/--
|
|
error: type mismatch
|
|
test n2 ?_
|
|
has type
|
|
?_ (?_ n2) = n2 : Prop
|
|
but is expected to have type
|
|
(fun x => x * 2) (g2 n2) = n2 : Prop
|
|
-/
|
|
#guard_msgs in
|
|
example {g2 : Nat → Nat} (n2 : Nat) : (fun x => x * 2) (g2 n2) = n2 := by
|
|
with_reducible refine test n2 ?_
|
|
|
|
|
|
/-!
|
|
Exposes an implicit argument because the explicit arguments can be unified.
|
|
-/
|
|
def f {a : Nat} (b : Nat) : Prop := a + b = 0
|
|
/--
|
|
error: type mismatch
|
|
sorry
|
|
has type
|
|
@f 0 ?_ : Prop
|
|
but is expected to have type
|
|
@f 1 2 : Prop
|
|
-/
|
|
#guard_msgs in
|
|
example : @f 1 2 := by
|
|
exact (sorry : @f 0 _)
|