(module flat_pat_shadow_leak
  (data IntList
    (ctor Nil)
    (ctor Cons (con Int) (con IntList)))
  (data Box (vars a)
    (ctor MkBox a))
  (fn blen
    (doc "borrow-only length over a borrowed IntList")
    (type (fn-type (params (borrow (con IntList))) (ret (own (con Int)))))
    (params xs)
    (body (match xs
      (case (pat-ctor Nil) 0)
      (case (pat-ctor Cons h t) (app + 1 (app blen t))))))
  (fn csum
    (doc "consuming sum over an IntList")
    (type (fn-type (params (own (con IntList))) (ret (own (con Int)))))
    (params xs)
    (body (match xs
      (case (pat-ctor Nil) 0)
      (case (pat-ctor Cons h t) (app + h (app csum t))))))
  (fn main
    (doc "A2b completeness fixture (refs #43): a flat-match pattern-binder `x` shadows the outer let `x`. The inner `x` (Box payload, a heap IntList) is borrow-only (consume_count 0) and must be dropped at arm close; the outer `x` is consumed once by csum (count 1). Under the (def,name) uniqueness-table collision the arm-close drop gate (match_lower.rs) reads the collapsed outer count 1 and suppresses the inner payload's drop, leaking 2 cells. Pairs with flat_pat_shadow_control.ail (same program, inner binder alpha-renamed to `y`); the live-count delta is exactly the suppressed drop. GREEN once binder names are made unique per fn at desugar.")
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (let x (term-ctor IntList Cons 1 (term-ctor IntList Nil))
        (seq
          (match (term-ctor Box MkBox (term-ctor IntList Cons 2 (term-ctor IntList Nil)))
            (case (pat-ctor MkBox x)
              (app print (app blen x))))
          (app print (app csum x)))))))