From 742429e3e80f09c2f0eee1983937f8e5cd86ec08 Mon Sep 17 00:00:00 2001 From: aaaxn Date: Sat, 17 Oct 2026 12:25:33 -0300 Subject: [PATCH 1/3] =?UTF-8?q?A=20term=20=CE=B7-expanded=20under=20a=20ne?= =?UTF-8?q?w=20=CE=BB=20keeps=20its=20annotations=20on=20its=20own=20binde?= =?UTF-8?q?rs,=20so=20--verdict=20checks=20what=20bend2=20checks=20(#1665)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- bend2/safe.ts | 16 +++++---- tests/check/eta_levels.bend | 65 +++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+), 6 deletions(-) create mode 100644 tests/check/eta_levels.bend diff --git a/bend2/safe.ts b/bend2/safe.ts index 12101fb56a..2ce96327da 100644 --- a/bend2/safe.ts +++ b/bend2/safe.ts @@ -769,7 +769,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 +876,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; + const f = x.$ === "Lam" ? x : open(eta(t, all, s.d))[0] as Extract; // 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, @@ -949,9 +949,13 @@ function all_of(e: Safe, T: HTerm | null): Extract | null { return G?.$ === "All" ? G : null; } -// λy => t(y), at t's type ∀y:A -> B -function eta(t: HTerm, all: Extract): HTerm { - return B.Ann(B.Lam(all.k, 0, (y: HTerm) => B.Ann(B.App(t, y), all.B(y))), all); +// λy => t(y), at t's type ∀y:A -> B, for t at depth d: y takes level d, +// and t's binders the levels after it. bend2's annotations name a +// variable by its level, so t goes in through its lowered form, where an +// annotation names t's binder as t's own uses do +function eta(t: HTerm, all: Extract, d: number): HTerm { + const u = subst(t, d, (o) => o.$ === "Var" && (o.i as number) >= 0 && (o.i as number) < d ? B.Var(o.k as Name, o.i as number) : undefined); + 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 +1338,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); } diff --git a/tests/check/eta_levels.bend b/tests/check/eta_levels.bend new file mode 100644 index 0000000000..969108978a --- /dev/null +++ b/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: + c => Box{4n} + +def take(-p: Cells(), n: Nat) -> Box: + Box{n} + +def refl(+n: Nat) -> Fact<{n == n : Nat}>: + Fact{{==}} + +def arg(-k: @+n: Nat -> Fact<{n == n : Nat}>) -> Box: + 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: + \{True: Box{8n}; mk2(n => {\{Fact: q => q} : Fact<{n == n : Nat}> -> {n == n : Nat}}(k(n)))} + +def num(b: Box) -> 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 From fce97a9b09decc734023590f69f8951b63f9242f Mon Sep 17 00:00:00 2001 From: aaaxn Date: Sat, 17 Oct 2026 12:53:36 -0300 Subject: [PATCH 2/3] subst keeps a variable below its depth, so eta's fix fits under safe.ts's cap (#1665) --- bend2/safe.ts | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/bend2/safe.ts b/bend2/safe.ts index 2ce96327da..8f96b96ed7 100644 --- a/bend2/safe.ts +++ b/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) => HTerm | undefined): HTerm { +// (so no closure hides one); a variable below d stays one +function subst(t: HTerm, d: number, f?: (o: Record) => HTerm | undefined): HTerm { const go = (u: unknown): unknown => { if (typeof u !== "object" || u === null) { return u; } const o = u as Record; - 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); @@ -949,12 +948,9 @@ function all_of(e: Safe, T: HTerm | null): Extract | null { return G?.$ === "All" ? G : null; } -// λy => t(y), at t's type ∀y:A -> B, for t at depth d: y takes level d, -// and t's binders the levels after it. bend2's annotations name a -// variable by its level, so t goes in through its lowered form, where an -// annotation names t's binder as t's own uses do +// λy => t(y), at t's type ∀y:A -> B function eta(t: HTerm, all: Extract, d: number): HTerm { - const u = subst(t, d, (o) => o.$ === "Var" && (o.i as number) >= 0 && (o.i as number) < d ? B.Var(o.k as Name, o.i as number) : undefined); + 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); } From 45716b3b51d9ee67d2330aa2593ce0d5290f7dd0 Mon Sep 17 00:00:00 2001 From: aaaxn Date: Sat, 17 Oct 2026 16:31:57 +0000 Subject: [PATCH 3/3] =?UTF-8?q?A=20=CE=BB=20rebuilt=20as=20a=20match=20kee?= =?UTF-8?q?ps=20its=20annotations=20on=20its=20own=20binders,=20so=20--ver?= =?UTF-8?q?dict=20checks=20what=20bend2=20checks=20(#1669)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- bend2/safe.ts | 2 +- tests/check/rebuild_levels.bend | 81 +++++++++++++++++++++++++++++++++ 2 files changed, 82 insertions(+), 1 deletion(-) create mode 100644 tests/check/rebuild_levels.bend diff --git a/bend2/safe.ts b/bend2/safe.ts index 8f96b96ed7..fcad612c07 100644 --- a/bend2/safe.ts +++ b/bend2/safe.ts @@ -936,7 +936,7 @@ function rebuild(e: Safe, s: Scope, x: Extract, 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((m, [k, U]) => B.Mat(k, arm(k, U, []), m), B.Efq()), all) : null; diff --git a/tests/check/rebuild_levels.bend b/tests/check/rebuild_levels.bend new file mode 100644 index 0000000000..85facf6ba2 --- /dev/null +++ b/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

-> 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

: + Tag{} + +def code(u: U) -> Nat: + match u: + case U1{}: + 1n + case U2{}: + 2n + +def utag(-u: U) -> UTag: + 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

-> Nat}(tag(p))), 1n) + +def unit() -> Nat: + use_u(u => Nat.add(code(u), {\{UTag: code(u)} : UTag -> 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