--verdict mismatch: a function in a type-parameter field (pair, Some) is η-expanded on only one side of an equation #1619

What you did

bend eta.bend --verdict

What happened

SOME PROOFS FAIL
In t:
expected: (keep λx1 => (x0 x1))
observed: (.Tuple, (x0, ((.False, ()), ())))
Sorry - this is a mismatch between the TypeScript implementation, and the formalized BendTT kernel. Your proofs may or may not be correct, and we cannot validate them yet. This will be addressed in a future update. Meanwhile, feel free to open an issue to report this bug.

bend eta.bend --check-only prints ALL PROOFS CHECK.

The file

import Base

def keep(v: U32 -> U32) -> (U32 -> U32) & Bool:
  (v, False{})

def t(v: U32 -> U32) -> {keep(v) == (v, False{}) : (U32 -> U32) & Bool}:
  {==}

bend --version

2.0.37 (main at 234cb9b)

uname -sm

Linux x86_64 (WSL2)

clang --version (the first line)

clang version 22.1.4 (bundled with Lean 4.34.0; not used by --verdict)

Diagnosis

In bend2/safe.ts, arg_term writes a function-typed argument η-long, so keep(v) goes out as (keep λx1 => (x0 x1)), which reduces to ((λx1 => (x0 x1)), False).

The right side (v, False{}) is a term inside a type, so it reaches the elaborator bare, with no type. arg_term gives a bare λ or match its goal A, but returns a bare constructor without it (safe.ts:1339):

return term(e, s, T === null && tree ? B.Ann(x, A) : x, live);

ctr_term then sees T === null, so the pair's parameters are unknown (ps are placeholders). The field's type is a bare parameter, not a ∀, so v stays x0. The kernel converts without η, so the sides cannot meet.

Variations:

• Some{v} through a template fails the same way.
• A constructor whose field is declared U32 -> U32 passes, because the field type is known without the parameters.
• id(v) == v passes, because the equation's sides are η-long leaves.

Related, but not the same path: #1133 (closed by #1136), where the η-long argument had no annotation. Here both sides are annotated, and only one side is η-long.

It is a false rejection, not a soundness problem. On BendHub it causes the --verdict mismatch in bend-collections-laws-containers@1.0.0.0 (0x5c489f5d9646d7cc9aa3dd8137e9dc07), files proofs/containers/dynamic_array/proof.bend and owned_instances.bend, at swap_rejected instantiated at ~(U32 -> U32).

A candidate fix (one line)

Give a bare constructor its goal, as is already done for a bare λ or match:

-  return term(e, s, T === null && tree ? B.Ann(x, A) : x, live);
+  return term(e, s, T === null && (tree || y.$ === "Ctr") ? B.Ann(x, A) : x, live);

Tested locally:

• the file above, plus pair, Some and template variants, pass --verdict;
• the controls still pass;
• all 1,666 tests/ and demos/*/PROOF.bend files keep their exact verdict class (1,071 agree, 492 bend2-rejects, 99 unsafe, 4 out of scope).

On all of BendHub (4,832 files from 631 packages), comparing per file with and without the fix:

• the two files above move from mismatch to agree;
• no file moves between agree, bend2-rejects, unsafe and out-of-scope;
• the only other moves are timeouts and memory caps under load. The two files that moved into a timeout give the same verdict with and without the fix at 180 s.

A PR with this change and a regression test follows.

Found and tested with Claude Code, running Claude Opus 5.5, during an audit of --verdict.