[nicolas-abril]

Fixes #1179.

Cause

spec_of in bend2/safe.ts decides which parameters of an item are specialized. On main it cached [] for an item while that item was still being computed, so any read before the answer was known counted as "nothing specialized". That happens with a later declaration (A before B), with a self-recursive type, and with a two-way cycle. A parameter that only a cycle makes specialized stayed live, and --verdict rejected its kind as "a kind that depends on a run-time value". Reordering can't fix the self-recursive or two-way cases.

Once cycles specialize correctly, a second problem shows up. A specialized parameter can recur at a bigger argument each time, and item_ref then names instances without end:

file	main	first version of this PR (f54dc5f)	this PR
S<n, m> with a field S<List<m>, n>	out of scope	hangs	out of scope
T<n> with a field T<List<n>>	hangs	hangs	out of scope
U<n: Nat> with a field U<1n+n>	hangs	hangs	out of scope
A<n> → B<List<n>> → A<m>	out of scope	hangs	out of scope
def f(c: Nat, n: Type, -A: Kind(qof(n))) calling f(p, List<n>, Unit)	stack overflow	stack overflow	out of scope

Fix

Which parameters are specialized is a reachability. The rules are:

• Seeds: a Quant or ~ parameter, or a variable that a kind reads.
• Flows: r's parameter j is specialized when its variable sits inside an argument at a specialized parameter i of h.

The least set these rules close is a graph reachability. spec_of walks each item's types once to collect its seeds and flows, then spreads the seeds along the flows. The answer can't depend on declaration order, and no item is computed twice: a book makes as many item computations as on main (a chain of 300 types: 303).

An instance that grows on one above it is out of scope. item_ref records which instance named each new one. A new instance is out of scope (a specialized argument that grows at each instance of S) when its arguments hold the arguments of an instance of the same item above it on that chain.

• Holds is a homeomorphic embedding: S~n is held in List<S~n>. A number holds a no bigger one, and a string literal holds one it contains in order.
• By Kruskal's theorem, every endless chain of instances has such a pair, so every row of the table ends.
• A finite cycle like S<m, n> has none, and neither does a shrinking index: V<3n> with a field V<Nat.sub(n, 1n)> still goes out, as its 4 instances.
• Each pair of parts is decided once, so a check costs |t|·|u|. A shrinking list of 24 equal heads takes 0.2 s.
• A bit per item along each chain skips the walk when the item isn't above. Only instances at specialized arguments get an entry, so memory stays at main's (defs_12800 peaks at 485 MB on both).

Known limit. The check is conservative and fails closed. A closed counter that cycles back down, such as M<Nat.mod(1n+n, 3n)> used at M<0n>, is reported out of scope even though it has only 3 instances. Main doesn't finish on that file at all: M's root instance at its opaque constant grows without end.

Size: safe.ts goes from 21,624 to 22,699 ttok (the cap is 24,000).

Checks

All run on this branch merged with main 08a6083.

Tests

• tests/check/spec_cycle.bend covers A-before-B, a self-recursive type and a two-way cycle, each also used at closed arguments. Main gives SOME PROOFS FAIL; this PR gives ALL PROOFS CHECK.
• tests/check/spec_grow.bend covers every growth case in the table, plus three that must stay in scope: V<3n>, a list of 24 equal heads, and a "ab"/"ba" flip. Main overflows the stack on it, the previous head of this PR times out after 60 s, and this PR finishes in 0.2 s.

Corpus

• Every .bend file in tests, demos, bench and guide (1,629) was emitted with -o on main and on this branch. Exit codes match, the 1,123 files that compile give byte-identical .bendtt, and the rest fail with the same messages.

Gates

• gates/test.ts: PASS: 1548 / 1548.
• gates/safe.ts tests: the same row for every existing file as main 08a6083 (992 agree, 1 false reject agree_32). The new rows are spec_cycle.bend agree and spec_grow.bend out of scope.
• gates/repo.ts: passes.
• Only gates/safe.ts runs these tests under --verdict, and it reports classes without failing, so a regression shows up in its table rather than as a failed gate.

Timing

• Whole -o runs are within noise of main on defs_12800, demos/app_pong_game_2d/PROOF.bend and a chain of 300 types.
• The growth check itself takes 10 ms on defs_12800, 20 ms on the chain and 40 ms on a type with 400 fields.

#1180 (binder levels in spec_of) is separate and not addressed here.

🤖 Generated with Claude Code

[nicolas-abril]

Code review of f54dc5f. The fixpoint itself looks correct: answers only grow, a recursive spec_of call can't happen, reads are recorded correctly, and the loop over the Set worklist stops. There are five findings. Only the first was confirmed by running it; the other four are about speed and test coverage, and weren't measured.

1. A type that recurses at a growing argument now hangs where main fails cleanly (confirmed). safe.ts:387

type S<n: Type, m: Type> is Kind(qof(n)):
  S1{s: S<List<m>, n>}

• main: -o exits 0 with S: a kind that depends on a run-time value.
• this PR: m is now specialized, so S is instantiated at (S~n, S~m), (List S~m, S~n), (List S~n, List S~m), and so on. It was stopped after 60 s (exit 124). --verdict goes through the same path.
• What to fix: item_ref has no limit on how many instances it makes, and the one-parameter form (T<n> with a field T<List<n>>) already hangs on main. So the real fix is a limit, or a check for growing instance keys, in item_ref/e.todo. This PR only makes more books reach that hang.

2. spec_of allocates on every call, even when cached. safe.ts:353

It builds a Set, a Map and three closures on each call. It's on hot paths:

• args() calls it for every application of a named item;
• root_cols calls it once per parameter;
• group_emit calls it per member.

Since spec_of never calls itself, every cached answer is final, so returning the cached value first is safe:

const sp = e.spec.get(k);
if (sp !== undefined) return sp;

3. Every self-recursive datatype with a specialized parameter is computed twice. safe.ts:366

A constructor's return type reads the type itself with its own parameters, which can't change the answer. This is the PR table's 301→601 on the chain and 202→403 on the fan-in. Two ways to avoid the second pass for almost every datatype:

• don't record the type as its own reader when it reads itself with parameter j's variable at position j;
• or solve each strongly connected component once.

4. Each recomputation redoes work that doesn't depend on the fixpoint. safe.ts:386

It lowers the telescope and every constructor type again, calls tele_unbind again, and runs is_qnt(term_wnf(…)) on every parameter type, though only got changes between passes. Computing the lowered terms and the is_qnt/template mask once per item removes that cost for datatypes in a cycle with many constructors or large parameter types.

5. The regression test is only guarded by gates/safe.ts. tests/check/spec_cycle.bend:27

• gates/test.ts runs it without --verdict, and it passes on main too. Going back to caching [] while an item is computed would pass gates/test.ts and gates/repo.ts, and only a manual gates/safe.ts run would catch it.
• Nothing uses S/C/D at concrete arguments.
• Nothing covers a newly specialized parameter that recurses at a growing argument, so the hang in 1 went uncaught.

Note: this review was written by an AI at my request. If anything here is wrong, reply and I will review it myself.

[Lorenzobattistela]

Picked this up: f77b1c3 (on top of a merge of main 1159f0b) reworks the fix and closes the hang from the review above.

What was left

Once a cycle specializes its parameters correctly, a specialized parameter can recur at a bigger argument each time, and item_ref names instances without end:

file	main	f54dc5f	f77b1c3
S<n, m> with a field S<List<m>, n>	out of scope	hangs	out of scope
T<n> with a field T<List<n>>	hangs	hangs	out of scope
U<n: Nat> with a field U<1n+n>	hangs	hangs	out of scope
A<n> → B<List<n>> → A<m>	out of scope	hangs	out of scope
def f(c: Nat, n: Type, -A: Kind(qof(n))) calling f(p, List<n>, Unit)	stack overflow	stack overflow	out of scope

The reason given is a specialized argument that grows at each instance of S. The def case shows that growth also comes from def bodies, not only from types, so a check over types alone isn't enough.

The change

spec_of is a reachability. The specialized parameters are the least set closed under the rules, which is graph reachability:

• Seeds: a Quant or ~ parameter, or a variable that a kind reads.
• Flows: an edge from h's parameter i to r's parameter j when r's j sits inside an argument at h's i.

Each item's types are walked once to collect seeds and flows, and the seeds then spread along the flows. The answer can't depend on declaration order, and no item is computed twice. This replaces the redo worklist and covers findings 2–4 above:

• spec_of returns a cached answer first.
• A type that reads itself is no longer computed a second time.
• Nothing is lowered or unbound again.

Computation counts are back to main's (chain of 300 types 303, fan-in with 400 fields 404).

item_ref stops growing instances. It records which instance named each new one. A new instance is out of scope when its arguments hold those of an instance of the same item above it on that chain. Holds is a homeomorphic embedding: S~n is held in List<S~n>, and a number or a string literal holds a smaller one.

• Every endless chain of instances must contain such a pair (Kruskal's theorem), so every case in the table ends.
• A finite cycle like S<m, n> has no such pair, so it still goes out.
• A shrinking index has none either: V<3n> with a field V<Nat.sub(n, 1n)> goes out as its 4 instances.
• A bit per item along each chain skips the walk when the item isn't above. Without it, the walk took 10.7M steps on the fan-in; on the corpus it now takes 0.

Tests

• tests/check/spec_cycle.bend now also uses the cycles at closed arguments (B<Nat>, S<Nat, Bool>, C<Nat, Bool>).
• tests/check/spec_grow.bend (new) covers the growth cases above, plus V<3n>, which must stay in scope.
• As before, only gates/safe.ts runs these under --verdict.

Checks

• Corpus: -o on all 1,629 .bend files in tests, demos, bench and guide gives the same exit codes as main. The 1,123 that compile give byte-identical .bendtt, and the rest fail with identical messages. The only differences are the two new tests.
• gates/test.ts: PASS: 1548 / 1548.
• gates/safe.ts tests: same row for every file as main (992 agree, 1 false reject agree_32). The new rows are spec_cycle.bend agree and spec_grow.bend out of scope, as designed.
• gates/repo.ts: passes. safe.ts goes from 21,624 to 22,510 ttok (cap 24,000).
• Timing: whole -o runs are within noise of main on defs_12800, the chain of 300 types and demos/app_pong_game_2d/PROOF.bend. On the 400-field fan-in, the median was 2.48 s vs 2.41 s for main.

#1180 (binder levels in spec_of) is separate and not addressed here.

🤖 Generated with Claude Code

[nicolas-abril]

Superseded by #1203 (ffeddf0): spec_of now specializes only template (~) parameters, so the fixpoint this PR computes is gone. Its test spec_cycle.bend passes --verdict on that commit, and #1179 is closed.