; RED fixture (refs #55, Implicit-cutover double-drop).
;
; Property under test: a ctor arm with a literal sub-pattern in a
; non-tail field — `(Cons (pat-lit K) _)` — must drop the matched
; value's owned children EXACTLY ONCE on the head!=K path.
;
; The 16c lit-sub-pattern desugar (crates/ailang-core/src/desugar.rs
; `desugar_one_arm` / `wrap_sub`) lowers `(Cons (pat-lit K) _)` into an
; outer Cons-match that binds the Cons fields, then an
; `if (== head K) body else fall_k`. `fall_k` is the rest of the arm
; chain, which RE-MATCHES the same owned scrutinee (re-binding its
; children). Once the param mode is `Own` (post-#55 cutover, was
; `Implicit`), the arm-close Iter-A drop in
; crates/ailang-codegen/src/match_lower.rs (gated on
; `scrutinee_is_owned`) fires on the tail child in BOTH the re-match arm
; AND the enclosing lit-arm's join — the same heap pointer (`arg_xs+16`)
; is dropped twice → double-free → SIGSEGV on the head!=K path.
;
; Pre-cutover this leaked instead of crashing (Implicit suppressed the
; drop entirely). The fixture pins single-drop, not merely exit-0:
; `cat` consumes its owned IntList arg, so a leak-free run frees every
; cell exactly once. `main` drives both the head==K (0) and head!=K (7)
; paths so the regression is visible on whichever path the fix touches.

(module lit_pat_ctor_tail_drop

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

  (fn cat
    (doc "Empty -> -1; first element 0 -> 0; otherwise the head.")
    (type (fn-type (params (borrow (con IntList))) (ret (own (con Int)))))
    (params xs)
    (body
      (match xs
        (case (pat-ctor Nil) -1)
        (case (pat-ctor Cons (pat-lit 0) _) 0)
        (case (pat-ctor Cons h _) h))))

  (fn main
    (doc "Drive head==0 then head!=0. Expected (per line): 0, 7.")
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (seq (seq (app print (app cat (term-ctor IntList Cons 0 (term-ctor IntList Nil)))) (do io/print_str "\n"))
           (seq (app print (app cat (term-ctor IntList Cons 7 (term-ctor IntList Nil)))) (do io/print_str "\n"))))))