unknown free variable introduced by rw ... at h

[thorimur]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

rw ... at h can introduce an unknown free variable in certain circumstances:

class Bar (α) where a : α

def f {α} [Bar α] (a : α) := a

def w (_ : Nat) : Prop := True

theorem foo {α} [Bar α] (a : α) : a = f a := sorry

set_option pp.explicit true in
example := by
  have h : w 5 := trivial
  let inst : Bar Nat := ⟨0⟩
  rw [foo 5] at h
  /-
  h✝: w 5
  h: w (@f Nat _uniq.124 5)
  inst: Bar Nat := @Bar.mk Nat 0
  ⊢ ?m.95
  -/

Context

rw ... at depends on replaceLocalDecl to replace h with its rewritten version. replaceLocalDecl uses an auxiliary function findMaxFVar to attempt to make sure that the type of the fvar it's inserting does not involve any fvars which come after the one it's inserting. It inserts the rewritten fvar after the latest fvar that the rewritten fvar's type depends on (after the original fvar itself). However, when findMaxFVar traverses the type, it's possible that it misses an occurrence of some fvar by passing over an uninstantiated metavariable that happens to be assigned to an expression which contains an fvar.

MVarId.rewrite does instantiateMVars in the expression eNew that gets passed to replaceLocalDecl, but does so too early—functions like postprocessAppMVars and isTypeCorrect can assign metavariables introduced by the theorem used to rewrite with. This includes synthesizing typeclass arguments.

EDIT: While this does seem to be an issue, it's not actually the issue in the minimized example above. The free variable above is in the context of a metavariable created during elaboration of foo 5, which means it doesn't get collected by rewrite at all. Strangely, it also doesn't seem to get assigned, despite being represented not as itself but as a free variable in its context. More investigation is required.

EDIT 2: This is occurring because the metavariable is postponed until the end of the do block, at which point it is synthesized by Term.withSynthesize. (Note the true argument to elabTerm.) Since it hasn't even been assigned yet, instantiateMVars has no effect in this case (but does in others), and replaceLocalDecl has no way of telling that the mvar will be assigned to an fvar that occurs later in the local context.

An easy fix here is just to perform replaceLocalDecl outside of Term.withSynthesize. For the general issue, see issue #2727.

Steps to reproduce

It's difficult to provide precise and exhaustive steps to reproduce this issue; broadly, whenever a theorem used by rw requires arguments, these become metavariables, which might get assigned during e.g. isTypeCorrect or postprocessAppMVars (as the typeclass argument in the given example does). If the assignment depends on a free variable which comes later in the local context than the re-insertion location of the rewritten fvar, and if that free variable appears nowhere else in the rewritten expression, the rewritten fvar will be inserted too early (i.e. before a free variable which its type depends on).

In the above example, this actually causes the FVarId of inst to change; what we see as _uniq.124 is the old FVarId of inst before the rewrite.

See Zulip.

Versions

Lean on web: 4.2.0-rc3

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[kim-em]

This can be closed now, right?

[thorimur]

This can be closed now, right?

Yep! The more general issue (which the fix to this issue works around) is preserved at #2727.