Positional-struct pattern rest (P(x, ..)) unsupported — if added, MirLower rest-skip needs the 60cc437f drop treatment

[ehartford]

Summary

During the A7 pattern-discard fixes (0e22d06f, 60cc437f), the enum-variant payload rest (.A(a, ..)) was found to leak its discarded Drop payloads (bare continue on NK_PAT_REST in the variant binding path) and was fixed. The positional-struct pattern path in MirLower.lower_pattern (the positional_struct_pattern_type branch) has its own NK_PAT_REST skip that was NOT probed or fixed.

Spec

§9.7 Pattern Matching — rest patterns discard the remaining elements; §2.4/§2.5 — discarded Drop values must drop exactly once (a leak is a soundness bug in the drop obligation, per the A7 precedent).

Repro sketch (unverified)

type P { a: W, b: W, c: W }   // W: impl Drop
match mk():
    P(x, ..) => ()            // if positional struct patterns parse — do the
                              // rest-discarded Drop fields b, c leak?

Probe heap-backed under --debug-alloc; expected leak count=0. If it leaks, apply the same anonymous drop-local treatment as the variant-path rest fix (60cc437f).

Workaround

None needed for named-field patterns ({ x, .. } was fixed in 0e22d06f).

[ehartford]

Probe result (heap-backed, HEAD): no leak possible — sema rejects the shape before lowering. match mk(): P(x, ..) => () fails check with "struct pattern 'P' expects 3 field pattern(s), found 2" — positional-struct patterns don't accept .. at all, so the suspect NK_PAT_REST skip in MirLower's positional path is unreachable from user code. The A7-family soundness concern is CLOSED.

Remaining (retitling): consistency gap — named-struct {x, ..} and enum-payload .A(a, ..) both support rest (the latter fixed in 60cc437f); positional-struct doesn't. If/when the arity check is relaxed to allow it (§9.7), the MirLower positional path's NK_PAT_REST skip MUST get the 60cc437f anonymous-drop-local treatment in the same change or the leak this issue feared becomes real. Left open as that small feature item with the soundness precondition documented.