[nicolas-abril]

Fixes #1133 in the kernel. Supersedes #1136, which annotated in the elaborator and made inferable stricter than Term.infer.

What fails

Term.infer's App rule returns B[x]. When x is a λ or λ-match (the η-long form safe.ts gives a function argument), each call (f a) in B becomes a redex with a λ head. Term.infer can't type a bare λ, and elim only covers a variable argument. A + let checks its inferred type as Data, which infers those calls:

!+x3 = (Equal.cong -(Pair -U32 -Bool) -Bool -λx3 => (snd_of x3) -x1 -(mk x0) x2); x3

V = {((λx3 => snd_of x3) x1) == ((λx3 => snd_of x3) (mk x0)) : Bool}. Checking V : *2 reaches infer (λx3 => …) on the right side and fails with expected: an annotated term. bend2 accepts, because its HOAS substitution β-reduces.

The change

def Term.arg (x A : Term) : Term :=
  if Term.takes x then Ann x A else x
...
      pure (Term.inst B (Term.arg x A))

The rule has just checked x : A, so it puts {x : A} into B. Every such call then has an annotated head, which the ordinary App rule infers. That covers any arity, partial applications, arguments that don't infer (constructors), and types that depend on the argument.

Proofs

Typed is unchanged. {x : A} reduces to x in one Par.unann step, so chk's App case adds one conversion. lean bendtt.lean elaborates with no sorry, and consistent, book_check, sr, progress, halts, empty and confluent depend only on propext, Classical.choice and Quot.sound.

Checks (macOS arm64, Lean 4.34.1)

• tests/proof/cong_lambda_argument.bend covers one and two arguments, a partial application (fst_snd(x) : U32 & Bool -> Bool) and a constructor argument (Bool.not(True{})). It prints True and --verdict says ALL PROOFS CHECK. The kernel on main rejects it.
• Three arguments and an inline lambda also check (not added as tests).
• Over all tests, the old and new kernel give the same verdict on every emitted .bendtt (1026) except the new test.
• Cost: 6560 arguments are annotated over the tests, but only 46 annotations land in a type. The rest go into a B that doesn't mention the argument, so the type comes out the same as without it. Over the suite the kernel retires 98.16G instructions against main's 98.27G (−0.11%). A build that never annotates is at +0.05%, so the difference is noise.
• bendtt.lean is at 63901 ttok. gates/repo.ts passes 49 / 49.

Not run: gates/safe.ts and gates/test.ts on the cluster.

A λ-headed redex written directly into .bendtt text still doesn't infer, as on main. The elaborator never emits one, because bend2's checked terms are already β-reduced.

🤖 Generated with Claude Code