A def's body goes to --verdict through its lowered form once, so its annotations move with its binders under η, rebuild and let inlining (#1665, #1669)

bend2/safe.ts

@@ -1307,7 +1307,7 @@ function arm(e: Safe, s: Scope, k: Name, cols: Cols, vs: Array<[Q, O]>): O {
   const tld = e.book.tlds[k] as Def;
   const ps = tld.x === 0 ? null : new Map(B.tele_unbind(e.book, tld.T).doms.slice(0, tld.x).map(([, p], j) => [k + "~" + p, cols[j]]));
   const t0 = B.term_higher(tld.e as B.LTerm);
-  let t = ps === null ? t0 : subst(t0, 0, (o) => o.$ === "Ref" ? ps.get(o.k as Name) ?? undefined : undefined);
+  let t = ps === null ? B.term_higher(B.term_lower(t0)) : subst(t0, 0, (o) => o.$ === "Ref" ? ps.get(o.k as Name) ?? undefined : undefined);
   let si: Scope = { ...s, c: [], d: 0, cols: cols.slice(tld.x), sub: false };
   let j = 0;
   for (let [x, T] = open(t); x.$ === "Lam" && T !== null; [x, T] = open(t)) {

tests/check/eta_levels.bend

@@ -0,0 +1,66 @@
+# a term of a function type goes out η-long, λy => t(y), and the new λ
+# puts t's binders a level deeper. bend2's annotations name a variable by
+# the level bend2 checked it at, so the type of the λ-match under n still
+# named n at the level y took: the kernel saw y's Bool where n's Nat was
+# expected (#1665). A def's body now goes through its lowered form once,
+# before --verdict builds it, so its annotations move with its binders. A
+# term goes η-long as an argument (arg), as a def's body (leaf), as a
+# match arm (arm) and as a default arm (rest). The law checks main's value
+# in the emitted book too
+import Base
+
+type Fact<-P: Type> is Data:
+  Fact{-proof: P}
+
+type Box<-P: Type> is Data:
+  Box{n: Nat}
+
+def Cells() -> Type:
+  @+b: Bool -> {b == b : Bool}
+
+def mk(-keeps: @+n: Nat -> {n == n : Nat}) -> Cells():
+  b => {==}
+
+def mk2(-keeps: @+n: Nat -> {n == n : Nat}) -> @c: Bool -> Box<Cells()>:
+  c => Box{4n}
+
+def take(-p: Cells(), n: Nat) -> Box<Cells()>:
+  Box{n}
+
+def refl(+n: Nat) -> Fact<{n == n : Nat}>:
+  Fact{{==}}
+
+def arg(-k: @+n: Nat -> Fact<{n == n : Nat}>) -> Box<Cells()>:
+  take(mk(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n))), 1n)
+
+def leaf(-k: @+n: Nat -> Fact<{n == n : Nat}>) -> Cells():
+  mk(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n)))
+
+def arm(-k: @+n: Nat -> Fact<{n == n : Nat}>, flag: Bool) -> Cells():
+  match flag:
+    case True{}:
+      b => {==}
+    case False{}:
+      mk(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n)))
+
+def rest(-k: @+n: Nat -> Fact<{n == n : Nat}>) -> @c: Bool -> Box<Cells()>:
+  \{True: Box{8n}; mk2(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n)))}
+
+def num(b: Box<Cells()>) -> Nat:
+  match b:
+    case Box{n}:
+      n
+
+def main() -> Nat:
+  Nat.add(num(arg(refl)),
+  Nat.add(num(take(leaf(refl), 2n)),
+  Nat.add(num(take(arm(refl, False{}), 3n)),
+    num(rest(refl, False{})))))
+
+law eta_levels_result:
+  {main() == 10n : Nat}
+
+def eta_levels_result():
+  {==}
+
+#|10n

tests/check/let_levels.bend

@@ -0,0 +1,34 @@
+# a let-bound λ passed to a self-call goes into the call, built at the
+# call's depth. bend2's annotations name a variable by the level bend2
+# checked it at, so the type of the λ-match under n still named n at the
+# let's depth, which at the call is g itself: building that type built g
+# again, and --verdict ran until the stack overflowed. A def's body now
+# goes through its lowered form once, before --verdict builds it, so its
+# annotations move with its binders. The law checks main's value in the
+# emitted book too
+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 => {==})
+
+law let_levels_result:
+  {main() == 0n : Nat}
+
+def let_levels_result():
+  {==}
+
+#|0n

tests/check/rebuild_levels.bend

@@ -0,0 +1,81 @@
+# a λ in an erased argument may use its variable twice: it goes out as a
+# λ-match on the variable, whose arms call its body on each constructor,
+# under a binder per field. bend2's annotations name a variable by the
+# level bend2 checked it at, so the type Tag<p> -> Nat of a λ-match in the
+# body still named p's level, now the first field's: the kernel saw a Nat
+# where a P was expected, and with no fields --verdict met a free variable
+# (#1669). A def's body now goes through its lowered form once, before
+# --verdict builds it, so its annotations move with its binders. The
+# annotation names the variable, of a type with two constructors (pair) or
+# with no fields (unit), or the binder of a λ inside the body (inner). The
+# law checks main's value in the emitted book too
+import Base
+
+type Fact<-P: Type> is Data:
+  Fact{-proof: P}
+
+type P is Type:
+  P{a: Nat, b: Nat}
+  Q{c: Nat}
+
+type Tag<-x: P> is Data:
+  Tag{}
+
+type U is Type:
+  U1{}
+  U2{}
+
+type UTag<-x: U> is Data:
+  UTag{}
+
+def first(p: P) -> Nat:
+  match p:
+    case P{a, b}:
+      a
+    case Q{c}:
+      c
+
+def tag(-p: P) -> Tag<p>:
+  Tag{}
+
+def code(u: U) -> Nat:
+  match u:
+    case U1{}:
+      1n
+    case U2{}:
+      2n
+
+def utag(-u: U) -> UTag<u>:
+  UTag{}
+
+def use(-f: P -> Nat, n: Nat) -> Nat:
+  n
+
+def use_u(-f: U -> Nat, n: Nat) -> Nat:
+  n
+
+def keep(-g: @+n: Nat -> {n == n : Nat}, x: Nat) -> Nat:
+  x
+
+def refl(+n: Nat) -> Fact<{n == n : Nat}>:
+  Fact{{==}}
+
+def pair() -> Nat:
+  use(p => Nat.add(first(p), {\{Tag: first(p)} : Tag<p> -> Nat}(tag(p))), 1n)
+
+def unit() -> Nat:
+  use_u(u => Nat.add(code(u), {\{UTag: code(u)} : UTag<u> -> Nat}(utag(u))), 2n)
+
+def inner(-k: @+n: Nat -> Fact<{n == n : Nat}>) -> Nat:
+  use(p => keep(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n)), Nat.add(first(p), first(p))), 3n)
+
+def main() -> Nat:
+  Nat.add(pair(), Nat.add(unit(), inner(refl)))
+
+law rebuild_levels_result:
+  {main() == 6n : Nat}
+
+def rebuild_levels_result():
+  {==}
+
+#|6n