Land the last unblocked TY7-internal sliver: a `..rest` capture now binds
the exact reduced size bound rather than the full scrutinee list type.
`[a, ..rest]` over `List<T, 8>` binds `rest: List<T, 7>` (the `Ty::Value`
size argument decremented by the fixed head count, saturating at 0); by
invariant generics that tail is now correctly rejected where the full
bound is wanted. Golden `match_list_rest_size_binder.cktest` proves it via
E0702 (`List<Cat, 7>` vs `List<Cat, 8>`), trapped; plus `list_rest_type`
unit tests.

Split the structural list-match path out of `match_check.rs` into a new
`match_list.rs` (a clean responsibility split: Maranget/list path vs
tag-set path) to hold the R3 per-file LoC cap; `process_pattern`, `Cover`,
and `ClosedTags` (+ `ClosedTags::none()`) become `pub(crate)`. The cap
stays pinned at 813 by `ck_resolve/src/bodies.rs`, so no gate is weakened.

Docs: TY7 slice doc -> nine slivers, deferred list rewritten so each
residual names its blocking slice (record-destructuring -> TY6,
`Panic::raise`->`Nothing` E0720 trigger -> TY8) or is out of locked scope;
README cascade row -> all TY7-internal slivers landed.

Gates: build + cargo test (incl. conformance + R3/R4 arch + untrapped
ratchet) + clippy --all-targets -D warnings all green.

@@ -0,0 +137,4 @@
+            &mut interner,
+        );
+        assert!(linked.diagnostics.is_empty(), "{:?}", linked.diagnostics);
+        let (_, scope) = linked.modules.iter().next().expect("one linked module");

@@ -0,0 +29,4 @@
+/// Type a list `match` and check its **structural** exhaustiveness (Maranget
+/// over the two list constructors — empty and cons). Returns the union of the
+/// arm bodies (synthesis-only), like the tag-set path.
+pub(crate) fn synth_list_match(