let bindings destructure, and so does let!

DESIGN.md

@@ -1035,6 +1035,24 @@ statement per nesting level; a record parameter reads one attribute per field it
 (`letter = _pf_arg0.letter`) and nothing for the fields it does not. A destructuring *lambda*
 therefore lowers to a named `def` rather than a Python `lambda`, which cannot hold a statement.
 
+**A `let` binding may destructure too**, under exactly the rule above and for exactly the same
+reason — `let (r, c) = parseCoord tok`, `let Point { x, y } = origin`, `let (a, (b, c)) = nested`.
+Python spells this `a, b = f()`, and Pyfun emits precisely that: a tuple of plain names unpacks in a
+single statement straight from the value, with no temp in the way. Anything deeper reads through a
+reserved temp, one statement per level (`a, _pf_t0_1 = p` then `b, c = _pf_t0_1`), and a record
+target reads one attribute per field it names. The target is held to irrefutability by the same
+check a parameter's is, so `let Some x = …` is rejected with a message naming what was written and
+pointing at `match`, which has somewhere to fall through to. Three positions take a target: a
+top-level `let`, a block-local `let`, and a computation expression's `let`/`let!` — where a
+destructuring bind costs nothing extra, because `result`'s pattern rides inside the `Ok` it already
+matches (`case Ok((r, c)):`). What cannot destructure is a binding that needs a single name to
+*be*: a function binding (`params` are what make it one) and a `let mut` (whose name is what `<-`
+reassigns) both reject a pattern target, each with its own message. Each name a destructuring
+binding introduces is generalized 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.
+`let _ = e` is the degenerate case: it binds nothing and exists so a value-producing expression can
+be run for its effect.
+
 MVP language features: immutable bindings by default with checked `let mut`/`<-` and indentation
 blocks (§3), expression `if`/`match`, **curried functions + partial application**, **pipe `|>`**, ADT
 and **record** declarations, the three computation expressions of §8, units of measure (§8), readable

INTERNALS.md

@@ -212,8 +212,10 @@ stdio. All features reuse the existing front end:
   It works because the checker, in a `record`-enabled pass (`types::check_collecting`, surfaced via
   `analyze`), accumulates a `(span, ty)` table for every expression node, binding name, function
   parameter, and pattern variable, then resolves each entry against the final substitution and renders
-  it. Bindings carry a `name_span`, and parameters / pattern variables carry their own spans, so a
+  it. Bindings carry a `target_span`, and parameters / pattern variables carry their own spans, so a
   function name hovers to its full inferred signature and a parameter hovers to its element type. A
+  destructuring binding records *both*: the whole target (hover the tuple, see the tuple's type) and
+  each name inside it, at its own span. A
   `##` doc attached to a top-level `let`/`type`/`extern` (DESIGN §7) is appended below the type when
   hovering the declaration name *or any reference resolving to it* (`resolve::symbol_at` → the item's
   `doc`); a documented symbol with no recorded type hovers to the doc text alone.
@@ -293,8 +295,11 @@ the project-wide cache. Diagnostics for a dependent are still *published* only w
 next analyzed; proactively re-publishing dependents' diagnostics on an import edit stays deferred.
 
 The AST changes that enable local navigation: function/binding parameters are `Param { name, span }`
-(was `Vec<String>`), `Pattern::Var { name, span }` (was `Var(String)`), and the
-`CeItem::Let`/`LetBang` variants carry a `name_span`. The spans are `NodeSpan` (which compares equal
+(was `Vec<String>`), `Pattern::Var { name, span }` (was `Var(String)`), and `LetBinding` and the
+`CeItem::Let`/`LetBang` variants carry a `target: Pattern` plus its `target_span` (each was a
+`String` name and its span, before a binding could destructure — `LetBinding::name()` is the
+plain-name shortcut every phase keeps for the common case, and `bound_names` / `bound_vars` are how
+a phase asks for *all* of them). The spans are `NodeSpan` (which compares equal
 unconditionally), so roundtrip/structural equality is unaffected; lowering erases them (`param_names`).
 
 Deferred: *truly* incremental reparsing — an edit still re-analyzes the whole document — and

ROADMAP.md

@@ -197,22 +197,22 @@ the higher-value of the two.
    `Option` builder as its worked example, gaining a line saying the built-in does this with a flat
    lowering and you are rebuilding it to see the mechanism, which documents why built-ins exist at all.
 
-9. **A `let` binding cannot destructure** (M) — `let (r, c) = parseCoord tok` does not parse anywhere in
-   the language: `LetBinding` carries `name: String` (`src/parser/ast.rs:289`) and so does
-   `CeItem::LetBang` (`:604`). It surfaced inside a CE body, where it forces a `match` that exists for
-   no reason other than to take a tuple apart, but it is not a CE papercut: top-level `let`, block `let`,
-   and CE `let`/`let!` all have it, and Python spells this `a, b = f()`. That makes it the broader of the
-   two findings and the one that pays out at every binding site.
-
-   Fix: `let` (and `let!`) accept an **irrefutable** pattern — tuples, single-constructor records,
-   wildcards, and nestings of those. Refutable patterns stay at `match`, which keeps "the compiler is the
-   gatekeeper, no runtime surprises" intact and makes the restriction explainable in one sentence. The
-   work is spread thin rather than deep: the parser stores a `Pattern` where it stores a name today, and
-   every path that asks what names a binding introduces (lowering's scope scan, the mutation and effect
-   checks, the LSP resolver) has to learn that one `let` can introduce several. The editor side should be
-   mostly free, since `Pattern::Var { name, span }` and `resolve::walk_pattern` already exist for match
-   arms. Emitted output is a plain Python tuple unpacking, so this costs nothing in readability — and on
-   top of #8 it is what removes the last lambda from a chained-`Option` function.
+9. ~~**A `let` binding cannot destructure**~~ **CLOSED 2026-08-02** (was M, reported the same day) —
+   `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!`.
+   `LetBinding` and `CeItem::Let`/`LetBang` carry a `Pattern` where they carried a `String`, with
+   `bound_names`/`bound_vars` on the AST as the one place every phase asks what a binding introduces.
+   The irrefutability rule turned out to already exist — `parser::refutable_in_param`, renamed
+   `refutable_shape` and now shared — so a `let` target admits exactly what a parameter does (a name,
+   `_`, tuples, records, nested) and rejects the rest 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. Lowering reuses `unpack_into`, so `let (r, c) = e` emits `r, c = e` with no temp, a nested
+   target reads through a reserved base (`_pf_t0_1`, never a name derived from the user's), a record
+   target reads one attribute per field named, and a destructuring `let!` in `result` rides inside the
+   `Ok` pattern it already matches (`case Ok((r, c)):`) for no extra statement. Each bound name
+   generalizes on its own, matching the single-name case. Canonical `DESIGN.md` §7; lesson 8 covers it;
+   the tree-sitter grammar accepts the new targets (and destructuring *parameters*, which the language
+   had but the grammar did not).
 
 ## Deferred (real features, no current demand — say the word and I'll scope it)
 

docs/src/learn/08-tuples.md

@@ -47,6 +47,54 @@ Tuples also bridge lists and maps. `Map.ofList` builds a `Map` from a list of pa
 `Map.toList` turns a map back into its pairs, so a zip followed by `Map.ofList` is a compact way to
 build a lookup table from two parallel lists.
 
+## Binding both parts at once
+
+When a pattern covers every value, as a tuple pattern does, a whole `match` is more ceremony than
+the job needs. A `let` takes the same pattern directly, which is how Python writes it too:
+
+```pyfun
+type Point = { x: int, y: int }
+
+let (name, score) = ("ada", 10)
+let (first, (second, third)) = (1, (2, 3))
+let Point { x, y } = Point { x = 3, y = 4 }
+
+let swap p =
+  let (a, b) = p
+  (b, a)
+
+print f"{name} scored {score}"
+print (first + second + third)
+print (x * y)
+print (swap (1, 2))
+```
+
+```console
+ada scored 10
+6
+12
+(2, 1)
+```
+
+A function parameter takes the same patterns, so `let line (name, score) = f"{name}: {score}"`
+binds both parts on the way in and skips the `match` from the previous example entirely.
+
+The rule in all three positions is that the pattern has to match every value of its type. Names,
+`_`, tuples and records qualify, and they nest. A constructor pattern does not, because it can
+fail:
+
+```pyfun
+let Some x = Some 1
+```
+
+```console
+error: a `let` binding must always match, so it takes a name, `_`, or a tuple or record of those,
+not a constructor pattern (use `match` instead, which has somewhere to fall through to)
+```
+
+That is the trade. `match` handles the patterns that can fail, because it has other arms to fall
+through to, and `let` handles the ones that cannot, because it does not.
+
 ## Lists destructure too
 
 The same `match` works over a `List`. A list pattern names elements in brackets, just like the

editors/tree-sitter-pyfun/grammar.js

@@ -71,13 +71,23 @@ module.exports = grammar({
     let_binding: $ => seq(
       'let',
       repeat(choice('mut', 'pure')),
-      field('name', choice($.identifier, $.wildcard)),
+      field('name', choice($.identifier, $.wildcard, $._binding_pattern)),
       repeat(field('parameter', $.parameter)),
       '=',
       field('body', $._body),
     ),
 
-    parameter: $ => $.identifier,
+    parameter: $ => choice($.identifier, $.wildcard, $._binding_pattern),
+
+    // What a binding position (a `let` target, a parameter, a CE `let`/`let!`)
+    // may destructure with. The compiler additionally holds these to
+    // irrefutability; the grammar stays permissive so code it rejects still
+    // highlights.
+    _binding_pattern: $ => choice(
+      $.parenthesized_pattern,
+      $.tuple_pattern,
+      $.record_pattern,
+    ),
 
     active_pattern_definition: $ => seq(
       'let',
@@ -515,8 +525,18 @@ module.exports = grammar({
       $.ce_yield,
     ),
 
-    ce_let: $ => seq('let', field('name', $.identifier), '=', $._expression),
-    ce_bind: $ => seq('let!', field('name', $.identifier), '=', $._expression),
+    ce_let: $ => seq(
+      'let',
+      field('name', choice($.identifier, $.wildcard, $._binding_pattern)),
+      '=',
+      $._expression,
+    ),
+    ce_bind: $ => seq(
+      'let!',
+      field('name', choice($.identifier, $.wildcard, $._binding_pattern)),
+      '=',
+      $._expression,
+    ),
     ce_do: $ => seq('do!', $._expression),
     ce_return: $ => seq(choice('return', 'return!'), $._expression),
     ce_yield: $ => seq(choice('yield', 'yield!'), $._expression),

editors/tree-sitter-pyfun/src/grammar.json

@@ -138,6 +138,10 @@
               {
                 "type": "SYMBOL",
                 "name": "wildcard"
+              },
+              {
+                "type": "SYMBOL",
+                "name": "_binding_pattern"
               }
             ]
           }
@@ -168,8 +172,38 @@
       ]
     },
     "parameter": {
-      "type": "SYMBOL",
-      "name": "identifier"
+      "type": "CHOICE",
+      "members": [
+        {
+          "type": "SYMBOL",
+          "name": "identifier"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "wildcard"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "_binding_pattern"
+        }
+      ]
+    },
+    "_binding_pattern": {
+      "type": "CHOICE",
+      "members": [
+        {
+          "type": "SYMBOL",
+          "name": "parenthesized_pattern"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "tuple_pattern"
+        },
+        {
+          "type": "SYMBOL",
+          "name": "record_pattern"
+        }
+      ]
     },
     "active_pattern_definition": {
       "type": "SEQ",
@@ -2566,8 +2600,21 @@
           "type": "FIELD",
           "name": "name",
           "content": {
-            "type": "SYMBOL",
-            "name": "identifier"
+            "type": "CHOICE",
+            "members": [
+              {
+                "type": "SYMBOL",
+                "name": "identifier"
+              },
+              {
+                "type": "SYMBOL",
+                "name": "wildcard"
+              },
+              {
+                "type": "SYMBOL",
+                "name": "_binding_pattern"
+              }
+            ]
           }
         },
         {
@@ -2591,8 +2638,21 @@
           "type": "FIELD",
           "name": "name",
           "content": {
-            "type": "SYMBOL",
-            "name": "identifier"
+            "type": "CHOICE",
+            "members": [
+              {
+                "type": "SYMBOL",
+                "name": "identifier"
+              },
+              {
+                "type": "SYMBOL",
+                "name": "wildcard"
+              },
+              {
+                "type": "SYMBOL",
+                "name": "_binding_pattern"
+              }
+            ]
           }
         },
         {

editors/tree-sitter-pyfun/src/node-types.json

@@ -1023,6 +1023,22 @@
           {
             "type": "identifier",
             "named": true
+          },
+          {
+            "type": "parenthesized_pattern",
+            "named": true
+          },
+          {
+            "type": "record_pattern",
+            "named": true
+          },
+          {
+            "type": "tuple_pattern",
+            "named": true
+          },
+          {
+            "type": "wildcard",
+            "named": true
           }
         ]
       }
@@ -1118,6 +1134,22 @@
           {
             "type": "identifier",
             "named": true
+          },
+          {
+            "type": "parenthesized_pattern",
+            "named": true
+          },
+          {
+            "type": "record_pattern",
+            "named": true
+          },
+          {
+            "type": "tuple_pattern",
+            "named": true
+          },
+          {
+            "type": "wildcard",
+            "named": true
           }
         ]
       }
@@ -2504,6 +2536,18 @@
             "type": "identifier",
             "named": true
           },
+          {
+            "type": "parenthesized_pattern",
+            "named": true
+          },
+          {
+            "type": "record_pattern",
+            "named": true
+          },
+          {
+            "type": "tuple_pattern",
+            "named": true
+          },
           {
             "type": "wildcard",
             "named": true
@@ -3388,6 +3432,22 @@
         {
           "type": "identifier",
           "named": true
+        },
+        {
+          "type": "parenthesized_pattern",
+          "named": true
+        },
+        {
+          "type": "record_pattern",
+          "named": true
+        },
+        {
+          "type": "tuple_pattern",
+          "named": true
+        },
+        {
+          "type": "wildcard",
+          "named": true
         }
       ]
     }