v2 infer: derive a call's result type from a declared return (instantiated, alias-normalized)

[gunbai-bot]

Fixes the class recorded in #13314 (the RFM row is not on main yet, so the code cites no row; the citation and climb receipt follow once #13314 lands): v2 infer never typed a call whose callee declares a non-kernel return, so the call stayed underived and every declared position it reached accepted it as undecidable. This is N7's (//v2/test/parse/expression_bodied_fn_decl_parse:all) wall after #13307: the test reads artifact.tree off a match over parse_module_prepared's Outcome<ParseArtifact>.

Derivation (DESIGN §6b)

• Earliest unjustified boundary: v2.compiler.infer infer_arrow_declared_return_type knew only kernel value types (dag_binding_denotation, plus Bool by authority). Every other declared type in the stage is already used as written; the call-result reader was the one consumer that wasn't.
• Second gap, for generic returns: infer_application_argument_inhabitance discarded the TypeVariableInstance list that infer_judge_formal_args (v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted #13187) builds, so Outcome<T> could never be instantiated at the call.

Change

1. infer_application_argument_inhabitance returns the instance list; infer_transform_derived_optional / infer_transform_application_optional take it (the "arguments decided" condition is unchanged).
2. infer_application_result_type(arrow, instances, declarations): the kernel answer FIRST (Int/Bool byte-identical); otherwise the declared return node, alias-normalized (infer_type_alias_normalized, v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted #13187) and instantiated with this call's instances. A return still mentioning one of the callee's own type parameters (read off the arrow, type_param_names) stays NOT derived (the counted frontier), never a fabricated instance.
3. Scope growth, stated: deriving boxed(1) as Box<Int> exposed that infer_projection_receiver only accepted a bare declaration path, so Box<Int>.item would newly REFUSE a correct program as declares_no_fields. The reader now splits head and arguments (infer_type_head_and_args), binds the head's type parameters to the arguments in declared order (the pairing infer_match_coproduct_of_type already uses), and types the field at that instantiation (infer_projected_field_type). A non-generic receiver is unchanged. An argument-count mismatch refuses with its own reason, infer_reason_projection_receiver_type_arity_mismatch.

Witnesses (DESIGN §3 witness rule)

v2.test.claim.compiler.declared_return_result: five claims SUPPLY the callee arrow and the call's instances at the result-type interface (no assembly); ONE claim runs the real path (source → assembly → infer) and asserts the ROUTE.

claim_batch, remote, sha pinned, memory cgroup bound. "Old behaviour" = this head with infer_application_result_type returning the replaced reader (infer_arrow_declared_return_type) and infer_projected_field_type returning the field as declared; the supplied claims call functions main does not have, so that mutant is their red-before.

Claim	head 4bb4bf5	old behaviour	eval_steps
a declared return is the call result (and the old reader answers Absent)	PASS	FAIL	611
a kernel return is unchanged	PASS	PASS	219
a generic return is instantiated at the call (Box<T> → Box<Tally>)	PASS	FAIL	1,021
a return mentioning an unbound type parameter is not derived	PASS	PASS	859
a generic record field projects at its instantiation	PASS	FAIL	174
a wrong type-argument count at a generic record projection refuses (ReceiverArityMismatch, reason infer_reason_projection_receiver_type_arity_mismatch); red with the arity check bypassed	PASS	FAIL*	1,027
real path: wants_bool(boxed(1).item) refuses as application_argument_does_not_inhabit	PASS	FAIL	931,162

*For the arity claim the red-before is a mutant with only the arity comparison bypassed (39add2b); the arm and its claim were added for review 76227. infer_projection_receiver_of_type is split out of infer_projection_receiver so the type-to-payload step takes supplied inputs.

The two claims that pass both ways are deliberate: one guards that kernel returns did not move, the other that an unbound parameter is never fabricated.

Neighbours at head (ab6fc3d, before the restructure): generic_formal_instantiation 12/12, field_projection_stages 25/25 (25/25 at main too, including fps_a_match_binder_receiver_is_not_yet_typed_holds).

Cost: the real-path claim (930,914 steps on the CI floor) is the module's ONE inhabitance claim; the others are supplied, the shape DESIGN §3 asks for. Its fixture program (drr_route_source) has no other demander, so #13043's derived sharing cannot cover it; it carries one NEW floor_single_claim_fill_debt member (SingleClaimFillDebtModule for v2.test.claim.compiler.declared_return_result, ActiveFillDebt), citing floor run 37247019357. New debt: sharp-raven-357 approves it. No floor_cross_claim_pure_producers_warm row is added.

Floor

Green at 2a96a45 (run 37274575061: floor, generated, emit-build, witnesses all pass). The route claim's assembly AND inference are one nullary producer (drr_route_reason) filled under its single-claim fill debt; at 39add2b (run 37268434424) only the assembly was billed to the debt and the inference left 125,904 steps in the claim's marginal.

Census (floor run 37247019357 at 4ee3045)

planned=677 executed=677 passed=667 known_red_held=5 claims_failed=0. No planned claim flipped from accepted to refused. The floor's only refusal is the cost line above. Bounded honestly: this is the floor's changed-witness population for this diff, not a corpus-wide v2-infer census (no such instrument exists). The N7 native route has not been re-run on this head.

Not done

• the RFM: a call's result is unjudged in v2 infer when the callee returns a declared type (below floor; N7 next wall) #13314 RFM receipt (that row is still open on its own branch);
• the N7 native route re-run at this head.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 76227 in 39add2b.

1. Unresolved citation. RFM: a call's result is unjudged in v2 infer when the callee returns a declared type (below floor; N7 next wall) #13314 is still open and not queued, so the two citations of call_result_of_a_declared_return_type_unjudged_in_v2_infer (04_infer.dag and declared_return_result_test.dag) are removed rather than copying the row here. They come back, with the climb receipt, once RFM: a call's result is unjudged in v2 infer when the callee returns a declared type (below floor; N7 next wall) #13314 lands.
2. Untested arity arm. infer_projection_receiver_of_type is split out of infer_projection_receiver (which now calls it), so the type-to-payload step takes supplied inputs. New claim drr_a_wrong_type_argument_count_at_a_generic_record_projection_refuses: a hand-built index declares Box with one type parameter; Box<Tally, Tally> yields ReceiverArityMismatch, Box reads the payload, and the arm's diagnostic reason is infer_reason_projection_receiver_type_arity_mismatch. Red first: with the arity check bypassed (the count comparison forced false), this claim FAILS and the other five still pass; at head all six PASS. Cost: 1,027 eval_steps (claim_batch, remote, sha pinned, memory cgroup bound).

— sent from calm-boar-904

[gunbai-bot]

Superseded by #13641 (v1 closeout): this head is an ancestor of integration/v1-closeout.