Recursive definition causes infinite loop/memory leak

[TwoFX]

Prerequisites

• 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

Put the following function into a file

def foo (pat : ByteArray) (stackPos : Nat) (hst : stackPos < pat.size) : { n : Nat // n ≤ stackPos } :=
  if h : stackPos = 0 then
    ⟨0, by simp⟩
  else
    go (stackPos - 1) (by omega)
where
  go (guess : Nat) (hg : guess < stackPos) : { n : Nat // n ≤ stackPos } :=
    if pat[guess] = pat[stackPos] then
      ⟨guess + 1, by omega⟩
    else if h : guess = 0 then
      ⟨0, by simp⟩
    else
      have : (foo pat (guess - 1) (by omega)) < guess := by
        have := (foo pat (guess - 1) (by omega)).property
        omega
      go (foo pat (guess - 1) (by omega)) (by omega)

Running the file in VS Code (or live.lean-lang.org) or building it via lake build will cause Lean to indefinitely use a CPU core while continuously eating memory.

This seems to be related to termination checking, since turning the function into a partial function makes it go through instantly.

Expected behavior: Function definition is accepted or rejected

Actual behavior: Hang

Versions

4.27.0 and nightly-2026-02-09

Impact

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

[nomeata]

Interesting.

The mutual recursion isn't necessary, it’s not kernel type checking, and it shows up with an explicit termination measure and decreasing proof as well:

set_option debug.skipKernelTC true
def go (pat : ByteArray) (stackPos : Nat) (hst : stackPos < pat.size) (guess : Nat) (hg : guess < stackPos) : { n : Nat // n ≤ stackPos } :=
    if pat[guess] = pat[stackPos] then
      ⟨guess + 1, by omega⟩
    else if h : guess = 0 then
      ⟨0, by simp⟩
    else
      have : (go pat stackPos hst (guess - 1) (by omega)) < guess := by
        sorry
      go pat stackPos hst (go pat stackPos hst (guess - 1) (by omega)) (by omega)
termination_by guess
decreasing_by all_goals sorry

The problem goes away if I replace any of the by omega in the nested recursive call with by sorry.

It also goes away if I use by grind rather than by sorry or by omega.

It does not help to write by as_aux_lemma => omega (I have a theory that we have a problem with large proofs terms that appear in argumens to nested recursive calls).

It seems to help to have-abstract the arguments to go manually (at this point my coding machine crashed from testing this, so I’ll better post these intermediate results before I lose them :-D)

[nomeata]

Ok, here is a work-around for your code before my minimiation:

def foo (pat : ByteArray) (stackPos : Nat) (hst : stackPos < pat.size) : { n : Nat // n ≤ stackPos } :=
  if h : stackPos = 0 then
    ⟨0, by simp⟩
  else
    go (stackPos - 1) (by omega)
where
  go (guess : Nat) (hg : guess < stackPos) : { n : Nat // n ≤ stackPos } :=
    if pat[guess] = pat[stackPos] then
      ⟨guess + 1, by omega⟩
    else if h : guess = 0 then
      ⟨0, by simp⟩
    else
      have : (foo pat (guess - 1) (by omega)) < guess := by
        have := (foo pat (guess - 1) (by omega)).property
        omega
      have : guess - 1 < pat.size := by omega
      go (foo pat (guess - 1) (by assumption)) (by omega)

[Rob23oba]

Just from the stack trace it seems like it gets stuck in mkLambdaFVars in Lean.Elab.WF.replaceRecApps.loopGo, getting deeper and deeper in MkBinding.elimApp and MkBinding.visit.

[nomeata]

Are you suggesting this is not “just” a huge proof term that we traverse in a costly way in replaceRecApp, but that there may be an actual looping bug in mkLambdasFVars?

[Rob23oba]

Using debug.definition.wf.replaceRecApps shows:

Details

set_option debug.definition.wf.replaceRecApps true in

/--
error: fail to show termination for
  foo.go
  foo
with errors
failed to infer structural recursion:
Not considering parameter pat of foo.go:
  it is unchanged in the recursive calls
Not considering parameter hst of foo.go:
  its type Nat.le is an inductive family and indices are not variables
    stackPos.succ.le pat.size
Not considering parameter hg of foo.go:
  its type is an inductive datatype
    guess.succ.le stackPos
  and the datatype parameter
    guess.succ
  depends on the function parameter
    guess
  which is not fixed.
Not considering parameter pat of foo:
  it is unchanged in the recursive calls
Not considering parameter hst of foo:
  its type Nat.le is an inductive family and indices are not variables
    stackPos.succ.le pat.size
Cannot use parameters stackPos of foo.go and stackPos of foo:
  failed to eliminate recursive application
    foo pat (guess - 1) ⋯
Cannot use parameters guess of foo.go and stackPos of foo:
  failed to eliminate recursive application
    foo pat (guess - 1) ⋯


Type not preserved transforming
  (foo.go._mutual
      (PSum.inr
        ⟨pat, ⟨guess - 1, Decidable.byContradiction fun a => foo.go._proof_1 pat stackPos hst guess hg a⟩⟩)).property
to
  (a✝ (PSum.inr ⟨pat, ⟨guess - 1, Decidable.byContradiction fun a => foo.go._proof_1 pat stackPos hst guess hg a⟩⟩)
      ?m.199).property
Type was
  (foo.go._mutual (PSum.inr ⟨pat, ⟨guess - 1, ⋯⟩⟩)).val ≤ guess - 1
and now is
  (a✝ (PSum.inr ⟨pat, ⟨guess - 1, ⋯⟩⟩) ?m.199).val ≤ guess - 1
-/
#guard_msgs in
def foo (pat : ByteArray) (stackPos : Nat) (hst : stackPos < pat.size) : { n : Nat // n ≤ stackPos } :=
  if h : stackPos = 0 then
    ⟨0, by simp⟩
  else
    go (stackPos - 1) (by omega)
where
  go (guess : Nat) (hg : guess < stackPos) : { n : Nat // n ≤ stackPos } :=
    if pat[guess] = pat[stackPos] then
      ⟨guess + 1, by omega⟩
    else if h : guess = 0 then
      ⟨0, by simp⟩
    else
      have : (foo pat (guess - 1) (by omega)) < guess := by
        have := (foo pat (guess - 1) (by omega)).property
        omega
      go (foo pat (guess - 1) (by omega)) (by omega)

where

?m.199 : (invImage
      (fun x =>
        PSum.casesOn x
          (fun _x =>
            PSigma.casesOn _x fun pat stackPos =>
              PSigma.casesOn stackPos fun stackPos hst =>
                PSigma.casesOn hst fun hst guess => PSigma.casesOn guess fun guess hg => (stackPos, guess))
          fun _x =>
          PSigma.casesOn _x fun pat stackPos => PSigma.casesOn stackPos fun stackPos hst => (stackPos, stackPos))
      Prod.instWellFoundedRelation).1
  (PSum.inr ⟨pat, ⟨guess - 1, ⋯⟩⟩) (PSum.inl ⟨pat, ⟨stackPos, ⟨hst, ⟨guess, hg⟩⟩⟩⟩)

so it seems like having a recursive reference to foo pat (guess - 1) (by omega) in the type of the have causes it to have an mvar that causes problems.

[Rob23oba]

@nomeata I have no clue (I haven't looked at what kind of term mkLambdaFVars has to deal with) but it takes surprisingly long (many seconds) for that mkLambdaFVars call to complete and it gets quite deep into elimApp.

[Rob23oba]

Alright, now I have looked at what kind of terms mkLambdaFVars has to deal with (here's a dump: newdump.txt). It seems like the problem is that mkLambdaFVars create multiple (delayed assigned?) meta-variables for the same mvar:

#148475: ?_uniq.201341 B0
#148476: !_uniq.192931 #126476 #148475
#148477: Subtype.val.{1} Nat #126465 #148476
#148478: Nat.cast.{0} Int instNatCastInt #148477
...
#148485: ?_uniq.201342 B0
#148486: !_uniq.192931 #126476 #148485
#148487: Subtype.val.{1} Nat #126465 #148486
#148488: Nat.cast.{0} Int instNatCastInt #148487
#148489: ?_uniq.201343 B0
#148490: !_uniq.192931 #126476 #148489
#148491: Subtype.val.{1} Nat #126465 #148490
#148492: Nat.cast.{0} Int instNatCastInt #148491
...
#148495: ?_uniq.201344 B0
#148496: !_uniq.192931 #126476 #148495
#148497: Subtype.val.{1} Nat #126465 #148496
#148498: Nat.cast.{0} Int instNatCastInt #148497
...
#148508: ?_uniq.201345 B0
#148509: !_uniq.192931 #126476 #148508
#148510: Subtype.val.{1} Nat #126465 #148509
#148511: Nat.cast.{0} Int instNatCastInt #148510
...
#148518: ?_uniq.201346 B0
#148519: !_uniq.192931 #126476 #148518
#148520: Subtype.val.{1} Nat #126465 #148519
#148521: Nat.cast.{0} Int instNatCastInt #148520
...
#148528: ?_uniq.201347 B0
#148529: !_uniq.192931 #126476 #148528
#148530: Subtype.val.{1} Nat #126465 #148529
#148531: Nat.cast.{0} Int instNatCastInt #148530
...
#148539: ?_uniq.201348 B0
#148540: !_uniq.192931 #126476 #148539
#148541: Subtype.val.{1} Nat #126465 #148540
#148542: Nat.cast.{0} Int instNatCastInt #148541
...
#148552: ?_uniq.201349 B0
#148553: !_uniq.192931 #126476 #148552
#148554: Subtype.val.{1} Nat #126465 #148553
#148555: Nat.cast.{0} Int instNatCastInt #148554
...
#148562: ?_uniq.201350 B0
#148563: !_uniq.192931 #126476 #148562
#148564: Subtype.val.{1} Nat #126465 #148563
#148565: Nat.cast.{0} Int instNatCastInt #148564
...
#148572: ?_uniq.201351 B0
#148573: !_uniq.192931 #126476 #148572
#148574: Subtype.val.{1} Nat #126465 #148573
#148575: Nat.cast.{0} Int instNatCastInt #148574
...
#148583: ?_uniq.201352 B0
#148584: !_uniq.192931 #126476 #148583
#148585: Subtype.val.{1} Nat #126465 #148584
#148586: Nat.cast.{0} Int instNatCastInt #148585
...
#148605: PSum.inl.{1, 1} #78898 #78904 #148604
#148606: !_uniq.192931 #148605 ?_uniq.201353
Doing mkLambdaFVars #[!_uniq.194141] #148606

[nomeata]

The only MVars we are facing here are those added by mkDecreasingProof, right? All elaboration-time mvars have been instantiated at this point, I assume.

Maybe one could avoid using MVars here. But it is somewhat the right tool here… hmm.

[Rob23oba]

Alright, I have a "fix": Instead of using the metavariable from mkDecreasingProof directly, we return an application of a delayed assigned metavariable which has an empty local context

/--
Returns a metavariable application `?newM ...` equivalent to `m` where `newM` is a delayed assigned
metavariable with an empty local context.
-/
private def _root_.Lean.MVarId.completeDelayedAssign (m : MVarId) : MetaM Expr := m.withContext do
  let lctx ← getLCtx
  let decl ← m.getDecl
  let fvars := lctx.decls.toArray.filterMap (·.map (·.toExpr))
  if fvars.isEmpty then
    return .mvar m
  let type ← mkForallFVars fvars decl.type
  let mvar ← mkFreshExprMVarAt {} {} type decl.kind decl.userName (decl.numScopeArgs + fvars.size)
  assignDelayedMVar mvar.mvarId! fvars m
  return mkAppN mvar fvars

/--
Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and
the current syntax reference is stored in the `MVar`’s type as a `RecApp` marker, for
use by `solveDecreasingGoals` below.
-/
private def mkDecreasingProof (decreasingProp : Expr) : TermElabM Expr := do
  -- We store the current Ref in the MVar as a RecApp annotation around the type
  let ref ← getRef
  let mvar ← mkFreshExprSyntheticOpaqueMVar (mkRecAppWithSyntax decreasingProp ref)
  let mvarId := mvar.mvarId!
  let _mvarId ← mvarId.cleanup
  mvarId.completeDelayedAssign

[Rob23oba]

Then it takes about 5 seconds instead of eternity (still not great, though)

[nomeata]

So could it be that mkLambdaFVar is correct (not actually looping) but that this is term hitting some bad asymptomatic behavior (deeply nested binders or so)? Or do you think there is something functionally broken?

[Rob23oba]

Yeah, from what I can tell, the problem is just that the amount of delayed-assigned metavariables grows (probably) exponentially.

[Rob23oba]

Okay, just to confirm; after the change mentioned above, mkLambdaFVars now only takes up roughly 100ms out of 3.5 seconds with replaceRecApps taking up a little less than 1.5 seconds and solveDecreasingGoals a little more than 1.5 seconds.

[nomeata]

Thanks a lot for the analysis! I wonder where else this shows up.

Your workaround is reasonable if this becomes pressing. I'm a bit hesitant to put it in though while there are workarounds.