; Fieldtest cut55-2b — decision (b), false-positive GUARD for the #58 fix.
;
; This is the legitimate borrow-traverse-and-rebuild that MUST be accepted.
; `bump` borrows xs and, in the Cons arm, reads the head `h` (a value-typed
; Int, copied), passes the tail `t` to its own recursive call, and packs a
; fresh Cons. The recursive `bump`'s param is `(borrow (con List))`, so `t`
; is only BORROWED, never moved into an `(own)` slot — nothing of the
; borrowed xs is consumed. A fresh List is allocated and returned `own`.
;
; This pins that the #58 fix (inherit borrow on heap sub-binders of a
; borrowed scrutinee) does NOT over-fire: a borrow-position use of a heap
; sub-binder is fine. Contrast cut55_2c (feeds `t` to an OWN sink -> reject)
; and cut55_2d (consumes the whole borrowed xs -> reject).
;
; Expected: ail check -> ok, exit 0.

(module cut55_2b_borrow_traversal_clean

  (data List
    (ctor Nil)
    (ctor Cons (con Int) (con List)))

  (fn bump
    (doc "Borrow xs and rebuild a fresh +1 list; tail t is only borrowed, not consumed.")
    (type
      (fn-type
        (params (borrow (con List)))
        (ret (own (con List)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) (term-ctor List Nil))
        (case (pat-ctor Cons h t)
          (term-ctor List Cons (app + h 1) (app bump t)))))))