v2 infer: application-argument inhabitance before admission

dag/gunbc/recurring_failure_mode/argument_type_obligation_absent_while_the_route_advances.dag

@@ -0,0 +1,34 @@
+module gunbc.recurring_failure_mode.argument_type_obligation_absent_while_the_route_advances
+
+import std.types { NonEmptyStr }
+import gunbc.recurring_failure_mode { RecurringFailureMode }
+
+data argument_type_obligation_absent_while_the_route_advances: RecurringFailureMode = RecurringFailureMode {
+  identity: "argument_type_obligation_absent_while_the_route_advances" as NonEmptyStr,
+
+  receipts: [
+    "INVALID STATE: a reached application advances on the compiler route while the argument's derived type is not judged against the parameter's declared type, so an incompatible argument is Accepted.",
+
+    "HARM: a silent wrong program; the class DESIGN section 5 forbids. The seed instance is is_deferred_field_access_base accepting item.value on unconstrained T. The v2 instance was absence of any argument-inhabitance judgment on v2.compiler.infer.",
+
+    "DISTINGUISHING FACT: the obligation is inhabitance of produced at declared, not a second compatibility predicate. Home is v2.std.inhabitance declared_type_inhabitance, which consumes find_witness over the declared singleton with preservation_rule_exact_structural_equality_zip_fold. It does not consume v2.std.coercion coercion_fold (target-language inhabitant selection) and does not consume refinement_widening_preservation_holds (that rule preserves a value-set algebra, not application type nodes).",
+
+    "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 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.",
+
+    "CEILING: structurally guaranteed on each path once every reached application is judged (frontier count zero) and a widening-legal pair is judged by preservation_rule_refinement_widening once integer value-set evidence exists on produced and declared.",
+
+    "NEXT-RUNG TRIGGER, native path: v2.std.inhabitance in the native 04_infer closure, sufficient that infer_incompatible_argument_refuses_holds refuses on the emitted binary.",
+
+    "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.",
+
+    "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.",
+  ],
+
+  evidence: [],
+}