Tricky `(kernel) deep recursion detected` error

Stream: lean4

[Alex Keizer]

I've been trying to debug a proof which gives a (kernel) deep recursion detected error. I've included a self-contained example below, however it seems to be resisting further attempt at minimization. I've tried removing several seemingly unrelated complexities from the example, all of which then make the error disappear without a giving me a clear intuition as to why.

Does anyone have a suggestion for what could cause this behaviour?

/-! # Preliminary -/

/--
`PoisonOr` is a simple wrapper around `Option`
-/
structure PoisonOr (α : Type) where
  toOption : Option α

namespace PoisonOr

def value : α → PoisonOr α := (⟨some ·⟩)

instance : Bind PoisonOr where
  bind := fun a f => match a with
    | ⟨none⟩    => ⟨none⟩
    | ⟨some a⟩  => f a

theorem bind_assoc (x : PoisonOr α) (f : α → PoisonOr β) (g : β → PoisonOr γ) :
    x >>= f >>= g = x >>= fun x => f x >>= g := by
  rcases x with (_|_) <;> rfl

end PoisonOr

/-! # MWE -/

def BitVec.umulOverflow' {w : Nat} (x y : BitVec w) : Prop :=
  x.toNat * y.toNat ≥ 0
  -- -----^
  -- Making this `+` has no effect, the error remains.
  --
  -- However, replacing `x.toNat` with a constant (even if large), does make the
  --   error disappear
  --
  -- Also note that the rhs was originally `2 ^ w`, but I've replaced it with
  -- `0` to rule out `2 ^ w` being computed. This had no effect on the error.

instance : DecidableRel (@BitVec.umulOverflow' w) := by
  unfold BitVec.umulOverflow';
  -- If we `sorry` out this instance, the error disappears
  -- sorry
  infer_instance


/-
The following gives the error:

  (kernel) deep recursion detected

-/
theorem mwe (x' : BitVec 32) :
    (do
      let _z ←
        (do
          let y' ← PoisonOr.value 0#32
          -- ----- ^^^^^^^^^^^^^^
          -- Replacing the `PoisonOr` wrapper with `Option` (in the whole MWE)
          -- makes the error disappear
          --
          if x'.umulOverflow' (65537#_) then
          -- ----------------- ^^^^^^^
          -- Making this constant smaller, or replacing it with a variable,
          -- makes the error disappear
          --
            PoisonOr.value 0#32
          else
            PoisonOr.value 0#32)
      PoisonOr.value 0) = PoisonOr.value 0 := by
  -- Running `simp only [ite_self]` first makes the error disappear
  --   (but is not applicable in my actual scenario, as the branches of the real
  --    code aren't the same)
  -- Similarly, rewriting the statement to not have the if-then-else also
  -- makes the error disappear.

  rw [PoisonOr.bind_assoc]
  -- ^^ This rewrite is what seems to trigger the recursion, removing it
  --    makes the error disappear.
  sorry

[Matthew Ballard]

Can you run it through lean4lean?

[Alex Keizer]

How would I do that? I've built lean4lean locally, and am trying to get it to check this MWE using

 lake env $lean4lean --fresh MWE

But lean4lean just complains that it can't find oleans (uncaught exception: Could not find any oleans for: MWE).

Presumably there's no oleans to be found, given that lean fails to build with the aforementioned error?

[Matthew Ballard]

Maybe @Mario Carneiro can help? I can try to trouble shoot at an unspecified later time but am surely far less useful.

[Alex Keizer]

I also ran a lake build through samply, which gave a stack trace showing a very deep mutual recursion--presumably the one being complained about--involving lean::type_checker::{whnf, reduce_nat}:
image.png

[Alex Keizer]

Matthew Ballard said:

Maybe Mario Carneiro can help? I can try to trouble shoot at an unspecified later time but am surely far less useful.

Ah, I managed to get the MWE to build (thus producing oleans) by setting debug.skipKernelTC to suppress the kernel error. Although, lean4lean seems to be giving unrelated errors. That is, it seems to be complaining about my preliminary definitions already existing:

PANIC at _private.Lean.Environment.0.Lean.EnvExtension.getStateImpl Lean.Environment:1297:4: invalid environment extension has been accessed
backtrace:
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_panic+0xf5) [0x7fe0605]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_panic_fn+0x15) [0x7fe07e5]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l___private_Lean_Environment_0__Lean_EnvExtension_getStateUnsafe___rarg+0x16b) [0x14b473b]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_ppConstNameWithInfos+0x4f) [0x25850ff]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_MessageData_ofConstName___elambda__2+0xaf) [0x1a7c27f]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_apply_2+0xa5f) [0x7fee7ef]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x2af) [0x1a7e0af]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0x172d) [0x1a7f52d]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_MessageData_formatAux+0xa97) [0x1a7e897]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_MessageData_toString+0x1c) [0x1a82a6c]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_throwKernelException___rarg+0x978) [0xfa9e78]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_addDecl___lambda__3+0x36d) [0xfad63d]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replayConstant+0x225d) [0xfb573d]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0x198) [0xfbc788]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replayConstants+0x19) [0xfb1ae9]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replayConstant+0x374) [0xfb3854]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0x198) [0xfbc788]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0xe8) [0xfbc6d8]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0xe8) [0xfbc6d8]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0xe8) [0xfbc6d8]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_Lean_RBNode_forIn_visit___at_replayConstants___spec__1+0xe8) [0xfbc6d8]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replay+0x6eb) [0xfc6deb]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replayFromImports___lambda__2+0x248) [0xfcce38]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_replayFromImports___lambda__4+0x15fa) [0xfcefea]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_apply_1+0x11dc) [0x7fecd1c]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(l_EIO_toBaseIO___rarg+0xa) [0x7f0e52a]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_apply_1+0x1219) [0x7fecd59]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean() [0x800a56e]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean(lean_apply_1+0x1219) [0x7fecd59]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean() [0x7fea546]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean() [0x7feb831]
/home/alex/Workspace/PhD/lean4lean/.lake/build/bin/lean4lean() [0x7fde325]
/nix/store/cg9s562sa33k78m63njfn1rw47dp9z0i-glibc-2.40-66/lib/libc.so.6(+0x97e63) [0x7f5ccd297e63]
/nix/store/cg9s562sa33k78m63njfn1rw47dp9z0i-glibc-2.40-66/lib/libc.so.6(+0x11bdbc) [0x7f5ccd31bdbc]
lean4lean found a problem in MWE:
(kernel) constant has already been declared '[Error pretty printing constant: (`Inhabited.default` for `IO.Error`). Falling back to raw printer.]
PoisonOr'

I figured trying out lean4lean with the --fresh flag could be more informative (as in lake env $lean4lean --fresh MWE), but this just complains about uncaught exception: (kernel) invalid form for primitive def Nat.gcd, even if I replace the entire module with a simple

def Foo : String := "foo"

I guess I must be doing something wrong, @Mario Carneiro help/guidance would be much appreciated!

[Mario Carneiro]

sorry, lean4lean was broken by one of the recent bumps and I haven't had time to fix it yet; this isn't your fault

[Mario Carneiro]

if you can, try using a previous version before the lean update

[Alex Keizer]

I figured it'd be something like that, I'll try an old version!

[Alex Keizer]

I've tried with commit c0273e3 of lean4lean, which is just before the latest lean bump, where lake env $lean4lean MWE gives no output (which presumably means lean4lean found no problems to report?), but trying --fresh still gives the same error about Nat.gcd.

I also tried 1574d0a, which is just before the lean version bump before that, on which neither lake env $lean4lean MWE nor lake env $lean4lean --fresh MWE give any output.

[Mario Carneiro]

I see, I wasn't aware of the Nat.gcd issue. Probably someone changed the definition?

[Mario Carneiro]

I think the list of primitives is also out of date

[Mario Carneiro]

I think the problem is that well founded definitions no longer reduce on constants, so the kernel override is adding defeqs that are not justified cc: @Joachim Breitner

[Mario Carneiro]

I think it needs to be implemented with fuel as Nat.div was

[Mario Carneiro]

@Alex Keizer if you want to ignore the issue you can replace line 81-83 of Primitive.lean with return true -- TODO

[Alex Keizer]

Mario Carneiro said:

I think the problem is that well founded definitions no longer reduce on constants, so the kernel override is adding defeqs that are not justified cc: Joachim Breitner

Do you mean this is an issue in lean4lean, or that this is the lean issue that causes my deep recursion error? I'm a bit lost.

if you want to ignore the issue you can replace line 81-83 of Primitive.lean with return true -- TODO

This is just talking about the lean4lean issue, right? I'm already satisfied that lean4lean seems to accept the MWE olean, confirming that this looks like a lean core issue

[Mario Carneiro]

this is unrelated to the deep recursion error, I think

[Alex Keizer]

I've opened an issue on the Github tracker for this problem as well: https://github.com/leanprover/lean4/issues/8898

[Mario Carneiro]

this is an issue in the way primitive declarations are being done in lean

[Tobias Grosser]

What does this mean?

[Tobias Grosser]

Any workaround we can apply?

[Jovan Gerbscheid]

The issues seems to be due to the constant 65537, which is being unfolded by the kernel. In general, working with big natural numbers brings the risk that the kernel will try to unfold them.

[Rish Vaishnav]

I've discovered that the issue is related to this commit. When I make the corresponding change to Lean4Lean to remove the e.hasFVar check, I get the same issue. The kernel tries to WHNF the second argument to Nat.ble 0 ((BitVec.toNat 32 x) * (BitVec.toNat 32 (BitVec.ofNat 32 65537))) so it can evaluate the Nat.ble application as a primitive op, which it wouldn't have done before because of the variable x. Was this change made because there was a particular case where we would want to evaluate primitive ops with fvars in their args? Or might this change have accidentally found its way into that commit?

[Mario Carneiro]

(FYI the unrelated bugs in lean4lean caused by the version bump have now been fixed, it should work on hello world files once more)

[Mario Carneiro]

that commit looks pretty sneaky, the second change seems entirely unrelated to the commit message

[Mario Carneiro]

it could be an accidental change?

[Mario Carneiro]

oh, the actual change is lean4#7386

[Rish Vaishnav]

Ah, so we need to also check that the variable isn't a let variable, perhaps? Rather than removing the check entirely

[Mario Carneiro]

well anything other than that particular check won't be O(1)

[Rish Vaishnav]

Oh, right, so to keep things O(1) we'll need to add a new entry to Expr.Data? Something like Expr.Data.hasLetVar?

[Mario Carneiro]

I don't think that can be computed in Expr.Data, since it depends on external information

[Rish Vaishnav]

Oh darn, yeah it depends on the context, tricky indeed...

[Rish Vaishnav]

Could this be a reasonable compromise?

def _root_.Lean.Expr.hasNonLetFVar (lctx : LocalContext) (e : Expr) : Bool := Id.run do
  let mut e := e
  for decl in lctx do
    if let .ldecl .. := decl then
      e := e.abstract #[decl.toExpr]
  return e.hasFVar

def reduceNat (e : Expr) : RecM (Option Expr) := do
  if e.hasNonLetFVar (← readThe Context).lctx then
    return none
  ...

The iteration for decl in lctx do is obviously not ideal, but we could perhaps reduce that cost by separately tracking a list of let-bound free variables in the typechecking context and only iterating over those instead.

[Rish Vaishnav]

^ if we do only iterate over let-bound fvars, this actually recovers O(1) in the common case (when there are no let-bound fvars in the context)

[Mario Carneiro]

I don't think it's practical, because this is being run on every subterm all the time - we don't even know yet whether it's a nat expression

[Mario Carneiro]

we may as well just step forward a bit and see if the head is Nat.add or whatever

[Mario Carneiro]

but maybe taking a step back, I'm not yet satisfied with the explanation of the issue. Why is this even triggering a big nat computation? It's just a bind reassociation which isn't unfolding anything

[Joachim Breitner]

Mario Carneiro schrieb:

but maybe taking a step back, I'm not yet satisfied with the explanation of the issue. Why is this even triggering a big nat computation? It's just a bind reassociation which isn't unfolding anything

It may be enough to be defeq checking, due to

/** \remark t_n, s_n are updated. */
lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
    while (true) {
        lbool r = is_def_eq_offset(t_n, s_n);
        if (r != l_undef) return r;

        if (!has_fvar(t_n) && !has_fvar(s_n)) {
            if (auto t_v = reduce_nat(t_n)) {
                return to_lbool(is_def_eq_core(*t_v, s_n));
            } else if (auto s_v = reduce_nat(s_n)) {
                return to_lbool(is_def_eq_core(t_n, *s_v));
            }

(related investigation at https://github.com/leanprover/lean4/issues/6152#issuecomment-2490917863)

[Mario Carneiro]

hm, needs more lazy

[Gavin Zhao]

Possibly similar problem: #lean4 > strange deep recursion error when using `rw` with `match`

[Devon Tuma]

I think they are essentially the same problem. I see the same reduce_nat involvement when debugging this. I would have thought that using Fin would be enough indirection to prevent this but maybe the expose in Fin.ofNat makes it still problematic in the same way? I'm trying to work around it by defining constants rather than using explicit numbers but it feels cumbersome.

[Devon Tuma]

The fact that that example relies on explicit match cases vs. a single default case probably comes down to some short circuiting that the compiler does when reducing a match?

[Alex Keizer]

So the way we worked around this issue is by introducing an opaque definition which is prop-eq to the identity function, but by virtue of being opaque blocks any reduction:

/-- Definition of `hide` and `hide_eq` -/
opaque hide_def : { hide : α → α // hide = id } := ⟨id, rfl⟩

/--
`hide` is an opaque version of the identity function.
By making it opaque, we prevent the kernel from trying to reduce the argument.
-/
def hide : α → α := hide_def.1

/-- A proof that `hide` is the identity. Note that this is deliberately *not*
a def-eq, since we made `hide` opaque. -/
theorem hide_eq {a : α} : hide a = a := by
  rw [hide, hide_def.2]; rfl

And then we wrote a simproc which rewrites problematic constants to hide them behind this opaque defintion:

/-- Symmetric version of `hide_eq`. -/
theorem eq_hide {a : α} : a = hide a := by
  symm; exact hide_eq

def simpHide (e : Expr) : Meta.SimpM Meta.Simp.Step := do
  let ctx ← Simp.getContext
  if let some parent := ctx.parent? then
    if parent.isAppOf ``hide then
      trace[LeanMLIR.Elab] "{Lean.crossEmoji}: parent ({parent}) is an application of `hide`"
      return .continue

  let expr ← Meta.mkAppM ``hide #[e]
  let proof ← Meta.mkAppOptM ``eq_hide #[none, e]
  return .done {
    expr := expr
    proof? := some proof
  }

protected partial def isConstant (e : Expr) : Bool :=
  match_expr e with
  | Neg.neg _α _self x => HideConstants.isConstant x
  | OfNat.ofNat _α x _self => HideConstants.isConstant x
  | _ => e.isRawNatLit
open HideConstants (isConstant)


simproc BitVec.hideOfIntConstants (BitVec.ofInt _ _) := fun e => do
  let_expr BitVec.ofInt _w x := e | return .continue
  withTraceNode `LeanMLIR.Elab (fun _ => pure m!"Hiding: {e}") <| do
    if !isConstant x then
      trace[Meta.Tactic.simp] "{Lean.crossEmoji}: {x} is not a constant"
      return .continue
    simpHide e

simproc LLVM.hideConst? (LLVM.const? _ _) := fun e => do
  let_expr LLVM.const? _w x := e | return .continue
  withTraceNode `LeanMLIR.Elab (fun _ => pure m!"Hiding: {e}") <| do
    if !isConstant x then
      trace[Meta.Tactic.simp] "{Lean.crossEmoji}: {x} is not a constant"
      return .continue
    simpHide e

macro "hide_constants" : tactic => `(tactic|
  simp -failIfUnchanged -memoize only [BitVec.hideOfIntConstants, LLVM.hideConst?]
  -- --------------------^^^^^^^
  -- NOTE: we have to disable the memoize option, since the simprocs
  -- inspect the parent expressions, which are disregarded by the cache
)

macro "unhide_constants" : tactic => `(tactic|
  all_goals simp -failIfUnchanged only [hide_eq]
)

Hopefully this workaround works in your situation also

[Aaron Liu]

There's irreducible_def from file#Tactic/IrreducibleDef

[Devon Tuma]

Thanks! The hide_def stuff does seem to solve my use case very well. These definitions made it very easy to tailor the simproc and isConstant definitions to our specific use case too

[Devon Tuma]

I've just had to add a few other cases so far for e.g. "variable * constant" that come up for us. But this was a very natural extension to make, and with multiple macros you can have different tiers of hiding things for use cases

[Devon Tuma]

I have found now though that in a couple of our cases hide_constants itself can cause the deep recusion error (seemingly when the constants involved are especially large). See for example:

namespace HideConstants

open Lean

/-- Definition of `hide` and `hide_eq` -/
opaque hide_def : { hide : α → α // hide = id } := ⟨id, rfl⟩

/--
`hide` is an opaque version of the identity function.
By making it opaque, we prevent the kernel from trying to reduce the argument.
-/
def hide : α → α := hide_def.1

/-- A proof that `hide` is the identity. Note that this is deliberately *not*
a def-eq, since we made `hide` opaque. -/
theorem hide_eq {a : α} : hide a = a := by
  rw [hide, hide_def.2]; rfl

/-- Symmetric version of `hide_eq`. -/
theorem eq_hide {a : α} : a = hide a := by
  symm; exact hide_eq

def simpHide (e : Expr) : Meta.SimpM Meta.Simp.Step := do
  let ctx ← Meta.Simp.getContext
  if let some parent := ctx.parent? then
    if parent.isAppOf ``hide then
      trace[LeanMLIR.Elab] "{Lean.crossEmoji}: parent ({parent}) is an application of `hide`"
      return .continue
  let expr ← Meta.mkAppM ``hide #[e]
  let proof ← Meta.mkAppOptM ``eq_hide #[none, e]
  return .done {
    expr := expr
    proof? := some proof
  }

protected partial def isConstant (e : Expr) : Bool :=
  match_expr e with
  | Neg.neg _α _self x => HideConstants.isConstant x
  | OfNat.ofNat _α x _self => HideConstants.isConstant x
  | Fin.val _α _x => true -- Also try to hide Fin values
  | _ => e.isRawNatLit
open HideConstants (isConstant)

simproc_decl BitVec.hideOfNatConstants (BitVec.ofNat _ _) := fun e => do
  let_expr BitVec.ofNat _w x := e | return .continue
  withTraceNode `LeanMLIR.Elab (fun _ => pure m!"Hiding: {e}") <| do
    if !isConstant x then
      trace[Meta.Tactic.simp] "{Lean.crossEmoji}: {x} is not a constant"
      return .continue
    simpHide e

macro "hide_constants" : tactic => `(tactic|
  simp -failIfUnchanged -memoize only [BitVec.hideOfNatConstants]
)

macro "unhide_constants" : tactic => `(tactic|
  all_goals simp -failIfUnchanged only [hide_eq]
)

example {n : Fin _} (s : Unit) :
    EStateM.run (do
      let _ ←
        (match
          (match ((BitVec.ofNat 1 (n * 100000 : Fin 1000000)))[0]'Nat.one_pos with
          | true => true
          | false => true) with
        | true => pure ()
        | false => pure () : EStateM Unit Unit Unit)
      return ()) s = EStateM.Result.ok () s := by
  hide_constants
  stop -- deep recursion is already caused by just calling `hide_constants`
  rw [EStateM.run_bind]
  unhide_constants
  cases (BitVec.ofNat 1 (n * _).val)[0]
  · simp only [EStateM.run_pure]
  · simp only [EStateM.run_pure]

end HideConstants

Although maybe this is also a problem with having the Fin.val case in general without checking things are full constants. There are at least fewer cases where this bug seems to happen.

[Devon Tuma]

Actually here's a very simple example I also came across as well. Seems that using n <<< 16 is over n * 2^16 is pretty necessary:

import Mathlib

example (n : ℕ) :
    (match
      (match BitVec.ofNat 64 (n * 2^16) with
      | 0#64 => some false
      | _ => some true) with
    | none => ()
    | some _ => ()) =
    if 1 + 1 = 2 then () else () := by
  rw [one_add_one_eq_two] -- causes deep recursion error