diff --git a/dag/gunbc/devboot/subject.dag b/dag/gunbc/devboot/subject.dag index 377b7ff57b1..7facbe5b3ee 100644 --- a/dag/gunbc/devboot/subject.dag +++ b/dag/gunbc/devboot/subject.dag @@ -514,7 +514,7 @@ fn build_environment_digest(environment: BuildEnvironmentSpec) -> Fnv1a64Structu // It is not reachable today: this repository's stores are SHA-1, so one family is in play and the collision has no way to occur. That is a fact about the current population, not about the carrier, and the repository is explicitly moving toward SHA-256 object format -- the moment both exist, an identity that ignores which one it is becomes wrong silently. // // The fix mirrors the ref token, which already prefixes its family for the same reason, so the two places that turn a hash into an identity string now agree instead of one quietly being weaker. Found by review, and the argument that convinced me is that the adjacent note already made the case -- the code simply did not do what its own reasoning said. -fn tree_oid_identity_atom(oid: GitObjectId) -> ContentHash { +fn tree_oid_identity_atom(oid: GitObjectId) -> Fnv1a64Structural { content_hash_combine_structural( left: content_hash_atom(value: git_object_format_identity_tag(format: git_object_id_format(oid: oid))), right: content_hash_atom(value: git_object_id_wire_hex(oid: oid)), diff --git a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag index d9acd2d48df..ed15091c39f 100644 --- a/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag @@ -7,7 +7,7 @@ import gunbc.compile_diagnostic_census { census_rows_of_class, census_total_count } -import std.types { String, Bool, Int } +import std.types { String, NonEmptyStr, List, Bool, Int } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } // SUBSTRATE-ONLY BY DELIBERATE CHOICE, AND THE SIBLING FILE EXPLAINS WHY IN ITS OWN VOICE. @@ -87,6 +87,64 @@ test fn w_undefined_name_at_the_direct_call_position_still_refuses() -> Bool { violation_count(source: undefined_name_arg_source, wanted: "InternalError") > 0 } +// THE TOP-LEVEL COLLECTION/NON-COLLECTION DISJOINTNESS ARM. Before this arm landed, a value +// already inferred as List bound to a NonEmptyStr parameter with no blocking diagnostic: +// the kernel mismatch arm only judges a kernel ACTUAL, while the nominal-product arm explicitly +// excludes containers. This is deliberately a variable rather than a list literal, so the +// fixture reaches application with the produced List type and cannot pass on the list-literal +// element judgment. A collection and a non-collection cannot be two representations of one +// value, so the shared declared_type_inhabitance relation can refuse this pair without a +// target-specific realization rule. +data list_value_at_non_empty_str_source: String = "module probe_inhabit_list_at_text\nimport std.types { Int, String, NonEmptyStr, List }\nfn takes_text(text: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int {\n let words: List = [\"forty\"]\n takes_text(text: words)\n}\n" + +test fn w_list_typed_value_at_non_empty_str_argument_is_refused() -> Bool { + violation_count(source: list_value_at_non_empty_str_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +data collection_disjointness_positive_source: String = "module probe_inhabit_list_text_ok\nimport std.types { Int, String, NonEmptyStr, List }\nfn takes_text(text: NonEmptyStr) -> Int { 1 }\nfn takes_words(words: List) -> Int { 1 }\nfn probe() -> Int {\n let words: List = [\"forty\"]\n takes_text(text: \"forty\" as NonEmptyStr) + takes_words(words: words)\n}\n" + +test fn w_collection_disjointness_keeps_conforming_arguments_admitted() -> Bool { + violation_count(source: collection_disjointness_positive_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +data record_value_at_scalar_source: String = "module probe_inhabit_record_at_scalar\nimport std.types { Int, String }\ntype Box { value: String }\nfn make_box() -> Box { Box { value: \"forty\" } }\nfn takes_text(text: String) -> Int { 1 }\nfn probe() -> Int { takes_text(text: make_box()) }\n" + +test fn w_record_typed_value_at_scalar_argument_is_counted_until_identity_is_grounded() -> Bool { + violation_count(source: record_value_at_scalar_source, wanted: "DeclaredTypeInhabitanceUndecided") > 0 + && violation_count(source: record_value_at_scalar_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +data coproduct_value_at_record_source: String = "module probe_inhabit_coproduct_at_record\nimport std.types { Int, String }\ntype Box { value: String }\ntype Choice = | ChoiceA { value: String } | ChoiceB\nfn make_choice() -> Choice { ChoiceA { value: \"forty\" } }\nfn takes_box(box: Box) -> Int { 1 }\nfn probe() -> Int { takes_box(box: make_choice()) }\n" + +test fn w_coproduct_typed_value_at_record_argument_is_refused() -> Bool { + violation_count(source: coproduct_value_at_record_source, wanted: "DeclaredTypeNotInhabited") > 0 +} + +data optional_value_at_required_source: String = "module probe_inhabit_optional_at_required\nimport std.types { Int, String }\nfn maybe_text() -> String? { none }\nfn takes_text(text: String) -> Int { 1 }\nfn probe() -> Int { takes_text(text: maybe_text()) }\n" + +test fn w_optional_value_at_required_binding_is_admitted_only_at_the_counted_boundary() -> Bool { + violation_count(source: optional_value_at_required_source, wanted: "DeclaredTypeInhabitanceUndecided") > 0 + && violation_count(source: optional_value_at_required_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// The syntax contrast that exposed the application hole. The cast seam already refused the same +// optional-to-required transition; keep that independently typed refusal beside the binding RED +// so neither seam can accidentally stand in as evidence for the other. +data optional_value_cast_to_required_source: String = "module probe_inhabit_optional_cast_required\nimport std.types { String }\nfn maybe_text() -> String? { none }\nfn probe() -> String { maybe_text() as String }\n" + +test fn w_optional_value_cast_to_required_is_independently_refused() -> Bool { + violation_count(source: optional_value_cast_to_required_source, wanted: "OptionalCastNotEliminated") > 0 +} + +// DECLARED COUNTED BOUNDARY. A generic formal has no instantiated type evidence at this seam, so +// this cut still admits it. Admission is not silence: the diagnostic census exposes one +// DeclaredTypeInhabitanceUndecided obligation to consumers on every execution of this fixture. +data generic_formal_counted_boundary_source: String = "module probe_inhabit_generic_boundary\nimport std.types { String }\nfn identity(value: T) -> T { value }\nfn probe() -> String { identity(value: \"forty\") }\n" + +test fn w_generic_formal_admission_is_visible_in_the_diagnostic_census() -> Bool { + violation_count(source: generic_formal_counted_boundary_source, wanted: "DeclaredTypeInhabitanceUndecided") > 0 +} + // THE LIST-ELEMENT GAP, AUTHORED AS A FIXTURE SO THE PRODUCTION SITE CAN BE REPAIRED. // dag/gunbc/heal_revalidation.dag passed List into check_coverage_admits's // required_gates: List -- the same mismatch as the argument beside it, one level diff --git a/docs/plans/compiler-guarantee-recovery-gap-analysis.md b/docs/plans/compiler-guarantee-recovery-gap-analysis.md index 051b4188e92..03758c9d00e 100644 --- a/docs/plans/compiler-guarantee-recovery-gap-analysis.md +++ b/docs/plans/compiler-guarantee-recovery-gap-analysis.md @@ -174,6 +174,10 @@ unless the row says otherwise, and `Unknown` is the honest default. | Direct-call argument TYPE conformance — **transparent-alias identity**, v2 corpus | **R2 built and approved for the alias-identity class (gunbc#8873 — OPEN, approved, mergeable as of 2026-08-22; NOT merged, and this row must not be read as landed until it is).** A precomputed transparent-alias identity relation, derived once at census build and consumed as a `String -> String` map lookup per comparison, admits two names that alias the same declaration and refuses everything else. It peels ONLY `type A = B` with zero params, no connective, no children, no properties and no type annotation, and a target with zero children/params/annotation and `return_cardinality == Required` — so brands, `sole_constructor` carriers, refinements, coproduct arms and applied generics are all excluded BY THE ADMISSION TEST rather than by a later filter. Cost bar was declared before implementation and measured after: four crossed A/B pairs, +2.0s on a 454s regen (+0.4%) against per-arm spreads of 29.9s and 40.9s — a measured null. **What it does NOT do is create substitutability: it makes an existing fact visible.** A pre-relation binary already accepts `CommitSha` at an `AttemptKey` formal and already refuses `IntKey` there | R2 for this class. R3 is not reachable at this seam and that is a property of the seam, not of the relation | **The residual population is a DIFFERENT class and the distinction is load-bearing.** Measured 2026-08-22 against the exemption-deleted corpus: 67 refusals, silent-badger-817's CI run 32562740527 at commit `d42bb3eb57c`. **Provenance caveat, stated because it changes what the 48 means:** that tree merged this relation at `9bfd5388c03`, TWO COMMITS behind head `c40ab2d8248`, and the intervening `b0f72158c80` ("Qualify alias targets at census-build time") is exactly the commit that decides the `CoreNode` group — those refusals turn on `Node` being ambiguous by BARE name. So the 67 is a measurement of an OLDER revision of this relation, not of a broken copy of it. Classification of those 67, derived from declarations and independent of any binary: 48 are this alias class; 8 are applied generics (row below); 11 are `Optional` against `String`/`Bool`/`Int` in `v2.extdeps.github.gha_fold_pilot_emit` and are NOT an alias class at all. **The 48-cleared half is verified on 5 specimens, not 48:** at head, with the exemption deleted in the mirror and `exempt=judged` on all 20352 ledger rows, the five comparisons that CI reports as errors in `00_compile.dag` (lines 319, 342, 408, 446, 497) are all present in the ledger and all read `Compatible`. The remaining 43 sit outside that entry's import closure and a whole-corpus re-run against head was in flight when this row landed — treat 48 as classified-and-partially-verified, never as measured. **Also NOT the alias class: the 11** — the diagnostic reads got `Primitive(String)`, so the optional marker is already gone upstream at pattern destructuring and no comparison-seam mechanism can reach them. That 11 was carried as alias residue by two independent sessions and by this lane's own framing; it is recorded here so it is not handed forward under a label that guarantees the next attempt fails. **Open question for whoever takes it, to be CHECKED rather than inherited from this row:** an optionality marker erased at destructuring means a value reaches a position whose declared type it does not inhabit, which is the same floor rule as the direct-call seam census (record-literal walled; data-initializer and list-element open). If Group C is a FIFTH seam of that class it belongs on that row and not on a new one — decide that before minting a class for it. **A second mechanism, `unanimity`, was designed, measured and ABANDONED as unsound, not deferred.** Its specimen and refutation are carried on the seam-split row above and are deliberately NOT restated here — one fact, one authority | gunbc#8873, 9 enrolled floor witnesses in `dag/test/claim/transparent_alias_identity_witness_test.dag` including the over-peel boundary (`IntHandle` at a `String` formal), a coproduct-projection climb, and a blast-radius pair whose Int-alias discriminator refuses. Shadow ledger re-run before the exemption was touched: 20527 rows, all 115 `WouldDiagnose` rows one mechanism. Receipt: `docs/probes/transparent_alias_identity_2026-08-22/README.md` — **FORWARD REFERENCE, NOT A PRESENT FACT:** that receipt lands with gunbc#8873, which is open at the time this row merges. Do not cite it as evidence until that PR is in | the `v2.` exemption arm cannot be deleted while the applied-generic class below still refuses 8 live sites; the exemption is NOT narrowed to those modules (a narrowing would be a shape test correlating with the distinction rather than naming it) | | Direct-call argument TYPE conformance — **applied-generic alias**, v2 corpus | **Below floor — 8 live false refusals, structurally unreachable from the comparison seam.** An alias whose right-hand side is a generic application (`type BlackConfigPatch = ConfigPatchRecord`) refuses at every call site passing it to the matching formal. Specimen, measured by execution 2026-08-22 on a fixture diffed byte-for-byte against the live `v2.std.patch` declaration, with the exemption deleted in the Rust MIRROR and `exempt=judged` on all 20352 ledger rows as the control: `formal_type = Primitive(ConfigPatchRecord)`, `actual_type = Node(BlackConfigPatch)`, `nominal=true container=false kernel=false`, `fname=ConfigPatchRecord aname=BlackConfigPatch`. Population: 9 declarations, all under `src/v2/extdeps/formatters/` (`black`, `clang_format`, `gofmt`, `google_java_format`, `ktfmt`, `lean4_format`, `prettier`, `rustfmt`, `swift_format`), of which 8 produced diagnostics in the CI arm — `lean4_format` is structurally identical and produced none in EITHER arm, so the population is 9 and the measured count is 8+k | R2, and it is decidable — the same equality already accepts the applied form when it is written directly at the formal | **THE FORMAL SIDE IS WHERE THE INFORMATION DIES, and that is the sentence that should stop the next attempt from this direction.** The formal is DECLARED `ConfigPatchRecord` and REACHES the comparison as the bare constructor, with the type argument already discarded. So the equality has one side that structurally cannot hold an argument, and the case split over any representative is EXHAUSTIVE: (a) representative = the applied form with every argument retained never equals the bare constructor, so it admits nothing and all 9 sites keep refusing; (b) representative = the bare constructor admits `ConfigPatchRecord` at `ConfigPatchRecord` for any X and Y, which is exactly the over-peel that erases the distinction. There is no third representative, and widening the carrier does not help — a node-valued map fails identically, because the missing information is not on the relation's side of the map. **Not to be confused with gunbc#8879**, the withdrawn repair that widened transparency AT RESOLVE and was refused by CI in three classes at once (20 direct-call comparisons, 18 variant projections, 3 files of regen drift). What that established is that resolve is the wrong place for a transparency JUDGMENT; preserving an applied form is resolve DISCARDING LESS, which hands the same consumers MORE structure, and is a different claim that has not been measured | executed fixture + shadow ledger with a positive control (`black.dag` must refuse; a zero there is decidably wrong). **NOT ENROLLED**: no probe pair asserts this class, so nothing reds if it changes. Three false zeros were produced while measuring it — twice from patching the `.dag` authority while the binary is built from the emitted Rust mirror, once from a run that PANICKED and reported zero diagnostics — each caught only by a positive control or by another session's raw per-line export, never by an aggregate | **RESOLVE CARRIES APPLIED FORMS AT THE FORMAL POSITION.** Explicitly NOT scoped as of 2026-08-22 (operator-lane ruling, swift-badger-524): a bounded floor-recovery lane whose completion condition has moved is closed honestly rather than extended, and nothing in that ruling says the change is wrong. Until it lands, the `v2.` exemption stays whole and gunbc#8886 stays blocked | | Direct-call argument TYPE conformance — **container element**, non-exempt module; and the witness family that reported it was **rung INFLATION** (DESIGN §4b(1) — *not* §4b(3): nothing regressed, the wall was never there, so "restore the previous behaviour" is not the remedy and a regression row would have read as authorising it) | **Below floor — the container-element judgment does not fire at a direct call argument.** Measured 2026-08-27 with the witness's OWN oracle (`compile_dag_rust_emit_check`) alongside `compile_dag_diagnostic_census`, over two corpora in two remote dispatches: `main` @ `ddb7f533e4e` and gunbc#9428's head. A fixture handing `FreeMonoid` to a declared `FreeMonoid` parameter — locally declared record, corpus-unique wrapper name, no `Node`, no `v2.std.node`, no occurrence identity anywhere in it — **compiles clean ON `main`**, 0 blocking; the argument surfaces only as advisory `DeclaredTypeInhabitanceUndecided` at "direct call argument". Distinct from the `module_skips_direct_call_arg_check` row above: that exemption keys on the CALLER's module name and this fixture's module is not `v2.`-prefixed, so the judgment is not switched off here — it is written, reached, and answers no. **THE INFLATION:** the class read as mechanically preventable on the strength of `test.claim.record_literal_call_arg_handoff_witness.record_literal_container_element_mismatch_at_call_arg_still_refuses` being green. That witness was green on an UNRELATED defect in its own closure — `v2.std.node` referenced `std.occurrence_identity.OccurrenceId` and `ScopedOccurrenceRef` fully qualified WITHOUT importing that module, so every closure importing `v2.std.node` inherited two `UnresolvedType` diagnostics and refused for that reason; measured on `main`, the fixture's refusal is exactly `UnresolvedType/std.occurrence_identity.OccurrenceId` ×2 + `ScopedOccurrenceRef` ×1, and contains no type-mismatch diagnostic at all. gunbc#9428 adds the import, those resolve, and the accidental refusal goes with them. **A witness green on a defect in its own closure is not weak coverage, it is NEGATIVE coverage** — it is cited as evidence the wall is live, so the class never ranks for climbing. That is DESIGN §4b's worse-than-absent case reached from a direction the document does not yet record: not an unauthorable RED, but an AUTHORABLE one satisfied by the WRONG CAUSE, which no reader of the witness can distinguish from the right one. The nominal sibling `record_literal_nominal_mismatch_at_call_arg_still_refuses` stays green through a DIFFERENT path (`literal_introduction_type_mismatch`, whose actual is a record LITERAL rather than a call), which is why the family read as coherent and was not | R2 (two distinct nominal element types under one container template is a decidable comparison the seam already reaches) | `container_element_nominal_brand_mismatch` is written and IS reached from `direct_call_arg_type_mismatch`, but it delegates to `nominal_call_arg_brand_mismatch`, which requires `structural_carrier_template_name(formal_el) == structural_carrier_template_name(actual_el)`; that name falls through `canonical_template_name` to the element's own authored name for any non-container type, so two DISTINCT nominal element types can never satisfy the conjunct that the mismatch arm needs. **Stated as a CODE READ, consistent with the measurement but not independently executed** — what is executed is that the compile is clean, not which conjunct declined | Measurement above (both corpora, `emit_check` + census). **Instrument not committed:** a throwaway cargo example over the two `pub` entry points in `cli_run`, kept out of the tree per the no-ad-hoc-script rule; re-deriving it needs a `.dag` entry point, which is this row's standing "name the instrument" debt | `container_element_nominal_brand_mismatch` reaching the direct-call-argument position — i.e. `nominal_call_arg_brand_mismatch` admitting distinct nominal element types under a shared container template. The witness is the ready-made RED and needs no new fixture; it is enrolled as expected-red in gunbc#9428, where it FAILS (on `main` it still passes on the accident, so enrolling it here would trip the roster's stale-quarantine arm and red main's own floor) | +| Direct-call declared-type inhabitance — decidable outer-shape disjointness | **Class rung remains below floor (the minimum across all rows); two measured arms rise to R2.** INVALID STATE: an application binds a `List` value to `NonEmptyStr` or a coproduct value to a record. HARM: the live fabric specimen passed `List` to `content_hash_of_value(value: NonEmptyStr)` and failed only inside `atom_identity_hash` at runtime. DISTINGUISHING FACTS: `build_call_application_plan` already builds an obligation for every non-callable formal, so the seam was not bypassed; the relation ran but could not decide these shapes. This change makes the two arms blocking R2 refusals, located at the application and naming the parameter, declared type, and supplied type. The rows below still admit, so the general property is not claimed enforced. | **Per-arm:** R2 for List→scalar and coproduct→record. **Class ceiling:** R2 after every boundary population is grounded; R3 requires normalized application IR whose binding edge cannot carry a non-inhabitant. | Other shapes remain in separately counted rows below; their admitting path fixes the class minimum below floor. | Binding REDs plus a conforming control in `test.claim.declared_type_inhabitance_direct_call_witness`. Production incident: `gunbc.instruments.fabric_control_plane_live_probe` `fci1_cell_observation_wire` calling `std.content_hash.content_hash_of_value`. | Retire each separately-triggered row below; only then may the class rise from its minimum below-floor rung. | +| Direct-call generic-formal inhabitance | **Declared counted boundary; class path admits.** The formal still contains a type variable and the binding edge carries no instantiated substitution proof, so asserting either inhabitance answer here would fabricate it. | R2 when instantiated substitution proof reaches the obligation; R3 when normalized application IR makes the proof intrinsic | This may be genuinely undecidable at the present seam, unlike the two wall-after-grounding rows below. | `compile_dag_diagnostic_census` counts `DeclaredTypeInhabitanceUndecided`; `test.claim.declared_type_inhabitance_direct_call_witness` executes a generic-formal fixture. The whole `dag` + `src/v2` population and per-reason counts are re-derived by `claim_executor --required-regen --source-root dag --source-root src/v2` with the undecided class temporarily blocking. | Carry the instantiated generic substitution proof to every binding obligation, then decide and retire `UndecidableGenericFormal`. | +| Direct-call record→scalar inhabitance with erased declaration identity | **Below floor on binding; counted rather than silent in this change.** INVALID STATE: a nominal record reaches a scalar parameter. HARM: the record can fail only inside a scalar primitive. DISTINGUISHING FACTS: the binding edge exposes `Product(name)` but not a reliable declaration identity; the aggravating fact is that `dag/std/types.FilePath` is a String refinement while `v2.extdeps.file_system.FilePath` is an unrelated record. Namespacing makes both legal, and bare-head lookup cannot distinguish them. A blocking arm exposed compiler-source sites whose actual identity cannot be recovered here. This change classifies the shape as `UndecidableProducedIdentityErased`, making its admission visible without inventing either answer. | R2 once the edge carries fully-qualified declaration identity; R3 when normalized IR makes that identity intrinsic | A spelling check or `FilePath` exemption would guess across the known homonym fork. | `test.claim.declared_type_inhabitance_direct_call_witness` counts the boundary. `claim_executor --required-regen --source-root dag --source-root src/v2` with undecided diagnostics temporarily blocking ranges over the whole named source-root population and re-derives the compiler-source occurrences; the row does not claim that compiler source is the universe. | Carry fully-qualified produced declaration identity through inference and application planning; then decide record→scalar from the exact type-head census and make the refusal blocking. | +| Direct-call Optional→required inhabitance after a nonempty-list guard | **Below floor on binding; R2 on cast; class rung is the binding-path minimum.** INVALID STATE: an `Optional` reaches a required `T` parameter without elimination. HARM: absence can cross the call boundary and fail only at use. DISTINGUISHING FACTS: the cast path blocks the shape as `OptionalCastNotEliminated`, while the binding path emits non-blocking `DeclaredTypeInhabitanceUndecided` and admits it. Making the binding verdict blocking exposed corpus sites that call `List.first()` only after `count()`/`length()` proves nonempty: those sites depend on a real nonempty-list fact that is present in author control flow but absent from the model. This is a wall after grounding, not a permanently undecidable boundary. | R2 when nonempty-list flow evidence grounds `first()` as `T`; R3 requires the normalized binding edge to make an uneliminated optional unwritable | Blocking immediately would correctly reject what the model cannot prove but would also reject every guarded `first()` use; hand-writing Present/Absent at each site is repeated mitigation and does not model the fact for the next site. | `test.claim.declared_type_inhabitance_direct_call_witness` executes both answers separately: binding is admitted and counted as `DeclaredTypeInhabitanceUndecided`; the same shape through cast blocks as `OptionalCastNotEliminated`. The corpus population is re-derived by `claim_executor --required-regen --source-root dag --source-root src/v2` with the undecided class temporarily blocking; no stale numeric count is stored here. | Model a nonempty-list fact in control flow so `first()` on a proven-nonempty list yields `T` rather than `T?`; then make Optional→required binding a blocking refusal with no site exemption. | | Producer/consumer cardinality | **UnknownUnmeasured** (typed-rejection vs silent-degeneration split unmeasured) | R3 (seam unwritable) | forgeable carrier; no signature propagation (`sole_constructor` audit pending) | §4b | Stage-3 vertical slice | | Refinement predicate (`where`) enforcement at construction | **Writable-and-unverified, one row spanning both measured SOURCE-FORM paths (declared subject grain — reconstruction is NOT in this row's grain; see the scope note at the end of this cell).** Source→v1-interpretation and source→v1-Rust-emission were independently measured and found identical — zero predicate/refinement check on either, no scope split between them. `v1_interpreter` `cast_identity_result` (the `as`-cast identity path) checks only that the underlying kernel name matches; it carries no refinement/predicate concept at all. `05_emit_rust` `render_rust_alias_rhs_type` peels a refinement node to its base type before emission (`is_where_refinement_type` true branch) and discards the predicate list — a **deliberate written branch**, not incidental loss: `04_infer`'s `is_where_refinement_type`/`where_refinement_chain`/`peel_where_refinement_base` carry the predicate live through typecheck, so the data exists at the emit boundary and is thrown away there. Where safety exists today for a refined type (e.g. `PathSegment = NonEmptyStr where brand("PathSegment")`) it comes **entirely from hand-authored per-callsite guards**, not the carrier — `gunbc.merge_admission_subject` `walk_attempt_id` and `gunbc.fleet_known_hosts_anchor` `fleet_ssh_attempt_identity` (mirrored in `claim_executor.rs`) each call `path_segment_is_safe` before casting. This is DESIGN §5's named tell, validation standing where construction was available: the law is declared once (`path_segment_safety_note`) and re-stated as a check every author must remember to write, never tied to the carrier itself. One construction form already bypasses even that discipline: `FilePathParts { segments: [...] }` struct literals (`extdeps.rust.cargo` `cargo_target_source_path`/`rust_module_candidate_paths`, `extdeps.linux.proc_self_cgroup`) coerce raw strings to `PathSegment` with no predicate call at all. A targeted search for an *existing* production site where a refined-type construction actually feeds a predicate-violating value through to a consumer (not manufactured) found none: the two real branded-`PathSegment` callers both guard, and the one `FilePathParts` caller with non-literal input has zero production callers (test-fixture only). A below-floor ("silent wrongness, demonstrated") claim was raised on this evidence and explicitly withdrawn — the class is confirmed writable and the one candidate gap is confirmed currently unexercised, not confirmed violated. **SCOPE NOTE, AND IT IS LOAD-BEARING: that withdrawal is scoped to the two SOURCE-FORM paths this row measures, and it has since been overtaken on a third path that this row does not cover.** The reconstruction seam — `recorded_fixture` `value_from_fixture_json` on replay, and `map_response_to_value_json` on live REST — builds runtime records and scalars from external JSON without passing through a source record literal or cast, so neither `cast_identity_result` nor `render_rust_alias_rhs_type` is on it and neither measurement above reaches it. On THAT path below-floor is not a withdrawn hypothesis but an EXECUTED demonstration: a predicate-violating value was silently accepted and consumed, and on the live-REST arm with no tampering of any kind. **The grain of that demonstration, stated so this cell cannot be read as more than it is:** it was executed against a PURPOSE-BUILT probe service, not against a production caller. What is established is that the MECHANISM silently admits and consumes violating values on an untampered path; what is NOT established is that any production field has actually received one. The production population sitting on that path is measured only as a declaration count (output-block fields typed as a refined alias), and none of those was executed — so read it as mechanism-demonstrated, population-unmeasured, never as demonstrated-in-production. It is intended to be carried as its own row rather than folded into this one, per §4b's one-row-per-structurally-distinct-path rule. **FORWARD REFERENCE, NOT A PRESENT FACT:** that row is authored in a separate in-flight change (gunbc#8658, reconstruction doors, findings-only) and is NOT part of this document as of this cell's landing. If this row merges first, the reconstruction row is pending rather than present, and this sentence is a statement of intent — do not cite it as evidence that the reconstruction path is documented, and do not let the absence of that row be read as the path having been cleared. **Do not read this cell as the class verdict**: per §4b a class's rung is the MINIMUM across its in-scope paths, so if the enclosing class is taken as "refinement enforcement at construction" — reconstruction being a construction path — the governing rung is the reconstruction row's, not this one's. Citing this row's writable-and-unverified while that path stayed silent is exactly the inflation §4b names | R2-shaped on the Rust target (newtype + validating constructor closes construction-time) | Bounded by what the **target** can express, not by what `.dag` knows: `.dag`'s own infer stage already carries the predicate live through typecheck, so the ceiling here is a target-capability question — the bare-alias Rust realization used today has no ceiling above writable-and-unverified regardless of source-side modeling quality; nothing on either measured path ties the declared law to the carrier, so enforcement is 100% per-callsite discipline, which has a zero-frequency-until-violated failure mode (the `FilePathParts` gap is exactly this: zero frequency because it has no caller yet, not because it is guarded) | node://adhoc-897a90b6-a9c items 1–2, 2026-08-20 (merry-tern-237/fierce-ant-91): 219 `where`-declared types found in `.dag` (`grep -rn '^type .* where ' dag/`), 49 confirmed reaching Rust as bare aliases with zero predicate residue (spot-checked `std_types.rs`); emission mechanism confirmed by reading `05_emit_rust` `render_rust_alias_rhs_type` against `04_infer` `is_where_refinement_type`; interpreter path confirmed by reading `v1_interpreter` `cast_identity_result`/`eval_cast`; violation search executed against `PathSegment` construction sites corpus-wide, empty result | a Rust-target realization for refined types (newtype + validating constructor, or equivalent) that ties the declared predicate to the emitted carrier once, replacing per-callsite discipline; the `sole_constructor` completeness audit (in flight, separate lane) is the adjacent unforgeable-construction mechanism this would likely compose with | | Duplicate top-level declaration in ONE module | **Was BELOW FLOOR — silent, with LIVE exposure; wall landed in this change.** INVALID STATE: one module declaring one name twice. HARM: `v1.compiler.env` `symbol_index_insert` is a `map_insert` on the qualified name, so the second declaration REPLACED the first and every reference bound the last one written, with no diagnostic of any severity. MEASURED BY EXECUTION through our own binary before the wall: `fn probe_dup() -> Int { 1 }` then `fn probe_dup() -> Int { 2 }` ran the caller to `2`; the single-definition control ran to `1`; same harness, duplication the only variable. The collision is NOT fn/fn only — a `data` and a `fn` of one name share the key, and a bare reference to the data yielded ``. DISTINGUISHING FACT vs the census-ambiguous last-import-wins row above: that one is ACROSS modules, this one is INSIDE one, so it needs no corpus walk and no import resolution — it is decidable from one module's own item list. LIVE EXPOSURE, denominator stated: a scan of 4163 authored `.dag` files found 2 modules carrying it — `dag/gunbc/systemctl_list_units.dag` (`data systemctl_list_units_all_states` shadowed by `fn systemctl_list_units_all_states`, so the ListUnits `state:` argument bound the FUNCTION, not the `"active,inactive,failed"` string) and `dag/test/claim/spark_managed_grant_reconcile_witness_test.dag` (one `data` row declared twice with an identical value). Both are repaired in this change; the deletion IS the census. THE BOUND THAT MATTERS MOST is not the compiler's: where the two definitions are semantically EQUIVALENT no behavioural witness can discriminate them whichever wins, so green-by-execution — which this repository leans on everywhere — is STRUCTURALLY blind to duplicate authorship. That is why the evidence is a compile-seam refusal and not a runtime probe. | R2 (mechanically preventable) reached; R4 (unwritable) is the honest ceiling only once ingestion carries a keyed declaration roster that cannot hold two entries for one name | the refusal is a fold over the module's item list in `v1.compiler.resolve` `check_duplicate_declarations`, not a property of the carrier: the duplicate is still AUTHORABLE and is refused after it is built | wall: `v1.compiler.resolve` `check_duplicate_declarations` emitting `DuplicateDeclaration` (blocking, default arm of `is_interpreter_blocking_diagnostic`). RED + positive control: `duplicate_declaration_wall_witness` in `v1.compiler.compiler_tests_rust`, authored at the FIXTURE boundary (two REDs — fn/fn and data/fn — and a green control on distinct names). ENROLMENT, stated rather than inherited: the Rust suite was removed from CI 2026-07-11, so that witness executes LOCALLY only and guards nothing on a push; `dag/test/claim/duplicate_definition_binding_probe_test.dag` asserts the same refusal in `.dag` and is `ReadsLiveTree`, hence `DeclinedLiveTree` in the required floor — discovered, counted, never run. So the wall is real and its EVIDENCE is unenrolled, which is a weaker claim than R2-with-a-guard and is written that way deliberately | next trigger, two and separable: (a) an enrolled route for a compiler FIXTURE red — either the `DeclinedLiveTree` arm's deletion (which `v2.workflow.required_floor` already carries as staged) flipping the `.dag` probe into the floor, or a hermetic census that does not walk the live tree; (b) for the R4 climb, an ingestion-time keyed declaration roster (`v1_compiler.declaration_index` is the nearest existing construction) | diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index a7da42b7336..f59b588f90b 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -13,7 +13,8 @@ import std.coercion { dag_can_cast, is_dag_cast_domain_type } import v1.compiler.type_head_exposure { TypeHeadView, KernelScalarHead, ApplicationHead, ProductHead, CoproductHead, CallableHead, TypeHeadExposure, ExposedTypeHead, OpaqueTypeHead, StuckTypeHead, MalformedApplicationHead, - type_declaration_identity_key + type_declaration_identity_key, + type_head_exposure_is_kernel_scalar, type_head_exposure_is_product, type_head_exposure_is_coproduct } import v1.std.core { Node, InternTable, @@ -2594,6 +2595,7 @@ type DeclaredTypePosition type DeclaredTypeObligation { position: DeclaredTypePosition + subject: String declared: Node produced: Node span: SourceSpan @@ -2621,7 +2623,7 @@ type InhabitanceVerdict | InhabitanceRefused { reason: InhabitanceRefusalReason } | InhabitanceUndecidable { reason: InhabitanceUndecidableReason } -fn declared_type_position_label(position: DeclaredTypePosition) -> String { +fn declared_type_position_label(position: DeclaredTypePosition, subject: String) -> String { match position { PositionRecordLiteralField => "record literal field" PositionListElement => "list element" @@ -2634,7 +2636,9 @@ fn declared_type_position_label(position: DeclaredTypePosition) -> String { PositionCastTarget => "cast target" PositionParameterDefault => "parameter default" PositionCallableReturn => "callable return" - PositionDirectCallArgument => "direct call argument" + PositionDirectCallArgument => + if subject == "" { "direct call argument" } + else { concat("direct call argument for parameter '", subject, "'") } } } @@ -2661,6 +2665,12 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco } else if declared_realizes_as_kernel_numeric( declared: declared, produced: produced, source_indices: source_indices) { Inhabits + } else if collection_at_scalar_declared_type(declared: declared, produced: produced, scope: scope) { + InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if record_at_scalar_needs_identity(declared: declared, produced: produced, scope: scope) { + InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if coproduct_at_record_declared_type(declared: declared, produced: produced, scope: scope) { + InhabitanceRefused { reason: RefusedKernelAtStructured } } else if kernel_value_declared_type_mismatch( formal: declared, actual: produced, type_env: scope.type_env, source_indices: source_indices) { @@ -2675,6 +2685,53 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco } } +// Collection spelling has a measured representation gap: FreeMonoid can arrive as List, +// so collection-vs-noncollection is not itself a proof of disjointness. Peel the declared side +// through the existing nominal-alias authority and refuse only when that established base is a +// kernel scalar. This catches List<_> at NonEmptyStr (whose base is String) without treating an +// algebraic collection spelling as a scalar merely because its outer node is not List. +fn collection_at_scalar_declared_type(declared: Node, produced: Node, scope: InferScope) -> Bool { + if node_is_collection(n: produced, source_indices: scope.type_env.source_indices) == false { + false + } else { + let peeled = peel_nominal_alias_identity(n: declared, env: scope.type_env, module_name: scope.module_name) + let peeled_is_kernel = is_kernel_type(name: authored_name_at(source_indices: scope.type_env.source_indices, node: peeled)) + let refinement_base_is_kernel = if is_where_refinement_type(ty: declared) { + match declared.children |> first { + Present { value: base } => + is_kernel_type(name: authored_name_at(source_indices: scope.type_env.source_indices, node: child_type_node(ch: base))) + Absent => false + } + } else { false } + peeled_is_kernel || refinement_base_is_kernel + } +} + +fn record_at_scalar_needs_identity(declared: Node, produced: Node, scope: InferScope) -> Bool { + type_head_exposure_is_kernel_scalar(exposure: expected_type_head_exposure(formal: declared, scope: scope)) + && type_head_exposure_is_product(exposure: expected_type_head_exposure(formal: produced, scope: scope)) +} + +// Product-vs-coproduct is settled from exact type-head census identities. A second bare-name +// declaration lookup can select a homonym and fabricate a refusal, so it is not an authority here. +fn coproduct_at_record_declared_type(declared: Node, produced: Node, scope: InferScope) -> Bool { + let declared_name = authored_name_at(source_indices: scope.type_env.source_indices, node: declared) + let produced_name = authored_name_at(source_indices: scope.type_env.source_indices, node: produced) + let declared_head = expected_type_head_exposure(formal: declared, scope: scope) + let produced_head = expected_type_head_exposure(formal: produced, scope: scope) + if application_type_names_compatible( + formal_name: declared_name, lit_name: produced_name, + type_env: scope.type_env, module_name: scope.module_name, + source_indices: scope.type_env.source_indices) + || transparent_alias_identity_agrees( + index: scope.type_env.symbol_index, left: declared_name, right: produced_name) { + false + } else { + type_head_exposure_is_product(exposure: declared_head) + && type_head_exposure_is_coproduct(exposure: produced_head) + } +} + // The obligation carries its own position, so ONE emitter locates every refusal. A per-position // diagnostic function would be the N-representation problem moved one layer down. // WHY A KERNEL LITERAL AT AN ALGEBRAICALLY-DECLARED NUMERIC IS ADMITTED, AND WHY THIS IS @@ -3006,7 +3063,7 @@ fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: Inf InhabitanceUndecidable { reason: r } => [make_error_node( diagnostic: DeclaredTypeInhabitanceUndecided { - position: declared_type_position_label(position: obligation.position), + position: declared_type_position_label(position: obligation.position, subject: obligation.subject), reason: inhabitance_undecidable_reason_label(reason: r), span: obligation.span }, @@ -3015,7 +3072,7 @@ fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: Inf InhabitanceRefused { reason: _ } => [make_error_node( diagnostic: DeclaredTypeNotInhabited { - position: declared_type_position_label(position: obligation.position), + position: declared_type_position_label(position: obligation.position, subject: obligation.subject), expected: node_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), got: node_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), span: obligation.span @@ -3395,6 +3452,7 @@ fn direct_call_argument_inhabitance_diags( declared_type_obligation_diags( obligation: DeclaredTypeObligation { position: PositionDirectCallArgument, + subject: app.param_name, declared: app.formal_subst, produced: resolved_type(n: actual_expr), span: actual_expr.span @@ -5711,6 +5769,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu declared_type_obligation_diags( obligation: DeclaredTypeObligation { position: PositionListElement, + subject: "", declared: declared_elem, produced: resolved_type(n: te), span: te.span diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 99b310179bc..b0d7887e2c7 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -173,13 +173,16 @@ pub use crate::v1_compiler_infer_types::{ template_return_is_receiver_self, }; pub use crate::v1_compiler_resolve::{ModuleGraph, ResolvedImport, ResolvedModule}; -pub use crate::v1_compiler_type_head_exposure::type_declaration_identity_key; use crate::v1_compiler_type_head_exposure::TypeHeadExposure::{ ExposedTypeHead, MalformedApplicationHead, OpaqueTypeHead, StuckTypeHead, }; use crate::v1_compiler_type_head_exposure::TypeHeadView::{ ApplicationHead, CallableHead, CoproductHead, KernelScalarHead, ProductHead, }; +pub use crate::v1_compiler_type_head_exposure::{ + type_declaration_identity_key, type_head_exposure_is_coproduct, + type_head_exposure_is_kernel_scalar, type_head_exposure_is_product, +}; pub use crate::v1_compiler_type_head_exposure::{TypeHeadExposure, TypeHeadView}; use crate::v1_rt; use crate::v1_rt::{VecCompat, VecJoin}; @@ -3672,6 +3675,7 @@ pub enum DeclaredTypePosition { #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] pub struct DeclaredTypeObligation { pub position: DeclaredTypePosition, + pub subject: String, pub declared: Rc, pub produced: Rc, pub span: Rc, @@ -3711,7 +3715,7 @@ pub enum InhabitanceVerdict { }, } -pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { +pub fn declared_type_position_label(position: DeclaredTypePosition, subject: String) -> String { match position.clone() { DeclaredTypePosition::PositionRecordLiteralField => "record literal field".to_string(), DeclaredTypePosition::PositionListElement => "list element".to_string(), @@ -3724,7 +3728,19 @@ pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { DeclaredTypePosition::PositionCastTarget => "cast target".to_string(), DeclaredTypePosition::PositionParameterDefault => "parameter default".to_string(), DeclaredTypePosition::PositionCallableReturn => "callable return".to_string(), - DeclaredTypePosition::PositionDirectCallArgument => "direct call argument".to_string(), + DeclaredTypePosition::PositionDirectCallArgument => { + if (subject.clone() == "".to_string()) { + "direct call argument".to_string() + } else { + v1_rt::concat( + v1_rt::concat( + "direct call argument for parameter '".to_string(), + subject.clone(), + ), + "'".to_string(), + ) + } + } } } @@ -3770,36 +3786,67 @@ pub fn declared_type_inhabitance( ) { Rc::new(InhabitanceVerdict::Inhabits) } else { - if kernel_value_declared_type_mismatch( + if collection_at_scalar_declared_type( declared.clone(), produced.clone(), - scope.type_env.clone(), - source_indices.clone(), + scope.clone(), ) { Rc::new(InhabitanceVerdict::InhabitanceRefused { reason: InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - if coproduct_payload_where_parent_required( + if record_at_scalar_needs_identity( declared.clone(), produced.clone(), scope.clone(), ) { - Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: InhabitanceRefusalReason::RefusedPayloadAtParent, - }) + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, +}) } else { - match nominal_product_inhabitance_refusal( + if coproduct_at_record_declared_type( declared.clone(), produced.clone(), scope.clone(), ) { - Some(r) => { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: + InhabitanceRefusalReason::RefusedKernelAtStructured, + }) + } else { + if kernel_value_declared_type_mismatch( + declared.clone(), + produced.clone(), + scope.type_env.clone(), + source_indices.clone(), + ) { Rc::new(InhabitanceVerdict::InhabitanceRefused { - reason: r.clone(), - }) + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, +}) + } else { + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, +}) + } else { + match nominal_product_inhabitance_refusal( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Some(r) => Rc::new( + InhabitanceVerdict::InhabitanceRefused { + reason: r.clone(), + }, + ), + None => Rc::new(InhabitanceVerdict::Inhabits), + } + } } - None => Rc::new(InhabitanceVerdict::Inhabits), } } } @@ -3811,6 +3858,97 @@ pub fn declared_type_inhabitance( } } +pub fn collection_at_scalar_declared_type( + declared: Rc, + produced: Rc, + scope: Rc, +) -> bool { + if (crate::v1_compiler_infer_types::node_is_collection( + produced.clone(), + scope.type_env.clone().source_indices.clone(), + ) == false) + { + false + } else { + { + let peeled = crate::v1_compiler_infer_resolve::peel_nominal_alias_identity( + declared.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + ); + let peeled_is_kernel = + crate::std_types::is_kernel_type(crate::v1_std_core::authored_name_at( + scope.type_env.clone().source_indices.clone(), + peeled.clone(), + )); + let refinement_base_is_kernel = if is_where_refinement_type(declared.clone()) { + match declared.children.clone().first().cloned() { + Some(base) => { + crate::std_types::is_kernel_type(crate::v1_std_core::authored_name_at( + scope.type_env.clone().source_indices.clone(), + crate::v1_compiler_infer_types::child_type_node(base.clone()), + )) + } + None => false, + } + } else { + false + }; + (peeled_is_kernel.clone() || refinement_base_is_kernel.clone()) + } + } +} + +pub fn record_at_scalar_needs_identity( + declared: Rc, + produced: Rc, + scope: Rc, +) -> bool { + (crate::v1_compiler_type_head_exposure::type_head_exposure_is_kernel_scalar( + expected_type_head_exposure(declared.clone(), scope.clone()), + ) && crate::v1_compiler_type_head_exposure::type_head_exposure_is_product( + expected_type_head_exposure(produced.clone(), scope.clone()), + )) +} + +pub fn coproduct_at_record_declared_type( + declared: Rc, + produced: Rc, + scope: Rc, +) -> bool { + { + let declared_name = crate::v1_std_core::authored_name_at( + scope.type_env.clone().source_indices.clone(), + declared.clone(), + ); + let produced_name = crate::v1_std_core::authored_name_at( + scope.type_env.clone().source_indices.clone(), + produced.clone(), + ); + let declared_head = expected_type_head_exposure(declared.clone(), scope.clone()); + let produced_head = expected_type_head_exposure(produced.clone(), scope.clone()); + if (application_type_names_compatible( + declared_name.clone(), + produced_name.clone(), + scope.type_env.clone(), + scope.module_name.clone(), + scope.type_env.clone().source_indices.clone(), + ) || transparent_alias_identity_agrees( + scope.type_env.clone().symbol_index.clone(), + declared_name.clone(), + produced_name.clone(), + )) { + false + } else { + (crate::v1_compiler_type_head_exposure::type_head_exposure_is_product( + declared_head.clone(), + ) && crate::v1_compiler_type_head_exposure::type_head_exposure_is_coproduct( + produced_head.clone(), + )) + } + } +} + pub fn declared_realizes_as_kernel_numeric( declared: Rc, produced: Rc, @@ -4110,7 +4248,10 @@ pub fn declared_type_obligation_diags( InhabitanceVerdict::InhabitanceUndecidable { reason: r, .. } => { Rc::new(vec![crate::v1_std_core::make_error_node( Rc::new(CompilerDiagnostic::DeclaredTypeInhabitanceUndecided { - position: declared_type_position_label(obligation.position.clone()), + position: declared_type_position_label( + obligation.position.clone(), + obligation.subject.clone(), + ), reason: inhabitance_undecidable_reason_label(r.clone()), span: obligation.span.clone(), }), @@ -4120,7 +4261,10 @@ pub fn declared_type_obligation_diags( InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => { Rc::new(vec![crate::v1_std_core::make_error_node( Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { - position: declared_type_position_label(obligation.position.clone()), + position: declared_type_position_label( + obligation.position.clone(), + obligation.subject.clone(), + ), expected: crate::v1_compiler_infer_types::node_type_shape( obligation.declared.clone(), scope.type_env.clone().source_indices.clone(), @@ -4890,6 +5034,7 @@ pub fn direct_call_argument_inhabitance_diags( declared_type_obligation_diags( Rc::new(DeclaredTypeObligation { position: DeclaredTypePosition::PositionDirectCallArgument, + subject: app.param_name.clone(), declared: app.formal_subst.clone(), produced: crate::v1_compiler_infer_types::resolved_type( actual_expr.clone(), @@ -9519,6 +9664,7 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), (*declared_type_obligation_diags( Rc::new(DeclaredTypeObligation { position: DeclaredTypePosition::PositionListElement, + subject: "".to_string(), declared: declared_elem.clone(), produced: crate::v1_compiler_infer_types::resolved_type( te.clone(), diff --git a/src/v1/stage0/src/v1_compiler_type_head_exposure.rs b/src/v1/stage0/src/v1_compiler_type_head_exposure.rs index c7ec1ee5c29..f6921291d03 100644 --- a/src/v1/stage0/src/v1_compiler_type_head_exposure.rs +++ b/src/v1/stage0/src/v1_compiler_type_head_exposure.rs @@ -46,3 +46,54 @@ pub fn type_declaration_identity_key(decl_file: String, declared_name: String) - declared_name.clone(), ) } + +pub fn type_head_exposure_is_kernel_scalar(exposure: Rc) -> bool { + match (*exposure.clone()).clone() { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::KernelScalarHead { .. }) => + { + let TypeHeadView::KernelScalarHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + true + } + _ => false, + } +} + +pub fn type_head_exposure_is_product(exposure: Rc) -> bool { + match (*exposure.clone()).clone() { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::ProductHead { .. }) => + { + let TypeHeadView::ProductHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + true + } + _ => false, + } +} + +pub fn type_head_exposure_is_coproduct(exposure: Rc) -> bool { + match (*exposure.clone()).clone() { + TypeHeadExposure::ExposedTypeHead { ref view, .. } + if matches!(view.as_ref(), TypeHeadView::CoproductHead { .. }) => + { + let TypeHeadView::CoproductHead { + type_identity: _, .. + } = view.as_ref() + else { + unreachable!() + }; + true + } + _ => false, + } +} diff --git a/src/v1/type_head_exposure.dag b/src/v1/type_head_exposure.dag index 405c63dbeb2..fdb428fa516 100644 --- a/src/v1/type_head_exposure.dag +++ b/src/v1/type_head_exposure.dag @@ -23,3 +23,24 @@ type TypeHeadExposure fn type_declaration_identity_key(decl_file: String, declared_name: String) -> String { concat(decl_file, "::", declared_name) } + +fn type_head_exposure_is_kernel_scalar(exposure: TypeHeadExposure) -> Bool { + match exposure { + ExposedTypeHead { view: KernelScalarHead { type_identity: _ } } => true + _ => false + } +} + +fn type_head_exposure_is_product(exposure: TypeHeadExposure) -> Bool { + match exposure { + ExposedTypeHead { view: ProductHead { type_identity: _ } } => true + _ => false + } +} + +fn type_head_exposure_is_coproduct(exposure: TypeHeadExposure) -> Bool { + match exposure { + ExposedTypeHead { view: CoproductHead { type_identity: _ } } => true + _ => false + } +} diff --git a/src/v2/test/claim/interface_summary/typed_module_key_test.dag b/src/v2/test/claim/interface_summary/typed_module_key_test.dag index a4e46e782c1..2283ae54c13 100644 --- a/src/v2/test/claim/interface_summary/typed_module_key_test.dag +++ b/src/v2/test/claim/interface_summary/typed_module_key_test.dag @@ -7,9 +7,8 @@ import std.interface_summary { typed_module_key, interface_summary_rollup } -import std.content_hash { content_hash_atom } +import std.content_hash { Fnv1a64Structural, content_hash_atom } import std.types { NonEmptyStr } -import std.content_hash { ContentHash } import v2.std.logic { Bool } data purpose_note: NonEmptyStr = "RED controls proving each term of typed_module_key is load-bearing: vary compiler_identity alone -> key changes; vary interface_key alone -> key changes; drop neither -> extends the interface key. Synthetic inputs only; no store, no live tree." @@ -32,11 +31,11 @@ fn interface_key_b() -> ModuleKey { ) } -fn compiler_id_x() -> ContentHash { +fn compiler_id_x() -> Fnv1a64Structural { content_hash_atom(value: "compiler-identity-x") } -fn compiler_id_y() -> ContentHash { +fn compiler_id_y() -> Fnv1a64Structural { content_hash_atom(value: "compiler-identity-y") }