Kernel error in list index notation

Stream: lean4

[Eric Wieser]

This is a regression, but I'm not entirely sure when it was introduced:

import Mathlib

open scoped ProbabilityTheory

theorem kernel_error
    (L : List ℝ) (hL : L.length = 2 ∧ ∀ i : Fin L.length, L[i] = 0) (i : ℕ) :
    L[i % 2] = 0 := hL.2 ⟨i%2, by simp [hL.1, Nat.mod_lt]⟩

#print axioms kernel_error -- no sorry

gives

(kernel) declaration has free variables 'kernel_error._proof_1'

[Eric Wieser]

It looks like the overloaded notation is being partially elaborated and some incomplete state is left behind when switching to the other elaborator

[Eric Wieser]

(deleted)

[Eric Wieser]

Mathlib-free:

structure Wrapper (α) where val : α

instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry

def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry

macro:max P:term noWs "[" term "]" : term => `(foo $P fun x => 0)

theorem kernel_error
    (L : List Nat) (hL : L.length = 2 ∧ ∀ i : Fin L.length, L[i] = 0) (i : Nat) :
    L[i % 2] = 0 := hL.2 ⟨i%2, by simp [hL.1, Nat.mod_lt]⟩

#print axioms kernel_error -- no sorry

[Notification Bot]

This topic was moved here from #mathlib4 > Kernel error in list index notation by Eric Wieser.

[Eric Wieser]

One thing that would probably help debug this is if the kernel could tell me what the statement of kernel_error._proof_1 is; it doesn't ever seem to make it into the environment

[Eric Wieser]

set_option trace.Kernel true provides [Kernel] ❌️ typechecking declarations [kernel_error._proof_1] where the name is not hoverable

[Eric Wieser]

@Sebastian Ullrich , setting set_option Elab.async false seems to make the kernel error go away

[Eric Wieser]

(I assume you're a sensible person to ping on async-related things?)

[Sebastian Ullrich]

Thanks, lean#10438

[Eric Wieser]

It seems that Elab.async is still misbehaving here; turning the setting off makes elaboration fail:

structure Wrapper (α) where val : α

instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry

def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry

macro:max P:term noWs "[" term "]" : term => `(foo $P fun x => 0)

set_option Elab.async false -- remove this and things pass
theorem kernel_error
    (L : List Nat) (hL : L.length = 2 ∧ ∀ i : Fin L.length, L[i] = 0) (i : Nat) :
    L[i % 2] = 0 := hL.2 ⟨i%2, by simp [hL.1, Nat.mod_lt]⟩
--  ^^^^^^^^ ambiguous notation here only with synchronous elaboration

[Eric Wieser]

Is there a future where Elab.async is removed and effectively always true, making the option increasingly vestigial? Or is it reasonable to expect behavior parity with the two setting values?

[Sebastian Ullrich]

In the above, it appears the behavior under Elab.async false is the incorrect one? I think it's fair to say that such bugs will be regarded as low priority, yes.

[Sebastian Ullrich]

Perhaps the option should be moved into the debug namespace to make that expectation explicit

[Eric Wieser]

I claim the true version is correct, since it's consistent with what happens when hL is simpler

[Eric Wieser]

Perhaps the syntax overloading of get_elem_tactic is to blame here?

[Sebastian Ullrich]

It could be something about how postponement of tactic mvars interacts with overloading

[Eric Wieser]

Regarding Elab.async; if the intended path is for this always to be true, and the default is false, I guess every custom frontend is expected to set this option?

[Sebastian Ullrich]

Good question. I would say that for simple custom frontends, it is unlikely they should run into such divergences and if that's not the case, we might want to fix them with slightly higher priority. For more ambitious frontends, it is likely worth the performance boost alone.

[Eric Wieser]

I mean, presumably even the simple frontends would crash if provided the code snippets above, which could otherwise appear without error in a regular Lean project built using the usual frontend

[Paul Lezeau]

In case it's helpful, here's a further minimisation of the issue:

structure Wrapper (α) where val : α

instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry

def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry

macro:max P:term noWs "|[" s:term "]|" : term => `(
  let h : $s ≤ List.length $P := by grind
  0)

macro:max P:term noWs "|[" term "]|" : term => `(foo $P fun x => 0)

set_option Elab.async false in -- remove this and things pass
theorem kernel_error
    (L : List Nat) (hL : L.length = 2 ∧ L|[0]| = 0) :
    L|[0]| = 0 := by sorry
--  ^^^^^^^^ ambiguous notation here only with synchronous elaboration

Interestingly, replacing grind by omega still results in an error, but replacing with simp fixes things.

[Eric Wieser]

(the above is for the lean nightly)

[Eric Wieser]

Here's some with fewer grinds (replacing the last part of Paul's):

set_option Elab.async false in -- remove this and things pass
theorem ambiguous_synchronously
    (L : List Nat) (hL : L.length = 2 ∧ let : True := (by trivial); True) : -- remove the `by` and things pass
    L|[0]| = 0 := by sorry

theorem ambiguous_synchronously
    (L : List Nat) (hL : L.length = 2 ∧ let : True := (by trivial); True) : -- remove the `by` and things pass
    set_option Elab.async false in -- remove this and things pass
    L|[0]| = 0 := by sorry

[Eric Wieser]

How can I get a list of all the grind components here in order to disable each one in turn to diagnose which one is causing the issue?

[Robin Arnez]

grind (config := { <trigger completion here> }) should show you every config (including all the modules you can disable)

[Robin Arnez]

Or grind (config := Lean.Grind.NoopConfig.toConfig {}) if you simply want to disable everything

[Kenny Lau]

is that documented anywhere?

[Robin Arnez]

Well, the first one is basically old config notation + regular structure autocompletion. The second one is just me happening to know it from the commit log (923c3d10a2457eb1413dc282b98cbdb50be5c5ee).

[Eric Wieser]

grind (config := Lean.Grind.NoopConfig.toConfig {}) seems sufficient to trigger the bug

[Eric Wieser]

Digging a little deeper, I think the cause is actually in the thread title; there is a kernel error occurring in the asynchronous code, which is being silenced by these lines. Should that catch be finer-grained?

[Eric Wieser]

Sebastian Ullrich said:

lean#10438

Which is to say; I think this is just masking the problem, and notation should never give a kernel error; and if it does, it shouldn't be hidden from the user.

[Eric Wieser]

It seems that mkAuxTheorem is being called with a synthetic opaque metavariable in the proof, which Closure.mkValueTypeClosure is incorrectly converting into an unbound free variable. I think this only happens when inside synthesizeSyntheticMVars (postpone := .no)

[Eric Wieser]

In particular, I think mkValueTypeClosure can't handle a metavariable whose type is itself a metavariable

[Eric Wieser]

#lean4 > kernel error caused by metavariables in mkAuxTheorem @ 💬 looks to be the cause, and async is just affecting when there are unassigned metavariables