Skip to content

v2: every type declaration lowers — plain aliases, bodyless and coproduct declarations leave the parse shell - #12574

Merged
gunbai-bot[bot] merged 1 commit into
mainfrom
session/silent-swift-419-type-decl-lowering
Sep 29, 2026
Merged

gunbai-bot[bot] merged 1 commit into
mainfrom
session/silent-swift-419-type-decl-lowering

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 28, 2026

Copy link
Copy Markdown
Contributor

Replacement migration for gunbc.recurring_failure_mode plain_type_alias_left_as_a_parse_shell_in_v2. This PR is lowering-only; the side chat ruled it option B, and declaration grounding is a separate infer change.

The defect

v2.compiler.body_lowering_fold body_lower_type_decl_by_body accepted any non-generic type declaration that was neither a record nor where-refined as its raw parse shell, through NoTypeParams => outcome_accepted(value: shell). body_lower_type_decl did the same for a declaration it could not read.

So type B = T | F, type I = Int and type W reached infer as grammar tokens. Measured through the closure route on main:

Declaration Nodes Not grounded after infer
type B = T | F 31 29
type I = Int 28 22

About 930 non-generic = declarations take that path.

The change

  • One lowering for every declaration.

    • body_lower_eq_type_decl, formerly the generic-only arm, now serves every = and bodyless declaration, generic or not.
    • A plain alias becomes type_alias_wrapper, and a plain bodyless declaration becomes type_opaque_wrapper; each carries an empty binder Conj (body_lower_decl_binders).
    • A plain coproduct becomes its Disj member.
    • The shell-accepting arms are removed, and an unreadable declaration now refuses with body_lowering_reason_type_decl_unreadable.
  • Shared contract. v2.std.node type_binder_conj_conforms now admits zero binders; the identity and uniqueness checks are unchanged.

  • The view. Its arms are renamed TypeAlias and OpaqueTypeDecl, which are cardinality-neutral, so no reader equates "wrapped" with "generic".

    • symbol_index_fill is unchanged in behaviour: an alias or opaque declaration still binds without declaring members.
    • semantic_decl_emission refuses an alias or opaque declaration at the struct and enum surfaces under its own reason, where it previously used a "generic declaration" reason.
  • Readers of the old representation are deleted. v2.compiler.namespace_graft's type_decl naming arm read a unit's shell. With that arm answering UnitResidual, all of these still held:

    • declaration_graft_assemble 16/16
    • type_param_binder_frame 37/37
    • the new claims 5/5

    It is deleted, along with namespace_graft_type_decl_name, _target and _named_edge.

Evidence

All numbers come from local claim_batch runs on this branch.

v2.test.claim.body_lowering.plain_type_decl_lowering asserts the lowered forms positively on real assemblies. It has five nullary verdict producers, each WARM in floor_pure_producer_share.

Row Result on this branch Result with the pass-through restored
type Decision = Allowed | Blocked is a Disj with exactly [Allowed, Blocked], and the index descends into it PASS FAIL
type Id = Int is the alias wrapper with 0 binders and an atom right-hand side, and the module assembles with keep(x: Id) -> Id PASS FAIL
type Ref = Id is an alias with 0 binders that declares no members PASS FAIL
type PointerWidth is opaque with 0 binders, not an empty record, and declares no members PASS FAIL
type Wrapped = Only { a: Int } stays a member PASS PASS (preservation control; it always took the record arm)

type_param_binder_frame's 37 existing claims pass on the change.

Not claimed

  • Grounding. After this change, infer leaves 7–8 structural nodes ungrounded per declaration: the module spine, the Disj, childless variants and the empty binder list. This is because the product-introduction rule has no Disj rule and keeps a childless Conj on the frontier. That frontier is left intact here and is the next, separate infer capability.
  • Emission. The walls are unchanged: the module wall renders only bodied functions, and a bodied-function signature still spells Bool as bool_node_symbol.

🤖 Generated with Claude Code

…oduct declarations leave the parse shell

Replacement migration for gunbc.recurring_failure_mode
plain_type_alias_left_as_a_parse_shell_in_v2 (side-chat ruling: lowering-only,
option B; declaration grounding is a separate infer change).

- body_lowering_fold: body_lower_eq_type_decl (was the generic-only arm) serves
  every `=`/bodyless declaration. Plain alias -> type_alias_wrapper and plain
  bodyless -> type_opaque_wrapper, each with an EMPTY binder Conj
  (body_lower_decl_binders); plain coproduct -> its Disj member. The NoTypeParams
  / TypeParamsUnreadable pass-throughs are gone; body_lower_type_decl refuses an
  unreadable declaration (body_lowering_reason_type_decl_unreadable) instead of
  returning its shell. Reason renamed body_lowering_reason_type_decl_member_uncarried.
- v2.std.node type_binder_conj_conforms admits zero binders (identity and
  uniqueness checks unchanged).
- v2.std.type_binder: view arms renamed TypeAlias / OpaqueTypeDecl
  (cardinality-neutral); consumers symbol_index_fill and semantic_decl_emission
  follow. semantic_decl_emission refuses alias/opaque at struct/enum surfaces
  with its own reason (semantic_decl_reason_alias_or_opaque_is_not_a_member).
- namespace_graft: the type_decl shell-reading arm and its three helpers are
  deleted; measured unreachable (declaration_graft_assemble 16/16,
  type_param_binder_frame 37/37, new claims 5/5 with it answering UnitResidual).
- New v2.test.claim.body_lowering.plain_type_decl_lowering: positive
  representation claims over real assemblies via five WARM-shared verdict
  producers. With the pass-through restored, the coproduct / alias /
  alias-of-alias / bodyless rows go FALSE; the payload single-variant row is a
  preservation control (green either way).
- The debt row records the climb.

Not claimed: grounding. infer derives no Disj and keeps childless Conj on the
frontier, so these declarations are partially grounded after infer.

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

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

APPROVE-MERGE at exact head c314f4c3c85bbc8dbfcf0b13b272ea5dff0b5711.

This satisfies the lowering-only / option-B boundary we agreed.

The replacement is at the producer: every readable non-record/non-where type declaration now reaches the shared body_lower_eq_type_decl path; plain aliases and bodyless declarations use the existing alias/opaque wrappers with a zero-cardinality binder collection; coproducts remain members; unreadable/uncarried declarations refuse located rather than returning the parse shell. I found no compatibility arm preserving the old accepted shell.

The consumer side is migrated rather than dual-read: TypeAlias / OpaqueTypeDecl are cardinality-neutral in type_decl_view; symbol_index_fill preserves the no-members semantics for alias/opaque forms; semantic declaration emission refuses those forms explicitly; and the obsolete namespace-graft type-declaration shell reader/helpers are deleted.

The five new real-assembly claims positively discriminate coproduct/member vs alias vs opaque shapes and member-index behavior. The required-floor log shows all five planned-and-passed, their five WARM shared producers populated, and enrollment-margin admission. Existing type-parameter claims remain covered by the floor. The reported local mutation restoring the NoTypeParams shell pass-through makes the four intended discriminating rows false; I did not independently rerun that local mutation.

The type_binder_conj_conforms relaxation from nonempty to zero-or-more binders is acceptable here: identity/uniqueness checks remain, and the binder collection's cardinality is now representation data rather than an implicit 'generic' discriminator. I found no new source producer that uses an empty binder list to fabricate a generic member or arrow.

The recurring-failure-mode row closes only the representation debt and explicitly leaves structural grounding/emission unclaimed. No infer rule, grounding suppression, or emission bypass is introduced. That is the correct boundary; the remaining Disj/childless-Conj grounding frontier should be a separate inference capability.

Exact-head CI is green across witnesses, generated, compiler, clippy, floor, and emit-build. GitHub reports the PR mergeable. No remaining merge-blocking finding.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 29, 2026
Merged via the queue into main with commit 112c398 Sep 29, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/silent-swift-419-type-decl-lowering branch September 29, 2026 05:03
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