Step 2: a generic fixed only by a lambda's return is solved from it (p8/p8b/p9 refuse; #9416 narrowing lifted)

[gunbai-bot]

Derived-node identity step 2. A generic fixed only by a lambda's return is now solved from that return, so a wrong value there becomes a located refusal instead of a silent acceptance.

Derivation (DESIGN §6b)

1. The narrowing. v1.compiler.infer infer_call_arguments_generic_pass skipped every lambda argument for unification. The note above expr_contains_lambda (A lambda parameter whose declared type is a type variable now binds it: two independent defects, one of them a fabricated empty type #9416) stated the consequence: "a lambda return feeding a later formal — is still out of reach". This PR lifts that narrowing and rewrites the note beside the change.
2. The representation. A typed lambda carries its body's return in inferred (infer_expr ExprLambda), not a callable type. A first build that unified resolved_type(lambda) against the formal Arrow had zero effect, measured. The repair builds the lambda's callable type at the call site with the existing authority make_callable_type (lambda_callable_type).
3. The unify arm. unify_generics gains an Arrow arm, unify_callable_generics. It unifies parameters positionally and then the return, each read through child_type_node.
4. What a lambda may contribute. It contributes in round 1 only, and only an informative binding that fills an Absent slot (unify_lambda_solves). It never overrides an existing binding. A lambda return that is itself an unresolved variable (callable_param) is dropped. Round 2 is unchanged, so the bound stays at two rounds.
5. Mismatches were already judged. A round-2 mismatch refuses on main and still refuses here. It is enrolled as a control below.

Removed after review: an empty-literal placeholder rule. It let a later actual replace a binding to the empty_list_element placeholder. It was spellable (any TypeVariable with that id matched, including an authored generic), and no case I could construct showed any effect: [] in argument position takes the formal as its expected type, and a let-bound [] gave identical results on main and here. Rule, id constant and lambda-path override are all deleted.

Enrolled witness: test.claim.lambda_return_solves_generic_witness_test

The witness runs each source through the real compile census (gunbc.compile_census_probe); each helper returns -1 when the census cannot run.

test	main	this PR
a_generic_fixed_by_a_lambda_return_refuses_a_wrong_argument_position (p8: lrs_take(b: lrs_idf(f: fn() { 5 })))	false	true
a_generic_fixed_by_a_lambda_return_refuses_a_wrong_declared_return (p9)	false	true
a_lambda_after_the_argument_that_fixes_its_parameter_solves_the_result (p8b)	false	true
the_same_calls_at_the_type_the_lambda_returns_are_accepted (control)	true	true
a_lambda_return_that_disagrees_with_a_fixed_parameter_refuses (round-2 mismatch control)	true	true
a_lambda_before_the_argument_that_fixes_its_parameter_stays_unsolved_at_the_two_round_bound (p7b boundary pin)	true	true

Removing the arm reds the first three. The p7b pin is expected to go red when the unbound_generic_reaches_conformance_unjudged wall lands, and is then rewritten to assert the refusal.

Predictions (sent to the program owner before the run) and outcomes

#	prediction	outcome
Q1	p8 refuses Int at a String/Bool position	HIT
Q2	p9 (declared-return form) refuses	HIT
Q3	p8b refuses	HIT
Q4	p7b stays Accepted (stated bound)	HIT: now pinned in the witness
Q5	p7c control accepted; p7a mismatch still refuses	HIT
Q6	nlF, fold_list(xs, empty: [], cons: snoc(acc, m)) then a field read, becomes Accepted	MISS: it still refuses no field 'module' on type 'Unit', as on main. The cause is not located. A self-contained copy with local generics reproduces the miss. It is a pre-existing refusal on main, not a regression, and it is owned by the shape-2 PR #13330.
Q7	regen converges	HIT: fresh checkout, first_generation_equal=true, rebuild_packages=0

P5: census before/after

gunbc test //gunbc/instruments:generic-identity-census over the v2 compile closure, run in place against main aae7da34ca (the main merged into this branch) and against this PR. STANDING held and all 7 controls held on both.

report line	main	this PR
foreign_in_a_value_argument	2612	1249
foreign_in_no_value_argument	4190	4212
in_scope body type declaration+type_variable	953	957
in_scope body type declaration_only	92	91
renamed_argument_child_unmarked	235375	238165

The two rises were diffed at identity grain. That row diff ran at base 864c9ce0c9, with the since-removed placeholder rule in; the matched deltas above are +2790 and +22, against +2780 and +22 there. I have not re-diffed the rows on this base.

• renamed_argument_child_unmarked: only gained rows, none lost. All are body_expression_type rows in which a body expression whose type was an unbound generic is now a concrete product, and the census counts that product's field children. The largest groups:
  • TargetText's empty/parts in v2.compiler.target_serialize serialize_relation_row_nested_bounded;
  • Cons's head/tail in v2.compiler.body_lowering_fold body_lower_collect_param_edges.
• foreign_in_no_value_argument: +22, none lost. The unsolved parameter moved one layer inward.
  • In v2.std.compilers.semantic_decl_emission semantic_decl_binding_spelling_rows_from_catalog, bind_outcome::<U> (main: foreign_in_a_value_argument) is now solved from the lambda's return. That return is outcome_rejected(...), whose own T no value argument carries.
  • optional_absent::<T> in v2.compiler.body_lowering_fold body_lower_declared_domain_from_param_list has the same shape.
  • These are pre-existing unsolved parameters made visible, which is the wall's population.

P6: self-host emitted-artifact diff

gunbc compile --entry src/v2/compiler/00_compile.dag --target rust, main aae7da34ca against this PR.

• Emitted files. 243 on both sides. Three differ, and each is one lambda parameter gaining its type:
  • v2_compiler_infer.rs: pair: _ becomes pair: Rc<InferTypePair>;
  • v2_std_demand_engine.rs: the sort closure's parameters become &Rc<DemandIdentity>;
  • v2_std_type_binder.rs: pa: _ becomes pa: Rc<TypeParamArgument>.
• Blocking errors. 0 on both sides.
• Advisories. 4067 on main, 4061 here: 6 removed, none added.
  • Five are "produced identity erased" inhabitance advisories, at 04_infer.dag:3432 (×2), fn_index.dag:268, qualified_name.dag:429 and type_binder.dag:314.
  • One is a "text boundary unjudged" advisory at 00_compile.dag:5924.

Whole-corpus refusals: none. CI's floor run (the whole-corpus check) is green on c431ac6ec0, as are emit-build, generated and witnesses.

Row: unbound_generic_reaches_conformance_unjudged records this PR closing its lambda-return member. Its NEXT TRIGGER now names p7b as the wall's discriminating member and p8/p8b/p9 as closure controls.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 76610 in a361b1e. The branch is now at 2ece97e after merging main and regenerating the infer mirror in a fresh checkout (round 3: first_generation_equal=true, convergence_stages=0, rebuild_packages=0).

• Spliced comment: correct, and fixed. The rationale sentence above expr_contains_lambda reads whole again, and the round-2 mismatch paragraph follows it.
• Commit pin: removed. I did not name the p8/p8b/p9 probes, because they are scratch fixtures, not enrolled witnesses, so naming them would cite something nothing re-derives. The note instead points at gunbc.recurring_failure_mode unbound_generic_reaches_conformance_unjudged, where those specimens and the wall that closes the open case are recorded. That row now also says that this PR closes its lambda-return member and that p7b stays open.

The PR body now also explains, at identity grain, the two census rises the program owner asked about.

— sent from jolly-pike-330

[briansrls]

NO-LAND at this exact head for one correctness blocker, plus one authority/control blocker.

1. empty_list_element_variable_id is not an identity; it is a spellable TypeVariable.id. unify_binding_is_placeholder claims that only the compiler-minted empty-list placeholder yields, but it returns true for every TypeVariable { id: "empty_list_element" } (and recursively for a one-child carrier containing one). Authored generic parameters use the same carrier with the authored parameter name as the id. Therefore a legal authored parameter named empty_list_element is treated as the compiler placeholder, and either unify_generics or unify_lambda_solves may overwrite that informative binding with a later concrete actual. That directly violates this PR's stated rule that an informative binding is never overridden, and can turn an outer generic into a concrete result by spelling collision.

Please give the minted placeholder an unauthorable identity/spelling, or use a declaration/origin-backed distinction, and add a collision control with an authored generic named empty_list_element proving it never yields. The control should exercise both the ordinary later-actual replacement path and the lambda merge path if both retain the predicate.

2. The repaired behavior has no committed executable witness: p8, p8b, p9, p7a/p7b/p7c exist only as scratch receipts/prose. This is a load-bearing infer rule and the current floor can remain green if the lambda contribution is later removed. Please enroll a small compile fixture that pins the concrete-return refusals, the round-2 mismatch control, and the stated p7b two-round boundary. While doing so, correct the canonical row's stale NEXT TRIGGER text: the preceding PARTIAL CLOSURE says p8/p8b now refuse with a concrete Int-vs-String mismatch, but the trigger still says p8, p8b and p7b must refuse with the future cannot infer cause. The future unresolved wall's discriminating member is now p7b; p8/p8b are closure controls, not members awaiting that cause.

The Arrow construction through make_callable_type, positional parameter/return unification, first-round-only merge, whole-closure census explanation, and the stated p7b boundary otherwise look coherent; exact-head CI is green.

[gunbai-bot]

Addressed review 76646, and the two blockers raised in the side-chat review of 2ece97e, at c431ac6 (with f84c29d).

1. No enrolled witness. Fixed. test.claim.lambda_return_solves_generic_witness_test runs sources through the real compile census. It has three reds (p8, p9, p8b), each asserting a blocking TypeMismatch, plus three controls: the accepted same-type calls, the round-2 mismatch that must still refuse, and the p7b two-round boundary pin. I measured all six against main's binary and this PR's: the three reds are false on main and true here, and the three controls hold on both. The table is in the body.
2. The placeholder rule widened every unification (and its id was spellable, so an authored generic named empty_list_element could collide). Removed rather than fixed. I could not construct any case where it changed an outcome: an argument-position [] takes the formal as its expected type, and a let-bound [] gives identical results on main and here. Rule, id constant and lambda-path override are all deleted. A lambda's contribution now only fills an Absent binding and never overrides one, so there is no replacement path left for a collision control to test.
3. The class row's trigger. It now names p7b as the wall's discriminating member, and p8/p8b/p9 as closure controls.

The mirror was regenerated in a fresh checkout (first_generation_equal=true, rebuild_packages=0). P5 and P6 were re-measured against the main this branch merged (aae7da34ca).

— sent from jolly-pike-330