46 lines
1.8 KiB
Text
46 lines
1.8 KiB
Text
/-!
|
||
# Ensure that `rw ... at h` does not create unknown free variables (issue #2711)
|
||
|
||
## Context
|
||
|
||
`rw ... at h` elaborates its rules with postponed metavariables, which, prior to this test, were
|
||
synthesized after the bulk of the tactic has taken place by `Term.withSynthesize`. Specifically,
|
||
these mvars were synthesized after `replaceLocalDecl` has executed.
|
||
|
||
`replaceLocalDecl` needs to be sure it's not inserting the new, rewritten hypothesis before any
|
||
fvars which the type of that hypothesis now depends on. For example, if the type of `h` got
|
||
rewritten to `f i` where `i` was a local declaration occurring after `h`, `replaceLocalDecl` should
|
||
insert the rewritten `h` after `i`.
|
||
|
||
To ensure this, it traverses the type looking for fvars to find the latest-occurring one. However,
|
||
the pending mvars it might encounter in the type have not even been assigned yet, and so
|
||
`replaceLocalDecl` will not find any fvars when it traverses over them. `Term.withSynthesize` might
|
||
nevertheless assign these mvars to later-occurring fvars afterwards. As such, the type of the
|
||
rewritten hypothesis might become ill-formed at the place `replaceLocalDecl` inserts it once the
|
||
pending mvars are assigned, as it might now include unknown `FVarId`s (the `FVarId`s following the
|
||
insertion spot will have been changed by the insertion).
|
||
|
||
This test reflects the choice to synthesize the pending mvars before `replaceLocalDecl` is
|
||
executed, thus avoiding this issue.
|
||
-/
|
||
|
||
class Bar (α) where a : α
|
||
|
||
def f {α} [Bar α] (a : α) := a
|
||
|
||
def w (_ : α) : Prop := True
|
||
|
||
theorem foo {a : α} [Bar α] : w a = w (f a) := rfl
|
||
|
||
set_option pp.explicit true in
|
||
example : True := by
|
||
have h : w 5 := trivial
|
||
let inst : Bar Nat := ⟨0⟩
|
||
rw [foo] at h
|
||
-- Previous goal state:
|
||
/-
|
||
h✝ : @w Nat 5
|
||
h : @w Nat (@f Nat _uniq.158 5)
|
||
inst : Bar Nat := @Bar.mk Nat 0
|
||
⊢ True
|
||
-/
|