out of scope let-variable can appear in fun binder type of metavariable assignment

[JovanGerb]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following declaration raises an error.

-- (kernel) declaration has free variables '_example'
example : Unit :=
  let x : Nat → Unit := _
  let N := Nat;
  (fun a : N =>
    have : x a = () := rfl
    ()) Nat.zero

The unification that results from have : x a = () := rfl asigns the metavariable in x to fun (a : N) => (). However, N is not in the context of x, so the free variable remains in the definition of x.

Context

I ran into an error caused by this isDefEq bug while programming. I reported the problem on Zulip.

Steps to Reproduce

Use the above problematic declaration.

Expected behavior: [Clear and concise description of what you expect to happen]

The elaboration succeeds, and results in either

let x : Nat → Unit := let N := Nat; fun (a : N) => ()

or the reduced form

let x : Nat → Unit := fun (a : Nat) => ()

Actual behavior: [Clear and concise description of what actually happens]

We get the error (kernel) declaration has free variables '_example'

Versions

4.13.0

Additional Information

The minimized original example that I ran into is this:

-- (kernel) declaration has free variables 'oops'
def oops : IO Unit := do
 pure ()
 match some () with
 | some u => do
  let pair := match () with | _ => ((),())
  let i := ()
  if h : i = pair.1 then
   let k := 0
 | _ => return

The same underlying problem is responsible for #4375 and #5387. One problematic case was fixed by #4410.

Impact

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

[JovanGerb]

I tried to fix the bug, and came to the conclusion that I could fix it by modifying the function mkLambdaFVarsWithLetDeps. However, I have now found out that this function is already buggy. In its implementation it assumes that the free variables xs appear in the order in which they appear in the local context. So out of these two examples: the first succeeds, and the second fails with a unification error:

example : Unit :=
  let x : Nat → Nat → Nat → Unit := _
  (fun a : Nat =>
  let F := Nat
  (fun b c : F =>
  have : x a b c = () := rfl
  ())) 0 0 0

example : Unit :=
  let x : Nat → Nat → Nat → Unit := _
  (fun a : Nat =>
  let F := Nat
  (fun b c : F =>
  have : x a c b = () := rfl
  ())) 0 0 0

The reason is that in the assignmen of x a c b := (), it considers the variables between a and b, but c isn't there, so the resulting assignment is a function with 2 arguments.

[JovanGerb]

Here is another bug that comes from a bad variable management when assigning during unification:

-- (kernel) declaration has free variables '_example'
example : Unit :=
  let x : Nat → Nat → Nat := _
  (fun (a : Nat) (b : let _ := a; Nat) =>
    have : x b a = Nat.zero := rfl
    ()
    ) Nat.zero Nat.zero

I have a fix for all of the above bugs at #5948.