deep structural recursion was detected

Stream: lean4

[Zygimantas Straznickas]

-- Using List as carrier of `children`: works
partial def recurseM [Monad μ] (curr: α) (action: α -> μ (List α)) : μ PUnit := do
  let children ← action curr
  children.forM (recurseM · action)

def specificTraverseList : Option Unit := recurseM () (fun _ => some [])


-- Using Array as carrier of `children`:
partial def recurseM2 [Monad μ] (curr: α) (action: α -> μ (Array α)) : μ PUnit := do
  let children ← action curr
  children.forM (recurseM2 · action)

-- When compiling definition below:
-- `deep recursion was detected at 'replace' (potential solution: increase stack space in your system)`
def specificTraverseArray : Option Unit := recurseM2 () (fun _ => some #[])

Possibly a bug? I tried setting the thread stack size to huge values and it didn't help.

[Leonardo de Moura]

Pushed a fix https://github.com/leanprover/lean4/commits/master