v2: kinded type params; type applications checked in exact bijection; de-fork MachineWidth onto std.machine_constraints

dag/gunbc/defork_type_name_census.dag

@@ -204,26 +204,17 @@ data defork_census_rows: List<SharedTypeNameRow> = [
     names: ["Int8", "Int16", "Int32", "Int64", "Int128", "UInt8", "UInt16", "UInt32", "UInt64", "UInt128"],
     reading: AuthoredResolutionReading {
       dag_side: "→ `std.machine_constraints` `Compose` / `MachineWidth<N>` + `std.integer` `Int`/`UInt`",
-      v2_side: "→ `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth<WordN>` + `v2.std.integer` `Int`/`UInt`",
-      class: "same concept, every referent divergent"
+      v2_side: "→ `std.machine_constraints` `Compose` / `MachineWidth<N>` + `v2.std.integer` `Int`/`UInt`",
+      class: "same concept, Int/UInt referent divergent"
     },
     disposition: ForkNeedsDecisionRecord { family: "integer family" }
   },
   SharedTypeNameRow {
     names: ["IntPlatform", "UIntPlatform"],
     reading: AuthoredResolutionReading {
       dag_side: "→ `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth`",
-      v2_side: "→ `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth`/`PointerWidth`",
-      class: "text near-identical, every referent divergent"
-    },
-    disposition: ForkNeedsDecisionRecord { family: "integer family" }
-  },
-  SharedTypeNameRow {
-    names: ["Compose", "MachineWidth"],
-    reading: AuthoredResolutionReading {
-      dag_side: "`std.machine_constraints` — phantom composition / width over `WidthResolution`",
-      v2_side: "`v2.std.integer` / `v2.std.machine` — opaque, unconstrained parameter",
-      class: "same concept, divergent constraint"
+      v2_side: "→ `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth`",
+      class: "text near-identical, Int/UInt referent divergent"
     },
     disposition: ForkNeedsDecisionRecord { family: "integer family" }
   },
@@ -248,6 +239,11 @@ data defork_census_rows: List<SharedTypeNameRow> = [
 ]
 
 data defork_census_resolved: List<ResolvedSharedTypeName> = [
+  ResolvedSharedTypeName {
+    names: ["Compose", "MachineWidth"],
+    resolution: ResolvedByDeletingV2 { reason: "N7-2 root B: v2 gained kinded type parameters (`v2.std.type_binder` `type_application_conformance`), so the kinded `std.machine_constraints` `MachineWidth<bits: WidthResolution>` normalizes on the native route; `v2.std.machine` `MachineWidth`/`PointerWidth` and `v2.std.integer` `Compose` are deleted and `v2.std.integer` imports them from `std.machine_constraints` (its `MachineWidth<WordN>` rows were kind-wrong and now read `MachineWidth<N>`)" },
+    change: 13038
+  },
   ResolvedSharedTypeName {
     names: ["String"],
     resolution: ResolvedByDeletingDag { reason: "operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid<Char>`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling)" },

dag/gunbc/recurring_failure_mode/a_binding_position_recorded_as_a_declaring_identity.dag

@@ -11,6 +11,7 @@ data a_binding_position_recorded_as_a_declaring_identity: RecurringFailureMode =
     "HARM. One declaration acquires one identity PER RELAY it is reached through, so the map that exists to make identity single-valued is the thing that forks it. Nothing refuses: every path resolves, and the reference is Accepted. It surfaces downstream as a wrong answer with no diagnostic -- a target that spells a declaration by its module emits a path into the relay module, which declares nothing and therefore has no item to name, so the emitted program refers to something that was never written.",
     "DISTINGUISHING FACTS. refusal_reason_minted_as_canonical_identity is a value minted from the WRONG VOCABULARY (a diagnostic reason standing in a name's place); this row is a value from the RIGHT vocabulary read at the WRONG LAYER -- a real qualified path, naming a real position, that is a binding rather than a declaration. The recognition rule is a question, not a spelling: when a field is named for a DECLARATION, ask whether every writer of it can only have written a declaration there, and follow one re-export before answering. An index whose lookup succeeds at a relay will answer that question wrong and stay green.",
     "RECEIPT (2026-09-22, fierce-wren-487, found by review 70003 on gunbc#12048). Uninhabited until resolution began CARRYING the declaring path: while a resolved reference was a bare leaf the recorded declaring path reached no consumer, so the fork existed in the index and was unobservable. The enrolled chain claim could not see it either -- it asserted only that the chain RESOLVES, and an index that stops at the relay resolves perfectly well. Repaired by chasing one step through symbol_index_claimants_at, which already answers who declares what lives at a position; a relay's own row was chased the same way when it bound, so one step reaches the home. Enrolled: v2.test.claim.namespace_xl0.cross_module_reference_resolution a_re_export_resolves_to_the_home_not_the_relay_holds, whose NEGATIVE conjunct is the discriminator -- measured FAIL before the chase and PASS after, with the sibling same-leaf row PASS in both runs.",
+    "RECEIPT, SECOND WRITER (2026-10-03, sunny-lynx-759, gunbc#13038). v2.compiler.symbol_index_fill symbol_index_fill_unique_variant_aliases writes a module-unique variant TWICE as an ENTRY: once at its declaring path under its coproduct (p.Resolution.Pointer, symbol_index_fill_containment_node) and again at the module-level binding position (p.Pointer), over the same arm node, through symbol_index_insert rather than a binding row. So symbol_index_declaring_path_of answers p.Pointer for p.Pointer -- the binding position is its own declaring identity, and the chase this row's first repair added cannot reach the home. MINIMAL REPRODUCER: `module p` / `type Resolution = Static | Pointer` / `type Width<bits: Resolution>` / `type UsesPointer = Width<Pointer>`. The bare `Pointer` resolves to declaration_reference p.Pointer; comparing it by declaring path against the kind's variant p.Resolution.Pointer judged a conforming argument OUTSIDE its kind (resolve_reason_type_argument_kind_not_inhabited, measured on the gunbc#13038 branch before the workaround). gunbc#13038 compares the indexed declaration NODE instead (v2.compiler.resolve resolve_path_declares_node), which is a consumer-side workaround and not the repair; v2.test.claim.type_application_kind tak_kinded_parameter_accepts_a_variant_of_its_kind is the control that went red. THE REPAIR this receipt names: the variant alias is a BINDING to its declaring path (recorded so symbol_index_claimants_at answers p.Resolution.Pointer), not a second entry, after which resolve_path_declares_node can be replaced by a declaring-path comparison.",
     "RUNG FOUND AT: outside the ladder -- silent wrongness.",
     "CEILING: structurally impossible. A binding position and a declaring position are different concepts sharing one carrier (QualifiedName), so either can be written where the other is owed. The wall is the type: a declaring identity a binding path cannot inhabit, which is the same wall refusal_reason_minted_as_canonical_identity names from its own direction.",
     "NEXT-RUNG TRIGGER: a declaration-identity carrier distinct from the qualified path of an arbitrary position, so that symbol_index_bind_at cannot be handed a binding position at all; until then the enrolled row above is the wall, and it is a permanent regression control rather than an expecting-red probe.",
@@ -19,5 +20,8 @@ data a_binding_position_recorded_as_a_declaring_identity: RecurringFailureMode =
     DeclarationRef { module_path: "v2.compiler.symbol_index_fill", decl_name: "symbol_index_bind_pending_round", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.std.symbol_index", decl_name: "symbol_index_declaring_path_of", field: WholeDeclaration },
     DeclarationRef { module_path: "v2.test.claim.namespace_xl0.cross_module_reference_resolution", decl_name: "a_re_export_resolves_to_the_home_not_the_relay_holds", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.symbol_index_fill", decl_name: "symbol_index_fill_unique_variant_aliases", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.compiler.resolve", decl_name: "resolve_path_declares_node", field: WholeDeclaration },
+    DeclarationRef { module_path: "v2.test.claim.type_application_kind", decl_name: "tak_kinded_parameter_accepts_a_variant_of_its_kind", field: WholeDeclaration },
   ],
 }

docs/plans/dag-v2-defork-audit.md

@@ -192,22 +192,22 @@ Definition-unification (§3b.2: delete the dag record-of-methods *definition*) a
 
 ## 2D. The shared type-name census (the one list): the population is derived, the dispositions are authored
 
-**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **20 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`.
+**Derived:** every name declared as a `type` (record, coproduct or alias) under both `dag/std` and `src/v2/std`, read from the namespace by `gunbc.defork_type_name_census` `shared_type_names` at generation — **18 names** in this projection. **Authored:** each row's disposition, and — until the frontier below lands — the reading of what each side's body RESOLVES to. The two meet in an identity join by name, refused in both directions (a derived name no row disposes of; a row naming a pair that no longer exists), so this section cannot be generated from a stale disposition. Resolution, not body text, is what separates the classes: `Float = Float64` was byte-identical on both sides and bound two different `Float64`s. A **meaning fork** is one name for materially different concepts (DESIGN §3), resolved by renaming or deleting one side at its declaration, delete-first with no alias, the new name taken from the cited framework. **Frontier:** module-scoped type-reference resolution over the live pool, consumable from .dag: for a type declaration, each name its body references resolved to the declaration it binds in that module's scope (its own declarations, else its imports). When it lands, the three reading columns of every row here are derived from it and the authored readings are deleted; nothing else retires this frontier. Candidate home: `v2.compiler.name_resolve::resolve_with_admission`.
 
 | name(s) | declared in (derived) | dag/std side (authored reading) | src/v2/std side (authored reading) | class (authored) | disposition |
 | --- | --- | --- | --- | --- | --- |
 | `NonNegativeInt`, `PositiveInt` | `dag/std/integer.dag`, `src/v2/std/refinement.dag` | `std.integer` — `= Nat` / `= Nat where gt_zero` (refinement of `std.nat` `Nat`) | `v2.std.refinement` — record `refined: Refined<Int>` (smart-constructor over `v2.std.integer` `Int`), consumed by the formatter extdeps | MEANING FORK | OPEN — next PR of the de-fork wave (the v2 side has ~40 consumer sites across `v2.extdeps.formatters.*`) |
 | `Int`, `UInt` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.nat` `Nat` (via `std.algebra` `GroupCompletion`) | → `v2.std.nat` `Nat` | same concept, divergent referent | NEEDS A DECISION RECORD (integer family) |
-| `Int8`, `Int16`, `Int32`, `Int64`, `Int128`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, `UInt128` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose` / `MachineWidth<N>` + `std.integer` `Int`/`UInt` | → `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth<WordN>` + `v2.std.integer` `Int`/`UInt` | same concept, every referent divergent | NEEDS A DECISION RECORD (integer family) |
-| `IntPlatform`, `UIntPlatform` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | → `v2.std.integer` `Compose`, `v2.std.machine` `MachineWidth`/`PointerWidth` | text near-identical, every referent divergent | NEEDS A DECISION RECORD (integer family) |
-| `Compose`, `MachineWidth` | `dag/std/machine_constraints.dag`, `src/v2/std/integer.dag`, `src/v2/std/machine.dag` | `std.machine_constraints` — phantom composition / width over `WidthResolution` | `v2.std.integer` / `v2.std.machine` — opaque, unconstrained parameter | same concept, divergent constraint | NEEDS A DECISION RECORD (integer family) |
+| `Int8`, `Int16`, `Int32`, `Int64`, `Int128`, `UInt8`, `UInt16`, `UInt32`, `UInt64`, `UInt128` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose` / `MachineWidth<N>` + `std.integer` `Int`/`UInt` | → `std.machine_constraints` `Compose` / `MachineWidth<N>` + `v2.std.integer` `Int`/`UInt` | same concept, Int/UInt referent divergent | NEEDS A DECISION RECORD (integer family) |
+| `IntPlatform`, `UIntPlatform` | `dag/std/integer.dag`, `src/v2/std/integer.dag` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | → `std.machine_constraints` `Compose`/`MachineWidth`/`PointerWidth` | text near-identical, Int/UInt referent divergent | NEEDS A DECISION RECORD (integer family) |
 | `TerminationProof` | `dag/std/termination.dag`, `src/v2/std/cardinality.dag` | `std.termination` — `dimensions: List<RankingDimension>` | `v2.std.cardinality` — `non_increasing: List<RankingComponent>`, `strict: RankingComponent` | same question, divergent model | NEEDS A DECISION RECORD (termination) |
 | `Unit` | `dag/std/types.dag`, `src/v2/std/cardinality.dag` | `std.types` — empty record | `v2.std.cardinality` — empty record | one concept, two declarations | NEEDS A DECISION RECORD (unit) |
 
 **Resolved — each name must stay absent from the derived population; a name here that is declared under both roots again refuses by name:**
 
 | name(s) | resolution | change |
 | --- | --- | --- |
+| `Compose`, `MachineWidth` | v2 side deleted — N7-2 root B: v2 gained kinded type parameters (`v2.std.type_binder` `type_application_conformance`), so the kinded `std.machine_constraints` `MachineWidth<bits: WidthResolution>` normalizes on the native route; `v2.std.machine` `MachineWidth`/`PointerWidth` and `v2.std.integer` `Compose` are deleted and `v2.std.integer` imports them from `std.machine_constraints` (its `MachineWidth<WordN>` rows were kind-wrong and now read `MachineWidth<N>`) | #13038 |
 | `String` | dag side deleted — operator-ruled retirement of `std.string_type` `String` (`= FreeMonoid<Char>`), the duplicate of `v2.std.text` `String`. It had zero importers after gunbc#12512 deleted the 81 that used it as host text (XL-0T ruling B), verified by the #12760 literal-site census. `v2.std.text` `String` stays the one structural declaration, and `v2.std.node` `String` is the distinct host-text concept (gunbc.recurring_failure_mode carrier_by_spelling) | #13089 |
 | `Nat` | v2 side deleted — operator ruling A (2026-09-30): the carrier is Peano, declared once in `std.nat` and realized as the kernel integer (`gunbc.structural_realization_bindings` `kernel_grounding_rows`); the `v2.std.nat` declaration is deleted, `std.magnitude` retired, and the semiring moved to inhabitance | #12846 |
 | `Float` | both sides deleted; the concept is homed at `extdeps.standards.ieee_754_2019 binary64` — IEEE 754-2019 §3.6 (operator ruling relayed 2026-09-28): `std.float` (Float = Float64, uncited) and `v2.std.float` (Float = Binary64) both deleted; kernel Float's meaning is the `std.kernel_type_denotation` row, not a std alias | #12547 |