[ScottMoore0]

Fixes #1619.

--verdict reported a mismatch for a proof bend2 accepts when a function sits in a field whose type is a parameter (a pair's component, Some's value):

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

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

In pair:
expected: (keep λx1 => (x0 x1))
observed: (.Tuple, (x0, ((.False, ()), ())))

Cause.

• arg_term sends the call's function-typed argument η-long.
• The equation's (v, False{}) is a term in a type, so it arrives bare.
• arg_term gives a bare λ or match its goal A, but not a bare constructor.
• So ctr_term gets T === null, cannot fill the pair's parameters, and leaves v bare.
• The kernel converts without η, so λx1 => (x0 x1) never meets x0.

Fix. Give a bare constructor its goal too:

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

The same cause, two more symptoms. Sebastian Griego reached the same fix independently (#1621). His two tests show that a bare constructor losing its goal breaks more than η:

• tests/proof/generic_constructor_erased_lambda.bend: a lambda in a generic Box at @-x: Type -> Type. The kernel reported a λ of its binder's liveness.
• tests/proof/generic_constructor_dependent_function.bend: a field whose type depends on an earlier field. Export reported an application past its head's known type, and --verdict rejected the file.

They are added here unchanged, with him as co-author.

Tests.

• tests/check/ctr_param_field_eta.bend covers the pair and a template's Some{v}.
• The two tests above.

All three check as before. On main (234cb9b), --verdict rejects each; with the fix, each prints ALL PROOFS CHECK. So gates/safe.ts tests fails without the fix.

What I ran (Linux x86_64 under WSL2; I can't run the minis):

• bend2's check and --verdict on the three tests: rejected on main, ALL PROOFS CHECK with the fix.
• gates/safe_node.ts locally over all of tests/ and demos/*/PROOF.bend: every file keeps its verdict class (1,071 agree, 492 bend2-rejects, 99 unsafe, 4 out of scope).
• The same over all of BendHub (4,832 files), per file, with and without the fix:
  • bend-collections-laws-containers@1.0.0.0 dynamic_array/{proof,owned_instances}.bend goes from mismatch to agree;
  • no file moves between agree, bend2-rejects, unsafe and out-of-scope;
  • the only other moves are 30 s timeouts and memory under load, and the two that slowed into a timeout give the same verdict with and without the fix at 180 s.

Not run: gates/test.ts and gates/perf.ts (the minis).

Size. safe.ts is 23,978 ttok on main by my local ttok==0.3, and 23,986 with this change, under the 24,000 cap. My local count also reads comp.ts on unmodified main as 64,092, over its cap, so it differs a little from CI's. The repo gate here will say.

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

[sebastian-griego]

I closed #1621 as a duplicate of this PR. I reached the same one-line fix independently. I missed your earlier PR before I opened mine.

My two additional tests cover different field types and may be useful here:

• generic_constructor_erased_lambda.bend: a generic Box stores x => Type at @-x: Type -> Type. Before the fix, export gives the lambda a live binder and the kernel reports a λ of its binder's liveness.
• generic_constructor_dependent_function.bend: a generic constructor has a function field whose result type depends on an earlier field. Before the fix, export reports an application past its head's known type, omits the theorem, and --verdict rejects the file.

Both tests pass source checking before and after the fix. Both fail --verdict on main 234cb9b9 and pass with the identical safe.ts change and unchanged BendTT kernel. The ordinary runs match their #| lines; --verdict is the check that detects these failures.

Please use either or both tests in this PR. They have no dependency on other changes.

[ScottMoore0]

Thank you - your tests caught the binder-liveness and out-of-scope failures, which mine didn't, so I've added both and attributed you.