A def specialized at a finite parameter also goes to --verdict as a λ-match on it, so the kernel checks that each value has an instance that fits its type (#1186)

[nicolas-abril]

Fixes #1186. Follows up on #1213, closed in favour of this approach.

Cause

root_cols in bend2/safe.ts enumerates a template (~) parameter of a finite type (Quant, or a datatype whose constructors have no fields), and each value goes out as its own instance. Nothing checked that those instances cover the def, so --verdict trusted the enumeration. At an empty type there are no values: the def never reached the kernel, and --verdict still printed ALL PROOFS CHECK.

Fix

root_cols becomes root_emit, one walk over the def's telescope that emits each instance at its leaf (through item_try, as main does). A def with a finite ~ parameter also goes out once, at <()>, as a λ-match that checks its instances in erased lets:

• a λ-match on each finite parameter, annotated ∀y:A -> <()>;
• each arm names an instance, annotated with the def's own type G (a λ on its ~ parameters, bound once in a let) applied to that instance's arguments, and returns ().

So the kernel checks that:

• every value of A has an arm (at an empty type, that there are none: λ{});
• each instance an arm names fits the def's declared type at its own arguments: the kernel computes G v … itself, so a wrong substitution in tele_fill no longer cancels out.

It does not check which arm names which instance. If every arm named the first value's instance, only that instance would go out, under both labels, and --verdict would still pass.

Fallback. If the def's type calls a template at one of its ~ parameters, G can't go out, because those parameters are bound in it. spec_val raises Open_Error (a Scope_Error subclass: "a template argument that depends on a run-time value"), what G registered is undone, and the arms name their instances unannotated. There, coverage still holds, but no instance is checked against G. Only Open_Error falls back: any other reason G can't go out puts the def out of scope with that reason.

skip : <()> =
  !-x0 = {λ-x0 => ∀x1 : Nat -> Nat : ∀-x0 : Void -> *(.Q1)}; !-x1 = {λ{(,): λ{}} : ∀x2 : Void -> <()>}; ()
same : <()> =
  !-x0 = {λ-x0 => {x0 == x0 : Bool} : ∀-x0 : Bool -> *(.Q1)}; !-x1 = {λ{(,): λ{.False: λ{(): !-x2 = {same.qv : (x0 -(.False, ()))}; (); λ{}}; λ{.True: λ{(): !-x2 = {same.qv_1 : (x0 -(.True, ()))}; (); λ{}}; λ{}}}} : ∀x2 : Bool -> <()>}; ()
wrap : <()> =
  !-x1 = {λ{(,): λ{.False: λ{(): !-x2 = wrap.qv; (); λ{}}; λ{.True: λ{(): !-x2 = wrap.qv_1; (); λ{}}; λ{}}}} : ∀x2 : Bool -> <()>}; ()

(wrap is the fallback: no G, bare names.)

Reporting. A root is out of scope at each distinct reason its instances are out for; else at its λ-match's reason; else, when neither went out, at no kernel def. An instance out of scope reports its own reason (- flip: uses the @unsafe def flip), and the good instances still go out. The last case is the guard against a revert of this fix: if the λ-match stops going out for a def with no instances, --verdict fails with - skip: no kernel def instead of passing.

The instances, the enumeration and how callers pick instances are unchanged. Only defs branch: since main's root_cols rewrite, a datatype's parameters never do. The match on a Σ chain's unit is one helper, unit. The chain of λ-match arms is another, mats, shared with adt_emit and group_emit. Quant's kernel labels are spelled once, in QS, and the unit type and value once, in UT and UV.

undo now pops a log of the keys emission added (put logs each new key in names, seen, taken and fail), instead of copying every key of those four. It costs what it removes, which matters now that a failed root and the G fallback undo too. Each ~ column's kernel term is made once for every leaf below it.

Checks

At head a29f0c62 (macOS):

• tests/check/spec_finite_match.bend adds size (the fallback when the template is called at a ~Nat parameter, which goes out at a constant) and both (two Quant parameters). --verdict prints ALL PROOFS CHECK.
• -o .bendtt on all 1223 files of tests/, demos/, bench/ and evals/ that elaborate: byte-identical to 29777d11 except spec_finite_match.bend, where only the λ-match codomain and arm values changed. With logging on the fallback, the only def in that corpus that takes it is wrap, with Open_Error, so narrowing the catch changes no output.
• Probes, all ALL PROOFS CHECK: an alias type, two Quants, a non-finite ~ before a finite one, a native op in the law type, an empty type between two finite ones.
• Kernel negatives, by hand-editing the .bendtt: an instance annotated at the wrong G arguments, a dropped Quant arm, and an arm at Void each give SOME PROOFS FAIL.
• An injected non-Open_Error Scope_Error while building same's G gives - same: injected (out of scope), while wrap still falls back.
• tsc: no new errors.
• Gates: repo 54/54, test 1625/1625, perf 124/124, ping 57/57 (bashka check skipped: not installed).
• Cluster gates/safe.ts tests (1636 files, 26 nodes): 1054 agree, 88 unsafe, 490 bend2 rejects, 4 out of scope, 0 false rejects, 0 timeouts, 0 infra. The table is identical, line for line, to the 29777d11 run; spec_finite_match.bend agrees.
• Not run: the hub corpus.

At head 29777d11, rebased on d0cb504e:

• tests/check/spec_finite_match.bend (new): the issue's repro (skip, ~v: Void), a ~ Bool (same), a kind that depends on the parameter (look), a later ~ parameter whose type names the first one (pick), an empty type after a ~ Bool (late), a Quant parameter (mode), and the fallback (wrap). Here, skip, same, look, pick, late, mode and wrap all go out and --verdict prints ALL PROOFS CHECK. On main, skip and late are missing from the .bendtt and --verdict still prints ALL PROOFS CHECK.
• Revert check: with the λ-match forced off (if (!fin) → if (true) in root_emit; now if (G === undefined)), --verdict on that file fails with - skip: no kernel def and - late: no kernel def. No gate runs this: the test gate doesn't run --verdict, and gates/safe.ts only tallies out-of-scope files. So the guard bites when --verdict is run on this file.
• -o .bendtt on the other 1635 test files gives byte-identical output to main (d0cb504e), including the out-of-scope lines (33 files on both).
• Gates on macOS: repo 54/54, ping 57/57, test 1625/1625, perf 124/124.
• Cluster gates/safe.ts tests on 29777d11 (1636 files, 26 nodes): 1054 agree, 88 unsafe, 490 bend2 rejects, 4 out of scope, 0 false rejects, 0 timeouts, 0 infra. Main gives the same table file by file, except tests/io/file_write_zero.bend, which main's run marks unsafe. That file comes from fix(io): fail file writes on zero progress #1446, which is newer than this branch's base.
• Not run: the hub corpus (needs a pulled hub store), Linux, CUDA, Metal.
• safe.ts grows from 22,578 to 23,500 ttok at 29777d11, 23,564 at a29f0c62 (cap 24,000). comp.ts is unchanged.

Limits and costs

• No check ties an arm's label to the instance it names (see above).
• In the fallback (a template call at a bound ~ parameter), no instance is checked against the def's type.
• The no kernel def guard fires only when a def reaches no kernel def at all. A λ-match dropped for a non-empty type would leave the instances checked, and nothing would flag the missing coverage check.
• A template whose ~ column is empty at some value of an earlier finite ~ parameter (for ~b: Bool; for ~h: {b == True{} : Bool}) is out of scope even when the body never uses h, since G names every column's constant. On main it is out of scope once the body uses h. Tracked in safe: refute empty ~ columns in a specialized def's cover instead of leaving it out of scope #1544.
• One extra def per root with a finite parameter. G goes out once per root, and each arm adds an annotation and its value.

🤖 Generated with Claude Code

[Lorenzobattistela]

I ran this locally, merged onto main 1159f0b, and through a /code-review pass. The approach is the right follow-up to #1213, and it holds up: spec_finite_match passes --verdict, and skip, same, look and pick all go out with their covering defs (on main skip is missing from the .bendtt). -o over all 1,558 test files runs with no crash. I haven't run the cluster gates. Two things to fix before merging, and one question.

The match path skips item_try (the Reroute retry, and each instance kept apart)

root_emit's body calls item_ref(e, k, r.cols, true) directly. Since this branch's base, #1215 put a Reroute retry in item_try (safe.ts:271 on main), and safe_book's loop only catches Scope_Error. So once this is rebased, an instance at a finite value that ends up on a rerouted cycle throws an uncaught Reroute from --verdict/-o instead of regrouping. I couldn't reach that from a test, but nothing rules it out.

The same call also changes what happens when an instance fails. On main each instance went through item_try: a failing one was listed out of scope and the rest still went to the kernel. Here the first failing arm throws out of root_emit, so the later instances are never emitted or checked, and the out-of-scope line doesn't say which value failed. The PR lists the single line under Costs, but the instances you lose go further than that.

Using item_try in body fixes both. A failing instance keeps its own reason, and the covering def goes out of scope through it, by the usual rule that a def naming an out-of-scope def goes with it. One related nit: fresh(e, name_tt(k)) is reserved before ty/body can throw, so on Scope_Error the catch at safe.ts:172 reserves k_ as well, and the first name is never used.

The test can't fail on main

spec_finite_match.bend only checks that main prints 3n, which main also does. gates/safe.ts scores main as agree: it prints ALL PROOFS CHECK while skip is silently missing. If root_emit went back to main's behaviour, every gate would stay green, so #1186 can come back unnoticed. I don't see a way to pin this without some check that a non-Base def reached the kernel. That's a gate change, so probably a question for Taelin, but it's worth saying in the PR that the test documents the fix rather than guarding it.

Question: what does the kernel actually check here?

Each arm of the covering def's type is that instance's own type_drop type, and a datatype's arms come from the same adt.c that root_of enumerated. So the kernel checks that the match is exhaustive over A and that each instance fits its own arm. It doesn't check against k's declared ∀ type: a wrong substitution in type_drop would land on both sides and still check. For Void the kernel sees λ{(,): λ{}} and still never sees skip's body, which I think is intended per your #1213 comment. If that's the claim, say so in the header comment, i.e. "the instances cover A's values". The current wording, "so the kernel checks that they cover it", reads stronger than that.

Smaller

• mat labels Quant arms by array index ("Q" + String(i)) and re-reads the datatype's c, so it silently depends on root_of's [None, Lone, Many] order and on adt.c order. Keeping the values in the Mat node and labelling from them removes that coupling and the second lookup.
• The covering type inlines every instance type, retranslated, with a nested annotated match at each level. That's the product of the finite parameters: three Quant parameters give 27 instance types in one def. The largest one in the test corpus is already a 1,342-char line. Referring to each instance's type would keep it linear.
• mat's Prj/Mat/unit chain is a third copy of the shape in group_emit's sel and adt_emit, and efq is still defined separately in root_emit and group_emit now that unit builds its own.
• The branch is 45 commits behind main, and safe.ts changed a lot since (Resolve BendTT recursive groups by membership (#1212) #1215, Bound BendTT model search and retain finite alternatives (#1181) #1218, A fallback past a type's last constructor goes to --verdict as \{}, as bend2 skips it, so a ~ argument or a type that has one checks (#1204) #1246). It merges cleanly as text, but the numbers in the description (974/552, the 41 covering defs, ttok 20,893) need re-measuring on current main.

[nicolas-abril]

Unsupervised AI action: rebased by an AI agent, no human checked it.

Rebased onto main d71f42e (fix(io) quiet exit, #1492). The four commits are kept as they were (old head 1d36887, new head 58e1426). Only bend2/safe.ts had conflicts:

• root_of now follows main's root_cols: it stops at tld.n, and only a template (~) parameter (j < tld.x) branches. spec_of is gone on main. The shared ~ constants from Roots share their ~ constants, so a template goes to the kernel once instead of once per root that uses it #1358 are unchanged.
• type_drop is gone on main. An instance's type in the covering def is now B.tele_fill(e.book, tld.T, cols.slice(0, tld.x), ctx_nil), the same type def_emit gives that instance.
• Since BendTT: kinds as quantity terms, meets, Σ at any kind and subsumption under ∀; --verdict emits generic defs once #1203, Typ holds a quantity term. The arms' motive *1 becomes *(.Q1), i.e. { $: "Typ", q: { $: "Lab", k: "Q1" } }.
• The header comment is merged with main's new kind/quantity paragraph.

None of the review's points were addressed in this rebase. body still calls item_ref directly, not item_try.

Checks (macOS, Bun 1.3.14):

• gates/repo.ts 54/54, gates/test.ts 1603/1603, gates/ping.ts 47/47 (bashka skipped).
• --verdict on all 1,614 test files matches main: 1,033 check, 581 fail. The new test is the only difference: main has no copy of it, and here it checks.
• -o .bendtt on every other test file is byte-identical to main, including the out-of-scope lines. No other test file has a finite ~ parameter now.
• The kernel rejects three tampered versions of the new test: a missing arm, swapped look instances, and a cover over Bool that claims it is empty.
• C and JS for bench/runtime/*/main.bend are byte-identical.
• Timing is the same as main: hyperfine of plain check and of --verdict stays within noise.
• comp.ts is unchanged (63,929). safe.ts goes from 22,287 to 23,026 (cap 24,000).
• The cluster gates (gates/safe.ts) and the hub corpus weren't run.

[nicolas-abril]

@Lorenzobattistela, thanks for the review. 7a5ef60, rebased onto main 381dc87, addresses it:

• item_try: root_emit's body now calls item_try, so a Reroute retries and a failing instance keeps its own reason. The covering def goes out of scope because it names that instance. For example, an @unsafe def at ~b: Bool now reports names flip.qv, out of scope: uses the @unsafe def flip. fresh now runs after the type and body are built, so no name is reserved and then lost.
• The test: agreed, it can't fail on main. The test header and the description now say that it documents the fix and doesn't guard it. Guarding it needs a gate change.
• What the kernel checks: the header comment, root_emit's comment and the description now say that the kernel checks that the instances cover the parameter's values, each at its own type, and not k's declared type.
• Quant order: the Mat node keeps its values, and the arms are labelled from them ("Q" + quant(q), or the constructor's name). The second adt.c lookup is gone.
• Duplication: a new helper, mats(ks, h), builds the λ-match chain. root_emit, adt_emit (D.arms) and both of group_emit's selector matches use it, and the separate efqs are gone. Sharing it saves 92 tokens compared with keeping it local.
• Covering type size: not changed. It is linear in the number of instances, but those are the product of the finite parameters. Referring to each instance's type would need a type def per instance, or would change the instance defs, which are currently byte-identical to main.
• Stale numbers: re-measured on current main. -o .bendtt is byte-identical to main everywhere except the new test, since no other test file has a finite ~ parameter now. safe.ts goes from 22,386 to 23,192 ttok. The description has the details.

Gates on macOS: repo 54/54, ping 55/55, test 1605/1605, perf 124/124. Every .bendtt is byte-identical to the previous head. The cluster --verdict gate wasn't run.

_{Unsupervised AI review/action.}

[nicolas-abril]

Pushed ec37001 on top of 2a90300 (bend2/safe.ts only):

• root_emit returns the covering def's name apart from its instances. Out-of-scope reasons come from the failing instances, and from the covering def only when no instance failed. This replaces ws.slice(0, -1), which relied on the covering def coming last.
• G is now two-state (the type, or null if it can't go out). A separate fin flag says whether the def has a finite parameter.
• A def that throws a scope error partway is undone (trail/undo), so it leaves no partial output.
• mats builds Efq directly; unit is mats(["()"], ...). Wrapped the long lines I touched (159 over 80 cols, main 160).

Checks on a merge with main 4ff8545: repo 54/54, ping 55/55, test 1607/1607, perf 124/124. All 1618 test files compile to byte-identical .bendtt output and logs before and after this commit. tsc --strict shows the same 5 errors as main. safe.ts is 23,340 ttok (cap 24,000; was 23,290).

Not done: the cluster --verdict gate (no bendtt binary on this machine), and the new test still passes on main.

_{Unsupervised AI review.}

[Lorenzobattistela]

Thanks. ec37001 reads better, and the outputs are the same as 2a90300 (every .bendtt byte-identical, gates green). The undo after a partial failure is correct.

One regression:

• The "no kernel def" guard is gone. On 2a90300, a root with no instances and no cover reported - skip: no kernel def. Now root_emit returns [] in that case, so --verdict prints ALL PROOFS CHECK and skip is missing from the .bendtt. That's the exact --verdict passes a def that the kernel never checks #1186 revert, and the safe.ts header and PR body still promise the guard. Real code doesn't reach that case today, but it's the only safety net for a revert. Something like ws.length > 0 ? ws : top !== null ? why(top) : ns.length > 0 ? [] : ["no kernel def"] brings it back. With it, dropping the cover fails again.

Still open from the last round:

• Wording. The header, the root_emit comment, the test header and the PR body say the kernel checks that the arm under label v was built for v. It doesn't: if every arm uses the first value's column, only same.qv goes out, it's named under both labels, and --verdict still passes. Please describe what's actually checked: every value has an arm, and each named instance fits G at its own arguments.
• Fallback. Any Scope_Error while G is built silently drops to the unannotated fallback, not only the template-call case. There, any arm can name any instance. Please narrow the catch or document it.
• Tests. Please add an empty type after a ~ Bool, a Quant parameter, and a fallback case. Nothing currently fails if the fix is reverted.
• PR body. Mention the undo, and update the "Dropping the cover fails…" line.
• Please run the cluster gates/safe.ts and the hub corpus before merging.

None of this is a soundness hole on main's paths. The #1186 fix itself holds.

[nicolas-abril]

Known regression, left as is on purpose: a template whose ~ column is empty at some value of an earlier finite ~ parameter is now out of scope even when the body never uses that column. For example for ~b: Bool; for ~h: {b == True{} : Bool} with body 1n: main prints ALL PROOFS CHECK, and this PR prints no model for only_true~h. That's because the cover's G annotation names every column's constant. On main the same def is already out of scope once the body uses h. The fix, refuting the leaf in the kernel with an absurd, is tracked in #1544.

[nicolas-abril]

Thanks @Lorenzobattistela. Pushed 29777d11 (rebased on d0cb504e, over ec37001d):

• Guard. Back. A root is out at its instances' reasons, else its λ-match's, else no kernel def (9a218d9c). With the λ-match forced off, --verdict on spec_finite_match.bend fails with - skip: no kernel def and - late: no kernel def.
• Wording. The header, the root_emit comment, the test header and the PR body now say what is checked: every value has an arm, and each named instance fits G at its own arguments. They also say what isn't: which arm names which instance.
• Fallback. Documented, not narrowed: any Scope_Error while building G undoes it and names the instances bare. The comment and the PR body say so.
• Tests. Added to spec_finite_match.bend: late (an empty type after a ~ Bool), mode (a Quant parameter), and wrap (the fallback: its type calls Two(~b), so G can't go out and the arms are bare). On main, skip and late are missing from the .bendtt and --verdict still passes. A revert still passes every gate, because no gate runs --verdict to failure on this file.
• PR body. Rewritten: the undo, the fallback, the revert check and the limits.

-o .bendtt output for the other 1635 test files is byte-identical to main. macOS gates pass (54/54, 57/57, 1625/1625, 124/124). safe.ts is at 23,500 ttok (main 22,578, cap 24,000). Edit: the cluster gates/safe.ts tests now runs on 29777d11: 1054 agree, 88 unsafe, 490 bend2 rejects, 4 out of scope, 0 false rejects, 0 timeouts, 0 infra. That matches main file by file, except tests/io/file_write_zero.bend, which main marks unsafe. That file comes from #1446, which is newer than the branch base. The hub corpus is not run yet because it needs a pulled hub store.

(Changes and this comment by an AI agent, at Nicolas's direction.)