; Iter 16b.6 — LetRec inside a polymorphic enclosing fn.
; `apply_n_times : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`
; applies `f` to `x` exactly `n` times. The recursive helper `loop`
; captures `f` from the enclosing fn's params — `f`'s declared type
; is `Fn(a) -> a`, which mentions the outer fn's type var `a`. The
; 16b.6 lift produces a synthetic top-level fn
;   `loop$lr_0 : Forall(a). Fn(Int, a, Fn(a) -> a) -> a`
; and rewrites `(app loop k acc)` → `(app loop$lr_0 k acc f)`.
;
; `main` drives `apply_n_times` at TWO distinct type instantiations
; so codegen's monomorphisation queue picks up `loop$lr_0` twice
; (once at `a = Int` to compute `succ` applied 5x to 0 → 5; once at
; `a = Bool` to compute `not` applied 4x to false → false). This
; exercises the substitution of the outer Forall.vars into both the
; original LetRec params and the appended capture types.
;
; Expected stdout (one per line): 5, false.

(module poly_rec_capture

  (fn succ
    (doc "Helper: increment Int. Used as the Fn(Int) -> Int instance.")
    (type (fn-type (params (con Int)) (ret (con Int))))
    (params x)
    (body (app + x 1)))

  (fn flip
    (doc "Helper: boolean negation as a top-level fn (so it has an adapter for value-position).")
    (type (fn-type (params (con Bool)) (ret (con Bool))))
    (params b)
    (body (app not b)))

  (fn apply_n_times
    (doc "Apply f to x exactly n times. Polymorphic in a.")
    (type
      (forall (vars a)
        (fn-type
          (params (con Int) a (fn-type (params a) (ret a)))
          (ret a))))
    (params n x f)
    (body
      (let-rec loop
        (params k acc)
        (type (fn-type (params (con Int) a) (ret a)))
        (body
          (if (app eq k 0)
            acc
            (app loop (app - k 1) (app f acc))))
        (in (app loop n x)))))

  (fn main
    (doc "Drive apply_n_times at Int (succ 5 times from 0) and Bool (not 4 times from false).")
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (seq (seq (app print (app apply_n_times 5 0 succ)) (do io/print_str "\n"))
           (seq (app print (app apply_n_times 4 false flip)) (do io/print_str "\n"))))))