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

[llllvvuu]

Closes #4375

The following example raises error: (kernel) declaration has free variables '_example':

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:

lean4/src/Lean/MetavarContext.lean

Line 567 in ea46bf2

instantiateExprMVars (f.betaRev args.reverse)

[nomeata]

Hello @llllvvuu and thanks for your first contribution to lean!

The src/Lean/Meta/ExprDefEq.lean file is very central to lean, and typically not the first module to touch when contributing to lean, and for the long-term maintainability of the code it is preferrable if such central modules are written by not too many people. Therefore it is possible and likely that the maintainers of this component will chose to implement their own fix, instead of using this one. Nevertheless your contribution is useful as it helps to understand the issue and points to one possible way to address it.

Good issue reports, including good minimized test cases, and contributions to less central components (error messages, leaf tactics, etc.) are a good way to build expertise, reputation and trust, before high-risk areas of the code.

[llllvvuu]

No worries, it's not a big deal to me whether this particular patch + test case is what gets merged. I'm glad if it's of some use.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-4410 has successfully built against this PR. (2024-06-09 11:16:58) View Log
• 🟡 Mathlib branch lean-pr-testing-4410 build against this PR was cancelled. (2024-06-10 03:22:37) View Log
• ✅ Mathlib branch lean-pr-testing-4410 has successfully built against this PR. (2024-06-10 04:27:22) View Log
• ✅ Mathlib branch lean-pr-testing-4410 has successfully built against this PR. (2024-06-10 06:58:22) View Log
• ✅ Mathlib branch lean-pr-testing-4410 has successfully built against this PR. (2024-06-10 08:10:38) View Log

[llllvvuu]

I just changed the fix/description, new one is just changing a flag. It still doesn't achieve not touching central modules, but I hope it sheds some more light on the issue (test case further minimized as well).

[leodemoura]

I just changed the fix/description, new one is just changing a flag. It still doesn't achieve not touching central modules, but I hope it sheds some more light on the issue (test case further minimized as well).

Looks good. We will merge it. Thanks!