Add nested literal, constructor and list patterns

[jasisz]

Syntax

• Constructor fields are patterns at any depth: Option.Some(0), Result.Ok("x"), Shape.Rect(0, h), Option.Some(true), Option.Some(Option.None), Option.Some((0, _)). Literal kinds are the ones a top-level arm takes: Int, String, Float, Bool.
• List patterns: [], [a], [a, b] (exact length), [a, b, ..rest] (at least two), [..all], with pattern elements ([0, ..rest], [Option.Some(x), ..rest]). ..rest is last and is a binder or _. [h, ..t] keeps its old flat form.

How it works

• Parser: Pattern::ConstructorNested(name, Vec<Pattern>) and Pattern::List { items, rest }. A constructor whose fields are all binders stays Pattern::Constructor, so existing programs are unchanged.
• The checker reads the patterns as written. Exhaustiveness spells list patterns as cons chains, so coverage is by length, and a literal never covers its constructor. Witnesses look like missing pattern Option.Some(_), Option.Some(false) and [_, _, _, .._]. Literal patterns are checked against their position's type, and a list pattern against a non-list is an error. Pattern errors now point at the arm line.
• src/ir/nested_patterns.rs: in the front door, after the program is checked as written, each match with a nested form is compiled into nested flat matches with a clause-matrix compilation. Arms keep first-match order. A switch has no _ default when its constructors cover the type, using the variant families the checker records. Binders keep user names where that cannot capture anything; otherwise they get fresh __patN names. A computed subject is evaluated once. The lowered program is then checked again. An arm that no leaf of the compiled tree reaches is reported as unreachable, which catches arms covered only by several earlier arms together. Dependencies go through the same step in lower_loaded_yield_modules.
• Backends (VM, Rust, wasm-gc, wasip2), the Lean exporter and the cert model therefore never see the new forms, and HIR resolve panics if one ever gets that far. Nested patterns inside a yield function are refused with an error for now.
• aver format has a new rule, bad-match-pattern, that prints arm patterns in canonical spelling. It only rewrites when the change is whitespace. It fires on nothing in examples/, stdlib/, self_hosted/, projects/ or tests/fixtures/.
• Fix in src/ir/escape.rs: a one-parameter body that contains a binding match was spliced into its caller together with a slot the caller does not have. On main this already breaks a hand-written match h | Holder.Full(inner) -> match inner | Option.Some(x) -> x ... called with a literal constructor: the VM panics with index out of bounds and wasm-gc fails validation. Nested patterns produce exactly this shape. Such bodies now stay calls.

Self-host

Not updated. Self-host parity only runs examples/core/{hello,calculator,shapes}, and none of them use the new syntax. aver run --self-host on a program that uses it fails with a parse error in the self-hosted parser; it does not run wrong code. tools/regenerate_self_host.py --check still reports that the checked-in output is fresh.

Tests

• parser_spec: the new forms, ..rest placement and binder rules, unparse round trip.
• typechecker_spec: positive and negative exhaustiveness, redundancy, literal and list type errors, binder types.
• src/ir/nested_patterns/tests.rs: lowering shape, no redundant defaults, dead-arm detection, the subject evaluated once.
• nested_patterns_spec: one fixture run on the VM, wasm-gc and wasip2 against one expected stdout, plus aver verify and CLI diagnostics.
• rust_codegen_differential: the same fixture built with Rust and run, stdout equal to the VM.
• proof_spec: laws over Option.Some(0) and [0, ..rest] build in Lean with 0 sorries (3 universal).
• format_cmd unit tests for the new rule.