A λ rebuilt as a match keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1669)

bend2/safe.ts

@@ -505,21 +505,20 @@ function spec_val(e: Safe, s: Scope, x: HTerm): HTerm {
 
 // x's normal form, when it is closed; null when it depends on a run-time value
 function closed_val(e: Safe, s: Scope, x: HTerm): HTerm | null {
-  // bend2's annotations name a variable by its level
-  const v = B.term_snf(e.book, subst(x, s.d, (o) => o.$ === "Var" && (o.i as number) >= 0 && (o.i as number) < s.d
-    ? s.c[o.i as number]?.v ?? B.Var(o.k as Name, o.i as number) : undefined));
+  const v = B.term_snf(e.book, subst(x, s.d, (o) => o.$ === "Var" ? s.c[o.i as number]?.v : undefined));
   return mentions(B.term_lower(v, s.d), (i) => i >= 0 && i < s.d) ? null : v;
 }
 
 // t at depth d, with each node f maps replaced, through its lowered form
-// (so no closure hides one)
-function subst(t: HTerm, d: number, f: (o: Record<string, unknown>) => HTerm | undefined): HTerm {
+// (so no closure hides one); a variable below d stays one
+function subst(t: HTerm, d: number, f?: (o: Record<string, unknown>) => HTerm | undefined): HTerm {
   const go = (u: unknown): unknown => {
     if (typeof u !== "object" || u === null) {
       return u;
     }
     const o = u as Record<string, unknown>;
-    const v = f(o);
+    const i = o.i as number;
+    const v = f?.(o) ?? (o.$ === "Var" && i >= 0 && i < d ? B.Var(o.k as Name, i) : undefined);
     return v !== undefined ? B.Var(o.k as Name, -1, undefined, v)
       : Array.isArray(u) ? u.map(go) : Object.fromEntries(Object.entries(o).map(([k, x]) => [k, k === "s" ? x : go(x)]));
   };
@@ -606,7 +605,7 @@ function model_at(e: Safe, T: HTerm, d: number, path: string[], hs: Array<[HTerm
       const x: HTerm = B.Var(F.k, d);
       const t = model_at(e, F.B(x), d + 1, path, F.q.$ === "None" ? hs : [...hs, [x, F.A]], proj, probe);
       return t === null ? null : B.Ann(B.Lam(F.k, d, (v: HTerm) =>
-        subst(t, d + 1, (o) => o.$ !== "Var" || (o.i as number) > d ? undefined : o.i === d ? v : B.Var(o.k as Name, o.i as number))), F);
+        subst(t, d + 1, (o) => o.$ === "Var" && o.i === d ? v : undefined)), F);
     }
     case "ADT": {
       const key = model_key(F, d);
@@ -769,7 +768,7 @@ function tree(e: Safe, s: Scope, t: HTerm, fs: Chain[]): O {
   // equation bend2 closes by η must be a λ
   if (x.$ !== "Lam" && x.$ !== "Mat" && x.$ !== "Efq") {
     if (all !== null) {
-      return tree(e, s, eta(t, all), fs);
+      return tree(e, s, eta(t, all, s.d), fs);
     }
     return top === undefined ? term(e, s, t, true) : oos("a match arm with no known type");
   }
@@ -876,7 +875,7 @@ function swi(e: Safe, s: Scope, t: HTerm, T: HTerm | null, fs: Chain[], cv: numb
       const q = quant(all.q);
       const [lt, la] = [s.D, s.D + 1];
       const s2 = scope_hide(scope_hide(s));
-      const f = x.$ === "Lam" ? x : open(eta(t, all))[0] as Extract<HTerm, { $: "Lam" }>;
+      const f = x.$ === "Lam" ? x : open(eta(t, all, s.d))[0] as Extract<HTerm, { $: "Lam" }>;
       // the default's binder is the pair of the tag and the fields
       const pair: O = { $: "Tup", q: 1, a: { $: "Var", l: lt }, b: { $: "Var", l: la } };
       const s2e = no_ctr(e, all.A) ? { ...s2, empty: [...s2.empty,
@@ -937,7 +936,7 @@ function rebuild(e: Safe, s: Scope, x: Extract<HTerm, { $: "Lam" }>, all: Extrac
   };
   const arm = (k: Name, U: HTerm, xs: HTerm[]): HTerm => {
     const G = B.term_wnf(e.book, U);
-    return G.$ !== "All" ? x.f(B.Ann(B.Ctr(k, xs), F)) : B.Lam(G.k, 0, (v: HTerm) => arm(k, G.B(v), [...xs, v]));
+    return G.$ !== "All" ? (subst(x, s.d) as typeof x).f(B.Ann(B.Ctr(k, xs), F)) : B.Lam(G.k, 0, (v: HTerm) => arm(k, G.B(v), [...xs, v]));
   };
   const cs = (e.book.tlds[F.k] as ADT).c.filter((c) => !F.r.includes(c.k)).map((c): [Name, HTerm] => [c.k, B.tele_fill(e.book, c.T, F.x, B.ctx_nil())]);
   return cs.every(([, U]) => data(U)) ? B.Ann(cs.reduceRight<HTerm>((m, [k, U]) => B.Mat(k, arm(k, U, []), m), B.Efq()), all) : null;
@@ -950,8 +949,9 @@ function all_of(e: Safe, T: HTerm | null): Extract<HTerm, { $: "All" }> | null {
 }
 
 // λy => t(y), at t's type ∀y:A -> B
-function eta(t: HTerm, all: Extract<HTerm, { $: "All" }>): HTerm {
-  return B.Ann(B.Lam(all.k, 0, (y: HTerm) => B.Ann(B.App(t, y), all.B(y))), all);
+function eta(t: HTerm, all: Extract<HTerm, { $: "All" }>, d: number): HTerm {
+  const u = subst(t, d);
+  return B.Ann(B.Lam(all.k, 0, (y: HTerm) => B.Ann(B.App(u, y), all.B(y))), all);
 }
 
 // whether a lowered term mentions a variable at a level p holds for
@@ -1334,7 +1334,7 @@ function arg_term(e: Safe, s: Scope, x: HTerm, A: HTerm, live: boolean): O {
   const tree = y.$ === "Lam" || y.$ === "Mat" || y.$ === "Efq";
   const all = tree || y.$ === "Ctr" ? null : all_of(e, A);
   if (all !== null && (!(live && s.sub) || T !== null && !qsig_eq(e, T, A, s.d))) {
-    return term(e, s, eta(x, all), live);
+    return term(e, s, eta(x, all, s.d), live);
   }
   return term(e, s, T === null && (tree || y.$ === "Ctr") ? B.Ann(x, A) : x, live);
 }

tests/check/eta_levels.bend

@@ -0,0 +1,65 @@
+# 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). t now goes under the λ through its lowered form, 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/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). The body now goes under the fields through its
+# lowered form, 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