[raramos9]

Closes #1940

Cause

check-let checks every binder's inferred type against Kind(qj). infer-app returns B(a) with the surface argument substituted, so x = tag(q => ..) has type Tag<q => ..>. Checking that type infers the ADT, and tele_check checks the lambda again. A lambda whose body holds another such let repeats the inner pair, so n nested lets cost 11·2ⁿ − 9 checker calls.

For an ordinary or erased binder that check is redundant. Kind(g) fits Kind(h) for every h other than +, so it can only confirm that the inferred type is a type, and inference already guarantees that: book types are checked when defined, context types come from checked goals and earlier lets, and B(a) is a type because B was checked under x : A in the signature and a checks against A. Only an unrestricted + binder adds an obligation, that its type is Data.

Change

check-let calls term_check_kind only when the binder's kind is Data, and the rule comment says so. That is a + binder outside an @unsafe def: in one, lhs_kind only asks a + binder to be a type.

This is BendTT's let rule. Typed.lett in bendtt.lean requires V : T2 only when q = Q2, and Term.check checks V against T2 only if q == Q2.

Measurements

Checker calls (term_check + term_infer) for the issue's family with n nested lets:

n	before	after
1	13	8
10	11,255	62
16	720,887	98
24	184,549,367 (formula)	146

Before is exactly 11·2ⁿ − 9 and after is exactly 6n + 2, through n = 32. At n = 24, --check-only takes 35.87 s before and 0.03 s after. The five checker benches are unchanged within noise.

Tests

• let_dependent_type: the issue's family 30 deep, a shadowed binder and an erased binder; accepted.
• let_unsafe_dependent_type: + binders of an @unsafe def, 30 deep; accepted.
• let_dependent_domain: a domain T: Data that fits the ADT's -T: Type; accepted.
• let_dependent_domain_bad: a domain T: Type that does not fit -T: Data; refused at the signature.
• let_plus_dependent_type: +x at a dependent type that is Type; refused.
• let_forward_refused: a malformed type from a signature below the let; refused at that signature's own event, which is what the skipped check relies on.

Depth 30 is 2^30 checks if the doubling returns, past the gates' 30 s cap, so a regression fails the run. A depth-10 test still passed on the exponential build.

On the rebased branch, against its base db64cf76:

• --check-only over all 1837 tests: identical verdicts and output, except the two 30-deep tests, which time out at 25 s on the base.
• -o .bendtt over the accepted tests: byte-identical.
• bun gates/_run.ts: test 1824 / 1824, repo 54 / 54, perf 124 / 124; ping skipped (no site repo).
• --verdict on the five tests above: the same verdicts as --check-only.

Merged onto main at d0949580: test 1825 / 1825; perf 123 / 124, the one miss being the merkle compile cell at 1.16x, which main also misses.

Not run: gates/safe.ts, which needs a kernel binary built on a Lean node.

Limitations

Only let binders are fixed. infer-app still substitutes the surface argument into B(a), so other checks of that type double the same way, and these stay exponential, to be handled in a follow-up PR:

• nested + lets outside @unsafe, which still check their type's kind. The kernel does the same at Q2.
• nested + lambdas, in and outside @unsafe.

An inferred type is not yet known to be a type when it comes from a signature below the let. A dead region or an @unsafe def can name one, and so can a live call to a foreign def. Every such program I probed is still refused, at that signature's event at the latest, but a let can now bind the malformed type first, with two effects:

• The error can blame later code. With def g() -> 0n below it, -x = g(); -y = h(x); reports expected Nat, observed 0n at h(x), not expected Kind(&0), observed Nat at the let. With a foreign def bad(a: Nat) -> 0n below it, x = bad(0n); -y = h(x); 0n in a live def does the same.
• The checker can hang instead of refusing. With def g() -> {(x => x(x)) : Nat}((x => x(x))) below it, -x = g(); -y = h(x); loops where the base refuses at the let. This is a new route to an existing hang, not a new kind: -y = h(g()) already hangs on the base.