; Iter 18g tidy negative-coverage fixture: a let-binder whose
; value is the result of an `Implicit`-ret-mode fn call must NOT
; be trackable for scope-close drop. Implicit is the back-compat
; lane (default for unannotated fns); 18c.3 documented "Implicit-
; mode params do not get any dec — they leak rather than mis-dec",
; and 18g.2's symmetric carve-out is "Implicit-returning calls do
; not flow ownership to the caller, the caller must NOT dec".
;
; The asymmetry to `(own T)`-returning calls is real and
; intentional: an Own-returning fn signs a static contract that
; the caller now owns the cell and must dec it; an Implicit-
; returning fn does not. If `is_rc_heap_allocated` were
; mistakenly to fire on this shape, the let-scope close would
; emit a dec for a cell whose ownership is not (statically) the
; caller's. The cell may be a fresh allocation the callee
; happens to return without explicit annotation, OR a static
; constant in BSS, OR a returned-borrow indistinguishable from
; an own at the callee's signature. Dec'ing it would be
; refcount underflow in the first two cases and use-after-free
; in the third.
;
; Properties guarded:
; (1) Build succeeds (no consume-while-borrowed false positive).
; (2) Binary exits cleanly with stdout `7` (no crash, no
;     refcount underflow).
; (3) `live = 1` at program exit — the one MkT cell leaks. The
;     leak is intentional under the Implicit back-compat lane;
;     it documents the asymmetry from the (own)-ret case (which
;     would have `live = 0`).

(module rc_let_implicit_returning_app

  (data T
    (ctor MkT (con Int)))

  ; No ret-mode annotation -> default Implicit. Takes one
  ; ignored Int param (form-A doesn't allow zero-arg fn-app).
  (fn alloc
    (type
      (fn-type
        (params (con Int))
        (ret (con T))))
    (params n)
    (body
      (term-ctor T MkT n)))

  (fn unbox
    (type
      (fn-type
        (params (borrow (con T)))
        (ret (con Int))))
    (params x)
    (body
      (match x
        (case (pat-ctor MkT v) v))))

  (fn main
    (type (fn-type (params) (ret (con Unit)) (effects IO)))
    (params)
    (body
      (let x (app alloc 7)
        (do io/print_int (app unbox x)))))
)
