[aaaxn]

Fixes #1665. Fixes #1669. This follows @Lorenzobattistela's suggestion in review: fix the levels once, where arm reads a def's body, instead of at each step that moves a term. It supersedes #1670, whose test is here.

Cause

bend2 wraps each node it checks in its type, as a cell (Infer and Check in bend.ts). arm raises a def's body with term_higher, which keeps a cell as it is. So a binder in the body becomes a closure, but an annotation still names it by the level bend2 checked it at. Any step that puts part of the body under binders bend2 didn't check it under leaves those annotations at the old levels:

• eta puts a term under a new λ (--verdict mismatch: an η-expanded argument keeps old binder levels in its inner annotations (Bool where Nat is expected) #1665).
• rebuild puts a λ's body under a binder per field (--verdict mismatch: a λ rebuilt as a match keeps its variable's old level in its annotations (Nat where P is expected) #1669).
• let_term builds a let's value at the self-call it is passed to, at the call's depth (the case from the review).

A template's body already goes through subst(t0, 0, …), which lowers and raises it. The issue's term in a def with a ~ parameter checks on main.

Fix

arm lowers and raises every other def's body once, term_higher(term_lower(t0)). Lowering forces each cell, so an annotation names the body's binders as the body's own uses do, and raising binds both. eta, rebuild and let_term are as on main.

The review's line sends every body through subst. The output is the same, but subst's copy recurses deeper per node than lowering does. With it, -o overflows the stack on a def whose body is a 3,800-element list literal, with or without η. Without the copy, the limit is main's. Here 4,000 elements pass and 4,500 overflow, on both, and a chain of 4,000 lets passes on both with the same -o. The exact limit depends on the machine's stack.

Checks

With main 64230dc merged in, Linux x86_64, kernel built from main's bendtt.lean with Lean 4.34.0:

• eta_levels (the four η sites), rebuild_levels (--verdict mismatch: a λ rebuilt as a match keeps its variable's old level in its annotations (Nat where P is expected) #1669: a type with two constructors, one with no fields, and a λ inside the body) and let_levels (the review's let) each fail --verdict on main and check here. Each prints its #| value when run and from the JS and C builds, and --checkup exits 0. Lowering at depth 1 instead of 0 fails all three.
• On main's 1,760 test, demo, and bench files, --verdict gives the same exit code and output as main: 1,137 check, 623 fail. -o differs in 15 files, all through three Base defs (String.cmp.group, Map.get.leaf, Str.split.fin). There, a variable that main passes through a match's convoy is now a copied binder, λ+x. Each of the three defs verifies in the 9 of those files that check. The other 6 fail on @unsafe before the kernel, as on main.
• Cost: lowering every body takes time. Over two sets of sequential runs on the checker benches, -o is 5 to 9% slower on defs_12800, 10 to 15% on generics_3200, and 14 to 21% on proofs_3200 (3.2 s on main, 3.8 s here). --verdict on proofs_3200 goes from 4.0 s to 4.7 s. Most of it is the lowering itself, which forces the cell at each node and lowers its type: 0.71 s of the 1.94 s safe_book takes on proofs_3200. With subst on every body, -o takes 1.8, 2.6, and 6.5 s on those three. Plain runs and --check-only don't change, so the perf gate's checker benches don't either. Over the 1,760-file sweep, total CPU goes up 1 to 2%.
• The review's 400-ary leaf: -o takes 2.7 s, the same as main, with the same output.
• bun gates/repo.ts: 54 / 54. safe.ts goes from 23,992 to 24,000 ttok, at its cap. tsc: 11 errors, the same as main.
• I didn't run the cluster gates.

Limits

safe.ts is at its cap, so this adds no comment at arm. The three test headers say why the body is lowered.

A fix at each site instead (η in one pass per leaf, plus rebuild and let_term) would keep --verdict near main's cost. The first version of this PR fixed only η that way and was within 3% of main on these benches. With all three sites, it doesn't fit under the cap today.

[Lorenzobattistela]

Thanks for this. The diagnosis in #1665 is clear, and the test covers all four η sites. I merged this onto main 8f86f73 and ran the gates on the mini cluster: repo 54/54, test 1658/1658, perf 124/124, ping 62/62. The safe gate shows 1079 agree vs 1078 on main (the +1 is eta_levels), with 0 false rejects. The new test fails --verdict on main and checks here, and each of its four defs does the same on its own. I'm requesting changes for the points below.

1. The same level mismatch is still reachable outside η. When a let-bound λ is passed to a self-call, safe.ts copies it in at the call site at a different depth. Its annotations still name n at the let's depth, and there that level is g itself, so --verdict loops:

import Base

type Fact<-P: Type> is Type:
  Fact{proof: P}

def refl(+n: Nat) -> Fact<{n == n : Nat}>:
  Fact{{==}}

def walk(c: Nat, keeps: @+n: Nat -> {n == n : Nat}) -> Nat:
  match c:
    case Zero{}:
      0n
    case Succ{p}:
      g : @+n: Nat -> {n == n : Nat} = n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(refl(n))
      walk(p, g)

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

It runs and prints 0n, but bend let_inline.bend --verdict fails with "Error: the machine stack overflowed" on both main and this PR. This isn't a regression, but it is the same bug class, and the PR doesn't cover it. Storing subst(x.v[j], s.d) where let_term keeps the value makes it check.

2. A possible fix at the source, offered as an idea; I haven't looked into it much. arm() turns each def body back into closures, while the annotations still name variables by the level they were checked at. Templates already go through subst(t0, 0, …) at that point, which may be why only non-template defs break. I tried sending every body through that subst, with eta left as on main:

let t = subst(t0, 0, (o) => o.$ === "Ref" && ps !== null ? ps.get(o.k as Name) ?? undefined : undefined);

With that change, eta_levels and the let probe above both check, and the --verdict sweep over tests/ matches main. safe.ts comes to 23,983 ttok. It might also cover rebuild (#1669 / #1670), but I haven't checked that. The costs I saw are about 8% more CPU over the suite and a different .bendtt for about 8 tests, which all still verify. There could be cases I'm missing, so please treat this as something to evaluate, not a drop-in replacement.

3. eta now lowers and re-raises the whole term on every η step. A leaf of an n-ary function type is expanded n times, each over a growing App spine, which makes it O(n·|t|). For def big() -> Fn(): h([0n, …, 1999n]), where Fn() is a 400-ary function type, -o takes 18.2s here vs 1.4s on main (200-ary: 4.2s vs 1.4s), with identical output. The extra recursion also lowers the stack limit: a 3800-element literal under an η-expanded leaf now overflows, while main still emits it (both fail at 4000).

4. Minor: eta's new d must be the depth bend2 checked t at, not the depth it is used at, but nothing says so, and the PR removes the only comment explaining why ("bend2's annotations name a variable by its level"). A short comment on eta would help. Relatedly, closed_val's f now reads s.c[o.i] for every Var, which is only correct while s.c.length === s.d. The old range guard made that explicit.

[aaaxn]

Thanks for the review and for the idea in 2. I took it, with one change, in bafce16 (main 64230dc merged in). The PR is now one line in safe.ts and three tests.

1. The let case is fixed by the change in 2. It is now tests/check/let_levels.bend, which overflows the stack on main and checks here.
2. arm now lowers and raises every non-template body, term_higher(term_lower(t0)), and eta, subst, closed_val and model_at are back to main. This also covers rebuild (--verdict mismatch: a λ rebuilt as a match keeps its variable's old level in its annotations (Nat where P is expected) #1669): rebuild_levels checks here, so I closed A λ rebuilt as a match keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1669) #1670 and moved its test here. The one change from your line: with every body through subst, -o overflows on a def whose body is a 3,800-element list literal, even without η, because subst's copy recurses deeper per node. Without the copy, the limit is main's (here 4,000 passes and 4,500 overflows, on both). The verdicts match main on all 1,760 files. -o differs in 15 files, through three Base defs, which verify. It isn't free: lowering every body makes -o 5 to 21% slower on the checker benches (proofs_3200: 3.2 s to 3.8 s), and your line costs more there (6.5 s), because of subst's copy. Plain runs don't change. A fix at each site instead (η in one pass per leaf, plus rebuild and let_term) would stay near main's cost, but it doesn't fit under the cap today. Do you prefer this version, or the per-site one once there is room?
3. With eta back to main, the 400-ary leaf takes the same time as main, with the same output.
4. eta and closed_val are back to main, with the range guard and its comment. safe.ts is now at 24,000, its cap, so I couldn't add a comment at arm. The test headers explain it.