[nicolas-abril]

Addresses #1190.

Conversion treated eta inconsistently. A bare def name (case "Ref") was eta-expanded, so l == r held when l and r agree on fresh arguments. A partial call like l(U) went through the stuck-call path, which compares the head by name, so l(U) == r(U) failed. With an inline {==}, the shared-cell merge in compare_go repointed r's cell, so Box<r(U)> read as Box<l(U)>. As a result the inline proof was accepted and the same proof written as a named def was rejected.

compare_go (bend2/bend.ts) now does this, with no new helpers:

• Var, Ref and App are one case. A single loop walks both spines while either side is an App, compares the argument pairs, and counts each side's arguments. After the loop, the two sides are same if both spines had the same length, every argument pair matched, and the heads match (same variable, same def name, or otherwise equal).
• If they are not same and a head is a Ref short of its def's arity (book.tlds[k].n), both sides get that many fresh arguments and are compared again. A bare def is a call with zero arguments. Eta runs only after a failed comparison, so terms that already compare equal never pay for it.
• Mat keeps its own case, as on main.
• The first pass (RIGID, empty book) sees every def as arity 0, so it never expands and calls still compare by name there.

Doing the eta in term_wnf instead (a short call reduces to a lambda) was tried and rejected: it changes partial calls outside conversion, and tests/check/template_inst_cycle.bend hangs.

Case	main	this PR
inline make()({==})	accepted	accepted
named make()(proof())	rejected	accepted
{l(U) == r(U) : Type -> Type}	rejected	accepted
x: Box<r(U)> returned as Box<l(U)>	rejected	accepted
r(A,B) = B (really different), inline {==}	rejected	rejected
r(A,B) = B, {l(U) == r(U)}	rejected	rejected

Tests: tests/check/partial_call_eta.bend (the issue's example and its variants) and tests/check/partial_call_eta_distinct.bend (the different-r case, which must fail).

Gates (macolas, on 749eb6d): repo 54/54, test 1699/1699, safe tests 1712 files: agree 1101, false reject 0, timeout 0. Not run: ping, perf gate, tsc, CUDA, Linux.

Cost: checker benches, main vs this PR, 9 interleaved rounds on one machine (median s): compute_1600 .529/.523, defs_12800 .324/.320, generics_3200 .409/.408, proofs_3200 .857/.858 (15 rounds: .850/.851), trees_400 .641/.641. The first version (ccbcfbb, eta before the switch with term_unapply) was 4-9% slower on all five.

— written by an AI agent (Unii) for @nicolas-abril

[nicolas-abril]

Closing: #1190 is not a discrepancy between bend2 and BendTT, and not a false positive. bend2 and BendTT agree on every repro (inline accepted by both; the named form is rejected by bend2 before reaching BendTT). What's left is a completeness gap in bend2, which a bend.ts change doesn't need to fix.

[Lorenzobattistela]

se a head dá match mas os argumentos são diferentes, a comparação falha e tenta eta, oq recompara tudo e se tiver aninhado fica exponencial (tem um repro de 4s no PR q demora 0.03 na main)

f(200001n) = f(200000n) passa na main e nao passa aqui pq da stack overflow pq desce um literal por vez

a fresh var do eta da leak pra uma shared cell externa (rhs.v = lhs.v e o erro buga, checker fica num estado bugado (tipo Box<c(U, _^1)>

os argumentos compara antes da head, oq faz comparar todos os args antes de falhar se a head for diferente

o eta roda quando um lado da def só é parcial

e um dos testes passa na main partial_call_eta_distinct.bend