The type-parameter-in-value-position wall fires: flip its pinned hole to a firing red (split of #11819, parts 1+3)

dag/gunbc/kind_reflection_seed_growth.dag

@@ -4,65 +4,37 @@ import gunbc.roadmap_model { RoadmapNodeId }
 import gunbc.seed_growth { SeedGrowthJustification }
 import std.decl_ref { DeclarationRef, WholeDeclaration }
 
-// FORWARD-FREEZE RECEIPT for the hand Rust carried into the seed by the kind-reflection work
-// merged from gunbc#11819. Authored because review 69733 found the growth undeclared, and it was
-// right: gunbc.seed_growth_admission makes unenumerated hand growth in src/v1 a stop-line, and
-// prose in a // annotation cannot discharge it. DESIGN section 4c is the reason the annotations
-// those declarations already carry are not enough -- a dissolution condition is a typed carrier's
-// job, and "replaced by generated bytes on the next regen" living only in a comment is
-// uncountable by the roster that exists to count it.
+// FORWARD-FREEZE RECEIPT for the seed divergences left by the kind-reflection work merged from
+// gunbc#11819 (via gunbc#11996). Review 69733 found the growth undeclared, and
+// gunbc.seed_growth_admission makes undeclared hand growth in src/v1 a stop-line.
 //
-// THE POPULATION SPLITS IN TWO, AND ONLY ONE HALF IS REAL GROWTH. Sixteen declarations were added
-// or modified across v1_compiler_infer_resolve, v1_compiler_parse, v1_std_core,
-// std_machine_constraints and v1_compiler_infer. FIFTEEN of them resolve in the .dag authority --
-// type_arg_kind_inhabitance, KindInhabitance, kind_admissible_inhabitant_name,
-// kind_names_admissible_inhabitant, kind_lookup_trace, kind_decl_for_message,
-// node_authored_or_own_name, type_arg_display_spelling, type_param_kind_diagnostics,
-// type_arg_name_is_bound_generic_parameter, parse_optional_type_param_kind,
-// with_type_param_kind_property, TypeParamKindResult, type_param_kind_property_name, and the
-// WidthResolution arms -- so they are generated bytes carried BY HAND AHEAD OF A REGEN, which is
-// ExistingSeedItemModified rather than addition. ONE does not: binding_resolves_to_type_parameter
-// occurs ZERO times in every .dag under src/v1. That one is the growth, and it is the only
-// declaration this row cites.
+// NARROWED, NOT RETIRED (gunbc#12163, after review 70608). This row first cited ONE declaration:
+// the literal-false stub binding_resolves_to_type_parameter. It stood where v1.compiler.infer
+// declares name_is_enclosing_declared_type_parameter. The regen in gunbc#12045 carried that half:
+// the stub is gone, the seed's InferScope carries enclosing_declared_type_param_names, and
+// TypeParameterInValuePosition now refuses (test.claim.type_argument_kind_inhabitance_witness_test
+// a_type_parameter_in_value_position_must_refuse). But the row's trigger ALSO required the regen to
+// carry the four-parameter kind-inhabitance fold, and that half has NOT landed. Deleting the row on
+// the first half would retire it with an artifact short of its stated capability (DESIGN 4b(3)),
+// and would leave the two remaining divergences with no typed carrier (DESIGN 7).
 //
-// WHAT IT IS: A STUB WHOSE BODY IS THE LITERAL false, AND SAYING SO IS THE POINT. It stands where
-// v1.compiler.infer declares name_is_enclosing_declared_type_parameter, which asks the DECLARED
-// type-parameter roster carried on InferScope as enclosing_declared_type_param_names. The seed's
-// InferScope HAS NO SUCH FIELD. Implementing the predicate by hand therefore means adding a struct
-// field and plumbing it through every InferScope construction site in generated Rust -- which is
-// cementing compiler logic into the seed to make a check go green, the direction DESIGN section 7
-// and this repository's standing instruction both refuse. The stub is the smaller, more honest
-// debt, and it is declared here rather than left silent.
-//
-// THE CURRENT BOUNDARY IS A DEAD BRANCH AND AN INERT WALL, MEASURED RATHER THAN ASSERTED. Because
-// the predicate is false, both call sites in v1_compiler_infer take their else arm always, so the
-// net behavioural delta of all three added items is ZERO -- and the consequence is that
-// TypeParameterInValuePosition, which v1.std.core declares with SeverityError and
-// GateBlocking and v1.compiler.infer constructs at two sites, CANNOT FIRE. A module whose entire
-// content is a generic function returning its own type parameter compiles with exit 0, zero
-// blocking errors, and emits. That is not a side note about this row; it is what this row is
-// declaring, and DESIGN section 4b names it: the tier where the machinery exists but nothing gates
-// on it, and an inert lens is itself a lie.
-//
-// THE SILENCE IS WITNESSED RATHER THAN DESCRIBED.
-// test.claim.type_argument_kind_inhabitance_witness_test pins it as a SILENCE assertion with an
-// adequacy control on the same harness and the same run, so the zero is the compiler's and not a
-// harness that never reached the judgment. It goes red the day the wall works, and that red means
-// flip the assertion, not relax it. The class is
-// gunbc.recurring_failure_mode.a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles.
-//
-// WHY THE STUB IS NOT SIMPLY DELETED, which is the first repair anyone should reach for. Deleting
-// it means deleting the two call sites with it, and those two branches DO resolve in the .dag --
-// v1.compiler.infer constructs the diagnostic at exactly those points. Removing them would put the
-// seed further from the authority rather than closer, and the next regen would re-add them. The
-// divergence worth removing is the predicate, and the way to remove it is the regen, not a second
-// hand edit.
+// THE TWO DIVERGENCES STILL LIVE, each hand-carried seed bytes that disagree with the .dag authority:
+//   - v1.compiler.infer_resolve type_arg_kind_inhabitance takes FOUR parameters (arg, kind_node, env,
+//     module_name) and consults kind_inhabitant_matches_resolved. The seed's takes THREE, and
+//     kind_inhabitant_matches_resolved does not exist in the seed.
+//   - std.machine_constraints WidthResolution is a TWO-ARM coproduct (StaticWidthIndex |
+//     PointerWidth). The seed's std_machine_constraints carries `pub type WidthResolution =
+//     PointerWidth`, the single-arm alias the .dag was changed away from.
+// The kind-wall claims pass on the seed as it stands, so neither divergence is observed to change a
+// verdict today. That is a reading over the witness fixtures, not over the corpus, and it is why
+// these rows stay declared rather than dismissed.
 data kind_reflection_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
   hand_authored_declarations: [
-    DeclarationRef { module_path: "v1_compiler.v1_compiler_infer", decl_name: "binding_resolves_to_type_parameter", field: WholeDeclaration }
+    DeclarationRef { module_path: "v1_compiler.v1_compiler_infer_resolve", decl_name: "type_arg_kind_inhabitance", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1_compiler.std_machine_constraints", decl_name: "WidthResolution", field: WholeDeclaration }
   ],
-  reason: "A stub standing where v1.compiler.infer declares name_is_enclosing_declared_type_parameter. The declared predicate reads InferScope's enclosing_declared_type_param_names roster; the seed's InferScope carries no such field, so honouring it by hand would mean adding a struct field and threading it through every construction site in generated Rust -- hand-authoring compiler logic into the seed to make a wall go green, which DESIGN section 7 refuses. Its body is the literal false, so both call sites take their else arm always and the behavioural delta of the whole kind-reflection seed carry is zero.\n\nWHAT IT COSTS, STATED AND NOT NETTED AWAY: TypeParameterInValuePosition is declared SeverityError/GateBlocking and constructed at two sites, and it cannot fire. A generic function returning its own type parameter compiles clean and emits. The silence is pinned by test.claim.type_argument_kind_inhabitance_witness_test as an explicit hole assertion with an adequacy control on the same run, and filed as gunbc.recurring_failure_mode.a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles.\n\nSCOPE, ENUMERATED RATHER THAN COUNTED. Fifteen further declarations in this change resolve in the .dag authority and are generated bytes carried ahead of a regen (ExistingSeedItemModified per gunbc.seed_growth_admission SeedGrowthChangeDisposition), so they are not counted as additions; they are named in this file's header rather than omitted. TWO of them diverge in SHAPE and both are disclosed for the same reason; an earlier revision of this row said ONE and was off by one on its own stated axis (review 69986, BLOCKING). FIRST: the seed's type_arg_kind_inhabitance takes three parameters where v1.compiler.infer_resolve declares four, because the seed lacks the kind_inhabitant_matches_resolved arm. SECOND: src/v1/stage0/src/std_machine_constraints.rs carries `pub type WidthResolution = PointerWidth;`, an ALIAS, where std.machine_constraints now declares the two-arm coproduct StaticWidthIndex | PointerWidth -- the emission convention for such a coproduct is one enum plus a marker struct per arm, visible in this same change at v1_compiler_infer_resolve's KindInhabitance, and StaticWidthIndex occurs nowhere under src/. So the mirror is not the bytes a regen would produce, and the seed cannot express the literal arm at all. Neither divergence is repaired by hand: hand-carrying either is the cementing DESIGN section 7 refuses, and both close on the same regen this row's trigger names. The behaviour they leave is measured rather than assumed -- the kind wall's reds and its positive control are witnessed on the BUILT compiler by test.claim.type_argument_kind_inhabitance_witness_test, and the literal axis is admitted unconditionally by the language-level rule in either tree, so the alias costs no refusal the coproduct would have made today.",
+  reason: "Hand-carried seed bytes that approximate the .dag authority rather than being generated from it. The seed's type_arg_kind_inhabitance is the three-parameter form without the resolved-identity comparison (kind_inhabitant_matches_resolved) that v1.compiler.infer_resolve declares. The seed's WidthResolution is the single-arm alias the .dag replaced with the two-arm coproduct StaticWidthIndex | PointerWidth, because an alias kind is unreadable at the kind-check site. Hand-patching either to match would cement compiler logic into the seed, which DESIGN section 7 refuses; the regen is the repair.",
   owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
-  trigger: "Regenerate the stage0 mirror from v1.compiler.infer and v1.compiler.infer_resolve -- SUFFICIENT FOR the built compiler to consult the declared type-parameter roster and to carry the four-parameter kind-inhabitance fold, so that a type name in value position refuses at its own location rather than at rustc's, and the seed's checking predicates are the authority's rather than hand-carried approximations of them. The regen is what deletes this row; a further hand patch to either declaration would not, because it would leave the seed and the authority disagreeing about which predicate decides.",
-  current_boundary: "Both call sites are dead branches: the predicate is false, so the net behavioural change is zero and no program is judged differently than before this change. The cost is not a wrong answer but an absent one -- the value-position wall is unreachable by construction, and gunbc#11819's claim that it fires is retracted in gunbc#11996 rather than carried. The kind-inhabitance wall it sits beside DOES fire and is witnessed in both directions on one run, so the two must not be read together: one wall discriminates, the other is inert, and the seed is why."
+  trigger: "Regenerate the stage0 mirror from v1.compiler.infer_resolve and std.machine_constraints -- SUFFICIENT FOR the built compiler to carry the four-parameter kind-inhabitance fold including kind_inhabitant_matches_resolved, and for the seed's WidthResolution to be the two-arm coproduct the .dag declares, so the seed's kind check is the authority's rather than a hand-carried approximation of it. The regen is what deletes this row; a further hand patch to either declaration would not, because it would leave the seed and the authority disagreeing. The value-position half of this row's original trigger was discharged by gunbc#12045 and is not re-cited here.",
+  current_boundary: "Every claim in test.claim.type_argument_kind_inhabitance_witness_test passes on the seed as it stands: named and same-shaped wrong-kind arguments refuse, both declared arms are admitted, and a type parameter in value position refuses. So the divergence is not observed to change a verdict on those fixtures. It is still a disagreement between the seed and its authority about how the check is computed, and a kind declared as an alias, or an argument that matches only by resolved identity, would be judged by the seed's form, not the .dag's."
 }

dag/gunbc/recurring_failure_mode/a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles.dag

@@ -18,12 +18,13 @@ data a_wall_declared_in_dag_is_inert_in_the_seed_that_compiles: RecurringFailure
 
     "WHY A GREEN WITNESS DOES NOT CATCH IT, WHICH IS THE PART WORTH CARRYING. A witness asserting the wall REFUSES goes red and cannot merge, so the pressure is to delete it -- and deleting it removes the only thing that would have noticed. A witness asserting the wall ADMITS is green, merges, and reads to every later reader as coverage of a working wall. The honest instrument is neither: pin the hole explicitly, assert the CURRENT silence, state in the claim that it must not be read as a guarantee, and ship an adequacy control on the same harness and the same run that DOES count a blocking row, so a zero is the compiler's silence rather than the harness never reaching the judgment.",
 
+    "THE RECEIPT INSTANCE CLIMBED, AND NOTHING REPORTED IT. That is the class's second face. gunbc#12045 regenerated v1_compiler_infer.rs from the .dag. The literal-false stub binding_resolves_to_type_parameter was gone, name_is_enclosing_declared_type_parameter and InferScope enclosing_declared_type_param_names were in the seed, and TypeParameterInValuePosition began to fire. The claim pinning the hole at == 0 was therefore red on main. It was found only because a later lane measured it: claim_batch on a clean tree at ada85b9 failed the pinned claim while its generic-function control and its named-non-inhabitant control passed on the same run. It is now the firing red test.claim.type_argument_kind_inhabitance_witness_test a_type_parameter_in_value_position_must_refuse, and the hand-growth receipt gunbc.kind_reflection_seed_growth was NARROWED rather than retired: its trigger also named the four-parameter kind-inhabitance fold, which the same regen did not carry, so only the value-position half was discharged (review 70608 caught a first draft that deleted the row on that half alone -- this class's own mistake, one level up). THE LESSON FOR THE INSTRUMENT: a pinned hole is honest only while something RUNS it on every change that could close it. A regen closes holes it was never aimed at, so the lane that regenerates the seed must run the pinned holes over the modules it regenerated, or the climb is as silent as the gap was.",
     "RUNG FOUND AT: below the ladder -- silent acceptance of a program the declared rules refuse, with the authority and the realization disagreeing and nothing reporting it. ATTAINABLE CEILING: mechanically preventable. Whether a declaration the .dag references is ABSENT FROM THE SEED is decidable from the two trees with no build, so a gate can refuse a change that adds a checking predicate the mirror does not carry. STRUCTURALLY GUARANTEED would need the seed to stop being a separately-edited artifact at all, which is the self-host program's own terminal state and not this row's to claim. NEXT-RUNG TRIGGER: a gate comparing declared checking predicates against the stage0 mirror -- SUFFICIENT FOR a change that authors a refusal in .dag to refuse merging while the seed cannot perform it, so no wall can be reported as firing on the strength of the authority alone.",
   ],
 
   evidence: [
     DeclarationRef { module_path: "v1.compiler.infer", decl_name: "name_is_enclosing_declared_type_parameter", field: WholeDeclaration },
     DeclarationRef { module_path: "v1.std.core", decl_name: "TypeParameterInValuePosition", field: WholeDeclaration },
-    DeclarationRef { module_path: "test.claim.type_argument_kind_inhabitance_witness_test", decl_name: "a_type_parameter_in_value_position_does_not_yet_refuse_and_this_pins_that_hole", field: WholeDeclaration },
+    DeclarationRef { module_path: "test.claim.type_argument_kind_inhabitance_witness_test", decl_name: "a_type_parameter_in_value_position_must_refuse", field: WholeDeclaration },
   ],
 }