; Fieldtest cut55-2d — decision (b), consume the borrowed param as a whole.
;
; passthrough borrows xs and hands the WHOLE xs to sum_own, an `(own)`
; sink that consumes it. The caller of passthrough still owns xs (borrow
; contract), so passthrough consuming it is a double-ownership violation.
; Per the ledger this is consume-while-borrowed and must be rejected.
;
; Expected: ail check -> error naming xs and the own-consuming call, exit 1.

(module cut55_2d_consume_borrow_whole

  (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 passthrough
    (doc "Borrow xs but pass the whole thing to an own sink — illegal consume.")
    (type
      (fn-type
        (params (borrow (con List)))
        (ret (own (con Int)))))
    (params xs)
    (body (app sum_own xs))))