(module loop_in_lambda_e2e

  (fn apply
    (doc "apply a fn-of-Int to an Int. Iter it.2: the supplied closure is loop-bearing, so its arrow carries !Diverge — the higher-order param type and apply's own effect row must reflect that (effects are part of the function type).")
    (type (fn-type (params (fn-type (params (con Int)) (ret (con Int)) (effects Diverge)) (con Int)) (ret (con Int)) (effects Diverge)))
    (params f x)
    (body (app f x)))

  (fn main
    (doc "Iter it.1 — a loop inside a lambda body, invoked via a closure. The lambda computes x*x by summing x exactly x times through an accumulator loop; apply 7 prints 49. Codegen-soundness gate for the lambda-boundary loop_frames save/restore. Iter it.2: !Diverge propagates out through apply (callee-effect propagation).")
    (type (fn-type (params) (ret (con Unit)) (effects IO Diverge)))
    (params)
    (body
      (app print
        (app apply
          ; Iter it.2: the loop lives in THIS lambda's body, so the
          ; lambda's arrow carries !Diverge (DD-4 lam boundary). The
          ; loop does not leak Diverge to `main` — `main`'s body does
          ; not syntactically contain the loop (it stops at the lam
          ; edge, exactly as !IO does).
          (lam
            (params (typed x (con Int)))
            (ret (con Int))
            (effects Diverge)
            (body
              (loop ((var acc (con Int) 0) (var k (con Int) 0))
                (if (app == k x)
                  acc
                  (recur (app + acc x) (app + k 1))))))
          7)))))