Recursive ForIn/ForM: Stack overflow b/c ForM.forIn inlined

Stream: new members

[smheidrich]

Would you guys agree that the snippet below should not cause a stack overflow or would it be considered user error if I posted it as a GitHub issue? For a slightly less minimal example, cf. also my Stack Overflow question about it.

inductive Countdown where
  | zero
  | one

-- ForM.forM implementation that does absolutely nothing & should terminate
-- after a single recursive call of itself (indirectly via `for` loop):
partial def Countdown.forM
  [Monad m] (c : Countdown) (_action : Unit → m PUnit) : m PUnit
:= do match c with
  | zero => pure ()
  | one =>
      -- Functions that allow synthesis of local ForM & ForIn instances, as
      -- suggested in "Instances for nested types" example from [1]:
      let {m'} := (⟨Countdown.forM⟩ : ForM m' Countdown Unit)
      let {m''} := (⟨ForM.forIn⟩ : ForIn m'' Countdown Unit)
      for () in zero do
        return

def main : IO Unit :=
  Countdown.one.forM pure

-- Uncomment to cause stack overflow in Lean 4 Web version:
-- #eval main

-- [1]: https://lean-lang.org/doc/reference/latest//Type-Classes/Instance-Declarations/#recursive-instances

It works fine if you explicitly use a non-inline version of ForM.forIn.

[Markus Himmel]

Thank you for the report. This is a miscompilation introduced by the new compiler which was enabled in Lean 4.22.0. I have created an issue with some further minimization at lean4#10925.

[smheidrich]

Thank you for looking into it! :slight_smile: So the non-inline thing fixing it was pure luck :sweat_smile: