Metavariable assignment can fail if created underneath `let`

Description

This issue has an example of using default_instance to create a metavariable underneath let that later fails to be assigned.

Context

This was found while studying the fix in #4410 to issue #4375. It appears that #4410 might not be a fix of the root cause of that issue.

The comment in instantiateMVars corresponding to the fix seems incorrect, since it should never be the case that metavariables are assigned values containing free variables not in the context.

Steps to Reproduce

Consider the following code.

class Foo (a b : Nat) (h : a = b) (β : Nat → Type) where
  val : β a

@[default_instance]
instance (a b : Nat) (h : a = b) : Foo a b h Fin where
  val := sorry

example :=
  let a : Nat := Nat.zero
  fun (h : a = Nat.zero) => Foo.val h -- fails

example (a : Nat) :=
  fun (h : a = Nat.zero) => Foo.val h -- succeeds

Expected behavior: both examples succed.

Actual behavior: only the second example succeeds.

Versions

4.12.0, commit 445c8f2ee02ec75cdd8b2811bd56f4fb16adb655

macOS 15.0, m3

Additional Information

Setting set_option trace.Meta.isDefEq.assign true and set_option pp.funBinderTypes true shows the following failure

  [checkTypes] ❌️ (goal✝ ?m.2141 : let a := Nat.zero;
    (h : a = Nat.zero) →
      Foo a Nat.zero h
        ((goal✝ ?m.2138)
          h)) := (fun (h : a = Nat.zero) =>
      instFooFin (goal✝ ?m.2155) (goal✝ ?m.2156)
        (goal✝ ?m.2157) : a = Nat.zero → Foo (goal✝ ?m.2155) (goal✝ ?m.2156) (goal✝ ?m.2157) Fin)

Notice that after the := that a is not being closed over. In particular, the type of the binder h has a free.

One can verify that ?m.2141 has an empty local context. One way is to add the following delaborator to show the metavariable's local context on hover.

open Lean Elab PrettyPrinter Delaborator SubExpr in
@[delab mvar]
def delabMVar' : Delab := do
  let stx ← delabMVar
  let goal ← Meta.ppGoal (← getExpr).mvarId!
  let pos := Pos.pushType (← getPos)
  let info := Info.ofOmissionInfo <| ← mkOmissionInfo goal stx (← getExpr)
  modify fun s => { s with infos := s.infos.insert pos info }
  let stx := annotatePos pos stx
  `(goal $stx)
where
  mkOmissionInfo (goal : Format) (stx : Syntax) (e : Expr) : MetaM OmissionInfo := return {
    toTermInfo := {
        elaborator := `Delab,
        stx := stx,
        lctx := (← getLCtx),
        expectedType? := none,
        expr := e,
        isBinder := false
        : TermInfo
    }
    reason := (toString goal).replace "\n" "\n\n"
  }

The fix in #4410 is hiding this issue — in that context, checkAssign succeeds and ends up assigning a term with unused let terms, where inside these terms there are some out-of-context free variables. By making instantiateMVars do zeta reduction, these problematic terms are erased.

Impact

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

Reproduce the two examples and enable the mentioned Meta.isDefEq.assign and pp.funBinderTypes traces. Then inspect src/kernel/instantiate_mvars.cpp around the linked instantiateMVars comment and compare the failing metavariable context with the successful case. Done means both examples elaborate successfully without assigning terms containing out-of-context free variables.