From 6a7bed94d35a0981a7e19bdf09903e15c62a3c3c Mon Sep 17 00:00:00 2001
From: L <git@llllvvuu.dev>
Date: Mon, 10 Jun 2024 12:02:27 -0700
Subject: [PATCH] fix: kernel exception from fvars left from `?m a b`
 instantiation (#4410)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Closes #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 (x._@.4375._hyg.13 : Nat) =>
    let b : Nat := Nat.zero
    fun (x._@.4375._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      | 8 ++++++--
 tests/lean/4375.lean              | 5 +++++
 tests/lean/4375.lean.expected.out | 0
 3 files changed, 11 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/4375.lean
 create mode 100644 tests/lean/4375.lean.expected.out

diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 711c59de5348..c6c743d8006a 100644
--- a/src/Lean/MetavarContext.lean
+++ b/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
diff --git a/tests/lean/4375.lean b/tests/lean/4375.lean
new file mode 100644
index 000000000000..16998f76b58f
--- /dev/null
+++ b/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)
diff --git a/tests/lean/4375.lean.expected.out b/tests/lean/4375.lean.expected.out
new file mode 100644
index 000000000000..e69de29bb2d1