let bindings destructure, and so does let!

[simontreanor]

Closes dogfooding finding 9. let (r, c) = parseCoord tok, let Point { x, y } = origin and let (a, (b, c)) = nested now parse at top level, in blocks, in an in-file module, and on a computation expression's let/let!.

What changed

LetBinding and CeItem::Let/LetBang carry a Pattern where they carried a String. Pattern::bound_names / bound_vars on the AST are the one place any phase asks what a binding introduces, which is what every scope-tracking path (lowering's scan, the fold pass, the module-alias mangling, the LSP resolver, the type checker's free-variable walk) now consults instead of a single name. LetBinding::name() stays as the plain-name shortcut for the common case, mirroring the Param::name() that was already there.

The irrefutability rule was already written: refutable_in_param, renamed refutable_shape and now shared between the two binding positions. A target admits exactly what a parameter does (a name, _, tuples, records, nested) and rejects everything else with a message naming what was written and pointing at match. A function binding and a let mut keep their single name, each with its own message.

Emitted Python

Lowering reuses the existing unpack_into, so the output is what a Python programmer would write:

source	emitted
let (r, c) = e	r, c = e
let (a, (b, c)) = p	a, _pf_t0_1 = p then b, c = _pf_t0_1
let Point { x, y } = p	x = p.x then y = p.y
let! (r, c) = e in result	case Ok((r, c)):

Nested targets read through a reserved base rather than a name derived from the user's, so a binding called p never has p_1 invented next to it. The result case is the one worth calling out: the target rides inside the Ok pattern the bespoke lowering already matches, so a destructuring bind costs no extra statement.

Each bound name generalizes on its own, the same let-generalization a single-name binding gets. There is no value restriction to trip over, since mut bindings are monomorphic and named.

Verification

• Full suite green (1023 tests), cargo fmt --check and cargo clippy --all-targets clean.
• New tests: roundtrip corpus entries for every target shape, parser rejection tests, type-checker tests (shape, arity, generalization, effect leak, let! unwrapping before destructuring), lowering assertions on the emitted Python, three e2e programs, one LSP go-to-definition test landing on one element of a tuple target.
• docs/verify_lessons.py passes on all 23 lessons, including the new lesson 8 section (its quoted diagnostic is checked against the real one).
• Tree-sitter: 45/45 corpus tests via Docker. The grammar now accepts the new targets and destructuring parameters, which the language already had but the grammar did not.

Docs

DESIGN.md §7 gains the canonical paragraph next to the parameter-destructuring one it shares its rule with; INTERNALS.md records the AST change; lesson 8 ("Tuples and destructuring") gains a section; CLAUDE.md status and the ROADMAP entry are updated.