v2 infer: declared returns are judged by the one inhabitance relation (replaces #12379's inline check)

[briansrls]

Claim

v2 judges a fn body at its declared return through the same relation that judges an argument at its formal: v2.std.inhabitance declared_type_inhabitance, with two producers (PositionDirectCallArgument, PositionDeclaredReturn) and one judge (v2.compiler.infer infer_judge_declared_position).

This is a replacement cut, as ruled by the lane manager. #12379 (landed 2026-09-28, after this branch was cut) had added an inline equality check, infer_arrow_body_inhabits_declared_return, on arrow introduction. That check is deleted here, and its reason arrow_body_does_not_inhabit_declared_return is kept, still located at the body, so diagnostics don't churn. Leaving both in place would have been a §3 fork: two checks for one fact.

What changes in behaviour:

• Declared types are compared as the value types they denote. Each atom is read through dag_binding_denotation, so Bool compares as bool_node. Without this step the relation refused fn f(x: Int) -> Bool { true }. The same step now applies to argument formals.
• A bare return that dag_binding_denotation doesn't recognise is counted. It gets UndecidableFormalUnresolved. v2 infer: arrow elimination + body/declared-return check; one Int, one Bool value type #12379 admitted it with no diagnostic (a §5 silent arm).
• A return that mentions the fn's own type variable is counted. It is admitted with UndecidableGenericFormal and never refused. By a source regex (approximate), 698 bodied generic fns in the corpus declare such a return (98 bare -> T, 600 inside a type). All stay admitted; before this change they were admitted silently.
• Instantiation formals are decided unless they mention a declared type variable. Instantiations were previously always counted as generic. Measured consequence: a record argument at a List<Int> formal now refuses (application_argument_does_not_inhabit) instead of being counted. The test is renamed inhabitance_product_produced_at_a_collection_formal_refuses_holds.

Controls and receipts

Run with a locally built claim_batch (built from the merged tree), over infer_declared_return_inhabitance_witness_test, infer_application_argument_inhabitance_witness_test and infer_arrow_elimination_witness_test.

Run	Result
origin/main	17/17 pass (argument + arrow-elimination files)
previous head (merged, before rework)	6 of main's claims FAIL (Bool-at-Bool refused, reason changed, undenoted return refused), and all 6 infer-routed declared-return claims FAIL, admits included
this head	29/29 pass (12 + 10 + 7)
this head, infer_arrow_declared_return_check neutralized	8 go red: the 3 return REDs, the undenoted and type-variable counted controls, and #12379's 3 REDs (infer_int_body_at_declared_bool_refuses_holds, infer_bool_body_at_declared_int_refuses_holds, infer_bare_arrow_with_mismatched_body_refuses_holds). All admits stay green.
this head, denotation step removed	4 go red: declared_return_bool_with_a_bool_body_admits_holds, declared_return_list_of_bool_with_a_bool_list_body_admits_holds, infer_bool_application_derives_bool_holds, eval_bool_application_is_the_evaluators_true_holds

Why the earlier head's admits failed even with the producer neutralized. The fixture's Arrow had an empty domain. Every node in these fixtures is OccurrenceSynthetic, and a childless product derives the childless synthetic node, which is itself, as its evidence. canonical_grounding_from_derived_type therefore refuses it with grounding_evidence_is_source before any return is judged. A lowered domain carries its fn's occurrence id and cannot reach that state. The fixture now has a one-parameter domain, the same shape as infer_arrow_elimination_witness_test ae_domain.

CI failure at 5366696. It was the same two causes: the fixture defect, and the declared side being compared as written against #12379's resolved value types.

Rows edited

• gunbc.recurring_failure_mode.argument_type_obligation_absent_while_the_route_advances: the RUNG FOUND AT receipt now records the second producer, the replacement of v2 infer: arrow elimination + body/declared-return check; one Int, one Bool value type #12379's check, the comparison at the declared type's denotation, the counted undenoted return, and the collection-formal refusal. The NEXT-RUNG trigger names an application's result type.
• gunbc.recurring_failure_mode.annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation (new): the annotated let is still judged by coercion_cast_crossing, a third relation for the same question. Found while wiring this producer and kept out of scope by ruling.
• gunbc.recurring_failure_mode.function_type_evidence_carries_its_body: its trigger now cites the surviving return check instead of the deleted one.

Not covered (stated, not papered over)

• A non-bare undenoted atom inside a declared type (e.g. List<Foo>) is compared as spelled. Only a bare undenoted return is counted.
• Native emission is unclaimed, as the row already records.
• These are infer-tree fixtures, not source text. A source-text v2 acceptance harness is the file's next-rung trigger.

🤖 Generated with Claude Code

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-28T21:58:13.197306Z	3653f3a	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 3653f3a13b

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Remove the mutually exclusive probe claims

When this claim entry runs, every test fn must return true, but pr_tree() deliberately has an Int return and a Bool body, so the new return check should reject it and make p_accepted return false. If the tree is accepted instead, the rejection probes below return false; moreover, p_rej_arg expects an application-argument reason even though this change maps return mismatches to declared_return_does_not_inhabit. Thus the committed debug probe guarantees claim-run failure and should be removed or replaced with a single assertion of the intended outcome.

Useful? React with 👍 / 👎.

[gunbai-bot]

Review 72379: fixed in 5366696. zz_probe_dr_test.dag is deleted (six mutually contradictory exploratory probes plus a copied fixture block, with no consumer). The reviewer called the remaining change sound (return check and argument check as one inhabitance relation with two producers).

Converted to DRAFT: this PR is an auto-save of bold-gull-638's branch after that session was archived. The body is still the unfilled template, with no summary, no test plan, and no record of which declared-return controls were run. It needs its owner to state the claim, the discriminating controls, and their results before it's ready.

— sent from neat-boar-16

[gunbai-bot]

Ownership moved to smart-newt-725 (bold-gull-638 is archived; neat-boar-16 ruling). New head 76bc35d: main merged, and the declared-return witness now hands infer a ResolvedTree through v2.test.lens_common.infer_fixture claim_resolved_tree_without_declarations at its four infer calls. It passed a bare Node, which the checker refuses at the direct call argument on current main. Scope is unchanged: the one judge. Local run on this head, claim_batch built from current main's seed: declared-return 12/12, application-argument 10/10, arrow-elimination 7/7.

[gunbai-bot]

Does this PR lower a rung for an optional returned where a required type is declared? Answered by execution: no, on the route that exists today.

Two one-line controls, run from source text through the production front end (tokenize, parse, normalize, resolve) into v2.compiler.infer infer, on both trees with the same claim_batch:

fn orp_f(x: Int?) -> Int { x }

fn orp_p(x: Int) -> Int? { x }
fn orp_f(x: Int) -> Int { orp_p(x: x) }

tree	both controls
origin/main fbdfd65 (the inline check this PR deletes)	Rejected, reason infer_descent_not_derived
this PR, 76bc35d	Rejected, reason infer_descent_not_derived

Neither verdict carries arrow_body_does_not_inhabit_declared_return, and neither is an acceptance. I found the reason by asking the verdict for each of the 46 refusal reasons v2.compiler.infer and v2.std.inhabitance can emit; exactly one answered, the same one on both trees. Beside them, on both trees: fn f(x: Int) -> Int { x } is accepted and fn f(x: Int) -> Int { true } refuses at the return.

So a program that mentions Int? is refused by infer before either return check is asked: the Cardinality type node has no descent witness. The deleted check never got to judge this case and neither does the new judge, and the verdict for these programs is unchanged by this PR.

What is still true by reading, and not reachable by execution today: the two checks differ at their own interface. The deleted check compared by structural equality, so a Cardinality body type at a denoted Int would have refused; the judge here answers UndecidableOptionalCarrier for a Cardinality node on either side and admits with an advisory. That difference becomes live the moment optional types get a descent witness. It is tracked as a follow-on in v2.std.inhabitance (the converse direction is decided, not undecidable), owned by this session.