; Fieldtest cut55-2c — decision (b), genuine consume-while-borrowed.
;
; leak borrows xs, but in the Cons arm it hands the tail `t` to sum_own,
; whose param is `(own (con List))` — that call CONSUMES t, which is a
; heap field of the borrowed xs. Per the ledger, consuming a value you
; only borrowed is rejected (consume-while-borrowed).
;
; Expected: ail check -> error naming the consumed binder and pointing at
; `own`, exit 1.

(module cut55_2c_consume_borrow_reject

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

  (fn sum_own
    (doc "Own xs, consume it, return the sum.")
    (type
      (fn-type
        (params (own (con List)))
        (ret (own (con Int)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) 0)
        (case (pat-ctor Cons h t) (app + h (app sum_own t))))))

  (fn leak
    (doc "Borrow xs but feed its tail to an own-consuming sink — illegal.")
    (type
      (fn-type
        (params (borrow (con List)))
        (ret (own (con Int)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) 0)
        (case (pat-ctor Cons h t) (app sum_own t))))))