Skip to content

v2: carry the type-declaration modifier slot on NormalizedTree (M0 precursor) - #13033

Merged
gunbai-bot[bot] merged 7 commits into
mainfrom
session/tidy-koi-264
Oct 3, 2026
Merged

gunbai-bot[bot] merged 7 commits into
mainfrom
session/tidy-koi-264

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 2, 2026

Copy link
Copy Markdown
Contributor

Precursor to M0 of the nominal-type plan (gunbc#13024, docs/plans/nominal-type-declaration-plan.md). sharp-raven-357 ruled option (2): M0's census rides census-resolve, and that walk could not see whether a type declaration carries nominal_opaque because G0 consumed the modifier slot and minted nothing. Without this change the census's Opaque class would fall silently into UnconstrainedNominal / TrueAlias.

Change

  • Vocabulary (v2.compiler.body_lowering_fold): a closed TypeDeclModifier vocabulary (NominalOpaqueModifier | SoleConstructorModifier). It is modeled as the slot plus a closed set, not a per-spelling flag, because plan §9 S1 puts constructor and view visibility in this same slot. The reader body_lower_type_decl_declared_modifiers reads the slot positionally off the parse, the same way body_lower_type_decl_eq_rhs_optional reads the body. A slot it cannot read refuses with body_lowering_reason_type_decl_modifier_unreadable at its location; it is never read as empty.
  • Carrier (v2.compiler.normalize): type_declaration_modifier_capture carries the rows on NormalizedTree type_declaration_modifiers, beside type_declaration_kinds, following the DeclaredTypeKind precedent. admit_normalized_tree takes the new argument. Hand-built roots pass no_type_declaration_modifiers(), and roots rebuilt from a tree pass that tree's own rows.
  • Consumers: nothing reads the carrier yet, so no existing consumer's behavior changes. The named consumer is M0 (gunbc.instruments.type_declaration_use_census), which lands next (§3c declared frontier).

Rung drop: narrowed, not retired

gunbc.rung_drop.g0_type_decl_modifier_parse_without_sealing_property is narrowed, not retired. This change mints the property, but its restoration trigger is the construction wall, which nothing on the native route enforces yet. A drop is retired by its trigger and by nothing else, so the population row now names the carried-but-unenforced state.

Controls (v2.test.parse.type_decl_modifier_carrier), all PASS locally on the seed

  • An unmodified alias carries no row (control).
  • nominal_opaque alias carries its modifier, and a sole_constructor record carries its own. Both were red against the first cut of the reader, which mis-read a present keyword atom as an empty slot.
  • A generic declaration carries both modifiers in slot order.
  • A modifier spelling used as the type's name is not a modifier.
  • Pairing claim: the real normalize route carries the row onto NormalizedTree, so deleting the capture turns it red.
  • An unknown spelling in the slot still refuses parse_g0_tokens_remain at its location. That is covered by the existing type_decl_modifier_g0_parse_probe (13/13 PASS).

Regression spot-checks of edited call sites (local)

  • fold_encoding_test: all PASS.
  • image_occurrence_projection_test: all PASS.
  • body_let_annotation_test: 34 PASS, 2 FAIL. The same 2 (bla_refinement_*) fail on main at d8eebae, so they predate this change.

Grammar: no production changed; only the comment above dag_grammar_type_decl_modifiers_expr (stern-bear-500 informed).

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 7 commits October 2, 2026 23:55
…nstructor) on NormalizedTree

The slot was consumed by G0 and minted nothing, so no reader of a lowered declaration could tell
`type X nominal_opaque = Y` from `type X = Y`. Precursor to M0 of the nominal-type plan
(gunbc#13024): the census's Opaque class is unobservable without it.

- v2.compiler.body_lowering_fold: closed vocabulary TypeDeclModifier and a positional reader of
  the slot off the parse (body_lower_type_decl_declared_modifiers); an unreadable slot refuses,
  located, never read as empty.
- v2.compiler.normalize: type_declaration_modifier_capture, carried on NormalizedTree
  type_declaration_modifiers beside type_declaration_kinds; admit_normalized_tree takes it.
- Control: v2.test.parse.type_decl_modifier_carrier (carries / does not / slot order / spelling as
  a name / real normalize route). Unknown spellings stay refused at parse by the existing probe.
- gunbc.rung_drop g0_type_decl_modifier_parse_without_sealing_property narrowed, not retired:
  carrying enforces nothing, and its trigger is the construction wall.

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

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…new-witness step budget (84854 > 72300 with an alias rhs)

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…nkeyed lexical refs in a hand-built fixture), first selected by this PR's call-site edit

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… minted occurrences (resolve keys lexical bindings by occurrence)

Drops the floor_expected_red row added in 588c329 (which also broke that file's parse).

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md g0_type_decl_modifier_parse_without_sealing_property
Ledger-Rows-Repaired: docs/design-rung-drops.md edited_bin_witness_wet_rows_not_executed_by_ci
Heal-Candidate-Run: 37090292139
@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Oct 3, 2026
Merged via the queue into main with commit 2900bfa Oct 3, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/tidy-koi-264 branch October 3, 2026 06:21
gunbai-bot Bot pushed a commit that referenced this pull request Oct 3, 2026
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
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.

0 participants