[nicolas-abril]

Stacked on #1203 (base: kernel-kind-terms).

Why

bend2's LE goes under a binder. It compares a function type's domains swapped and its codomain along, so:

• g : Type -> Nat fits Kind(&0) -> Nat;
• K : Nat -> Kind(&2) fits Nat -> Type;
• a rewrite of type Nat -> Kind(&0) fits a Nat -> Type goal.

The kernel fitted only at the top, so on #1203 safe.ts bridged the gap:

• a self-call's argument went η-long where its domains or kinds differed from the column's (qsig_eq);
• a rewrite went out at its own type (rwt_type).

--verdict trusted that bridge, and all three divergences that review found were in it. This moves the rule into the kernel, with proofs, so the kernel decides those fits itself.

Kernel (bend2/bendtt.lean)

• Fits is inductive: conversion, kinds (*(g) fits *(h) where g is .Q2 wherever h is, as before), enums (fewer labels), ∀q A B fits ∀q C D when C fits A and B fits D, and transitivity. Transitivity is a rule, so the old nine-way fits_trans is gone.
• Fits.at / fits_at read a fit at a former, in both directions. If T converts to a former X, then U converts to a Y that fits X part by part, and the same from U's side. fits_all, fits_conv, fits2 and fits_former follow from it. They replace the case analysis of the old disjunction, including fits_conv's "any non-kind fit converts", which a ∀ rule breaks.
• Term.fits threads fuel, as qge does, and fits two ∀s of one quantity by their parts. fits_sound proves it.
• Subject reduction and progress take the rule:
  • β casts the argument along the domain fit and the result along the codomain's;
  • a split, a hit and a miss do the same;
  • a λ-match on an enum may now receive a smaller enum;
  • lab_in reads a label through a fit.
• Every claim (consistent, book_check, confluent, sr, progress, halts, empty) checks with no sorry under Lean v4.34.0 (the pinned version) and v4.34.1. Each depends only on [propext, Classical.choice, Quot.sound]. The claim statements are unchanged; the typing judgment they quantify over is now more general.
• 63,988 ttok, against the cap of 64,000. The next kernel change has to simplify first.

Elaborator (bend2/safe.ts)

• qsig_eq compares binder quantities only, since the kernel's fit still needs them equal.
• rwt_type and the annotation it added are gone.

Checks

• Hand-written books, run through the built kernel:
  • Rejected: K : <A> -> *1 at <A> -> *2; ∀(∀ *1 -> <A>) -> <A> at ∀(∀ *2 -> <A>) -> <A>; a function on <A> at <A, B>; a ∀ at a ∀+.
  • Accepted: each fit in the sound direction, including two levels of contravariance.
• BendTT: kinds as quantity terms, meets, Σ at any kind and subsumption under ∀; --verdict emits generic defs once #1203's kind tests (kind_*, meet_*) pass. In kind_none_is_type, the self-call now passes K0 whole, and the kernel fits ∀ Nat -> *(.Q0) to ∀ Nat -> *(.Q1) itself; on BendTT: kinds as quantity terms, meets, Σ at any kind and subsumption under ∀; --verdict emits generic defs once #1203 it went out as λx2 => (K0 x2).
• Cluster gates on this head:
  • repo PASS 50 / 50, test PASS 1551 / 1551.
  • perf: the cluster was noisy. main itself scored 89 / 124 and this branch 49–110 / 124 in back-to-back runs. This branch doesn't touch bend.ts, comp.ts or main.ts, which are all perf measures.
  • ping was skipped: there is no site repo here.
  • gates/safe.ts tests with this kernel: per file, identical to main's table plus BendTT: kinds as quantity terms, meets, Σ at any kind and subsumption under ∀; --verdict emits generic defs once #1203's new tests (999 agree, 69 unsafe, 491 bend2 rejects, 2 out of scope, 1 false reject: --verdict: the kernel runs out of fuel on conversion_shared_cells_once.bend, which bend2 checks by sharing (2.0.34) #1193).
• The snippets in the open issues give the same results as BendTT: kinds as quantity terms, meets, Σ at any kind and subsumption under ∀; --verdict emits generic defs once #1203's head.
• tsc: the same 12 errors as main.
• Not measured: kernel time. The fit now recurses through ∀s instead of converting them, and fewer arguments go out η-long.

Paper

bend2/docs/BendTT/main.typ and paper/BendTT.pdf give the ∀ rule:

• in the kinds section, with Bend examples;
• in Figure 3's caption for U <= T, together with transitivity;
• in the subject-reduction sketch, where a fit is inverted at a type former, so β casts along the domains' and codomains' fits.

The Lean line count is now 4,157.

🤖 Generated with Claude Code

[nicolas-abril]

Folded into #1203: kernel-kind-terms was fast-forwarded to this branch, so its commits (a8b85f0, daa9295) are part of #1203, and #1203's description covers the ∀ rule.