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

dag/gunbc/recurring_failure_mode/annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation.dag

@@ -0,0 +1,26 @@
+module gunbc.recurring_failure_mode.annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation: RecurringFailureMode = RecurringFailureMode {
+  identity: "annotated_let_judged_by_the_cast_relation_not_the_inhabitance_relation" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: v2 answers one question -- does this produced value inhabit this declared type? -- through two relations chosen by position. An argument at its formal and a fn body at its declared return build a DeclaredTypeObligation and consult v2.std.inhabitance declared_type_inhabitance; an annotated let (`let x: T = e`) is judged by v2.compiler.infer infer_bind_annotation_check through v2.std.coercion coercion_cast_crossing, the fold a cast's crossing asks.",
+
+    "HARM: a meaning fork at the relation layer (DESIGN section 3). The two relations are different procedures -- coercion selects a target-language inhabitant spelling under a TargetSelectionPolicy with its own mismatch vocabulary, inhabitance is find_witness over the declared singleton -- so one produced/declared pair can be admitted at a let and refused at an argument or a return, or refused under two different reason vocabularies. v2.std.inhabitance declared_type_inhabitance already records why routing an inhabitance question through coercion_fold would nickname target selection as typechecking; the let position does exactly that.",
+
+    "DISTINGUISHING FACTS: an ascription converts nothing (infer_bind_annotation_check uses only the verdict, never a crossed value), so the let question is inhabitance, not a cast. DeclaredTypePosition names PositionDirectCallArgument and PositionDeclaredReturn and has no let arm; v1's DeclaredTypePosition carries PositionLetAnnotation, so the seed already models the let as a declared-type position of the one relation.",
+
+    "RECOGNITION RULE: a DeclaredTypePosition-shaped question (produced type at an authored declared type) answered anywhere other than declared_type_inhabitance. Found 2026-09-27 while wiring the PositionDeclaredReturn producer (brief node adhoc-0e837314-c3c), and kept out of that change by the lane manager's ruling so the return producer lands on the relation its frontier named.",
+
+    "RUNG FOUND AT: mitigatable on the let path (a mismatch coercion recognises refuses, located at the annotation, infer_reason_bound_value_does_not_inhabit_annotation); the fork itself is unrefused by any gate and held only by review.",
+
+    "CEILING: structurally impossible -- one relation, positions as data. Decidable and fully modeled: the relation and the position vocabulary both exist.",
+
+    "NEXT-RUNG TRIGGER: a PositionLetAnnotation arm on v2.std.inhabitance DeclaredTypePosition with infer_bind_annotation_check building a DeclaredTypeObligation and consulting declared_type_inhabitance, and coercion_cast_crossing no longer imported by that check, sufficient that every declared-type position in v2.compiler.infer reaches one relation; the let's discriminating RED and positive control re-enrolled on that route.",
+  ],
+
+  evidence: [],
+}

dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag

@@ -15,7 +15,7 @@ data argument_type_obligation_absent_while_the_route_advances: RecurringFailureM
 
     "RECOGNITION RULE: an application whose argument type is derived and a distinct constructor from the formal is Accepted. The discriminating RED is v2.test.claim.compiler.infer_application_argument_inhabitance_witness_test infer_incompatible_argument_refuses_holds (Bool at an Int formal). Positive control: infer_compatible_argument_admits_holds.",
 
-    "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). A TypeNode Cardinality formal is not yet that counted frontier on infer: connective_multiplicity maps Cardinality to RequiresTerminationProof, so infer_node_facts Rejects before application inhabitance runs. infer_descent_witness_for_node remaps the upstream cardinality_descent_not_proven diagnostic to infer_descent_not_derived; that is the reason on the Outcome (infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.",
+    "RUNG FOUND AT, source to interpretation (v2.compiler.infer consuming declared_type_inhabitance): mechanically preventable for a structurally unequal pair of derived type nodes (Bool at Int refuses with application_argument_does_not_inhabit). Unjudgeable applications that infer reaches (ArgumentTypeNotDerived, FormalUnresolved, GenericFormal) are InhabitanceUndecidable on the Accepted path, counted, not silent. Since 2026-09-27 GenericFormal means a formal that MENTIONS one of the callee's declared type variables (DeclaredTypeObligation.type_variables, read off the Arrow by v2.std.type_binder type_param_names); an Instantiation whose constructor and arguments are all established is decided by the same structural zip, so a `List<Int>` formal is judged rather than counted (a product argument at it now refuses, inhabitance_product_produced_at_a_collection_formal_refuses_holds). The declared side is read at its denotation (v2.extdeps.languages.dag dag_binding_denotation over each atom), and a bare declared atom that join does not denote is counted FormalUnresolved. The same relation now has a second producer, PositionDeclaredReturn: v2.compiler.infer infer_arrow_declared_return_check judges each Arrow body at its declared return and REPLACED the inline equality check #12379 had put on arrow introduction (infer_arrow_body_inhabits_declared_return, deleted; its reason arrow_body_does_not_inhabit_declared_return is kept, located at the body). Before the replacement a return that join did not denote was admitted with no diagnostic; it is now counted. Witnesses: v2.test.claim.compiler.infer_declared_return_inhabitance_witness_test (RED declared_return_int_with_a_bool_body_refuses_holds, controls declared_return_int_with_an_int_body_admits_holds and declared_return_bool_with_a_bool_body_admits_holds) and v2.test.claim.compiler.infer_arrow_elimination_witness_test. OptionalCarrier is enrolled on v2.std.inhabitance inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). A TypeNode Cardinality formal is not yet that counted frontier on infer: connective_multiplicity maps Cardinality to RequiresTerminationProof, so infer_node_facts Rejects before application inhabitance runs. infer_descent_witness_for_node remaps the upstream cardinality_descent_not_proven diagnostic to infer_descent_not_derived; that is the reason on the Outcome (infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds). That is not inhabitance-by-widening and not 'every reached application is judged'.",
 
     "RUNG FOUND AT, source to native emission: unclaimed. Native emission stays a declared frontier until v2.std.inhabitance is in the native 04_infer closure and infer_incompatible_argument_refuses_holds refuses on the emitted binary.",
 
@@ -25,7 +25,7 @@ data argument_type_obligation_absent_while_the_route_advances: RecurringFailureM
 
     "NEXT-RUNG TRIGGER, widening: a producer supplies integer value-set evidence on produced and declared; then declared_type_inhabitance consumes preservation_rule_refinement_widening on that algebra.",
 
-    "NEXT-RUNG TRIGGER, unjudgeable applications: operator Arrow from ResolvedTree.bindings, argument type derivation, generic instantiation, and an honest TypeNode Cardinality / Optional multiplicity that does not dissolve RequiresTerminationProof without a replacement RED, sufficient that inhabitance OptionalCarrier is counted on infer (not Outcome Rejected for descent) and the InhabitanceUndecidable frontier count over reached applications is zero on both routes. The v2 arm of this class retires only when that count is zero on both routes.",
+    "NEXT-RUNG TRIGGER, unjudgeable applications: operator Arrow from ResolvedTree.bindings, argument type derivation (including an application's RESULT type, which infer leaves GroundingNotDerived, so a call producing `Outcome<Record>` at an `Outcome<Node>` formal or return is counted rather than decided), generic instantiation, and an honest TypeNode Cardinality / Optional multiplicity that does not dissolve RequiresTerminationProof without a replacement RED, sufficient that inhabitance OptionalCarrier is counted on infer (not Outcome Rejected for descent) and the InhabitanceUndecidable frontier count over reached applications is zero on both routes. The v2 arm of this class retires only when that count is zero on both routes.",
 
     "THIS IS NOT rest_ok_over_uninhabiting_body: that class is HTTP 200 mapped as RestOk over an uninhabiting body. This class is a compiler application-argument obligation absent while the route advances.",
   ],

dag/gunbc/recurring_failure_mode/function_type_evidence_carries_its_body.dag

@@ -19,7 +19,7 @@ data function_type_evidence_carries_its_body: RecurringFailureMode = RecurringFa
 
     "CEILING: structurally impossible, since the Arrow's type node can be constructed as domain to codomain only.",
 
-    "NEXT-RUNG TRIGGER: a function-type introduction rule in v2.compiler.infer that derives an Arrow's type from its domain and declared return alone, with the body judged against the return (infer_arrow_body_inhabits_declared_return) instead of composed into the type, and a fixture constructor carrying the return once. It must be sufficient that two Arrows differing only in body derive equal types.",
+    "NEXT-RUNG TRIGGER: a function-type introduction rule in v2.compiler.infer that derives an Arrow's type from its domain and declared return alone, with the body judged against the return (v2.compiler.infer infer_arrow_declared_return_check) instead of composed into the type, and a fixture constructor carrying the return once. It must be sufficient that two Arrows differing only in body derive equal types.",
   ],
 
   evidence: [],