Infer: keep Arrow type arguments, and make the type relations read the signature

[gunbai-bot]

Problem

A call through a binding whose type comes from a function type written as a type argument (List<fn() -> R>) was refused with function 'r' not found in scope. This broke gunbc-private CI through extdeps.apple.app_attest first_assertion_refusal, which folds over List<fn() -> AssertionRefusal?>.

Reproduction (steps 1 and 4 of the brief)

Built the seed from main e01e3d4 and compiled a public fixture with gunbc compile --source-root dag --source-root src/v2 --entry <fixture> --target dag|rust. Both targets refused, identically, on 6 forms:

• free fold(rs, …) and method rs |> fold(…) over List<fn() -> Int?>
• method map and free map over List<fn() -> Int>
• a unary element type List<fn(Int) -> Int>
• match rs |> first { Present { value: r } => r() … }

The refusal comes from shared inference, not from the dag emit path, and it has nothing to do with lambdas: a match-arm binding refuses the same way. Public CI stays green only because no required lane compiles app_attest.

Root cause, per §6b

Walking back from the call seam: the seam's callability test (type_node_is_callable, already repaired for the nullary case) was never given an Arrow. v1.compiler.infer_types child_type_node reads a type argument's inferred field as the type the child denotes. But an Arrow stores its codomain in inferred (make_callable_type, parse_callable_type_expr), so the element of List<fn() -> Int> came out as Int. That is the earliest boundary that can't be justified. The fix is there: an Arrow child denotes itself.

I also built a guard one link later (teaching type_node_is_established that a nullary arrow counts as established). Every specimen compiled without it once the arrow survived, so I withdrew it rather than ship an unneeded guard.

Evidence (all run locally with the rebuilt seed)

• test.claim.infer_callable_type_argument_witness_test: 3 discriminating cells (fold over nullary thunks, map over unary callables, match arm over first). Before the fix, the seed refused each of these shapes. Plus a control: an unbound callee inside the same lambda still refuses, with that callee as the subject. 4/4 PASS.
• Existing test.claim.infer_nullary_local_callable_witness_test: 6/6 PASS.
• The self_host_emitted_call_target_realization_witness_test cells over an arrow type argument (w_arrow_type_argument_at_a_record_field_renders_the_callable_carrier, and both w_sort_by_* cells): 3/3 PASS.
• gunbc compile --entry dag/extdeps/apple/app_attest.dag --target dag: 0 blocking.
• claim_executor --required-regen: first_generation_equal=true, planned=executed=161, so the stage0 mirror edit matches the generated output. (The first attempt caught a v2-parse ambiguity: != Arrow { … } inside an if read as a record literal. It is now parenthesised.)

Sweep

The only production site with a function type inside a type argument is extdeps.apple.app_attest. The other hits are a witness probe string (above, green) and a comment in 05_emit_rust.dag.

Failure-mode row

This is the same class, so I didn't file a new one. I added a residue receipt and evidence refs to gunbc.recurring_failure_mode arity_proxy_for_callability_misroutes_a_found_local.

Not claimed

I didn't compile the private composed root. The new witness drives the seed through gunbc.compile_census_probe (inference, shared by all targets). The --target dag receipt is the app_attest compile above.

Rework after the merge-review hold on 4108026

The hold was right: once child_type_node keeps the arrow, the relations downstream meet function types they never read. An arrow's signature lives in params and inferred, not children.

• node_type_equals_core used to compare two arrows by the name Callable, so List<fn() -> Int> and List<fn() -> String> compared equal. Now it compares arity, parameter types and codomain through one helper, v1.compiler.infer_types callable_signatures_agree, which takes the component relation as a parameter. The equality arm that already compared params (unreachable for arrows) now goes through the same helper, so there is still only one signature relation.
• node_type_compatible now applies that relation with compatibility as the component, where it used to fall through to name compatibility.
• type_resolution_verdict gets an arrow arm that checks params and the codomain. It runs first because the checks below it read inferred as the node's own type, which on an arrow is the codomain.
• node_type_shape renders Callable(params->codomain).
• A refusal main had only because of the erasure is kept on purpose. Returning List<fn() -> Int> where List<fn() -> String> is declared was refused on main only because the pair read as List<Int> against List<String>. I measured this with a binary built from main. With the arrow kept, neither side counts as ground and the pair was going unjudged. declared_type_conformance_diags now has a one-level element arm, callable_element_signature_mismatch, which hands both element arrows to the existing callable_signature_mismatch, so no second conformance relation is added. Parameter and arity mismatches also refuse now; main accepted both.

New cells in test.claim.infer_callable_type_argument_witness_test (floor-admitted), all run locally: 10/10 PASS

• Declared-return cells: codomain, parameter and arity mismatches each refuse with TypeMismatch. For example: expected 'Container(List,Callable(->Primitive(String)))', got 'Container(List,Callable(->Primitive(Int)))'. The control: the same signature is accepted with 0 blocking.
• Common-field consumer (enum_field_type_consistent), observed through the Rust emitter. On a coproduct whose variants carry List<fn() -> Int> and List<fn() -> String>, the previous head rendered m.callbacks |> count as m.callbacks(), a call to an accessor that is never generated. I diffed the output of the 4108026 binary against this head. That call is now gone, matching main. The control: one shared signature still renders impl SameCallbacks and s.callbacks().

Re-verified on the new seed

• claim_executor --required-regen: first_generation_equal=true (the v1 self-compile runs clean under the new relations).
• app_attest, std.algebra and std.materialization_ladder compile under --target dag with 0 blocking.
• infer_nullary_local_callable_witness_test: 6/6. The arrow cells of self_host_emitted_call_target_realization_witness_test: 3/3.
• Main is merged in; main hadn't touched any file in this diff.

Not covered by a gated cell: the resolution-verdict arm. No floor witness can import v1 compiler modules. The regen fixed point exercises it over the whole v1 corpus.

🤖 Generated with Claude Code