Repository navigation
--verdict: the kernel rejects a +-bound Equal.cong over a pair whose endpoint is a call (an unannotated eta-expansion), and the verdict does not say why #1133
Description
What you did
bend lemma.bend # the file below
bend lemma.bend --verdict
bend lemma.bend -o lemma.bendtt && ~/.bend/bendtt/7f6ef51c9f75d7de/bendtt lemma.bendttWhat happened
bend2 accepts the file, and the BendTT kernel rejects the term bend2 accepted:
$ bend lemma.bend
ALL PROOFS CHECK
Use --verdict for mathematical validity.
$ bend lemma.bend --verdict
SOME PROOFS FAIL
Sorry - this is a mismatch between the TypeScript implementation, and the formalized BendTT kernel. [...] feel free to open an issue to report this bug.
$ ~/.bend/bendtt/7f6ef51c9f75d7de/bendtt lemma.bendtt
SOME PROOFS FAIL
In lemma:
expected: an annotated term
observed: λx3 => (snd_of x3)
The translation eta-expands snd_of (the f of Equal.cong) into a lambda with no annotation, and the kernel cannot infer its type. What it takes, each variant checked with bend2 and with the kernel binary:
| variant | kernel |
|---|---|
the file below: +h2 = Equal.cong(U32 & Bool, Bool, snd_of, x, mk(n), h) |
rejects |
the same without the + on the let (h2 = …) |
accepts |
the same with a variable endpoint (y) instead of the call mk(n) |
accepts |
Equal.cong(…) returned directly, no let |
accepts |
a non-pair domain (Box{t: Tag}), variable endpoints, + let |
accepts |
So the trigger seems to be a +-bound let of an Equal.cong whose endpoint is a call and whose domain is a pair. Writing the function as p => snd_of(p) at the source gives the same unannotated term. We hit it in a larger proof (a map lemma: Equal.cong((String & String) & Cmp, Cmp, cmp_of, r, String.cmp(key, k), hr) bound with +), where it was the only def the kernel refused in a ~3,000-line proof file.
A smaller ask, in the same spot: --verdict's FAIL says only "Sorry - this is a mismatch"; the kernel's own line (In lemma: expected: an annotated term) is visible only through -o and the cached kernel binary. Printing that line under the verdict would say which def and why.
The file
import Base
def snd_of(p: U32 & Bool) -> Bool:
(a, b) = p
b
def mk(n: U32) -> U32 & Bool:
(n, True{})
def lemma(+n: U32, x: U32 & Bool, +h: {x == mk(n) : U32 & Bool}) -> {snd_of(x) == snd_of(mk(n)) : Bool}:
+h2 = Equal.cong(U32 & Bool, Bool, snd_of, x, mk(n), h)
h2bend --version
bend 2.0.32
uname -sm
Linux x86_64
clang --version (the first line)
clang version 22.1.8
Activity
jkbennitt commentedon Sep 27, 2026
Thanks for the minimal repro — same failure mode on bend 2.0.32 here.
We hit the same polarity (
bend/--check-onlyPASS,--verdict+ BendTT FAIL with the elaborator/kernel mismatch message) beyondU32 & Bool. The+-boundEqual.cong+ pair domain + call endpoint pattern also fired for us on at least:Bool & U32Nat & BoolU32 & NatBool & BoolString & StringSame shape as your table: drop the
+on the let, or use a variable endpoint instead of a call, and those variants check under the kernel again.Also agreed on the smaller ask: surface the kernel’s
expected: an annotated term(or equivalent) under--verdictinstead of only the generic mismatch line.Happy to paste a second minimal file for one of the other pair domains if that would help.
aldeni commentedon Sep 27, 2026
Thank you for checking it, and for the list. That matches what I found while writing #1136: the pair's type plays no part. The elaborator (
safe.ts) counts an application as inferable when its head is, whatever its arguments; the function argument goes to the kernel η-long, a lambda the kernel cannot infer; and a+let is inferred rather than checked. So any+-boundEqual.congover a function name can trip it. One correction to what I first wrote here: with a variable endpoint the emitted.bendttis the same to the letter, the same+let and the same unannotated lambda, and the kernel accepts it, so why a call endpoint makes the kernel refuse is on the kernel's side and I can't say. The one-line fix in #1136 sidesteps the question: it counts the arguments too, so the let goes out annotated with the type bend2 already knows, and the kernel has nothing to infer.I just ran two of your variants on that branch:
Nat & BoolandString & Stringboth go fromSOME PROOFS FAILtoALL PROOFS CHECKunder--verdict, so a second file isn't needed, though if you have one with a different shape (say, a non-pair domain that also fails) that would be worth adding to the test.Agreed on the smaller ask too: the kernel's own line,
expected: an annotated term / observed: λx3 => (snd_of x3), says at once what the generic mismatch line hides.The kernel puts a λ argument into a type annotated with its domain, s…