Metavariable assignment can fail if created underneath let

[kmill]

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 445c8f2

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.

[kmill]

Here's what appears to be another manifestation of this issue. The elaborated term contains a free variable at 0 in let k := 0.

def oops : IO Unit :=  do
  pure ()
  match some () with
  | some _ => do
    let pair := (1,2)
    let pair := match pair with | (a,b) => (a,b)
    let i := 0
    if h : i < pair.1 then
      let k := 0
  | _ => return

The elaborated value of k is

@OfNat.ofNat.{0} Nat 0
  ((let i : Nat := @OfNat.ofNat.{0} Nat 0 (instOfNatNat 0);
  fun (h : @LT.lt.{0} Nat instLTNat i (@Prod.fst.{0, 0} Nat Nat _fvar.164)) => instOfNatNat 0)
  h)

(Reported by @JovanGerb on Zulip)