v2 native infer accepts variant-scrutinee matches (payload binder typing + coverage through the inhabitance relation) - #13210
Open
gunbai-bot[bot] wants to merge 46 commits into
Open
gunbai-bot[bot] wants to merge 46 commits into
gunbai-bot[bot] wants to merge 46 commits into
Conversation
added 19 commits
October 5, 2026 05:41
…der types; let-typed operands
…ol + coverage control)
… restore 3-arg public operand read (entries thread is inference-internal; census keeps facts-only fallback)
…iants enumerated) so no non-fold-residue roster rows are owed
…ecodes CI adjudication into bits; deleted once the gap is fixed)
…rier -- resolve bare and module-qualified spellings through the symbol index's global unique lookup; probe tag lens follows the index
…separate the construct-read gap from the coproduct-match gap
…clarations The variant-construct read normalized the tag through the global bare index, which is dead as a mechanism (03_resolve, global_bare comment): the corpus law is that a reader needing a body's resolved type reads ResolvedTree.resolved_declarations (gunbc#12629) -- never symbol_index. The tag is a resolved reference, bare or qualified alike (the qualified door and the atom walk meet in resolve_atom_bound), so the variant's declaring path is the reference's own path; the helper and the global lookup beside it are deleted. Probe: the bisection ladder (chain/fixture-split/XOR rows) is deleted; the one real-path inhabitance claim moves to the long home (v2.test.long.variant_field_infer_round_trip) where the cost gate reports rather than decides; the remaining controls read the warm producer (sharing conjunct: 5 and 2 consumers). One temporary decode field (construct_read) names what infer_record_construct_read answers on the fixture's construction; it goes out with the RFM retirement.
A bare variant spelling resolves through the fill's unique-variant alias (p.Boxed: module plus arm name), which does not name its declaring coproduct -- so the construct read typed the construction by the module and no fact could derive. The separate alias walk is deleted (it was the fork): the containment walk, which owns the variant's declared path, now mints the alias entry and an alias->carrier row on the index together, and the construct read types by the carrier through one shared mint for both path forms. The decode instrument carries the carrier half (construct_read_carrier: the read names ^Seal); the tag-path lens claims go out -- their premise (the tag's own path carries the carrier) is false under the alias mechanism.
The previous commit's splice left four defects, all caught by the corpus: a law comment inside the fold body (source annotation inside a declaration body), two SymbolIndex literals missing the new map field (symbol_index_insert, the bind-at literal), the splice's dangling fragment, and two neighboring fns (bindings_to_fixed_point, alias_bindings) eaten by the alias-walk deletion's comment cut. The v1 mirror comment now names the walk that owns the alias arm.
qualified_name_init returns the list itself, not an Optional; the mint's Absent/Present arms were the three hard emit diagnostics.
The walk's new arity (the module-wide variant counts and the module path, threaded so the alias arm can mint the carrier row) reaches four claim fixtures that call it directly.
disj_variant_counts_in_module is defined beside the containment walk, not in the index's std module; the three re-armed fixtures imported it from the wrong home.
The binder-to-Bind link was re-derived by a whole-tree walk on every unannotated binder-operand read (quadratic in binder reads x tree size), when resolve mints the binding at the frame that has the Bind node in hand. LexicalBinding now carries the value node beside the binder site -- the let frame mints its second positional child, every other frame mints Absent -- and the read is one map entry plus one fold-entry lookup. The walk and its children fold are deleted.
gunbai-bot
Bot
force-pushed
the
session/clever-bat-68
branch
from
October 5, 2026 06:18
420bbf5 to
398456c
Compare
added 10 commits
October 5, 2026 07:09
mark_module_root gained the carrier map, mark_variant_alias_carrier gained module_roots -- main's drift landed the field between my two edits.
…al with variant_alias_carriers The corpus floor refused on this hand-built literal (missing required field after the variant-alias-carrier map joined SymbolIndex). The literal re-binds entries over an in-scope base index, so it carries the base's alias map through unchanged.
…ge accepts with its reason (review 76451) - resolve_first_declared_payload_path and the qualified arm of resolve_pattern_tag_declared_payload_path_optional no longer name an arm by candidate order: a tag with several declared-payload candidates leaves the binder untyped (the pre-binder-typing behaviour) instead of fabricating a type from the first candidate. DESIGN 5: a failure arm refuses, never widens. - infer_coproduct_coverage_obligation no longer reports an undecidable inhabitance verdict as non-exhaustive: InhabitanceUndecidable accepts the match with inhabitance_undecidable_diagnostic carrying the reason, uniform with every other declared_type_inhabitance consumer (advisory acceptance, fail-open). Only InhabitanceRefused rejects.
…c-coproduct control (review 76531)
The operand read's declared arm handed the arm body the raw declared
type node -- for a payload field declared by a coproduct formal
(Some { value: T }), the bare formal T instead of the scrutinee's
argument. The read now instantiates exactly as the lexical facts path
does: the construct's instances where it holds them (the match arm
bodies get the scrutinee coproduct's), and an atom no instance binds
is held only when it names a type-denoting binding (the facts fold's
own dag_binding_denotation test); a free formal falls through to the
facts, the answer the caller had before the read existed.
The probe gains the generic control: an arm binder under a formal-typed
field must read as Int, never T.
Also: resolve_declared_payload_candidates is typed in FreeMonoid (the
alias List does not fold Cons literals).
# Conflicts: # src/v2/compiler/04_infer.dag # src/v2/std/symbol_index.dag
…coverage refuses; dedupe the comment (reviews 76607, 76611) - The import block carries both sides: the variant-carrier names and main's roster-signature + dotted-string names. - InhabitanceUndecidable at the coverage obligation now refuses with infer_match_coverage_undecidable -- undecided exhaustiveness is not exhaustiveness, and the refusal must not widen (DESIGN 5) -- instead of accepting with an advisory. It is distinct from infer_match_non_exhaustive because the relation did not decide the arms wrong; it could not decide them. - One comment block above infer_operand_declared_type_instantiated, not two.
…eview 76630)
The instantiation stopped at the head atom, so a compound declared type
(Cons { tail: t } over FreeMonoid<Int>, the reviewer's case) held the
raw compound with the formal riding inside. Substitution now descends
through the type arguments: an argument no instance binds leaves the
whole declared type unheld and the read falls through to the facts
rather than fabricate a partially formal type.
The probe gains the compound control: an arm binder over
boxed: Box<T> must read as Box<Int> -- the body b.inner types as Int
only then -- and goes red while the formal rides inside.
… the facts (review 76656) The fall-through arm held every non-Atom type node raw, so an arrow-typed generic field (f: fn(Int) -> T) preempted the facts with the formal riding inside. Non-atom types are now held only when no free formal appears anywhere in them (infer_declared_type_mentions_free_formal); otherwise the read falls through to the facts, as its contract states. The probe gains the arrow control: an arm binder over f: fn(Int) -> T must read as fn(Int) -> Int -- the body g(x) types as Int only then.
added 2 commits
October 5, 2026 16:59
…, not edges The free-formal scan and the substitution descent iterated the raw children (edges); the reads want the child targets.
…iew 76673) The move of the fixed-point fns left a second, unattached copy of their leading block above the pass-A comment, ending mid-sentence. The original stays with the declarations it describes.
Contributor
Author
|
All findings from reviews 76607, 76611, 76630, 76656 and 76673 are addressed on head 9fd44bf:
Two new discriminating controls in
— sent from clever-bat-68 |
added 14 commits
October 5, 2026 17:25
…red_payload_path The fn no longer picks the first candidate: it names the payload only when exactly one candidate is a declared payload and refuses ambiguity (review 76677's non-blocking note; DESIGN 3 -- a materially different contract needs a materially different name).
…nce_id The deep substitution passed child NODES into the Node literal's children field, which holds edges -- the dag checker unifies them, the emitted Rust does not (expected Rc<Vector<Rc<Edge>>>). The walk now keeps each child edge's label and substitutes its target, and the rebuild goes through node_with_occurrence_id.
# Conflicts: # src/v2/compiler/symbol_index_fill.dag
main's re-land of the fixed-point helpers and my branch's copies were both present; one declaration of each name remains.
… homes The merge left the block's first half orphaned above disj_variant_counts_in_module and its second half above the remaining declarations. One comment now sits above the fns it describes.
The complete block sits above the remaining declarations; the partial copy the merge left above disj_variant_counts_in_module is gone.
…t stays open on the verdict layer The enrolled label derives universe=4 population=4 file_refusals=0 at 00cead6 (was: four NativeTestRefused rows at prepare, head reason infer_match_scrutinee_not_bool). The route's verdict layer recorded no verdicts for the selection (the three qualification refusals recorded -not-chased on the main lane), so no NativeTestPassed rows exist and the row's own NEXT-RUNG TRIGGER is not met -- the receipt records the rung and the blocker, and the row stays open.
… stage0 mirror The generated-artifact gate refused on surface drift: the mirror lacked the self_parse_all_modules test the generator spec carries. This is the byte-for-byte candidate the regen child produced (verified by diffing the candidate on the runner).
… NonFoldResidueRosterDiverged) The infer derive now types the scrutinees these reads sit under, so their bare wildcard arms over closed coproducts entered the non-fold-residue census as unrostered sites: - resolve_pattern_tag_declared_payload_path_optional (tag path shapes and the candidate-list shapes) -- the qualified shapes share a helper, resolve_qualified_tag_declared_payload; - resolve_sole_declared_payload_path (solo-vs-many); - infer_declared_type_mentions_free_formal and infer_operand_declared_type_instantiated (NodeKind's two variants). No roster rows owed: every match now names all its shapes.
…he generating spec The mirror now matches the regen candidate byte-for-byte (verified by diffing the candidate on the runner: MIRROR-CLEAN, executed=163).
…e follow-up Review 76896 is right that the arm-body FACTS are minted by the lexical facts path (shallow infer_frame_instantiated under the parent frame), so compound and arrow declared types hold the formal riding inside and nested uses never reach the operand-level helper. Per the split with the parent: these two rows now assert the defect as it stands (fact == the formal) and flip to the instantiation when the follow-up PR lands deep substitution inside infer_frame_instantiated; the operand helper is interim there. The bare-formal control and the prepare-stage refusal results stand as today's evidence.
Contributor
Author
|
Answering review 76896 with the split agreed with the maintainer session:
— sent from clever-bat-68 |
…s, not symbol_index (review 76912) infer_match_coproduct_of_type took the variant body and its type params from the authored index while this PR's own construct reader takes the same kind of fact from the declarations with resolved bodies (03_resolve ResolvedTree resolved_declarations, gunbc#12629 -- one fact, one place). Both lookups now read resolved_declarations; the authored index keeps only what it is the authority for.
Contributor
Author
|
Fixed on head 1ee0c5a: both lookups in — sent from clever-bat-68 |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Variant-scrutinee native infer (debt paydown:
native_infer_accepts_only_bool_and_int_match_scrutinees)v2 native infer now accepts variant-scrutinee matches: match inference over closed coproducts, binder typing from variant payloads (named and positional), and exhaustiveness through the single inhabitance relation (
PositionMatchCoverageonv2.std.inhabitance'sDeclaredTypePosition); the per-tag coverage count and the separate alias walk are deleted, not kept beside the new code.Evidence. The enrolled label
//v2/test/claim/variant_field_native_binding:allderivesuniverse=4 population=4 file_refusals=0at head 00cead6 (baseline, head 17fccbf: the same label recorded all four identitiesNativeTestRefusedatNativeTestStagePrepare, head reasoninfer_match_scrutinee_not_bool). The probe modulev2.test.claim.variant_field_infer_probecarries the discriminating controls: a partial (non-exhaustive) refusal control, a bare-formal instantiation control, and two DECLARED REDS (..._still_rides_the_formal_pending_deep_instantiation) that assert the compound/arrow facts-layer defect as it stands and flip when the follow-up lands.Known limits, stated not hidden. (1) A pattern binder's facts are minted by the lexical facts path under the parent frame, whose
infer_frame_instantiatedsubstitutes shallowly -- compound (Box<T>) and arrow (fn(Int) -> T) declared types hold the formal riding inside; the operand-level deep helper (infer_operand_declared_type_instantiated) is INTERIM and is deleted by the follow-up PR, which moves deep substitution intoinfer_frame_instantiateditself (with match arms a coproduct-instance frame if the facts still do not flow), measures the floor re-pricing in eval_steps, and flips the two declared reds. (2) The route's verdict layer recorded no verdicts for the selection (admission refused:positive_population_empty,required_native_pass_regressed,unattributed_exclusions_present-- the same trio recorded-not-chased on the main lane), so noNativeTestPassedrows exist; the RFM row stays open with a dated receipt recording the rung and the blocker.Dependencies. #13010 owns the node.dag prepare refusal (the specimen's red waits on it); #13028 owns the fold cons-handler binder. The corpus floor's main-lane qualification refusals are recorded above, not chased here.