Repository navigation
Refuse phantom classification without evidence - #9983
Conversation
23f01e7 to
f0ed0fd
Compare
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES at exact head f0ed0fd2a8e2a9e96a42cd084a4e34d857aeaf5d.
The technical repair is accepted: the module-own TypeEnv reaches the applied-type renderer, observation is no longer conflated with absence, UnitVariantPhantomEvidenceUnavailable becomes a distinct located refusal rather than fabricated UnresolvedType, and the two mutations discriminate both refusal presence and refusal identity. The bounded claim is also honest: this proves the renderer seam, not every marker-classification consumer or the separate NS-0B alias population.
The present head cannot be authorized for landing because its exact-tree evidence is stale against current main. f0ed0fd2... is one commit on parent 99ace7a...; live main is now 3ac78310..., nine commits ahead. Both histories changed src/v1/compiler_tests_rust.dag, and both changed its generated projections src/v1/stage0/src/compiler_tests.rs and src/v1/stage0/src/v1_compiler_compiler_tests_rust.rs. The branch's 149/149/149 fixed point and exact-head CI therefore certify only the pre-composition tree. --match-head-commit would pin the source head but would not prove the automatically composed landing tree or its generated fixed point.
The cached GitHub merge subject is also unusable: it still names a merge into 87ecf818..., while the live pull endpoint currently reports mergeability unknown against a stale base snapshot.
Required re-review bar: merge current main forward into this branch (do not rebase away the reviewed history); preserve both authority edits; regenerate the generated projections from the composed authority rather than accepting a textual merge; reach a fresh exact-head fixed point and install bridge; run exact-head CI; return the new SHA.
Metadata correction on return: the PR body sentence saying these edits add 'zero declarations or public items' is literally too broad because UnitVariantPhantomLookup is a new modeled declaration and generated public enum. The seed-growth conclusion can remain, but should say zero hand-authored Rust seed declarations/public items.
Purpose
This v1-freeze maintenance cut serves the v2 self-host program. It fixes an evidence defect at the Rust applied-type renderer seam: the renderer previously received an empty
TypeEnv, and an unobserved unit-variant census silently answered “absent.” The advertised lookup never had identity evidence; NS-0B removed the fallback coincidence rather than breaking rendering.This does not fix or claim the separate 48-alias NS-0B marker regression. Main's emitted marker bytes remain correct by coincidence until the occurrence-to-renderer identity modeling question is resolved separately.
Change
TypeEnvthrough the shared applied-type renderer path.EvidenceUnavailablerather than widening “no evidence” into “not a marker.”UnitVariantPhantomIdentityEvidenceUnavailable { name, span }diagnostic; do not fabricateUnresolvedTypewhen the missing census prevents that conclusion.Timecontribution renders through the positive arm.The refusal is established AT THIS RENDERER SEAM, by a fixture that reaches the real applied-type renderer. It does not establish that every consumer of the marker classification refuses on empty evidence, and it does not fire #9915's ceiling trigger.
Authority and regenerated projections are one atomic commit; an authority-only head would be an invalid intermediate.
Constructor census
The raw brace-form census found 25 matches under stage0. One is the
TypeEnvstruct definition, leaving 24 constructors = 17 generated + 7 hand-maintained. No alternateTypeEnv::new,TypeEnv::default, or braceless construction path exists. The seven hand sites all truthfully setunit_variant_index_observed: false, for distinct local reasons:infer_semantics_witness.rs:336:empty_type_envis unobserved by definition.:1078,:1109,:1140: Optional fixtures carry Optional through cardinality and do not build this census.:1279: ordinaryUserTypeBinding; it never runsbuild_unit_variant_index.:2004: ordinary genericBoxTypeBinding; it never runs that census.cli_run.rs:34880: a SymbolIndex/bindings probe; it does not scan a unit-variant census.No hand-maintained site is observed=true. Production establishes that state only through
build_unit_variant_index; the populated renderer fixture exercises that true path with a realTimecontribution.The seed-growth rosters govern DeclarationRef/public-item additions. These edits change existing bodies and add zero declarations or public items, so no roster member is added. The PURPOSE admission is explicit: this frozen-v1 maintenance enables the v2 self-host program.
Evidence
empty census silently answered absence; rendered=Box<Time>.render_rust_applied_type_routes_qualified_base_through_leaf_namepasses with both empty-evidence refusal and populated-index positive control.99ace7a15668f0d2d364a1aeef53076215524459: the original lineage changed eight projections; the resolver-diagnostic correction then changed exactlyv1_std_core.rsandv1_compiler_infer_resolve.rs; the final exact-tree regeneration reachedfirst_generation_equal=true, planned/executed/adjudicated149/149/149.v1_std_core.rsmoved because it is the generated projection of the diagnostic type, span, and message authority;v1_compiler_infer_resolve.rsmoved because it projects the resolver emission arm.Cargo.tomlwas neither offered nor applied.cargo test --release -p v1-compiler --all-targets --no-runsucceeds, covering test-only and binary constructors.git diff --checkand pre-commit/pre-push formatting checks succeed.Resolver-refusal instrument correction
The speculative-peel witness already said it counted typed resolver refusals, but its filter counted only
UnresolvedType. The refusal population legitimately grew when missing marker evidence became the distinct, truthfulUnitVariantPhantomIdentityEvidenceUnavailable; the instrument now counts the enumerated union and separately asserts that both observed refusals are the evidence-unavailable variant. The union is deliberately enumerated: a broad “any diagnostic” predicate would accept unrelated diagnostics, while adding another typed refusal variant to this path now obliges updating this roster.With the correction present, the exact witness observes total typed resolver refusals
2, evidence-unavailable refusals2, retired diagnostics0, and quiet diagnostics0. A dropped-arm mutation that emitted no diagnostic went RED atcli_run.rs:34965:a resolver refusal during speculative peel must remain typed and countable, withleft: 0,right: 2. A second mutation replaced the truthful evidence-unavailable diagnostic with fabricatedUnresolvedType: the union-total assertion passed at2, then the composition assertion went RED atcli_run.rs:34969:an unobserved marker census must remain a distinct typed refusal, withleft: 0,right: 2. Each mutation was restored by SHA-256 and byte comparison before its green rerun.Named emitted consequence:
Natfield realizationWalkPopulationBudgetRefusal.population_indexchanges from the authored alias spellingNatto its grounded Rust realizationi64. This is the evidence fix exposing an existing native-numeric decision, not a unit-variant decision:v1.compiler.coercion.numeric_realization_declaring_modulesenrollsdag/std/nat.dag, andrust_seed_host_numeric_aliastherefore realizes that declaration asi64. The generatedstd_nat.rsindependently declarespub type Nat = i64.At this exact head there is no
Measure<..., Nat>occurrence instd_realization_schedule.rs. The remainingNatspelling is the import pluscost_account_time_count's return. That return takes the function-signature path, whererust_fn_sig_preserves_authored_alias_leafexplicitly preservesNat; it does not consult the applied-type unit-variant census. The record field takesrender_rust_field_type_with_applied_bindingand the native-numeric realization authority. The spellings differ by a declared renderer policy but denote the same Rust type throughpub type Nat = i64; this PR newly changes only the field because the formerly empty renderer environment prevented that path from seeing the grounded declaration.The complete terminal emitted candidate crate was checked directly with
cargo check --releaseand succeeds. This is separate from the seed all-target build.