Skip to content

Optional de-fork PR-1: bind the seed's kernel Optional mint to the v2.std.optional declaration - #13178

Merged
briansrls merged 16 commits into
mainfrom
session/bright-fox-661
Oct 5, 2026
Merged

briansrls merged 16 commits into
mainfrom
session/bright-fox-661

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 4, 2026 •

Copy link
Copy Markdown
Contributor

Optional de-fork, PR-1 of 4 (node adhoc-ce2b73a7-f4e; plan and rework route approved by calm-boar-904). It binds the seed's kernel Optional to the corpus declaration, gives that binding a consumer in the emitter, and changes no corpus source.

The fork

Optional has three carriers: the seed's kernel T?, the declared coproduct v2.std.optional Optional, and the none literal. The seed's kernel Optional is not a declaration. v1.compiler.infer mints a synthetic coproduct named Optional into its kernel scope, in three identical copies. An arm reached through T? reported its owner as unrecovered, while the same arm reached through an import reported the declaration: one concept, two identities. The emitter then decided Some/None by the arm's and parent's spelling.

What changes

  • Row. std.literal_elaboration KernelMintDeclaration, its three-way lookup kernel_mint_declaration_for (found, absent, ambiguous), and kernel_mint_ownership (owns, does not own, ambiguous), the question the emitter asks of an arm's declaration. gunbc.structural_realization_bindings kernel_mint_declaration_rows binds the kernel Optional to v2.std.optional Optional by DeclarationRef.
  • One mint. The three copies become v1.compiler.infer kernel_optional_type_node.
  • Arm identity. kernel_mint_parent_identity reads the row; variant_parent_identity_of and the optional-wrapper arm of annotate_pattern_parent_enums answer VariantParentDeclaration for Present/Absent.
  • The identity's consumer. v1.compiler.emit_rust host_option_arm_reading decides whether a pattern arm lowers to Some/None, at emit_resolved_variant_pattern and its twin emit_resolved_variant_pattern_rc_aware:
    • an arm whose identified owner is the bound declaration lowers to the host option;
    • so does an arm whose identified owner is a declaration the Rust target realizes as its host option, by a new identity row: gunbc.rust_source_type_bindings rust_host_option_carrier_declarations = v2.std.diagnostic Diagnostics (None | Some { diagnostics }), which the emitter previously recognised by a name table of its own. That table is gone as an authority: is_host_diagnostics_carrier_alias now projects the declaration names off the row, and the other two spellings of "Diagnostics" call it, so a name-keyed site cannot disagree with an identity-keyed one (review 75565);
    • an arm with any other identified owner does not, whatever it is spelled (no fallback to spelling);
    • if two rows bind the kernel optional, an identified arm is refused with a located compile_error! instead of being answered as not-the-optional (review 75454);
    • an arm inference did not identify keeps the spelling rule over the parent the emitter resolves from the scrutinee's type name; this is the unidentified residue and is PR-2 population;
    • an unidentified arm whose parent INFERENCE named as the kernel optional is refused with a located compile_error!, because inference names that parent and stamps the identity in one branch.
  • Generated seed unit tests. v1.compiler.compiler_tests_rust passes the new identity argument at its four direct calls of the pattern lowering.
  • Typed shape wall. kernel_optional_shape_refusal judges the bound declaration itself: exactly one type parameter, exactly two arms, one arm with no payload, one arm with a single field named as the mint names it whose type is that parameter. The parameter is read through v1.compiler.infer_env declaration_substitution_basis, the existing authority for "is this leaf one of this declaration's parameters". It is keyed on the row's DeclarationRef, so the re-home changes the row and not the check.
  • Diagnostic class. KernelMintShapeMismatch in v1.std.core CompilerDiagnostic, with its three hand-Rust arms in cli_run::compile_clean.

Controls

test.claim.kernel_optional_mint_shape_witness_test, through the isolated multi-module fixture compile, asserting by class and subject:

claim compiler without this change this change bypass mutant
conforming declaration admitted pass pass pass
Present { value: Int } refused fail pass pass
second type parameter refused fail pass pass
renamed payload field refused fail pass pass
third arm refused fail pass pass
match over Int? emits Some(v) / None pass pass fail

Both mutants were last rebuilt and run before the final two changes to this branch: the commit that makes the emitter's name-keyed Diagnostics predicate read its row, and a merge of main. They were not re-run after the merge. A second mutant, the kernel optional bound twice (the row duplicated, regenerated, rebuilt), gives the same column as the bypass mutant: the consumer claim alone fails. I did not capture which refusal message the emitted text carried there; with the row doubled inference also stops stamping the identity, so it is most likely the missing-identity refusal and not the emitter's ambiguity message. The ambiguity decision itself is enrolled at its own interface: kernel_mint_ownership over the real rows says the bound declaration owns the mint and v2.std.diagnostic Diagnostics does not, and over a doubled row answers ambiguous, never does-not-own.

The bypass mutant replaces the identity at the optional-wrapper arm with VariantParentUnrecovered, regenerates and rebuilds. v2.test.claim.self_host.kernel_optional_mint_binding_test (seven claims at the row and ownership interfaces, plus an executed round trip between T? and Optional<Int>) passes on the new compiler.

Two honest limits. The consumer claim passes on a compiler without this change, where lowering was by spelling; what it discriminates is the identity being lost afterwards. And two wrong versions of the shape check were caught by the wall itself refusing the real declaration on the way here, which is the positive control doing its job.

Receipts

BuildBuddy, self-bound 20 GiB memory cgroup, on this branch merged with main at 9db1a8bbaa:

  • claim_executor --required-regen, planned=162 executed=162: the only mirrors that change are those of sources this PR edits (gunbc_structural_realization_bindings.rs, gunbc_rust_source_type_bindings.rs, std_literal_elaboration.rs, v1_compiler_emit_rust.rs, v1_compiler_infer.rs, v1_std_core.rs, v1_compiler_compiler_tests_rust.rs, and compiler_tests.rs, which is rendered from the last). No other seed module's emission moved under the identity-keyed lowering. On the pushed head, after installing them, a clean run reports first_generation_equal=true.
  • gunbc test //gunbc/instruments:self-host on the pushed tree: 241 files emitted, built with exit_status=0 warning_count=0, emitted compiler binary sha256 9e41a65bf52fbb33b9fca2e68c9fd2c2c2670db3a8d087ad9d79e77e8ea7079e, identical to the binary the same instrument builds at the merge base 9db1a8bbaa (and identical to base at the previous merge base bc7838f7b4 too, 1f2a010f… on both sides). The seed binaries differ (62b14cc6dc4e… here, 4ad00dece5a8… at base), which is the control that the two sides are different compilers. This is identity of the built self-host compiler, not a hash of the emitted source tree.
  • cargo clippy --all-targets -- -D warnings and cargo fmt --all --check: clean on the pushed tree.

Two earlier heads of this rework were wrong and this receipt is what caught them: the self-host build failed first on arms the emitter resolves itself, then on the Diagnostics carrier. Both are handled above, and both populations are named.

Not run locally: the whole floor and cargo test. CI is the instrument for the floor; the seed unit tests run on no CI path (gunbc.rung_drop rust_unit_tests_off_the_merge_path).

Interim, and its dissolution

A mint bound to a declaration and checked against it is still two representations reconciled by a check. It is accepted here only as an interim. Dissolution: the mint is deleted in the re-home PR or in PR-2, at which point T? resolves to the declaration itself. That requires the declaring module to be in the closure of every module that writes T?; how that lands is not designed yet and is owed by whichever PR deletes the mint.

Declared split: what still decides Optional by spelling

One emitter decision is now identity-keyed. These still read the spelling Optional, Present/Absent or Some/None, and are PR-2's population, by symbol:

  • v1.compiler.infer: annotate_pattern_parent_enums, coproduct_name_is_unnamed_or_optional_carrier, coproduct_payload_where_parent_required, direct_call_arg_type_mismatch, equality_operand_admission, infer_record_lit_structural, kernel_value_declared_type_mismatch_bounded, nominal_coproduct_application_head_name, nominal_product_head_name, optional_cast_diags, optional_produced_at_required_declared, overlay_skips_kernel_name, validate_cast.
  • v1.compiler.infer_patterns: lookup_variant_in_type. v1.compiler.infer_types: extract_optional_inner_node.
  • v1.compiler.emit_rust: resolved_variant_pattern_shape_for (a third copy of the rule converted here), and the name-keyed readers is_host_diagnostics_carrier_alias and is_host_diagnostics_carrier_type, which now read the identity row but still key on a name because their call sites hold no identity, analyze_rc_match, analyze_rc_pattern, box_bound_fields_for_pattern, collect_pattern_rc_variant_guards, collect_pattern_string_guards, collect_rc_pattern_prelude_parent_enums, contextual_variant_parent_absent, effective_variant_parent_from_resolved, emit_rust_expr_record_lit, emit_type_def_from_connective, emit_typed_expr_base, emit_typed_record_lit, emit_var_ref, is_already_optional, is_grounded_coproduct_native_alias, is_host_optional_carrier_alias, is_host_optional_carrier_type, is_optional_like_parent_name, is_optional_parent, rc_pattern_preludes, render_rust_applied_type, render_rust_decl_type, render_rust_fn_sig_type, render_rust_type, render_rust_type_without_applied_binding, rust_call_arg_fail_closed_unwrap, variant_pattern_parent_unresolved; and the unidentified-arm branch of host_option_arm_reading itself.
  • v1_interpreter.rs: five parent_enum_is(.., "Optional") reads.

What follows

  1. Re-home (waits on Unimported-bare-provider gate reads the compiler's NonDeclarationBinding classification (unblocks #12951) #13116): the declaration moves to std.optional under the dag root, v2.std.optional is deleted with no re-export, and its importers are repointed by a modeled, re-runnable rewrite. Nineteen modules evaluated without src/v2 cannot import it today (valiant-stag-606, CI runs 37162821539 and 37164442913).
  2. B: none becomes Absent inside the N7 closure, with a compiler wall and a shrink-only roster keeping new none sites out elsewhere.
  3. Transition 2: the rest of the corpus; the roster, the wall, the keyword rows, LitNull and the universal-null join are deleted together.

v1 maintenance purpose (gunbc.v1_maintenance_standing v1_seed_standing): this serves the v2 self-host. It gives the seed's T? arms the identity v2 already uses, so the later cut can remove the seed-only null without a second binding beside it.

🤖 Generated with Claude Code

Brian Searls and others added 3 commits October 4, 2026 00:22
….optional Optional

One row (gunbc.structural_realization_bindings kernel_mint_declaration_rows) names the
declaration the seed's synthetic kernel Optional stands for. Present/Absent arms reached
through T? now carry that declaration's identity instead of an unrecovered owner. The three
identical copies of the mint in v1.compiler.infer become one function, and typechecking the
declaring module refuses if its arms stop matching the mint. No corpus source changes.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…smatch, identity-keyed pattern lowering (mirrors not yet regenerated)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rom main; regeneration follows)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls and others added 6 commits October 4, 2026 03:46
…ugh declaration_substitution_basis

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…on BuildBuddy)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ithout identity; Diagnostics identity row; test call sites; regenerated mirrors

- host_option_arm_reading refuses only when INFERENCE named the kernel optional as the parent
  with no identity; an unidentified arm whose parent the emitter resolves keeps the spelling rule.
- gunbc.rust_source_type_bindings rust_host_option_carrier_declarations: v2.std.diagnostic
  Diagnostics, so an identified owner is judged by identity and not by spelling.
- The four generated seed unit tests pass the new identity argument.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…al binding (review 75454)

host_option_arm_reading reads kernel_mint_declaration_for directly; two rows binding the kernel
optional refuse the arm instead of answering not-the-optional. kernel_mint_is_bound_to, which
folded Ambiguous into false, is deleted.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…olled ambiguity red

std.literal_elaboration kernel_mint_ownership answers owns / does not own / ambiguous; the emitter
refuses on ambiguous. Three claims at that interface, including the doubled-row red.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…entity row (review 75565)

is_host_diagnostics_carrier_alias reads declaration names off
gunbc.rust_source_type_bindings rust_host_option_carrier_declarations instead of holding its own
spelling, so the host-option carrier fact has one authority.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 4, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Oct 4, 2026
Brian Searls and others added 2 commits October 4, 2026 14:14
…aken from main; regeneration follows)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…fixed point)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 4, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to a conflict with the base branch Oct 4, 2026
Brian Searls and others added 5 commits October 4, 2026 21:43
…rors taken from main; regeneration follows)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…fixed point)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…rom main; regeneration follows)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ging main (fixed point)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls merged commit b4bbc33 into main Oct 5, 2026
4 checks passed
@briansrls
briansrls deleted the session/bright-fox-661 branch October 5, 2026 01:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant