Type a let-bound lambda at its arrow; bind a CallableOf return to an arrow's return (#12143 items 5+6)

[gunbai-bot]

Follow-up to #12143 — gunbc.recurring_failure_mode function_typed_argument_mismatch_accepted, open items 5 and 6.

(5) v1.compiler.infer ExprLet bound an unannotated local at resolved_type(val). For a lambda that is its BODY type, so a local holding a function could reach an argument seam typed Int/Bool. It now binds at expression_value_type, which already mints a lambda's arrow. With that in place the expression_is_local_value exclusions on the one-sided arm have no reason left, so they are deleted.

(6) v1.compiler.infer_types unify_template: a CallableOf return variable bound to the whole argument type, which is wrong for a function value (typed as its arrow). xs |> map(nm) typed its elements as nm. An arrow argument is now read at its return.

Found on the way (one-sided arm): let f = fn(x) { 1 } is an arrow whose parameter is a fresh type variable. The old guard "either side has an unbound variable ⇒ unjudged" hid it. Function-ness is the arrow connective, not the arrow's leaves, so only an open NON-arrow side is now left unjudged (one_sided_non_arrow_side_is_open, both seams). This also judges a non-function given to a generic arrow formal; the ledger's path (5) is updated to say so.

Evidence — extends test.claim.infer_function_value_argument_arrow_witness_test:

• REDs: local_lambda_at_kernel_formal_refuses, local_lambda_return_mismatch_refuses, map_named_function_wrong_elements_refuses (item 6's discriminating RED), generic_formal_non_function_refuses.
• Controls: local_lambda_matching_accepted, local_lambda_called_accepted, map_named_function_elements_accepted, map_local_lambda_elements_accepted.
• Mutation run (the fix reverted, claims kept): https://github.com/gunb-ai/gunbc/actions/runs/36025711081. The floor failed exactly local_lambda_at_kernel_formal_refuses, local_lambda_return_mismatch_refuses, map_named_function_wrong_elements_refuses and local_lambda_called_accepted (a call of a let-bound lambda was refused before the fix). Nothing else failed.
• What the mutation run does not cover:
  • map_named_function_elements_accepted and map_local_lambda_elements_accepted pass without the fix too, so they are controls only.
  • generic_formal_non_function_refuses was added after the mutation run, so the mutation does not cover it.
• Green run on the fixed head: https://github.com/gunb-ai/gunbc/actions/runs/36046063862. All 8 new cells passed ([changed-witness] … outcome=passed), and the floor reports phases_failed=0.
• Mirror: --required-regen ran in one remote dispatch over the merged tree. Only my hunks were installed (v1_compiler_infer.rs, v1_compiler_infer_types.rs). The confirming regen reports first_generation_equal=true, and the installed and candidate sha256 are byte-identical.

Corpus population: measured only over the compiler closure. The gen-2 seed compiles the whole v1 compiler, v1.compiler.emit_rust emit_lib_rs_from_paths included, with 0 new refusals. Refusals outside that closure are covered by the existing declared drop gunbc.rung_drop compiler_change_refusals_land_outside_every_compiled_closure.

🤖 Generated with Claude Code

[gunbai-bot]

Re review 70934: agreed. The head is the deliberate mutation commit (6df7dfc), there to show the new REDs fail without the fix, as #12205 did. It gets reverted as soon as its floor run (36025711081) finishes, so the head will carry the fix, the ledger row and the claims together. The PR body will link both runs. Not for merge until then. — sent from nimble-wolf-724

[briansrls]

APPROVE-MERGE at exact head 7573b6e58ba14a75d5ce92802760cd0fa312f6ee.

The two open paths from function_typed_argument_mismatch_accepted are repaired at their respective inference authorities.

1. ExprLet now records an unannotated value at expression_value_type. For every non-lambda this is the prior resolved type; for a lambda it is the callable arrow already constructed from the parameter nodes and body result. That makes a let-bound lambda statically a function value, so deleting the special exemption for local values is justified rather than merely widening the checker.

2. The one-sided callable wall now treats function-ness as the top-level Arrow connective. Open leaves inside an arrow no longer hide that it is a function. Only an open non-arrow side remains unjudged, preserving the stated residual population. This correctly rejects both a local lambda at a kernel formal and a ground non-function at a generic arrow formal without pretending to solve unresolved/optional/non-ground non-arrow shapes.

3. CallableOf substitution now reads an arrow argument at its resolved return node. That matches the compiler's callable representation (make_callable_type stores the return under the arrow's Resolved inference), while a direct lambda continues to arrive as its body type. Consequently map(named_fn) binds the mapped element to what invoking the callback produces, not to the callback arrow itself; the same rule composes correctly for flat_map, fold, and the other CallableOf templates.

The witness set is appropriately discriminating: the local-lambda one-sided mismatch, local-lambda return mismatch, and wrong map(named_fn) element type are REDs; matching/callability and named/local callback cases are controls; the generic-arrow-formal case covers the open-leaf correction. The disclosed mutation limitation is acceptable: run 36025711081 reverted the implementation while retaining the claims and made the principal local-lambda and named-callback REDs fail, while the green exact-head run restores all eight cells. The generic-formal RED was added later, but it exercises the same small top-level-arrow decision and does not leave an unsupported parallel mechanism.

The ledger remains honest: record-field and method/pipe seams, non-ground nominal leaves, unresolved/optional non-arrow shapes, and block-produced one-sided return/data positions remain named residue. The compiler-closure census reports no new refusals; outside-closure exposure remains under the existing compiler_change_refusals_land_outside_every_compiled_closure drop rather than being claimed away.

The generated v1_compiler_infer.rs and v1_compiler_infer_types.rs changes are faithful projections of the .dag authority, and the reported fixed point is byte-identical.

Run 36046063862 passes compiler, clippy, emit-build, floor, and witnesses at this exact SHA. GitHub reports CLEAN and mergeable. No source condition remains; a later merge-group stage0-mirror or composed-tree red remains a real red to repair, not grounds to bypass the queue.