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".
56 lines
1.2 KiB
Text
56 lines
1.2 KiB
Text
import Lean.Elab.Command
|
|
|
|
set_option pp.mvars false
|
|
|
|
/--
|
|
error: application type mismatch
|
|
⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
|
|
argument
|
|
Fin.is_lt (?_ n)
|
|
has type
|
|
↑(?_ n) < ?_ n : Prop
|
|
but is expected to have type
|
|
↑(?_ n) < ↑(?_ n) : Prop
|
|
-/
|
|
#guard_msgs in
|
|
def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
|
|
|
|
/--
|
|
error: type mismatch
|
|
Fin.is_lt ?_
|
|
has type
|
|
↑?_ < ?_ : Prop
|
|
but is expected to have type
|
|
?_ < ?_ : Prop
|
|
---
|
|
error: unsolved goals
|
|
case a
|
|
⊢ Nat
|
|
|
|
this : ?_ < ?_
|
|
⊢ True
|
|
-/
|
|
#guard_msgs in
|
|
def test : True := by
|
|
have : ((?a : Nat) < ?a : Prop) := by
|
|
refine Fin.is_lt ?_
|
|
done
|
|
done
|
|
|
|
open Lean Meta
|
|
/--
|
|
info: Defeq?: false
|
|
---
|
|
info: fun x_0 x_1 => x_1
|
|
-/
|
|
#guard_msgs in
|
|
run_meta do
|
|
let mvarIdNat ← mkFreshExprMVar (.some (.const ``Nat []))
|
|
let mvarIdFin ← mkFreshExprMVar (.some (.app (.const `Fin []) mvarIdNat))
|
|
-- mvarIdNat.assign (.app (.const ``Fin.val []) mvaridFin))
|
|
let b ← isDefEq mvarIdNat (mkApp2 (.const ``Fin.val []) mvarIdNat mvarIdFin)
|
|
logInfo m!"Defeq?: {b}" -- prints true
|
|
-- Now mvaridNat occurs in its own type
|
|
-- This will stack overflow
|
|
let r ← abstractMVars mvarIdFin (levels := false)
|
|
logInfo m!"{r.expr}"
|