Repository navigation
Split the reference-site identity fallback by structure, census it, declare the production key (CARRIER-KEY-1 step 1) - #11503
Conversation
…eclare the production key as a rung drop (CARRIER-KEY-1 step 1) type_reference_provenance answers 'this node is its declaration' and 'this reference's declaration was not recovered' with one arm keyed on the node's own span. The new query v1.std.core type_reference_identity (std.coercion TypeReferenceIdentity) tells them apart from STRUCTURE -- the parser's ModuleItemTypeDeclaration mark, the kernel mint, an inferred TypeVariable binder -- and refuses the rest with a cause. Production reads are unchanged; the mis-keyed production key is declared as gunbc.rung_drop type_reference_location_fallback_keys_production_realization. Adds the split_identity column to v1.tests.claim.carrier_realization_census, the executing witness ct_type_reference_identity_split_test (RED confirmed by reverting the declaration test in the emitted mirror), a record on the occurrence census, a receipt on state_space_conflation, and the recurring failure mode resolved_value_computed_then_discarded_for_the_authored_one for the field-type discard in v1.compiler.infer_resolve resolve_item_types. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Ledger-Repair-Judged: docs/design-rung-drops.md Ledger-Rows-Repaired: docs/design-rung-drops.md type_reference_location_fallback_keys_production_realization
…instead of a wildcard Bool helper (review 67150) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Addressed review 67150 in 55743bf. |
|
On review 67170's note that |
CARRIER-KEY-1, step 1 only: split the collapsed reference-site identity fallback by structure, report the split per occurrence in the census, and declare the key production still uses as a rung drop. Production answers are unchanged, and this does not fix any E0308.
The brief's symbols are stale
The brief names
v1.compiler.coercion type_reference_decl_file. #10006 replaced it withv1.std.core type_reference_provenance, which returnsstd.coercion TypeDeclarationProvenance. Its own-span fallback arm, the defect this PR splits, is unchanged. The brief's "0 of 111 resolved / 8 true by accident" figure was measured on the pre-reconcile tree, anddocs/plans/carrier-realization-arbiter-repair-design.mdwithdraws it. The step 2 finding below was taken on the typed tree instead.What lands
std.coercionTypeReferenceIdentityhas four arms:ReferenceResolvedToDeclaration,ReferenceIsTheDeclaration,ReferenceIsTypeVariableBinder, andReferenceIdentityUnavailable { cause }. The cause isNoResolutionBoundAtReference,ResolvedNodeIsNotADeclarationorDeclarationNodeCarriesNoSpan.v1.std.coretype_reference_identitydecides from structure: the parser'sModuleItemTypeDeclarationmark, the existing kernel recognizer (throughdeclaration_provenance_of), and aninferred TypeVariablebinder. It never decides from "is aResolvednode bound" or "is a span present", because the step 2 finding shows both proxies put each state on both sides. Everything else refuses.v1.tests.claim.carrier_realization_censusgets asplit_identitycolumn.gunbc.type_reference_decl_file_occurrence_censusgets aFallbackArmSplitrecord naming the query, the instrument and the witness. It carries no counts; the instrument re-derives them.v1.compiler.compiler_tests_rustct_type_reference_identity_split_test, with seven cases. The RED case is an unresolved reference outside its declaring module: it must refuse, and the same case asserts the legacy read keys it on its own file.gunbc.rung_droptype_reference_location_fallback_keys_production_realization(§4b(3)), previousMechanicallyPreventable, temporaryOutsideTheLadder. It is restored when every production reader of the key uses a declaration-node or env-binding authority and the own-span fallback arm is deleted.state_space_conflation, and a new row,resolved_value_computed_then_discarded_for_the_authored_one, for the field-type discard (step 2).Evidence (local, head of this PR)
cargo test --release -p v1-compiler --lib type_reference_identity_split: 1 passed.v1_std_core.rs, I replaceddeclaration_node_provenance's declaration test withtrue. The witness then failed with "an unresolved reference must refuse, never key on the file it sits in". The mirror was restored afterwards.claim_executor --required-regengavefirst_generation_equal=true, exit 0, with a rebuilt binary. The drift was confined tostd_coercion.rs,v1_std_core.rs,v1_compiler_compiler_tests_rust.rs,compiler_tests.rsandv1_tests_claim_carrier_realization_census.rs, and every production function is byte-identical. The self-host K=64 A/B has not been run; that is fierce-seal-607's run.gunbc.rung_drop rust_unit_tests_off_the_merge_path). Its execution is local only.First run of the split column
Run
carrier_realization_censusover the import closure ofsrc/v2/compiler/01_tokenize.dagand joinsplit_identityto the identity and legacy key columns. Results are qualitative here, not transcribed:IsTheDeclarationagrees with the environment's declaration. No false declaration answers.std.algebra.FreeMonoidminted on its kernel pseudo-file answersResolvedToDeclaration:KernelMintedwhile the environment namesdag/std/algebra.dag. That behaviour comes from the existing kernel recognizer (state_space_conflationthird form), and the census record documents it.Step 2 finding (why
n.inferredis notResolved), typed treev1.compiler.infer_resolvereplaces the reference with the declaration node, keeping the declaration's span, and adds noResolvedwrapper. So "notResolved" does not mean "inference unavailable".Resolvednode of an applied reference is built on the reference's own span. That makes the resolved arm location-keyed too.resolve_item_typesresolves each record and coproduct field type, then rebuilds the field fromchild.childrenandchild.inferred, keeping only diagnostics and properties.resolve_field, which keeps the resolved type, has no callers.v1.compiler.emit_rust type_reference_provenance_in_envpatches the symptom downstream (§6b). The same kernelString,IntandBoolare keyed correctly as function parameters and wrongly as record fields.Repair targets (step 3, not touched here): stop discarding
tr.resolvedin the field arms, makeresolve_fieldtheir single route or delete it, remove the env re-resolution downstream, and key identity on the declaration node rather than a span. Each changes emission, so each needs the step 3 measurement.Not in scope
Step 3: the pinned-tree census, the A/B/C/D counterfactual, and the renderer reroute. No resolver edit, no short-circuit deletion, no monomorphization, and no constructor-only repair.
🤖 Generated with Claude Code