From fdb9aa550a33e8fbdc0d125f99dd36a38aec8ea4 Mon Sep 17 00:00:00 2001
From: Dev Chiniwala <dev.chiniwala@gmail.com>
Date: Wed, 28 Oct 2026 14:13:01 +0530
Subject: [PATCH] fix: reject rest parameters in callback lambdas

Reject rest parameters in expression arrow lambdas before their argument
collection semantics are lost. Preserve named variadic declaration
metadata, document the boundary, and cover unsupported and supported
callback forms with regressions.
---
 SPEC.md                                   |  2 +
 tools/src/extract.ts                      |  3 ++
 tools/tests/arrow-rest-parameters.test.ts | 56 +++++++++++++++++++++++
 3 files changed, 61 insertions(+)
 create mode 100644 tools/tests/arrow-rest-parameters.test.ts

diff --git a/SPEC.md b/SPEC.md
index e800a8d..26eff28 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -645,6 +645,8 @@ Lambda bodies can be expressions (`(x) => x + 1`) or statement blocks (`(x) => {
 
 Flat object destructuring in a lambda parameter is supported, including aliases (`({ id, hidden: isHidden }) => ...`). It remains one callback parameter and lowers to immutable field bindings inside the lambda. Array patterns, nested object patterns, defaults, and rest properties are rejected during extraction with an explicit unsupported-pattern error.
 
+Arrow lambdas used as expressions reject rest parameters during extraction: the lambda model does not collect callback arguments into a rest array.
+
 **filterMap.** `xs.map(x => ... | undefined).filter((x): x is T => x !== undefined)` drops the `undefined`s *and* unwraps to `seq<T>` — lowered to the proven `SeqFilterSome` preamble (a plain `Map(.value, Filter(.Some?, ...))` wouldn't verify, since `.value` is partial).
 
 **`.map` (Dafny).** Lowered to a `seq` comprehension with the element access inlined (`var x := arr[i]; e`), not `Seq.Map`. `Seq.Map` hides the element behind a closure, so a recursive rebuild walker (`Node(kids.map(walk))`) fails Dafny's termination check — the obligation gets quantified over the lambda's parameter instead of anchored at `kids[i]`. Applying a lambda inside the comprehension fails the same way, hence the inlining.
diff --git a/tools/src/extract.ts b/tools/src/extract.ts
index 795cd28..d0c1613 100644
--- a/tools/src/extract.ts
+++ b/tools/src/extract.ts
@@ -541,6 +541,9 @@ function extractExpr(node: Expression): RawExpr {
     // generated backend identifier.
     const destructureBindings: RawStmt[] = [];
     const params = node.getParameters().map((p, paramIndex) => {
+      if (p.isRestParameter()) {
+        throw new Error(`rest parameter in arrow lambda not yet supported: ${p.getText()}`);
+      }
       const typeNode = p.getTypeNode();
       const tsType = typeNode ? typeNode.getText() : undefined;
       const nameNode = p.getNameNode();
diff --git a/tools/tests/arrow-rest-parameters.test.ts b/tools/tests/arrow-rest-parameters.test.ts
new file mode 100644
index 0000000..e9192f3
--- /dev/null
+++ b/tools/tests/arrow-rest-parameters.test.ts
@@ -0,0 +1,56 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { Project, ScriptTarget } from "ts-morph";
+import { extractModule } from "../src/extract.ts";
+
+function extract(text: string) {
+  const project = new Project({ compilerOptions: { strict: true,
+    target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } });
+  const source = project.createSourceFile("rest.ts", text);
+  assert.deepEqual(project.getPreEmitDiagnostics(), [], "input must be valid TypeScript");
+  return extractModule(source);
+}
+
+test("map callbacks receive three arguments, rather than the array element's contents", () => {
+  const counts = [[7]].map((...args: (number | number[] | number[][])[]) => args.length);
+  assert.deepEqual(counts, [3]);
+  assert.deepEqual([[7]].map(value => value.length), [1]);
+});
+
+for (const [name, source] of [
+  ["map expression callback", `export function counts(): number[] {
+    return [[7]].map((...args: (number | number[] | number[][])[]) => args.length);
+  }`],
+  ["map block callback", `export function counts(): number[] {
+    return [[7]].map((...args: (number | number[] | number[][])[]) => { return args.length; });
+  }`],
+  ["some callback", `export function count(): boolean {
+    return [[7]].some((...args: (number | number[] | number[][])[]) => args.length === 1);
+  }`],
+  ["fixed parameter followed by rest", `export function counts(): number[] {
+    return [7].map((value, ...tail: (number | number[])[]) => tail.length);
+  }`],
+] as const) {
+  test(`extraction rejects rest parameters in a lambda: ${name}`, () => {
+    assert.throws(() => extract(source), /rest.*(lambda|arrow)|(lambda|arrow).*rest/i);
+  });
+}
+
+test("ordinary array parameters and object bindings remain supported", () => {
+  assert.doesNotThrow(() => extract(`
+    export function lengths(xs: number[][]): number[] { return xs.map(value => value.length); }
+    export function fields(xs: { value: number }[]): number[] { return xs.map(({value}) => value); }
+    export function many(xs: number[]): number[] { return xs.map((value, index) => value + index); }
+  `));
+});
+
+test("named variadic declarations retain their rest grouping metadata", () => {
+  const module = extract(`
+    export function named(...values: number[]): number { return values.length; }
+    export const arrow = (...values: number[]): number => values.length;
+  `);
+  assert.equal(module.functions.length, 2);
+  for (const fn of module.functions) {
+    assert.deepEqual(fn.tsParams, [{kind: "rest", binds: ["values"]}]);
+  }
+});