(kernel) declaration has free variables

Stream: lean4

[Jovan Gerbscheid]

The following minimal example throws the error "(kernel) declaration has free variables"

def oops : IO Unit :=  do
  pure ()
  match some () with
  | some _ => do
    let pair := (1,2)
    let pair := match pair with | (a,b) => (a,b)
    let i := 0
    if h : i < pair.1 then
      let k := 0
  | _ => return

using set_option pp.all true, set_option trace.Elab.definition.body true, we can see where the free variable is coming from: it is the variable pair, which shows up in the definition of k, which is

@OfNat.ofNat.{0} Nat 0
  ((let i : Nat := @OfNat.ofNat.{0} Nat 0 (instOfNatNat 0);
  fun (h : @LT.lt.{0} Nat instLTNat i (@Prod.fst.{0, 0} Nat Nat _fvar.164)) => instOfNatNat 0)
  h)

[Joachim Breitner]

Could be one of these, typical symptom related to the old code generator: https://github.com/leanprover/lean4/issues?q=is%3Aopen+is%3Aissue+label%3A%22depends+on+new+code+generator%22

[Jovan Gerbscheid]

It's a problem with the elaboration, not the code generation. The unknown free variable is produced by the elaboration. And the same error shows up if we use noncomputable.

[Jovan Gerbscheid]

I would guess there must be an oversight with a let-variable being forgotten to be abstracted, because it secretly exists inside a metavariable assignment, and the metavariable isn't instantiated.

On the other hand, the definition of k looks really weird to me: it literally just reduces to @OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)

[Kyle Miller]

There's a chance it's related to lean4#5387. That's a concrete manifestation, but it can crop up when you have synthetic opaque metavariables (for example due to postponed elaboration problems, in this case the default instance for Nat at let k := 0) underneath let bindings.

I have been wondering if it has to do with some optimizations to let handling in isDefEq, but it's not something I've been able to figure out.

[Jovan Gerbscheid]

It does look like the same problem.

A slightly more minimal version:

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

Now, the problematic definition of k is:

@OfNat.ofNat Nat 0
  ((let i := ();
    fun (h : i = Prod.fst _fvar.148) => instOfNatNat 0)
    h)

Using set_option trace.Meta.isDefEq.assign true, we can see the following assignment is taking place:

[beforeMkLambda] ?m.271 [u, h] := instOfNatNat ?m.312
[checkTypes] ✅️ (?m.271 : (u : Unit) →
    let pair := ?m.268 u;
    let i := ();
    (h : i = ?m.270 u pair i) → OfNat (?m.267 u h) 0) := (fun (u : Unit) =>
    let i := ();
    fun (h : i = ?m.315 u pair i) => instOfNatNat (?m.313 u) : (u : Unit) →
    let i := ();
    i = ?m.315 u pair i → OfNat Nat (?m.313 u))

The variable pair is not bound in the assignment and also doesn't exist in the context of ?m.271.
So, this is an illegal assignment.

[Jovan Gerbscheid]

What is going wrong in the isDefEq algorithm is at the function processAssignment, in this part:

match (← checkAssignment mvarId args v) with
| none   => useFOApprox args
| some v => do
  trace[Meta.isDefEq.assign.beforeMkLambda] "{mvar} {args} := {v}"
  let some v ← mkLambdaFVarsWithLetDeps args v | return false

We use checkAssignment to make sure the assignment is legal, and then we change the assignment with mkLambdaFVarsWithLetDeps, which gives the possibility of now having an illegal assignment again.

[Jovan Gerbscheid]

What I don't understand however is why the "fix" at lean4#4410 doesn't help with my example. I would expect the useZeta := true in beta-reduction when instantiating mvars to get rid of the illegal fvar in my case.

[Jovan Gerbscheid]

Here is a minimal example that shows more clearly what the bug in isDefEq is:

-- (kernel) declaration has free variables '_example'
example : Unit :=
  let x : Nat → Unit := _
  let N := Nat;
  match (none : Option N) with
  | none => ()
  | some a =>
    have : x a = () := rfl
    ()

Here x is defined to be a metavariable, and x a =?= () causes it to be assigned to fun (a : N) => (). But N isn't in the context of x, so the free variable remains.

[Kim Morrison]

Could you open an issue with this example?

[Jovan Gerbscheid]

lean4#5939

[Jovan Gerbscheid]

(also written as a commend on the issue)
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.

[Jovan Gerbscheid]

I have figured out how to fix both bugs. The PR is at lean#5948.

At first, I fixed the fact that the lambda binder types weren't checked, which was what caused my issue. I did this by checking the types of the free variables, and then replacing the type in the local context with this possibly-updated (but def-eq) type. However, this didn't yet solve @Kyle Miller's issue.

In lean4#5387, he observed "Notice that after the := that a is not being closed over. In particular, the type of the binder h has a free.". This was fixed, but there was still a problem in the assignment, which is that

fun (h : a = Nat.zero) =>
      instFooFin (goal✝ ?m.2155) (goal✝ ?m.2156)
        (goal✝ ?m.2157)

can only be a constant function. In fact, this problem was already present in the trace line before it:

[beforeMkLambda] ?m.113 [h] := instFooFin ?m.127 ?m.128 ?m.129

where we can verify that the metavariables on the right aren't allowed to depend on h or a.

The function responsible for restricting the context of these metavariables is Lean.Meta.CheckAssignment.checkMVar, and what goes wrong is the following.

The metavariable that we are assigning has an empty context. So in particular, the assignment of it won't be allowed to depend on a. And since a appears in the type of h, it also won't be allowed to depend on h.

So, I also made a fix so that instead of removing h from the metavariable local context, it replaces the type of h with the checked type (in this case Nat.zero = Nat.zero instead of a = Nat.zero), which means that h can now safely exists in the localContext of the new metavariable.

[Young]

(deleted)