[nicolas-abril]

What

The BendTT kernel can now express bend2's kinds as terms, and it fits function types by their parts, as bend2's LE does. --verdict no longer monomorphizes on quantities: a Quant parameter, and any parameter a kind reads, is an ordinary kernel variable, and each def goes out once, as bend2 writes it. Only template (~) parameters are still specialized.

Trust moves from bend2 to the kernel:

• no quantity is computed by bend2's evaluator before the kernel sees it;
• subsumption under ∀ is a proven kernel rule, not a bridge in safe.ts.

(This includes what was #1344.)

Rebased on main (bf96827, which includes #1339's Lean-versioned kernel cache). At this head: repo PASS 50 / 50, test PASS 1559 / 1559, and gates/safe.ts tests gives 1004 agree, 72 unsafe, 491 bend2 rejects, 2 out of scope and 1 false reject (#1193).

Closes and supersedes

Closes #1175, #1179 and #1180. Supersedes #1201 and #1208.

Each repro and test below fails --verdict on main and passes here.

	what it was	why it goes away
#1175	run3's generic root went out of scope: "a Quant that is not a literal" (the head annotation was fixed in 0187512; this was the open part)	the root is emitted once, with Kind(q1(f)) as a kernel term
#1179	spec_of's cycle guard under-approximated its fixpoint, so --verdict depended on declaration order ("a kind that depends on a run-time value")	spec_of only marks ~ parameters, so there is no fixpoint. ab.bend and self.bend both check, in either order
#1180	spec_of lowered each domain at depth 0, so an inner binder marked a later live parameter as specialized. Its second file silently dropped h	same; use checks, and h is now emitted and checked by the kernel
#1201 (PR, for #1175)	split a root stuck on a constant at the constructors or Quant literals it reads	nothing is stuck on a Quant constant any more. Both of its tests pass here: spec_root_split.bend checks, and so does spec_root_split_out.bend, whose ap_f and void_f it left out of scope; both are emitted and checked here
#1208 (PR, for #1179)	made spec_of a least fixpoint	the computation it fixes is gone; its test spec_cycle.bend checks here

Checked and not affected:

• --verdict passes a def that the kernel never checks #1186 / 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) #1225 (a ~ parameter of an empty type gets no root): ~ parameters are still enumerated, so it stays open.
• BendTT mismatch for opaque higher-order template with dependent equality result #1182 / The ~ constants of a root take models that hold together, so a ~ law of a ~ function reaches the kernel (#1182) #1263 (no model for an opaque ~F): it fails the same way on both.

Every Bend snippet in the 82 open issues (92 files) was also run under --verdict on main and here. #1175 and #1180 now pass. #984's chain and #1205's file now fail, as described under Elaborator.

Kernel (bend2/bendtt.lean)

• Typ carries a quantity term, as bend2's Kind(g) does: *(q) is the kind of a quantity q : <Q0, Q1, Q2>, with *1 = *(.Q1) (Type) and *2 = *(.Q2) (Data). Two kinds convert where their quantities do (conv_typ), as in bend2's EQ, so *(.Q0) and *(.Q1) are two kinds that fit each other. Like every type, a kind is dead: it is never evaluated.

• (a <&> b), the meet (minimum) of two quantities. It reduces as bend2's does: .Q2 is its identity and .Q0 absorbs, on either side, even next to a stuck quantity (Term.qmin). It may be live: Term.live and Term.uses read both sides, and a live meet steps to a label.

• Σ at any kind *(g), with each field at kindof(q, *(g)), and *(g) shifted under the field binder. So Either<a, b> is Kind(a <&> b) goes out as written.

• Fits is inductive, with these rules:

  • conversion;
  • kinds: *(g) fits *(h) when g is .Q2 wherever h is, under every substitution;
  • enums: fewer labels;
  • ∀q A B fits ∀q C D when C fits A and B fits D: the domain reversed and the codomain along, as in bend2's LE;
  • transitivity.

  The checker decides kinds with bend2's rules (qge): .Q2 is the top, .Q0/.Q1 the bottom, a meet on the left needs both sides, and a meet on the right needs either. Term.fits threads fuel, compares two ∀s' binder quantities first, and then fits them by their parts. qge_sound and fits_sound prove the checker against the rules.

• Fits.at / fits_at read a fit at a type former, in both directions: where T converts to a former, U converts to one of the same former whose parts fit. fits_all, fits_conv, fits2 and fits_former follow from it. Subject reduction and progress use them:

  • β casts the argument along the domains' fit and the result along the codomains';
  • a split, a hit and a miss do the same;
  • a λ-match on an enum may receive a smaller enum.

• Unchanged: binder quantities stay literal, so the live check still reads quantities off the syntax. A type of kind *(q) is Data only where q reduces to .Q2, so canon_data keeps its route.

• lean bendtt.lean checks with no sorry under Lean v4.34.0 (the pinned version) and v4.34.1. Every claim (consistent, book_check, confluent, sr, progress, halts, empty) depends only on [propext, Classical.choice, Quot.sound], as before. The claim statements are unchanged; the typing judgment they quantify over is more general.

• +5,146 ttok (58,839 → 63,985, cap 64,000). The next kernel change has to simplify first.

Elaborator (bend2/safe.ts, −415 ttok against main at 1a2e5cd: 21,749 → 21,334, cap 24,000)

• Kind(g) becomes *(g) with g's term, and a <&> b becomes (a <&> b), as bend2 writes them. A literal Kind(&0) and a generic Kind(q) at &0 are then one kernel term, *(.Q0): no quantity is raised to its rung.
• No quantity is folded, closed or not: the kernel computes every one itself, so --verdict does not trust bend2's evaluator for them. (main folded closed meets, and its specialized quantities, by bend2's evaluator.) Two consequences, both from the open issues' snippets:
  • A linear chain of quantity definitions makes kind checking exponential #984's chain q(n+1) = q(n) <&> q(n) up to q26 runs the kernel out of fuel, a false reject. The kernel does not share the two unfoldings of q(n), as bend2 does.
  • The unsafe/foreign gate misses an @unsafe dependency that appears only in a datatype's is Kind(..) #1205's Kind(qsize(Array.join(...))) names the @unsafe Array.join and fails, as The unsafe/foreign gate misses an @unsafe dependency that appears only in a datatype's is Kind(..) #1205 asks.
• A datatype's kind is emitted as a term.
• spec_of specializes template parameters only.
• A self-call's argument goes out whole when its binder quantities match the column's (qsig_eq), since the kernel fits domains, codomains and kinds itself. For example, K0 : Nat -> Kind(&0) passed at a Nat -> Type column is no longer η-expanded, and a rewrite goes out as written.
• uses counts both sides of a meet, as the kernel does: a meet is live code.
• kind() reads a closed kind's quantity to pick how a λ that uses its variable twice goes out: rebuilt when the kind is Type, and at q=2 when it is Data or open. For an open kind, the kernel decides; after a match, the kind may reduce to .Q2. It shares closed_val with spec_val, which no longer throws to say that a term is open.
• The quantity-only out-of-scope guards are gone: a Quant bound inside a match, a Quant argument to a variable, a type over Quant.

Now in scope

• A spliced inline lambda applied to a rebuilt column emits an un-annotated beta-redex, so --verdict rejects what bend2 accepts #1175's run3, and kinds that read nested fields: no splitting needed, so --verdict: split a root stuck on a constant at the constructors it reads (#1175) #1201 isn't needed either.
• A kind that reads a value through recursion, e.g. elem_q(stages) over a List.
• Quantities picked at run time: keep(pick(b), …) and meet(pick(b), …) with Kind(a <&> b), and a meet computed at run time (m(a, b) = a <&> b).
• Generic datatypes whose kind is a meet, and generic functions over them, each emitted once.

Hand-written books, run through the built kernel, check what should be rejected:

• a + copy of an Either of stuck kind, generic or Either .Q2 b, is rejected;
• a function type in a Data Either is rejected;
• a Data type passed at a stuck kind is accepted;
• through ∀, these are rejected: K : <A> -> *1 at <A> -> *2, ∀(∀ *1 -> <A>) -> <A> at ∀(∀ *2 -> <A>) -> <A>, a function on <A> at <A, B>, and a ∀ at a ∀+. Each fit in the sound direction is accepted, two levels of contravariance included.

Tests

• New tests in tests/check/, each passing --verdict here:
  • kind_terms.bend (fails on main), with a law on main's value. It covers everything above, plus a branch that relies on its kind, ∀ subsumption in both directions, and the equation {Kind(x <&> &2) == Kind(x)}.
  • kind_self_call_eta.bend (fails on main): a self-call passing Kq(q) : Nat -> Kind(q) at a Nat -> Type column.
  • Regression guards that main passes and this branch once failed:
    • kind_none_is_type.bend: the same self-call with Kind(&0).
    • kind_generic_none.bend: a generic kind at &0 against a literal Kind(&0), by a law and by a self-call.
    • meet_at_run_time.bend: a meet of run-time quantities in live code, with laws on every row of its table.
    • kind_domain_self_call.bend: a self-call passing g : Type -> Nat at a Kind(&0) -> Nat column.
    • kind_rewrite_goal.bend: a rewrite of type Nat -> Kind(&0) at a Nat -> Type goal.
    • meet_uses_in_arms.bend: a variable used inside a meet in one arm and again in another.
• Each rule for quantity terms in bendtt.lean was compared with bend2's. These agree: the meet's reduction, conv against EQ, fits against LE (now under ∀ too), Kind/Min typing, kindof against the binder, let, λ and constructor-field kinds, and the live check's usage of a meet. The last three regression guards above come from the three places where they did not. Two of those (the self-call's domains and the rewrite goal) are now decided by the kernel's ∀ rule.
• Known, harmless difference: Quant is an enum in the kernel, so it is Data there and Type in bend2; the kernel accepts more.
• Full local --verdict sweep over every file in tests/, on main, this branch before the fixes, and at each later head. The 1,554 files common to all of them get the same class on each (agree, unsafe, bend2 rejects, out of scope with the same reasons, false reject), and each new test agrees.
• tsc: the same 12 errors as main. gates/repo.ts: PASS 50 / 50.
• Cluster gates at 3548a98, rebased on 1a2e5cd:
  • gates/_run.ts: repo PASS 50 / 50, test PASS 1554 / 1554, all within the 30 s cap. perf reported PASS, but scored between 40 and 121 / 124 across today's runs, and main itself scored 49–89 / 124 back to back. This PR doesn't touch bend.ts, comp.ts or main.ts. ping was skipped: there is no site repo checkout here.
  • gates/safe.ts tests, on 26 nodes, side by side with main at 1a2e5cd: per file, identical to main's table plus the eight new tests/check files, all "agree". That is 1000 agree (992 on main), 71 unsafe, 491 bend2 rejects, 2 out of scope and 1 false reject (conversion_shared_cells_once, --verdict: the kernel runs out of fuel on conversion_shared_cells_once.bend, which bend2 checks by sharing (2.0.34) #1193), the same files on each.
  • Not run: gates/safe.ts hub (no BendHub store here).
• A fresh review of the final diff found no soundness issue. Its findings and what happened to each:
  • Fixed: the open-kind case of kind() (above), and the order of Term.fits's ∀ case.
  • Not reproduced: a law over Quant losing its model (a law with no body is a TODO, so bend2 stops first), and a nested domain quantity mismatch (bend2's LE rejects it too).
  • Known: see below.

Known limitations

• The kernel's meet evaluates its right side even when the left is .Q0, which bend2 skips. A costly right side can therefore run the kernel out of fuel where bend2 is instant: a false reject, never a false accept. Short-circuiting needs a wnf case and its proofs, and the kernel has 15 ttok left under its cap.
• A linear chain of quantity definitions makes kind checking exponential #984's chain q(n+1) = q(n) <&> q(n) runs the kernel out of fuel, also a false reject: the kernel does not share unfoldings as bend2 does.
• kind() still uses bend2's evaluator, but only to choose how a term goes out. Whatever it chooses, the kernel checks the result.

Performance

These are local measurements on an Apple M4 under background load, with the trees interleaved per file and per run in one process. Elaboration is safe_emit, kernel is the BendTT binary on its text, and figures are medians.

	elaborator	kernel
all 994 files bend2 accepts, sum of per-file medians (3 runs)	main 5,687 ms, this PR 5,974 ms (+5%)	main 19,945 ms, this PR 20,196 ms (+1%)
300 generic defs with Kind(a <&> (b <&> (a <&> b))), used at &2, &1 (15 runs, load average ~55)	main 76.9 ms, this PR 11.7 ms	main 44.6 ms, this PR 12.6 ms

On the test corpus the difference is within noise. Per-file ratios swing between 0.2× and 6× in both directions, and the sums move by a few percent. The corpus row was measured at 1a3fa1e, before the later commits. The stress row was measured before the ∀ rule, which emits the same text for that file. Kernel time with the ∀ rule was not measured separately. On kind-heavy code, emitting each def once instead of a copy per quantity cuts elaboration about 6× and kernel time about 3×.

Paper

bend2/docs/BendTT/main.typ and paper/BendTT.pdf (rebuilt with typst 0.15.1, now 10 pages) describe the kernel as it now is:

• kinds over quantity terms, *(g) and (g <&> h), with Q = <Q0, Q1, Q2>;
• Σ at any kind, and the kind case of U <= T with the checker's rules for it;
• the SORT and MEET rules;
• the meet's evaluation step and its place in the live check and in the measure;
• *(g) ≡ *(h) only when g ≡ h;
• generic defs going out once;
• the ∀ rule of U <= T, and subject reduction reading a fit at a former.

It said the compiler emits a copy of each generic def per quantity. It also gets Bend's Kind(&1) / List<&2, Nat> spelling and the Lean line count (4,158; it said 4,247).

Closes #1175
Closes #1179
Closes #1180

🤖 Generated with Claude Code

[Lorenzobattistela]

Ran this locally (merged onto main a3b0dfe) and through a /code-review pass. The kernel side holds up: all 7 claims print only propext, Classical.choice, Quot.sound, the 8 new tests pass --verdict (kind_terms and kind_self_call_eta fail on main), #1201's spec_root_split{,_out} pass too, and gates/repo.ts is 50/50. One regression though.

Regression: a rewrite passed as a self-call argument now fails --verdict

import Base

def K0(A: Nat) -> Kind(&0):
  Nat

def F(n: Nat) -> Type:
  Nat -> Kind(&0)

def go(n: Nat, e: {n == n : Nat}, f: Nat -> Type) -> Nat:
  match n:
    case 0n: 0n
    case 1n+p: go(p, {==}, (%e : F(_); K0))

def main() -> Nat:
  go(3n, {==}, K0)

On main it checks, here it fails.

The emitted call is (go x0 {==} {%x1 : ...; K0 : (F (.Succ, (x0, ())))}) at the column ∀x2 : Nat -> *(.Q1). arg_term (safe.ts:1208) gives qsig_eq the rewrite's bend2 goal rather than its own type P[b, e], so the argument isn't η-expanded. The new Rwt case in term() then annotates it at P[b, e], and the kernel has to convert Nat -> *(.Q0) to Nat -> *(.Q1) under a binder, which fails. Narrow fix: use rwt_type's result for a Rwt argument in arg_term, or always η-expand a rewrite there.

Design question

Kind(&0) is no longer raised to *1, so *(.Q0) fits *(.Q1) but doesn't convert to it. Every spot where bend2's LE goes under a binder now needs its own η-long or annotation case in safe.ts (qsig_eq's domain check, rwt_type annotations, the Rwt head in spine), and the bug above is two of those meeting. Would a ∀ rule in Term.fits (domain swapped, qge on the codomain kind, with a lemma like qge_sound) be cleaner than patching each case? I know that costs kernel ttok, with ~900 left under the cap.

Smaller

• rwt_type runs twice for a rewrite at an application head, and the Ann re-elaborates the evidence and motive after rwt_term already did, which compounds when rewrites nest. rwt_type also repeats rwt_term's lookup of the evidence type; better to share it so they can't drift.
• Term.wnf on Min normalizes both sides even when the left is .Q0.
• Dead code: datatypes are never specialized now, so adt_emit/tele_open keep unused cols paths and a stale comment. spec_val is a one-line wrapper with one caller.
• bend2/docs/BendTT/main.typ still describes *1/*2 and one copy per quantity, so paper/BendTT.pdf no longer matches the kernel.