"Unknown free variable" during isDefEq for delayed assignments when synthetic opaque assignable

Description

When synthetic opaque metavariables are assignable, it is possible to get an "unknown free variable" error from isDefEq.

Context

Zulip discussion where this was reported.

Steps to Reproduce

This reports "unknown free variable '_fvar.2067'" at refine:

example : (fun _ : Nat => 2) = (fun _ => 2) := by
  refine (?_ : (fun n : Nat => ?e) = _)
  rfl

Expected behavior: This succeeds, or at least gives a type mismatch error.

Versions

#eval Lean.versionString -- "4.6.0-rc1"

Additional Information

It appears that Lean.Meta.expandDelayedAssigned? is causing the type of a metavariable to leak an fvar from its local context. In mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs, the metavariable mvarIdPending might have a type that's not compatible with the current local context. In the above example, ?e has a type that depends on n.

For the test, it seems to be important that the type of the equality in the type ascription is a metavariable. Replacing the RHS _ of the equality with (_ : Nat → Nat) suppresses the issue.

Impact

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

Start by reproducing the example at refine, then inspect Lean.Meta.expandDelayedAssigned? and the mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs path described in the issue. Trace how the metavariable type can retain an out-of-scope local variable, and verify the fix with the supplied reproduction, where elaboration should succeed or report a type mismatch instead of an unknown free variable.