Unknown fvars when synthesizing mvars in hypothesis types

[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

Suppose a local declaration h has a type that involves ?m where ?m is a pending metavariable. If ?m can be solved using one of its local instances via Term.synthesizeSyntheticMVars, but the fvar of that local instance no longer available at h (and thus h's type is now not well-formed), then an unknown free variable appears in the type of h.

In the following example tactic test t via inst, where t is a term and inst is a local declaration, we elaborate t while postponing mvars that occur in it. We expect one of these mvars to be given by inst. We then create a hypothesis whose type is the type of t, and make the fvar of inst unavailable. We then synthesize that fvar with synthesizeSyntheticMVars. The tactic state contains an unknown free variable.

import Lean

open Lean Meta Elab Tactic in
elab "test " hWithPending:term " via " inst:ident : tactic => withMainContext do
  -- elaborate with mayPostpone := true to create pending mvars
  let hWithPending ← Tactic.elabTerm hWithPending none (mayPostpone := true)
  -- make the existing fvar unavailable
  -- (here we simply clear it, but this can also occur by unexpected means)
  let g ← (← getMainGoal).clear (← getFVarId inst)
  -- create the hypothesis that includes the pending mvar in its type
  let g ← g.assert `h (← inferType hWithPending) hWithPending
  let (_,g) ← g.intro1
  -- synthesize the pending mvar
  Term.synthesizeSyntheticMVars (mayPostpone := false)
  replaceMainGoal [g]

class Bar (α) where a : α

def f [Bar α] : α → α := id 

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

set_option pp.explicit true in
example : False := by
  let inst : Bar Nat := ⟨0⟩
  test foo 5 via inst
  /-
  h✝ : @Eq Nat 5 (@f Nat _uniq.84943 5)
  ⊢ False
  -/

Context

This originated as a bug in rw, which was brought up on Zulip and led to #2711. The issue there was Term.withSynthesize do ... in which we perform replaceLocalDecl; this tries to insert the new decl after the last fvar its type depends on so that it's well-formed, but since the mvar has not been synthesized yet, it cannot in principle know that it will involve this fvar without synthesizing the mvar itself. The issue is really that Term.withSynthesize can introduce ill-formedness of local declaration types in unexpected ways.

However, the rw case can be solved by merely moving replaceLocalDecl outside of Term.withSynthesize. The current issue is instead about the underlying mechanism. Currently, manipulating the local context while inside Term.withSynthesize can be a footgun (indeed, this footgun was present in rw already). Many tactics manipulate fvarids under the hood, and since Term.withSynthesize takes in any TacticM, debugging an unknown FVarId error caused by this phenomenon might be difficult. It is of course possible to say "just don't do that"—but fewer footguns is better than more rules about not using footguns. :)

Would it be possible or desirable to bulletproof mvar synthesis against this kind of thing? Or could something else be bulletproofed? For example, maybe the types of fvars in the local context should not contain pending mvars. Or maybe some other solution is available: it would be nice to get let inst := ...; inst in place of the unknown fvar.

Versions

Lean on web

Impact

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