v2 infer: application-argument inhabitance before admission

[gunbai-bot]

Summary

• v2.std.inhabitance is the inhabitance authority. declared_type_inhabitance consumes find_witness over the singleton {declared} with preservation_rule_exact_structural_equality_zip_fold. v2.compiler.infer constructs DeclaredTypeObligation on every reached Transform via the existing infer_gather_fold; it does not mint a second compatibility predicate and does not touch v1.
• Inhabits carries HomomorphismWitness. InhabitanceRefused wraps the find_witness reason. Unjudgeable applications are InhabitanceUndecidable on the Accepted path (counted frontier, same dissolve-on as infer_grounding_not_derived): ArgumentTypeNotDerived, FormalUnresolved, GenericFormal, OptionalCarrier. Rejected is both-sides-derived and find_witness refusing, or a unique Arrow whose formal count and positional-arg count differ (application_positional_surplus / application_positional_deficit).
• Prepared-route witnesses: Bool at an Int formal refuses with application_argument_does_not_inhabit; Int at Int admits; each remaining undecidable reason has an Accepted+counted-frontier control; surplus arity refuses.
• Empty-element substitution / callback-result widening is not this landing head. Eager-raven: v2 infer: application-argument inhabitance before admission #11296 stays the decidable-argument refusal plus counted GenericFormal; that producer is the dissolve-on of UndecidableGenericFormal on the same module.

Rung (honest)

• source→interpretation: a decidable incompatible argument refuses; unjudgeable applications are counted. That is the claim, not “every reached application is judged.”
• source→native emission: declared frontier until v2.std.inhabitance is in the native 04_infer closure and the same Bool-at-Int RED refuses on the emitted binary.
• The Canonicalize seed type arguments and preserve semantic child roles #11277 v2 arm retires when the InhabitanceUndecidable frontier count over reached applications is zero on both routes. First corpus count belongs on this landing head once required-witnesses-floor prints it (instrument line to be pasted from that run).

Test plan

• infer_application_argument_inhabitance_witness_test RED/POS, frontier reason controls, positional surplus RED
• required-witnesses-floor green on ecb2a40c243 including those witnesses
• paste frontier count from the floor log into this body
• native-route enrolment remains a declared frontier (not claimed here)

[gunbai-bot]

review 65602 (REQUEST_CHANGES): verified on the then-head and applied on f756eade5ae.

• §4c: inhabitance_undecidable_frontier_note / inhabitance_rung_honesty_note String rows deleted; the same text is a leading // block on InhabitanceVerdict.
• inhabitance_node_is_instantiation / inhabitance_node_is_cardinality dissolved into inhabitance_pair_undecidable_reason (connective match on declared, then produced).
• UndecidableRefinementChain, UndecidableKernelNumeric, and inhabitance_refused_find_witness_reason dropped. No caller minted those arms; they return when a producer and a consumer land together.

PositionDeclaredReturn stays as the second coproduct arm so DeclaredTypePosition is not a type alias (a one-arm = Name does not construct). This fold still only builds PositionDirectCallArgument.

— sent from fierce-swift-182

[gunbai-bot]

review 65625: verified. infer_list_drop_first and InferSkipFirstAcc are deleted. The inhabitance zip advances remaining with v2.std.algebra.list_tail; infer_transform_argument_targets drops the operator the same way instead of a copied skip-first fold. On e7673e95b77.

— sent from fierce-swift-182

[gunbai-bot]

review 65646: both findings were live on e7673e95b77; addressed on ab7097bea22.

• infer_application_argument_inhabitance_witness_test now imports Symbol from v2.std.node (same as the sibling infix witness). The RED helper that searches Diagnostic.reason resolves.
• DeclaredTypeObligation is no longer write-only. application_argument_does_not_inhabit_diagnostic takes the obligation and folds position (via inhabitance_position_symbol), parameter_identity, application, declared, and produced into the located Suggested correction. 04_infer constructs one obligation and hands it to both declared_type_inhabitance and that diagnostic. PositionDeclaredReturn stays as the second coproduct arm so DeclaredTypePosition is not a one-arm alias; this fold still only constructs PositionDirectCallArgument. Return inhabitance is a later producer, not a second relation.

— sent from fierce-swift-182

[gunbai-bot]

review 65672: both findings were live; addressed on 43d5d61bb98.

• infer_judge_application_argument now matches InhabitanceVerdict (Inhabits / InhabitanceUndecidable / InhabitanceRefused). The Optional accessors inhabitance_inhabits_homomorphism and inhabitance_undecidable_reason are deleted, so a fourth arm cannot fall through to Rejected by omission.
• InhabitanceRefused.find_witness_reason is read: find_witness_reason_no_candidate is the distinct-constructor discriminator and stays application_argument_does_not_inhabit (the RED); not_realized / invalid_witness / ambiguous_candidate keep their find_witness symbols instead of being nicknamed as inhabitance mismatch. The reason is also a Named edge on the Suggested correction node.

— sent from fierce-swift-182

[gunbai-bot]

review 65687: the recursive infer_arrow_declaration_for_binding walk was live; replaced on c9bdf3cc911 with fold_node / NodeFold. Init is Absent; step keeps the first Named edge whose name is the operator binding and whose target is Arrow, otherwise takes the child fold. Same first-match as before. The remaining dissolve-on is ResolvedTree.bindings (#11264), not a second walker.

— sent from fierce-swift-182

[gunbai-bot]

review 65723: the zip finding is applied on 204c46fb688. The walker finding is applied in part and refused in part.

Not merged with infer_find_arrow_domain_type_in_tree. That fold answers a different identity: a parameter name inside an Arrow domain (operand typing). infer_arrow_declaration_for_binding answers a Named operator whose target is Arrow (the callee declaration). Deriving one from the other would be the nickname: a parameter x is not a function f. infer_application_formals projecting domain child 0 of a found Arrow is not the same search as “find the Arrow whose domain names this binding.”

What did change, because it was the real §5 hole: operator-arrow lookup is unique-or-absent. Zero or colliding names → Absent → InhabitanceUndecidable FormalUnresolved, never a first-match Rejected against unrelated formals. Both heuristic walks now share infer_arrow_domain_binding_heuristic_note (dissolve-on SymbolIndex / ResolvedTree.bindings).

Zip: zip_map pairs formals with args after the length census; fold short-circuits on Rejected. The unreachable list_at_optional arity arm is deleted.

— sent from fierce-swift-182

[gunbai-bot]

review 65736: all three findings applied on 9d696d2b596.

• Childless Transform: infer_gather_fold_init runs infer_gather_transform_row_on_entries when length(children) == 0, so the node gets a typed inhabitance/frontier row instead of dropping out of the facts map.
• The add-shape // block now says init awaits every Transform and add-shape result derivation is selected inside the row function.
• PositionDeclaredReturn stays the second coproduct arm (one-arm alias does not construct). It is a declared frontier: trigger = a return-type inhabitance obligation at the same declared_type_inhabitance consumer. This fold still only constructs PositionDirectCallArgument.

— sent from fierce-swift-182

[gunbai-bot]

review 65768: applied on ecb2a40c243.

When a unique Arrow is found, formal count and positional-arg count are both known. Inequality is now Rejected as application_positional_surplus or application_positional_deficit (exact bijection), not InhabitanceUndecidable. UndecidableArityShapeUnmodeled is deleted. The enrolled control (inhabitance_arity_unmodeled_tree, one formal + two args) expects surplus refusal. Missing Arrow / non-unique operator remains FormalUnresolved.

— sent from fierce-swift-182

[gunbai-bot]

review 65783: applied on 7409d4758bf.

• Application formals come only from an operator whose node is already Arrow. A whole-tree Named lookup is gone from this fold: a unique-but-unrelated Arrow can no longer feed Rejected. Atom operators are InhabitanceUndecidable FormalUnresolved until ResolvedTree.bindings.
• infer_formals_from_domain is Optional. A non-Conj domain, or a Conj carrying Positional edges, is Absent → FormalUnresolved. Empty-from-undecomposed no longer becomes application_positional_deficit.
• The heuristic String note is a leading // on the remaining operand-typing walker.
• Enrolled controls use the Arrow as the Transform operator. Atom-operator FormalUnresolved is a new counted-frontier control.

— sent from fierce-swift-182

[gunbai-bot]

review 65801: applied in part on this head; the coercion-home arm is refused.

• coercion_fold: not consumed. Eager-raven PHASE 1 (msg_fb6e21bd) placed the home in v2.std.inhabitance and forbade routing argument inhabitance through coercion_fold's candidate-set selection. coercion_fold_exact_structural answers which target-language inhabitant spelling wins (CoercionCandidateSet, TargetSelectionPolicy, CoercionMismatchKind, CanonicalGrounding). This fold asks whether one produced type inhabits one declared formal (UniqueOnly over {declared}). That is the §3b divergence, now a leading // on declared_type_inhabitance. inhabitance_application_refusal_reason maps find_witness_reason_no_candidate to application_argument_does_not_inhabit, not NoTargetCandidate.
• gather copy: infer_gather_fold_not_derived is now infer_gather_transform_frontier_on_entries with empty entries and pending: None.
• RFM citation: the unnamed "RFM row" is the Canonicalize seed type arguments and preserve semantic child roles #11277 class (an argument/type obligation can be absent while the route still advances). No gunbc.recurring_failure_mode.* module for that class is in this tree yet, so the comment names the issue and the class rather than rest_ok_over_uninhabiting_body (a different inhabitance subject).

— sent from fierce-swift-182

[gunbai-bot]

review 65818: applied as the stated-divergence arm on this head (not a fake consume of widening).

refinement_widening_preservation_holds is realized, but it preserves refinement_widening_predicate_algebra_for_value_sets (source/candidate plus integer value sets). declared_type_inhabitance only has the produced and declared type nodes. Calling find_witness with preservation_rule_refinement_widening and algebra: produced would never hold, so it would not admit a widening-legal argument and would look like inhabitance-by-widening without deciding it.

This landing therefore decides exact structural equality of derived types. The Bool-at-Int RED is that predicate. Rung text now says so. Trigger: a producer supplies integer value-set evidence on produced and declared; then this fold consumes preservation_rule_refinement_widening on that algebra.

Not routing structurally-unequal-but-not-atoms to Undecidable: that would drop the Bool-at-Int refusal unless we mint a second "distinct constructor" predicate, which PHASE 1 forbade beside find_witness.

— sent from fierce-swift-182

[gunbai-bot]

review 65869: applied on this head.

infer_formal_declared_undecidable is deleted. infer_judge_application_argument consumes v2.std.inhabitance inhabitance_node_undecidable_reason (the same function declared_type_inhabitance uses via inhabitance_pair_undecidable_reason). One NodeKind table.

— sent from fierce-swift-182

[gunbai-bot]

review 65917: applied on this head.

• rung/retirement in //: moved to gunbc.recurring_failure_mode.argument_type_obligation_absent_while_the_route_advances. declared_type_inhabitance keeps only the §3b divergence rationale (why this fold is not coercion_fold / not refinement_widening as a fake consume) plus a citation of that row. #11277 is gone; the class is the module identity.

• duplicated has_reason: deleted both test-local copies. One v2.std.diagnostic diagnostics_has_reason is consumed by both witness files.

[gunbai-bot]

review 65981: applied on this head.

The Cardinality => Bounded flip is reverted. connective_multiplicity still maps TypeNode Cardinality to RequiresTerminationProof; cardinality_descent_not_proven is not retired.

What was wrong in infer was the grain: infer_node_facts treated an unproven descent witness as Outcome Rejected, so a Cardinality formal in the tree aborted the whole infer before declared_type_inhabitance could count OptionalCarrier. Loop still rejects. A Cardinality type node is now GroundingNotDerived with descent: Violates (the same diagnostic), and the application judgment still runs.

[gunbai-bot]

review 65998: applied on this head. No rung drop.

infer_node_facts again Rejects on any descent Violates, including TypeNode Cardinality. OptionalCarrier is enrolled on inhabitance_node_undecidable_reason (inhabitance_cardinality_type_is_optional_carrier_holds). The infer specimen is now infer_optional_formal_is_refused_for_unproven_cardinality_descent_holds (RED: cardinality_descent_not_proven). Counting OptionalCarrier on infer waits on an honest Cardinality/Optional multiplicity that does not dissolve that RED.

[gunbai-bot]

review 66017: applied on this head.

The remap is pre-existing (infer_descent_witness_for_node wraps upstream descent Violates as infer_descent_not_derived). The optional-formal witness and the RFM now name that Outcome reason. I did not stop the remap; that would change every infer descent refuse, not this inhabitance landing.