Tail-call optimization when specializing monad?

Stream: lean4

[Phil Nguyen]

In Lean 4.18, the following code doesn't cause stack overflow:

partial def loop : IO Unit := loop
def main : IO Unit := loop

, but the following does:

@[specialize] partial def loop [Monad m] : m Unit := loop
def main : IO Unit := loop
-- Stack overflow detected. Aborting.

Is there a way to ask the compiler to try to apply tail-call optimization when it's possible in the specialized code?

Many thanks!

[Phil Nguyen]

Not very related to the original question, but I tried a few things and found the result intriguing.

The following program causes a stack overflow, which can be unintuitive for someone more familiar with imperative constructs:

def main : IO Unit := do repeat pure ()
-- Stack overflow detected. Aborting.

The following program, however, keeps running without blowing up the stack: (at least I let it run until 8 digits)

def main : IO Unit := do
  let mut x := 0
  repeat
    IO.println x
    x := x + 1

The following program causes an internal error. I wonder if it's a bug I should report:

def main : IO Unit := do
  let mut x := 0
  repeat
    pure ()
    x := x + 1
-- INTERNAL PANIC: unreachable code has been reached

[Jz Pan]

Phil Nguyen said:

The following program causes an internal error. I wonder if it's a bug I should report:

def main : IO Unit := do
  let mut x := 0
  repeat
    pure ()
    x := x + 1
-- INTERNAL PANIC: unreachable code has been reached

That is a feature that dead loops without side effects will be compiled into unreachable code.

[Mario Carneiro]

no, "INTERNAL PANIC" is not desirable behavior

[Mario Carneiro]

Lean uses rust-style semantics on empty loops: they spin (as compared to C-style semantics of "they cause UB")

[Mario Carneiro]

It is not sound for lean to allow empty loops to be optimized away

[Mario Carneiro]

The above is a miscompilation. Please report it

[Mario Carneiro]

The fact that do repeat pure () stack overflows also seems like a bug, I would definitely expect that to have bounded stack usage and it sounds like an inlining issue

[Phil Nguyen]

I filed the bugs on Github (1 and 2). Thanks!!