fix: kernel exception from fvars left from ?m a b instantiation (le…

…anprover#4410)

Closes leanprover#4375

The following example raises `error: (kernel) declaration has free
variables '_example'`:
```lean
example: Nat → Nat :=
  let a : Nat := Nat.zero
  fun (_ : Nat) =>
    let b : Nat := Nat.zero
    (fun (_ : a = b) => 0) (Eq.refl a)
```

During elaboration of `0`, `elabNumLit` creates a synthetic mvar
`?_uniq.16` which gets abstracted by `elabFun` to `?_uniq.16 :=
?_uniq.50 _uniq.6 _uniq.12`. The `isDefEq` to `instOfNatNat 0` results
in:
```
?_uniq.50 :=
  fun ([email protected]._hyg.13 : Nat) =>
    let b : Nat := Nat.zero
    fun ([email protected]._hyg.23 : Eq.{1} Nat _uniq.4 b) =>
      instOfNatNat 0
```

This has a free variable `_uniq.4` which was `a`.

When the application of `?_uniq.50` to `#[#2, #0]` is instantiated, the
`let b : Nat := Nat.zero` blocks the beta-reduction and `_uniq.4`
remains in the expression.

fix: add `(useZeta := true)` here:

https://github.com/leanprover/lean4/blob/ea46bf2839ad1c98d3a0c3e5caad8a81f812934c/src/Lean/MetavarContext.lean#L567

src/Lean/MetavarContext.lean

@@ -563,8 +563,12 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi
         let wasMVar := f.isMVar
         let f ← instantiateExprMVars f
         if wasMVar && f.isLambda then
-          /- Some of the arguments in args are irrelevant after we beta reduce. -/
-          instantiateExprMVars (f.betaRev args.reverse)
+          /- Some of the arguments in `args` are irrelevant after we beta
+             reduce. Also, it may be a bug to not instantiate them, since they
+             may depend on free variables that are not in the context (see
+             issue #4375). So we pass `useZeta := true` to ensure that they are
+             instantiated. -/
+          instantiateExprMVars (f.betaRev args.reverse (useZeta := true))
         else
           instArgs f
       match f with

tests/lean/4375.lean

@@ -0,0 +1,5 @@
+example: Nat → Nat :=
+  let a : Nat := Nat.zero
+  fun (_ : Nat) =>
+    let b : Nat := Nat.zero
+    (fun (_ : a = b) => 0) (Eq.refl a)