diff --git a/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag new file mode 100644 index 00000000000..7cb15ea3fa5 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/lookup_miss_read_as_positive_classification.dag @@ -0,0 +1,32 @@ +module gunbc.recurring_failure_mode.lookup_miss_read_as_positive_classification + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data lookup_miss_read_as_positive_classification: RecurringFailureMode = RecurringFailureMode { + identity: "lookup_miss_read_as_positive_classification" as NonEmptyStr, + + receipts: [ + "**a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. ", + + "WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. ", + + "SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. ", + + "Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable \{ id: \}`. Unconditional on that route, not sporadic. ", + + "THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable \{ UndecidableGenericFormal \}`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. ", + + "THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. ", + + "RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. ", + + "REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. ", + + "THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. ", + + "NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.)", + ], + + evidence: [], +} diff --git a/dag/gunbc/recurring_failure_mode/roster.dag b/dag/gunbc/recurring_failure_mode/roster.dag index 32d65d05e03..55622420044 100644 --- a/dag/gunbc/recurring_failure_mode/roster.dag +++ b/dag/gunbc/recurring_failure_mode/roster.dag @@ -179,6 +179,7 @@ import gunbc.recurring_failure_mode.permissiveness_promoted_into_a_higher_safety import gunbc.recurring_failure_mode.evaluation_model_cleanup_undeclared { evaluation_model_cleanup_undeclared } import gunbc.recurring_failure_mode.docs_markdown_projections_have_no_completing_actuator { docs_markdown_projections_have_no_completing_actuator } import gunbc.recurring_failure_mode.type_name_field_carries_rendered_value { type_name_field_carries_rendered_value } +import gunbc.recurring_failure_mode.lookup_miss_read_as_positive_classification { lookup_miss_read_as_positive_classification } import gunbc.recurring_failure_mode.capability_arrives_outside_the_converged_path { capability_arrives_outside_the_converged_path } data recurring_failure_mode_roster: List = [ @@ -349,5 +350,6 @@ data recurring_failure_mode_roster: List = [ evaluation_model_cleanup_undeclared, docs_markdown_projections_have_no_completing_actuator, type_name_field_carries_rendered_value, + lookup_miss_read_as_positive_classification, capability_arrives_outside_the_converged_path, ] 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 d36cbadaa45..a81d4b1f02e 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 @@ -316,3 +316,147 @@ data phantom_distinct_type_argument_source: String = "module probe_inhabit_phant test fn w_a_phantom_type_argument_with_identical_representation_is_still_separated() -> Bool { violation_count(source: phantom_distinct_type_argument_source, wanted: "DeclaredTypeNotInhabited") > 0 } + +// REFINEMENT WIDENING ADMITS -- the positive control for refinement_inhabitance, and the +// regression control for the arm that used to refuse it. product.placement_supply declares +// `HostIdentity = NonEmptyStr where brand("HostIdentity")`, so a HostIdentity reaching a +// NonEmptyStr formal is widening to its own declared base. Before the refinement arm landed this +// REFUSED at two live corpus sites in dag/test/claim/ci/ci_deploy_target_host_witness_test.dag, +// as RefusedDistinctProductConstructor, because +// nominal_product_head_name_if_declared_product read a where-refinement's Conj-with-one-child as +// a nominal product. +// +// BOTH COUNTS ARE ASSERTED AND THE SECOND IS THE DISCRIMINATING HALF. Zero refusals alone would +// also hold if the arm merely stopped deciding, which is the failure mode this lane exists to +// refuse; requiring zero UNDECIDED as well pins the site to INHABITS. Measured live before +// enrolment: undecided=0, refused=0. +// THE PARTNERS EXIST BECAUSE THE COUNT IS CORPUS-WIDE, NOT FIXTURE-LOCAL. violation_count reports +// every row of the class in the census, so a per-fixture literal can never be its oracle -- the +// literal would be a measurement of the current tree copied into the assertion, which DESIGN 5 +// refuses by name. Each control below is therefore a PAIR differing on exactly one axis, so the +// shared corpus contribution cancels and only the axis is measured. +// +// AND THAT INCLUDES THE ZEROES AND THE ONES. An arm reading `== 0` or `== 1` looks fixture-local +// and is not: the census carries the fixture's whole import closure, so any unrelated change in +// std.types that adds or removes a row of the class flips it, and the literal records TODAY'S TREE +// rather than the mutation the arm claims to discriminate. Refusal counts happen to be zero across +// that closure at this writing, which is exactly the coincidence that makes the absolute form look +// safe -- and is not a time-stable fact. So EVERY arm below is a difference between two fixtures, +// with no exception for the ones whose number is small. Review 62112, claude/opus. +data refinement_baseline_source: String = "module probe_refinement_baseline\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { 0 }\n" + +data probe_exact_refinement_source: String = "module probe_exact_refinement\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host_x: HostIdentity = \"srv1\" as HostIdentity\nfn takes_host(s: HostIdentity) -> Int { 1 }\nfn probe() -> Int { takes_host(s: probe_host_x) }\n" + +data probe_exact_brand_source: String = "module probe_exact_brand\nimport std.types { Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host_y: HostIdentity = \"srv1\" as HostIdentity\nfn takes_host2(x: HostIdentity) -> Int { 1 }\nfn probe() -> Int { takes_host2(x: probe_host_y) }\n" + +data refinement_widening_source: String = "module probe_refinement_widening\nimport std.types { NonEmptyStr, Int }\nimport product.placement_supply { HostIdentity }\ndata probe_host: HostIdentity = \"srv1\" as HostIdentity\nfn takes_base(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_base(s: probe_host) }\n" + +test fn w_a_branded_refinement_at_its_own_declared_base_inhabits() -> Bool { + violation_count(source: refinement_widening_source, wanted: "DeclaredTypeNotInhabited") + == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeNotInhabited") + && violation_count(source: refinement_widening_source, wanted: "DeclaredTypeInhabitanceUndecided") + == violation_count(source: probe_exact_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") +} + +// +// BOTH HALVES OF THE DELEGATION ARE ASSERTED HERE, AND THE SECOND IS WHY THIS WITNESS IS NOT +// GREEN-FOR-THE-WRONG-REASON. The abstain half -- this relation adds an undecided and no refusal -- +// says only that WE did not decide. If the brand wall regressed, stopped reaching the argument +// path, or lost its consumer, that half would stay green while the horizontal pair was admitted in +// silence by both relations, and the abstention would be a hole rather than a delegation with the +// only record of the difference sitting in a PR body. So the refuse half is asserted in the same +// witness, against the same exact-match partner so the corpus term cancels: the wall's TypeMismatch +// FIRES on the horizontal pair and does not on the matching one. Review finding, tidy-lynx-804. +// THE HORIZONTAL CASE IS REFUSED BY THE BRAND AUTHORITY, NOT BY THIS RELATION, AND THAT +// DIVISION IS THE POINT. HostIdentity and PhysicalAssetIdentity are both +// `NonEmptyStr where brand(...)`, so their chains meet at NonEmptyStr with neither an ancestor of +// the other. refinement_inhabitance cannot see brands and therefore DECLINES -- refusing there +// would be a second authority for a judgment where_refinement_brand_nominal_verdict already makes +// on brand DECLARATION SITES, and it would drag in the peer-predicate false refusals measured +// when that was tried: declared NonEmptyStr <- produced FilePath, GcpProjectId, Sha512DigestHex, +// none of which carries a conflicting brand at all. +// +// THE PATH IS THE WHOLE QUESTION AND IT WAS EXECUTED, NOT ASSUMED. That wall is reached through +// with_expected_where_refinement_diags, and rung honesty is per-path: refused on the cast path +// would not establish refused at a formal parameter. This fixture puts it at the DIRECT CALL +// ARGUMENT seam and it refuses there -- `type mismatch: expected 'Product(PhysicalAssetIdentity)', +// got 'Product(HostIdentity)'`. So this relation's abstention is a delegation and not a hole. +data brand_horizontal_at_argument_source: String = "module probe_brand_horizontal_at_argument\nimport std.types { Int }\nimport product.placement_supply { HostIdentity, PhysicalAssetIdentity }\ndata probe_host2: HostIdentity = \"srv1\" as HostIdentity\nfn takes_asset(x: PhysicalAssetIdentity) -> Int { 1 }\nfn probe() -> Int { takes_asset(x: probe_host2) }\n" + +test fn w_two_distinct_brands_over_one_base_are_not_refused_twice() -> Bool { + violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeNotInhabited") + == violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeNotInhabited") + && violation_count(source: brand_horizontal_at_argument_source, wanted: "DeclaredTypeInhabitanceUndecided") + > violation_count(source: probe_exact_brand_source, wanted: "DeclaredTypeInhabitanceUndecided") + && violation_count(source: brand_horizontal_at_argument_source, wanted: "TypeMismatch") + > violation_count(source: probe_exact_brand_source, wanted: "TypeMismatch") +} + +// nominal_opaque DOES NOT GROUND TO ITS BASE, and the control exists because the chain walk is +// exactly the thing that could delete that wall. std.types declares `Secret nominal_opaque = +// String` in a form DELIBERATELY DISTINCT from `where brand(...)`: brand is a refinement whose +// value inhabits its base, nominal_opaque is bidirectional separation. where_refinement_chain +// follows only where-refinements, so Secret's chain is one link and this relation returns absent +// for it -- structurally, not by a test. +// +// IT IS ENROLLED ANYWAY BECAUSE THE RED IS AUTHORABLE (DESIGN 4b). If the chain ever followed a +// nominal_opaque alias, Secret's chain would become [Secret, String] and would meet NonEmptyStr's +// [NonEmptyStr, String] at String -- a sibling pair, which this relation declines. So the +// discriminating mutation produces exactly one UNDECIDED here, and asserting zero reds on it. +// THE Secret-FREE PARTNER, differing on exactly the nominal_opaque axis: same module shape, same +// imports, same formal, same call -- the produced value is a NonEmptyStr rather than a Secret. Its +// refusal count is the closure's contribution, so the difference is this fixture's own refusal. +data nominal_opaque_partner_source: String = "module probe_nominal_opaque_partner\nimport std.types { NonEmptyStr, Int }\ndata probe_plain: NonEmptyStr = \"shh\" as NonEmptyStr\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: probe_plain) }\n" + +data nominal_opaque_not_grounded_source: String = "module probe_nominal_opaque_not_grounded\nimport std.types { NonEmptyStr, Secret, Int }\ndata probe_secret: Secret = \"shh\" as Secret\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: probe_secret) }\n" + +test fn w_a_nominal_opaque_alias_does_not_ground_through_the_refinement_chain() -> Bool { + violation_count(source: nominal_opaque_not_grounded_source, wanted: "DeclaredTypeNotInhabited") + > violation_count(source: nominal_opaque_partner_source, wanted: "DeclaredTypeNotInhabited") +} + +// THE POSITIVE CENSUS ARM IS NOT AUTHORABLE HERE, AND THAT IS THE FINDING RATHER THAN AN OMISSION. +// It was to assert that a DECLARED generic clause is still classified generic through the census +// route, over a bare cross-module call (optional_present). Measured on this head: that fixture +// contributes ZERO rows of this class -- its count equals a fixture with no call at all -- so the +// seam emits nothing there whether the classification is right or wrong. An arm asserting a count +// of one is then false, and an arm asserting zero would be green by construction and would be +// cited later as coverage of a thing it never measured, which DESIGN 4b forbids by name: ask +// whether the RED is authorable BEFORE writing the check. The negative arm below IS authorable and +// is enrolled. The residue -- no executing positive control for the census route's generic half -- +// is stated in the PR body rather than papered over with a decoration. + +// NEGATIVE: a CONCRETE declared leaf is no longer classified generic. std.content_hash declares +// fn sha256_digest_wire_form(digest: Sha256Digest) -> NonEmptyStr; Sha256Digest is an ordinary +// declared type and nothing about it is generic. Before this repair the census declaration +// environment carried no bindings at all, so the local-only lookup missed it and it was enrolled +// as one of that declaration's generic parameters and stamped TypeVariable { id: "Sha256Digest" }, +// and the seam declined. DISCRIMINATING MUTATION: restore the deleted local-miss classification in +// either declaration_unbound_leaf_names or declaration_substitution_basis and this arm goes red on +// one UndecidableGenericFormal. +data concrete_via_global_bare_source: String = "module probe_concrete_via_global_bare\nimport std.content_hash { Sha256Digest }\nimport std.types { NonEmptyStr, Int }\nfn probe(d: Sha256Digest) -> NonEmptyStr { sha256_digest_wire_form(digest: d) }\n" + +test fn w_a_concrete_declared_leaf_is_not_classified_generic_through_the_census() -> Bool { + violation_count(source: concrete_via_global_bare_source, wanted: "DeclaredTypeInhabitanceUndecided") + == violation_count(source: refinement_baseline_source, wanted: "DeclaredTypeInhabitanceUndecided") +} + +// THE REFINEMENT DECLINE IS THE INTRODUCTION QUESTION, NOT EVERY REFINEMENT PAIR. A reviewer's +// natural suspicion is that refinement_inhabitance simply made refinement pairs undecidable; these +// two arms refuse that reading by pairing a bare literal against a cast one at the SAME formal. +// The bare literal declines and the cast one does not, so the relation is discriminating on the +// carried introduction rather than on the refinement relation. +// +// AND THE PREDICATE IS ALREADY ENFORCED, which is why the decline is redundant ignorance rather +// than an exposed hole: takes_non_empty(s: "") is REFUSED by the where-refinement machinery with +// `type mismatch: expected Product(NonEmptyStr), got Primitive(String)`, while +// takes_non_empty(s: "x") is admitted by it. Measured live before enrolment. That is what fixes +// this relation's next-rung trigger at CONSULTING the existing verdict. +data bare_literal_at_refinement_source: String = "module probe_bare_literal_at_refinement\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: \"x\") }\n" + +data cast_literal_at_refinement_source: String = "module probe_cast_literal_at_refinement\nimport std.types { NonEmptyStr, Int }\nfn takes_non_empty(s: NonEmptyStr) -> Int { 1 }\nfn probe() -> Int { takes_non_empty(s: \"x\" as NonEmptyStr) }\n" + +test fn w_a_bare_literal_at_a_refinement_formal_declines_and_a_cast_one_does_not() -> Bool { + violation_count(source: bare_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") + > violation_count(source: cast_literal_at_refinement_source, wanted: "DeclaredTypeInhabitanceUndecided") +} diff --git a/docs/design-failure-modes.md b/docs/design-failure-modes.md index 24a8ced774c..ce67f600e24 100644 --- a/docs/design-failure-modes.md +++ b/docs/design-failure-modes.md @@ -171,6 +171,7 @@ The exact `RecurringFailureMode.identity` population, which no other projection - `evaluation_model_cleanup_undeclared` - `docs_markdown_projections_have_no_completing_actuator` - `type_name_field_carries_rendered_value` +- `lookup_miss_read_as_positive_classification` - `capability_arrives_outside_the_converged_path` --- @@ -358,4 +359,5 @@ The landing measurement partitions the 31 parser-visible identities into **2 cit - **DESTRUCTIVE CLEANUP CORRECTNESS DEPENDING ON AN UNDECLARED EVALUATION-MODEL PROPERTY. THREE TRANSPORTS ARE CORRECT BY ACCIDENT OF REALIZATION, NOT BY CONSTRUCTION. INVALID STATE:** the interpreter implements `let` as eager/strict (eval_let evaluates the value expression unconditionally at the point of binding). Nothing declares this as a language guarantee — it is a property of the current interpreter realization, not a declared semantic axis. The companion divergence — that interpreter `&&` evaluates both operands while emitted Rust `&&` short-circuits — is already filed as realization_arms_diverge_on_whether_the_program_refuses. It does not affect these transports: their cleanups are let-bound, not &&-bound, and under eager let a short-circuit && cannot change any conjunction's value because it skips only the right operand when the left is false — a path where the answer is already determined and the skipped operand is a pure field read (.success) on a record whose effect already fired at its let binding. STRUCTURALLY, no transport in this class depends on && eagerness, and no addition to the corpus can create such a dependence as long as let stays eager. If `let` became lazy, cleanup would never run in the namespace_import_closure_behavioral_transport (where cleanup is bound but never consumed), and would be unobserved in the other two (where cleanup .success would not be consumed, though the eager `let` at binding point would still fire). The distinction matters: 'effect does not reach the filesystem' is a leak; 'effect reaches the filesystem but its success is unobserved' is an unobserved cleanup failure — different harms, different severities.POPULATION, BOUNDED AND ENUMERABLE — THE THREE TRANSPORTS: `tools.self_host_logic_behavioral_transport::slb_comparison_observation` (let-bound cleanup_src/cleanup_out consumed in the staged conjunction), `tools.emit_host_transport::run_rust_smoke` / `::run_python_smoke` / `::run_go_smoke` (let-bound cleanup consumed in a conjunction), `tools.namespace_import_closure_behavioral_transport::nic_emitted_crate_evidence` (let-bound cleanup_src/cleanup_out NEVER consumed — correct only because let is eager).CEILING: cleanup that does not depend on the evaluation model at all — an effect the transport sequences explicitly rather than one it gets from strictness. Every transport's destructive cleanup would be structurally sequenced (e.g. a `do cleanup after body` pattern) rather than relying on let-eagerness for its effect to reach the filesystem.NEXT-RUNG TRIGGER, A CAPABILITY — either (a) the evaluation model declared as a typed guarantee that a check can execute against — a property of the interpreter that is named, bounded, and verifiable, not prose — or (b) every transport whose correctness turns on eager evaluation sequences its destructive effects explicitly rather than inheriting them from let-strictness. Both capabilities are genuine transitions; neither is satisfied by documentation or by this row.CORPUS POPULATION MEASUREMENT — the && divergence has no live hazard in this corpus: zero sites place a non-total or effectful operation directly as the right operand of `&&` (the two found are read-only). Twenty sites let-bind destructive effects and then consume their .success in a `&&` chain; under the structural argument above, none depends on && eagerness. HOWEVER, A=0 is a SURVIVOR PROPERTY OF THE STRICTER ARM HAVING FILTERED THE CORPUS, not evidence the class is harmless. The interpreter evaluates both operands unconditionally, so any author who wrote `guard && dangerous` would have hit the refusal while authoring and rewritten before commit. Under a short-circuit `&&`, authors would write these patterns freely and they would compile — and the emitted arm would silently produce a wrong answer where the interpreter refuses. That is the existing row's subject.INSTRUMENT — DISCRIMINATING PROBES, THEIR NAMES AND INVOCATION, SO A FUTURE READER CAN RE-DERIVE THIS FINDING AND RE-RUN IT. Five executed probes in module `test.claim.eval_model_probe` (dag/test/claim/eval_model_probe_test.dag): `let_is_eager_when_unused` (let-binds a Remove without consuming its result; PASS means eager), `let_is_eager_when_consumed` (positive control), `and_demands_right_even_when_left_false` (let-binds false and Remove separately, && computes; PASS means Remove ran despite false), `and_short_circuit_direct_probe` (false && Remove directly; PASS means Remove ran), `and_with_true_left_removes_file` (positive control). Each was run as: `gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/eval_model_probe_test.dag --function --claim-run`. All five returned PASS (exit 0). Probes observed the filesystem side effect out-of-band (shell.Test.IsFile) rather than consuming a returned value, so no measurement-created dependency could confound the result. - **generated `docs/*.md` ledger projections have no ProcessExit actuator and no regen coverage, so an EDIT to a still-present row can sit in the authority, absent from the projection, with every completing instrument green** (INVALID STATE: `gunbc.recurring_failure_mode` is the authority; `docs/design-failure-modes.md` is the projection DESIGN.md points readers at. `expected_design_failure_modes_md` returns `String`. The refusal exits 2 with EMPTY STDOUT and interpolates the rendered value into the diagnostic on stderr: classify_exit's non-variant arm is type_name: ctx.format_value(other). Executed: wise-badger-902, EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown heading; quick-heron-85, proj3.err 1062137 bytes, same delimiters. The enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` forbids print-AND-SUCCEED, and holds. The content is therefore obtainable ONLY by scraping a half-megabyte stderr diagnostic between delimiters that are message prose (returned-open-quote and not-ProcessExit-close-quote), unversioned and enrolled by nothing. Extractable only by scraping an unversioned diagnostic — which is why the ProcessExit regen is the repair. `claim_executor --required-regen` compares only `is_compared_generated_basename` = ends_with .rs into `target/stage0-regen-candidate`. HARM: three rows can be edited in `.dag` after the last projection and nothing that exits 0 will say the markdown is stale. The meaning-fork in the field named type_name is a separate row, `type_name_field_carries_rendered_value`, not this class. SPECIMEN, measured by another lane while regenerating the projection, 2026-09-06: `instrument_answers_outside_its_domain`, `stale_claim_survives_its_own_correct_edit`, and `native_stack_recursion_unbounded_over_corpus_shaped_structure` had been edited in their authorities after the doc was last projected and had grown by 2349, 5519 and 1152 characters. Regenerating carried the repairs through. On origin/main as of 3531d30bb82 those three `.dag` files are older than `docs/design-failure-modes.md` (`81686f7bea8`), so CURRENT main is not claimed still stale; the class is that nothing completing could have said so while they were. SPECIMEN, review 58567 on gunbc#9864, on the host comment above `exit_status_for_class`: a relocation dropped the `status: refused — printing the value and exiting 0 would report success for a run whose outcome is unknown.` sentence while the comment claimed byte-for-byte equivalence. The doc lied, not the code. The sentence was restored rather than the claim weakened. That is this class on a different pair: an authority and its projection disagreeing with nothing completing to say so, and a real specimen rather than an injected literal. INCIDENT, not a fixture and not a perturbation ordered for this PR, produced by quick-heron-85 without looking for this class, commit b1c6378c6d: their authority row unresolved_callee_conflated_with_dispatched_elsewhere was UNPARSEABLE for a full commit. An authored receipt contained a quoted phrase using bare double quotes inside a double-quoted string; the string terminated early and the parser refused undefined variable this and undefined variable leaf. THE AUTHORITY DID NOT COMPILE, so docs/design-failure-modes.md kept rendering the previous vintage while presenting as current. They found it only by running the projection; reading the row does not surface the break. This PR's gate would go red on that commit because an unparseable authority makes the projector refuse — from the committed markdown alone, STALE bytes and an UNBUILDABLE authority are indistinguishable. THIS ROW IS THE DETECTOR GAP. The quoting injury that silently disabled the row they were filing is a neighbouring class they are filing separately; its next-rung trigger is string escaping in the .dag lexer. This gate makes that injury loud; it does not make it unwritable. Do not read this row as closing that class. THE IDENTITY-JOIN CORRECTION, which is the transferable part and which corrects a rule this project holds. Completeness is an identity join, not a count equality — and AN IDENTITY JOIN OVER ROW NAMES WOULD HAVE REPORTED THAT FILE COMPLETE AND CORRECT: every identity present, none missing, none extra. The drift was pure EDIT. Only a regenerated byte diff sees an edit. Worse: a first pass comparing line SETS read the three as REORDERINGS, because the changed rows shared an 80-character prefix with their old text, so the cheap check does not merely miss the drift, it manufactures a benign explanation for it. An identity join proves MEMBERSHIP, not CONTENT. THE TWO NEIGHBOURS THIS IS NOT. `authority_merges_unprotected_while_its_projection_is_guarded` is MERGE POLARITY: the generated projection is driver-bound while the hand-authored authority is not. Adjacent files, distinct defect — this row is the absence of a completing actuator or content gate, reachable with no merge in sight. `green_reported_over_a_population_the_instrument_does_not_own` is a split of actuators whose GREEN is read as covering the half it does not enumerate; that climb joined registry-projections to stage0-mirrors inside one required phase, and still does not give `gunbc run` a ProcessExit projector for the markdown, nor put `.md` in `--required-regen`. RECOGNITION RULE: when a generated file is what readers are pointed at, ask (1) whether any `ProcessExit` entry writes those exact bytes and exits 0, (2) whether regen's compared population includes that path, and (3) whether the gate compares CONTENT, not row-name membership. A complete identity set of names is not a content agreement. RUNG FOUND AT: outside the ladder until a completing content agreement exists — silent wrongness, not a weak wall. After a ProcessExit projector and a required content compare execute, mechanically preventable: the stale file remains writable. CEILING: structurally guaranteed when membership of every committed generated `docs/` path in a content-agreement adjudicator is derived from `gunbc.generated_artifact` `committed_generated_artifacts`, so omitting the arm is a compile refusal. NEXT-RUNG TRIGGER, a capability: required-run dispatch consumes a content agreement — byte identity of generated vs committed — over every committed generated artifact whose location directory is `docs`, derived from the registry so adding a committed `docs/` path without that agreement will not compile. A trigger naming one command, one test file, or `docs_projection_gate.dag` is less than the capability and would fire while edit-only drift can still sit uncompared.) - **a field named type_name holds a type name on three arms and a fully rendered value on the fourth** (INVALID STATE: ExitClass::NotProcessExit is one spelling whose payload field is called type_name. `classify_exit` Variant arms that are not ProcessExit put ctx.resolve of the variant type symbol, or ProcessExit plus the unknown variant, into it — an actual type or variant name. The final other arm puts ctx.format_value of the non-variant value — the rendered value — into the same field. `exit_status_for_class` interpolates that field into the returned-quote slot with no second match, so every refusal path reads one name for two facts. HARM: a reader of the interpolation site infers the field's contents from its NAME and concludes a String projector yields the word String; a reader of the producer and a live stderr file concludes the markdown body is in the diagnostic. Both readings of adjacent code are correct; the name is a third surface and it lied. SPECIMEN, 2026-09-06, executed both ways. clever-otter-298 read `exit_status_for_class` and the enrolled control `non_process_exit_refuses_rather_than_printing_and_succeeding` (which constructs NotProcessExit with a fixture type_name Bool and never goes through `classify_exit`) and asserted the diagnostic names the type. wise-badger-902 read the interpolation site and ruled the same. quick-heron-85 held proj3.err at 1062137 bytes. The manager then RAN the projector: EXIT=2, stdout 0 bytes, stderr 578588 bytes opening with the markdown. The field name said type; the field held format_value. WHY THE FORK SURVIVED, and it is a section 4b evidence gap not a naming smell. `non_process_exit_refuses_rather_than_printing_and_succeeding` hand-constructs ExitClass::NotProcessExit with type_name the literal Bool and starts from an already-classified value. It never calls `classify_exit`. Nothing executing joins the field's name to its contents on the non-variant path — the only enrolled evidence feeds the field a literal that matches its name, which is exactly the input that cannot discriminate. The control's RED is unauthorable for this defect, so it was permanently green over the case that mattered and got cited as coverage. A field carrying two facts is ordinary; a field carrying two facts with a control that only ever sees one of them is why three of us read adjacent code correctly and reached three answers. THIS IS NOT `docs_markdown_projections_have_no_completing_actuator`. That row is the absence of a ProcessExit actuator and a content gate over generated `docs/*.md`. This row is a meaning fork inside `ExitClass`, reachable with no docs file in sight. Neighbour `meaning_fork` is the generic class; this instance is filed because the fork sat in the struct every refusal path reads and produced the three-way contradiction. Neighbour `diagnostic_name_mechanism_silent` is a diagnostic NAME silent about its predicate; here the FIELD name is accurate for three arms and false for the fourth. RECOGNITION RULE: when a field is named for a kind of contents, read every constructor, not the interpolation site. If one constructor writes a different kind, the name has forked. RUNG FOUND AT: mitigatable — the wrong inference is a human reading; the runtime still refuses with exit 2 and does not print-and-succeed. CEILING: structurally impossible when `NotProcessExit` cannot be constructed with a rendered value under a field named for a type — two variants, or a field named for what it actually holds. NEXT-RUNG TRIGGER, a capability: `ExitClass` distinguishes a type-name refusal from a rendered-value refusal in the type, so interpolating one as the other will not compile.) +- **a lookup miss is read as POSITIVE evidence of a property, against an environment that could not have answered** (a classifier decides `this thing IS an X` from the fact that a lookup for it returned nothing. The miss is evidence of nothing at all when the consulted authority does not carry the population the question ranges over -- and when it carries none of it, the classifier is not a heuristic that occasionally misfires, it is TOTAL: every subject reaching it is classified X, always, and the predicate's other disjuncts never run. WHY THIS IS ITS OWN CLASS. `absence_classifier_default_bucket` and `absent_reads_identically_to_never_looked` both concern absence read as a NEGATIVE -- an accepted bucket, a zero finding. This is the converse and it is worse: absence MINTS A POSITIVE TYPED CLAIM that then travels as a fact, so downstream consumers are not merely uninformed, they are misinformed with something that looks derived. It is also distinct from `absorbing_fallback`, whose arm widens the ANSWER to a superset while still answering the right question; here the question itself is answered backwards from a miss. SPECIMEN, gunbc 595870431b, at the DESIGN 4b floor (`values inhabit declared types`). `v1.compiler.env census_declaration_type_env` builds a declaration environment with `bindings`, `str_bindings`, `ancestry_str_bindings` and `intern_table` ALL EMPTY, seeded only with the declaration's type-parameter bindings, so `lookup_binding_by_name_local` in that environment can only ever find a type parameter. Two sites read a miss there as generic ownership: `v1.compiler.lookup declaration_unbound_leaf_names`, whose collected names were concatenated into the generic-name roster, and `v1.compiler.env declaration_substitution_basis`, whose second disjunct repeated the same test. So for EVERY census-borrowed declaration, EVERY unqualified non-kernel concrete type name in EVERY parameter was enrolled as one of that declaration's generic parameters and stamped `TypeVariable { id: }`. Unconditional on that route, not sporadic. THE HARM, and it is a floor hole rather than a lost refinement. `v1.compiler.infer direct_call_argument_inhabitance_diags` selects the substitution basis as the DECLARED side whenever it carries an unbound type variable, and `declared_type_inhabitance` reads that stamp as a generic formal and declines `InhabitanceUndecidable { UndecidableGenericFormal }`. A value of any constructor reaching a `NonEmptyStr` or a `HostIdentity` position was therefore admitted in silence -- not because the pair was undecidable, but because the declared side's identity had been overwritten before the judgment ran. The neighbouring mismatch arms are gated on the same stamp and were suppressed with it. THE TELL THAT MAKES IT RECOGNISABLE ELSEWHERE, and the reason it survived review: the authority the guess was approximating was ALREADY CONSULTED ONE FIELD OVER. `borrowed_census_callable_candidate` computes `borrowed_generic_param_names` on its first line and classifies the RETURN type of the same declaration positively with it; the PARAMETER types, in the next field of the same record literal, went through the miss. One question with two answers inside a single record literal is a DESIGN section 3 fork, and the half that reads a miss is always the wrong half. RUNG FOUND AT: below the ladder -- silent wrongness, since an unrelated constructor was ACCEPTED at a declared position with no diagnostic in either direction. CEILING: 3 (structurally guaranteed) FOR THE CLAUSE-DERIVED POPULATION, AND MECHANICALLY PREVENTABLE (2) FOR AUTHORED PARAMETERS -- the two are stated separately because a bare ceiling 3 would send a reader past the exception. Generic ownership IS a declared fact: `parse_optional_type_params` mints one parameter per name in the angle-bracket clause whose name and type-expression name are both that name, and that encoding is the only carrier the CLAUSE has. But the classification is decided by a PREDICATE over that shape, not by the clause, and an authored shape can satisfy it: the `make_param_node` producer census found EIGHT structural producers that cannot mint `pname == type-expr name`, and FOUR authored-dependent sites that can -- an author writing `fn f(Vendor: Vendor)` produces a parameter the roster predicate cannot distinguish from a generic clause. The subject of this row is the CLASSIFICATION, not the clause, so the reported rung is the minimum across both populations. WHAT STANDS BETWEEN THIS AND 3 OUTRIGHT: the authored `pname == type-expr name` shape, which no clause-side encoding can exclude. REPAIR: consult the roster and delete the miss from both sites together, since they were one classification authority written twice. THE ROSTER PASSED IS A UNION AND THAT HALF IS NOT OPTIONAL: the declared `` clause and the borrowed-parameter roster are two facts and neither subsumes the other -- the borrowed predicate is narrower on two axes, so passing it ALONE would reclassify a declared type param whose type expression is not a childless leaf as a concrete unresolved name, reintroducing the same misclassification through the opposite door. Deleting the absence disjunct is the repair; replacing the declared-clause predicate beside it was a second change and is not part of it. THE RESIDUE'S DISPOSITION IS AN UNEXERCISED BOUNDARY AND IS RECORDED AS ONE. The repair's author predicted that a leaf which is neither on the roster nor resolvable would be reported `UndecidableFormalUnresolved`, a different fact from genericity. THE CORPUS DID NOT DEMONSTRATE IT: measured across the repair, that population moved by ZERO -- 6 sites before, 6 after, not one of them new. So the boundary is stated here as ASSERTED AND UNEXERCISED rather than as behaviour, because a row is the durable artifact and a disposition nothing executed is exactly the specification-without-execution DESIGN section 5 names. It becomes a fact when a specimen lands on it, not before. NEXT-RUNG TRIGGER for that residue: an owner-generic carrier on a synthesized or member declaration that borrows an enclosing owner's generic without restating it, which its own roster cannot name.) - **a host holds a capability that no modeled path put there, so every later green on that host is uninterpretable.** INVALID STATE: a host answers ready for some capability while the convergence that is supposed to be the only way that capability arrives has not delivered it. The harm is not the capability -- it usually works -- it is that a receipt naming the host can no longer distinguish the modeled path working from a hand-run answering, and the ambiguity is permanent and travels with every future citation of that host. DISTINGUISHING FACTS, against neighbours it is easy to file as. It is not `execution_provenance_loss`: there an observation may never have run, whereas here the observation runs and reports faithfully -- the host really does hold the capability. It is not `head_landed_by_hand_before_its_own_verification_reported`: that is an artifact landing uncertified, this is DURABLE HOST STATE whose origin is unrecorded. The tell is a convergence that reports `already satisfied` for a host it never satisfied. THE STRUCTURAL CAUSE IS A CAPABILITY AUTHORIZED BY ONE MODULE, DISCLAIMED BY ANOTHER, AND EXECUTED BY NEITHER, which is DESIGN section 6's out-of-band actuation wearing convergence vocabulary. `gunbc.runner.runner_host_grants` emits EnsureSupplementaryGroupMembership and `runner_host_sudoers_content` renders permission to run its argv; `gunbc.runner_microvm_host_ready` explicitly disclaims applying it, naming the result 'a hole an operator falls into once per host, by hand'. A modeled capability with no executor is a manual step, and the roster row that grants it makes the manual step look converged. SPECIMEN A, srv2 KVM (2026-09-05): an operator ran `sudo usermod -aG kvm ghrunner` by hand, the argv already rendered at provisioning/srv2/gunbc-ghrunner.sudoers. srv2 has read kvm=writable ever since while every sibling host reads present-not-writable. The module's own annotation recording the earlier measurement went stale at that moment and COULD NOT GO RED, because DESIGN section 4c says no Accepted program reads an annotation; it was caught only because someone asked whether the grant was converged. SPECIMEN B, srv1 Firecracker (2026-09-06, this row's occasion): a session ran the modeled `runner_microvm_host_converge_wet` by hand on srv1, which installed Firecracker v1.16.1-aarch64 into the executor-owned root -- 30 paths under ~/.local/share/gunbc-firecracker, the root directory itself created by the run, so nothing pre-existed. It was digest-verified, idempotent, and spent no host grant, and it was STILL wrong: srv1 is the canary of record, and its capability would not have come from the host-image path that is supposed to own it. THE RULING, AND WHY DECLARING THE DEVIATION WAS REJECTED AS THE WEAKER ARM. The first recommendation was to keep the install and write it down. The operator overrode it: declaring makes the ambiguity legible but leaves every later srv1 receipt carrying a provenance caveat forever, whereas removing it makes the question stop existing. CONVERGENCE IS ONLY MEANINGFUL IF IT IS THE ONLY WAY STATE ARRIVES. Specimen B was reverted the same day -- the enumerated tree removed and nothing adjacent touched -- and the honest post-revert state is that srv1 cannot run a guest, which is what makes the convergence gap visible instead of papered over. RUNG FOUND AT: BELOW THE FLOOR, which is not a rung -- DESIGN section 4b puts silent wrongness outside the ladder and forbids it outright, and that is where both specimens sit. Nothing executed distinguishes a converged capability from a hand-placed one: `runner_microvm_host_ready` observes WHETHER the host holds a capability and never WHAT PLACED IT, so a hand-run host and a converged host produce byte-identical standing. The srv2 specimen is the measured proof -- the writability persisted from 2026-09-05 through every subsequent standing read, the annotation recording the pre-hand-run measurement went stale at that instant and could not go red because no Accepted program reads one, and it surfaced only when a human asked whether the grant was converged. The srv1 specimen adds that the converge itself reports success without recording that its operator was a hand session. Provenance has no mechanism at all, not a weak one. CEILING, DERIVED AND DIFFERENT FOR TWO HOST SHAPES, so a single number would be dishonest. On a host whose runtime root is reconstructed from a repository-built image at every boot, the ceiling is STRUCTURALLY IMPOSSIBLE: no persistent root survives to hold a capability the image did not place, so the invalid state has no constructor and the question stops being askable rather than being checked. On a MUTABLE persistent host the ceiling is MECHANICALLY PREVENTABLE and no higher, because an operator holding sudo can always place state -- the best reachable is an observation that refuses a capability it cannot attribute, which depends on that check executing and staying enrolled. Per DESIGN section 4b(1) a class's rung is the MINIMUM across its in-scope paths, so while any mutable host remains in the population the class's attainable ceiling is mechanically preventable, and the structural arm is available only to the hosts that stop being mutable. NEXT-RUNG TRIGGER, A CAPABILITY AND NOT AN ARTIFACT, stated at the grain of the loss. The loss is plural -- every host, every capability -- so a trigger naming one host or one grant would be satisfied while the class stayed dead. FROM BELOW-THE-FLOOR TO MECHANICALLY PREVENTABLE: a host-standing observation that reports, for each capability, the identity of the converge run that placed it, such that a capability with no attributable placing run is a typed refusal rather than a ready standing. That is the whole capability; a receipt that merely RECORDS provenance without refusing on its absence does not reach it, because the srv2 specimen was already recorded in prose and still could not go red. FROM MECHANICALLY PREVENTABLE TO STRUCTURALLY IMPOSSIBLE, and only for hosts that reach it: a runtime root reconstructed from a repository-built image on every boot, so that no capability persists that the image did not place. Naming a specific host-image pull request would be naming an artifact; what discharges this row is the property that a rebooted host cannot carry unattributed capability, whichever change delivers it. THE APPLIER IS BUILT AND UNREACHABLE, NOT MISSING, AND THE DISTINCTION DECIDES THE REPAIR. This row's first draft implied the executing half had to be written. It does not: `gunbc.executor_privileged_apply apply_executor_privileged_operations_wet` exists, elevates with `sudo -n` so an uncovered command REFUSES instead of hanging on a prompt no automated converge will answer, and renders its argv through the SAME `executor_privileged_operation_argv` the sudoers line is rendered from -- so what is permitted and what is executed are one fact by construction rather than by review. It has ZERO callers anywhere in the corpus, test modules included; the only other occurrence is a decl_ref citation. So DESIGN section 4b(2)'s three-way split lands on its strongest arm -- not `cannot climb`, not `can climb after one grounding`, but CAN CLIMB NOW WITH THE MECHANISM ALREADY WRITTEN -- and the remaining work is one wiring into the converge path. Recording this is load-bearing because the opposite reading sends the next author to build a second applier beside the first, which is precisely the argv fork that module's own annotation says it exists to prevent. AND THE REASON IT HAS NO CALLER IS ITSELF A NAMED CLASS, WHICH IS WHY THE WIRING NEVER HAPPENED. The module was not deferred pending an ownership decision and it is not a half-finished design: #10628 introduced it WHOLE, expressly to close this gap -- that commit's own account is that `executor_privileged_operation_argv` had no production consumer, that `runner_host_privileged_operations` fed only the sudoers renderer, and that this module 'closes it, and executes THE SAME argv function' -- and then landed it without the caller it was written for. That is DESIGN section 3c exactly, down to the tell that section lists in its own words: consumption described in the PR body but absent from the diff. So the repair that was supposed to end this class was itself an instance of a neighbouring one, and the two facts are the same fact: 'one wiring remains' and 'a section 3c dangling consumer' describe the same missing edge, but only the second says WHY it is missing and therefore why waiting will not produce it. REPAIR, IN PREFERENCE ORDER: bake the capability into a host image so the question cannot be asked, or close it in fleet converge. NOT an applier bolted beside the disclaiming module, and never the sudoers argv by hand -- that converts a modeled hole into a second undeclared deviation, which is how specimen A was produced. The reviewer's question for any host-capability claim: which run put it there, and can you name it. diff --git a/src/v1/04_env.dag b/src/v1/04_env.dag index 2905a358e45..dfa88052576 100644 --- a/src/v1/04_env.dag +++ b/src/v1/04_env.dag @@ -1091,6 +1091,13 @@ fn lookup_type_by_name(env: TypeEnv, name: String) -> Node? { // substitution basis. Synthesized constructors can mention a parent generic that is not exposed // as one of their own generic params; after resolution that leaf otherwise looks like a concrete // Primitive(T). No consumer may reconstruct this distinction through the caller environment. +// THE ROSTER IS THE WHOLE TEST. A second disjunct used to stamp any bare, unqualified, +// non-kernel leaf that lookup_binding_by_name_local missed, which read absence from a lookup as +// positive evidence of generic ownership (DESIGN section 5's absorbing fallback) and, at the +// census caller whose declaration env carries no bindings at all, was total over every concrete +// type name a parameter mentions. generic_names is the authority for this question and is now +// the only one consulted; a leaf that is not on it and resolves nowhere is UNRESOLVED, which is +// a different fact with its own reported reason. fn declaration_substitution_basis(n: Node, env: TypeEnv, generic_names: List) -> Node { let children = n.children |> map(ch => declaration_substitution_basis(n: ch, env: env, generic_names: generic_names)) let with_children = node_with_children(n: n, children: children) @@ -1098,10 +1105,7 @@ fn declaration_substitution_basis(n: Node, env: TypeEnv, generic_names: List count) == 0 && name != "" - && ((generic_names |> any(g => g == name)) - || (!contains(name, ".") - && !is_kernel_type(name: name) - && lookup_binding_by_name_local(env: env, name: name) == none)) + && (generic_names |> any(g => g == name)) if generic_leaf { node_with_inferred(n: with_children, inferred: Present { value: TypeVariable { id: name } }) } else { diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index ce6c134cb3a..e79aa4f3633 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -3269,6 +3269,8 @@ type InhabitanceUndecidableReason | UndecidableOptionalCarrier | UndecidableFormalUnresolved | UndecidableProducedIdentityErased + | UndecidableRefinementIntroduction + | UndecidableRefinementPeerChains type InhabitanceRefusalReason = RefusedPayloadAtParent @@ -3276,6 +3278,7 @@ type InhabitanceRefusalReason | RefusedDistinctProductConstructor | RefusedDistinctAppliedTypeArgument + type InhabitanceVerdict = Inhabits | InhabitanceRefused { reason: InhabitanceRefusalReason } @@ -3300,6 +3303,191 @@ fn declared_type_position_label(position: DeclaredTypePosition, subject: String) } } +// REFINEMENT INHABITANCE, DECIDED FROM THE CHAIN AND IN BOTH DIRECTIONS BY ONE AUTHORITY. +// +// std.types declares refinements in layers -- NonEmptyStr = String where non_empty, +// PathSegment = NonEmptyStr where brand("PathSegment"), Char = Int where unicode_scalar, +// brand("Char") -- so a refinement pair is not two unrelated names, it is two positions on one +// chain, and which position each side occupies is the whole verdict. std states the direction it +// cares about on the RenderedTerminalText declaration: a raw stdout pipe cannot inhabit the brand, +// so feeding one to a parser that requires it is a type error. That is NARROWING refused. It says +// nothing against widening, and the PathSegment note reasons about a branded NonEmptyStr as +// though it simply is one. +// +// ONE RELATION, EVERY DIRECTION, DELIBERATELY. Deciding widening in one predicate and the other +// directions in another lets them drift apart, and only one would carry a test. All three arms +// are read off where_refinement_chain rather than off any particular pair, so a brand over Int +// decides the same way a brand over NonEmptyStr does and a two-level chain decides the same way a +// one-level chain does. +// +// THE NARROWING DIRECTION DECLINES, AND BOTH HALVES OF THAT ARE MEASURED, NOT REASONED. +// std's brand prose refuses narrowing, and the first build of this relation refused it here -- +// which turned 10 corpus refusals into 4928, every one of them a base value at a refinement +// formal, 3870 of those a plain String at a NonEmptyStr formal. That is not four thousand +// defects, so the refusal was withdrawn and the pair is declined instead. +// +// WHAT THE DECLINE IS, AND TWO WRONG ACCOUNTS OF IT THAT MEASUREMENT KILLED. It is NOT that +// introduction is uncarried: an EXPLICIT CAST IS ALREADY VISIBLE HERE -- +// takes_non_empty(s: "x" as NonEmptyStr) produces nothing from this relation, while bare literals +// decline. And it is NOT that the predicate goes unchecked: a three-way fixture pair settles it. +// takes_non_empty(s: "") -> REFUSED, `type mismatch: expected Product(NonEmptyStr), got +// Primitive(String)`, from the where-refinement predicate machinery +// takes_non_empty(s: "x") -> admitted by that same machinery, no mismatch +// both -> this relation declines with UndecidableRefinementIntroduction +// +// So the introduction question IS ALREADY DECIDED, by an authority this relation does not consult. +// That is the same shape the numeric note above records: the class was never undecidable, it was +// UNCONSULTED. Refusing here would fabricate a verdict in the direction DESIGN section 5 forbids +// as firmly as fabricating a success, and admitting here would assert a proof this relation did +// not perform; so the pair is reported UndecidableRefinementIntroduction -- located, per-reason, +// countable -- and the deficit ranks instead of vanishing. +// +// THE PEER ARM CARRIES ITS OWN NAME AND ITS OWN REASON, BECAUSE IT IS A DIFFERENT FACT AND ONE +// NAME MAY NOT HOLD TWO -- and the CONSTRUCTOR was renamed with the reason, since calling them +// sibling BRANDS encoded the same conflation one level up: the measured population is not brands. +// Narrowing is introduction: the produced type sits at or above the declared refinement on +// its own chain. Peers MEET on a shared link with neither nesting inside the other, and the +// measured population makes the difference concrete -- declared NonEmptyStr <- produced FilePath, +// GcpProjectId, Sha512DigestHex are peer predicates over one base, not introductions and not +// conflicting brands. Filing them under a reason whose text says they are introductions is the +// meaning fork DESIGN section 3 names, and it would defeat the very property this note claims: +// a mixed bucket is not located, per-reason or countable. It would also mis-aim the trigger +// below -- consulting the introduction verdict would discharge the trigger while leaving a sibling +// residue behind under a name asserting it had been handled. Review finding, cursor/auto on +// review 62043, upheld by tidy-lynx-804, 2026-09-07. +// +// NEXT-RUNG TRIGGER, and it is CHEAPER than the one first written here: this relation consulting +// the where-refinement predicate verdict that already decides the pair, rather than a new +// elaboration fact reaching the seam. An earlier draft of this annotation claimed the predicate +// was unchecked at introduction, on a probe that reported no diagnostic for an empty literal; the +// fixture pair above refutes that, and the claim is withdrawn rather than defended. +// +// THE SIBLING ARM DECLINES TOO, AND THAT IS A SECTION 3 ANSWER RATHER THAN A GAP. Two refinements +// that share a base without either being the other's ancestor look like the horizontal case brands +// exist to refuse -- but DISTINCT BRAND DECLARATIONS ARE ALREADY WALLED, by +// where_refinement_brand_nominal_verdict through where_refinement_mismatch_diags, which compares +// brand DECLARATION SITES rather than spellings and refuses BrandNominalDistinctDeclarations. +// Refusing here as well would be a second authority for one judgment. It would also be wrong at +// this grain, and that was measured rather than reasoned: refusing every sibling pair turned up +// FilePath at a NonEmptyStr formal, GcpProjectId at a NonEmptyStr formal, Sha512DigestHex at a +// NonEmptyStr formal -- peer predicate refinements over the same base, carrying no conflicting +// brand at all, whose chains fail to nest only because each is declared over String directly. A +// sibling relation is not a brand conflict, and only the brand authority can tell them apart. +// +// WHY IT IS REACHABLE ONLY NOW. Every site this relation answers had its declared side rewritten +// into a generic formal before any arm ran, so the refinement question was never put. Measured on +// the corpus at the moment that stamp was removed: HostIdentity flowing into a NonEmptyStr formal +// -- widening to its own declared base, correct code -- refused as a distinct product +// constructor. This is the arm that state was hiding, not a widening of scope. +// THE CHAIN IS COMPARED AT RESOLVED DECLARATION IDENTITY, AND IT IS UNAVAILABLE ON ANY MISS. +// Three corrections live here, each from a review and each falsifying something an earlier form of +// this function asserted about itself. +// +// FIRST, it compared qualified_last_segment -- a module-STRIPPED last segment -- so two homonymous +// refinements would have compared EQUAL and widening would have admitted a pair that does not +// inhabit. This file already suffered that class: a second HostIdentity was minted beside +// product.placement_supply's and did not surface as a duplicate declaration. Only one survives +// because the incident was CLEANED UP, not avoided. +// +// SECOND, it keyed on where_refinement_brand_declaration_site applied to the node in hand, and +// ident_span IS NOT DECLARATION PROVENANCE: default_ident_span sets it from the node's OWN +// name_span at construction, so on a link that did not resolve the key was a REFERENCE-site key. +// That is wrong in BOTH directions at once -- two distinct declarations referenced from one file +// key EQUAL, one declaration referenced from two files keys UNEQUAL -- and a key that can both +// merge distinct things and split identical ones is not an identity at all. There is no tightening +// that repairs a non-identity, so the fallback is gone rather than sharpened: every link is +// resolved through lookup_type_for, the NODE-AWARE authority that matches node.ident first, and the +// site is taken from the resolved DECLARATION. +// +// THIRD, the entry point took authored_name_at and then looked the type up BY NAME, so a node that +// already carried identity was rebound by spelling at the head of a relation whose whole subject is +// spelling collision. It resolves through lookup_type_for too. +// +// AND THE COMPLETENESS CHECK NOW MEASURES RESOLUTION RATHER THAN NAMING. The count equality below +// used to compare ident_span PRESENCE, which every named node has, so it proved the links were +// NAMED and could not fail for the reason it existed. It now compares RESOLVED links, and any miss +// discards the whole chain: the pair is simply not this relation's subject. +// +// WHY DISCARD RATHER THAN COMPACT, since the earlier form dropped unidentified links and claimed +// that was conservative. IT IS NOT, and the counterexample is the HEAD: drop the declared side's +// head and its BASE is promoted to head, so the produced chain contains it, the widening arm fires, +// and a value is admitted at a strictly narrower declared refinement it was never shown to inhabit. +// Compaction is not the conservative direction; it is the widening one, one link up. +// +// ONE PRINCIPLE, THREE POSITIONS, AND IT IS WORTH STATING ONCE RATHER THAN PATCHING THREE TIMES: +// ABSENCE OF IDENTITY IS NOT REPAIRABLE BY DEGRADING WHAT YOU COMPARE. Every arm above reached for +// a weaker comparison when the precise one was unavailable -- lowering the GRAIN to a spelling, +// shortening the CHAIN past a link it could not identify, substituting a REFERENCE for a +// declaration -- and each was assessed as conservative in general while reversing direction at some +// particular position. A failure arm refuses; it does not widen, and it does not compare something +// else instead. Reviews 62130 and 62172, and GitHub review 5135375330, 2026-09-07. + +fn refinement_chain_link_identity(link: Node, type_env: TypeEnv) -> String? { + match lookup_type_for(env: type_env, node: link) { + Present { value: declaration } => + where_refinement_brand_declaration_site( + ty: declaration, source_indices: type_env.source_indices) + Absent => Absent + } +} + +fn refinement_chain_link_identities(links: List, type_env: TypeEnv) -> List { + let identified = links + |> map(link => refinement_chain_link_identity(link: link, type_env: type_env)) + |> filter(site => site != none) + |> map(site => match site { Present { value: id } => id Absent => "" }) + |> filter(id => id != "") + if (identified |> count) == (links |> count) { + identified + } else { + [] + } +} + +fn refinement_chain_names(n: Node, scope: InferScope) -> List { + match lookup_type_for(env: scope.type_env, node: n) { + Present { value: declaration } => + refinement_chain_link_identities( + links: where_refinement_chain(ty: declaration, type_env: scope.type_env), + type_env: scope.type_env) + Absent => [] + } +} + +type RefinementInhabitance + = RefinementWidensToDeclaredBase + | RefinementNarrowsToDeclaredBrand + | RefinementPeerChains + +// ABSENT MEANS "NOT THIS RELATION'S SUBJECT", NEVER "COMPATIBLE". Every guard hands the pair back +// to the arms below rather than admitting it, so this can only convert a silence into a decision +// for a pair whose two chains are both established and actually meet. +fn refinement_inhabitance(declared: Node, produced: Node, scope: InferScope) -> RefinementInhabitance? { + let declared_chain = refinement_chain_names(n: declared, scope: scope) + let produced_chain = refinement_chain_names(n: produced, scope: scope) + match declared_chain |> first { + Absent => none + Present { value: declared_head } => + match produced_chain |> first { + Absent => none + Present { value: produced_head } => + if declared_head == produced_head { + none + } else if (declared_chain |> count) <= 1 && (produced_chain |> count) <= 1 { + none + } else if produced_chain |> any(link => link == declared_head) { + Present { value: RefinementWidensToDeclaredBase } + } else if declared_chain |> any(link => link == produced_head) { + Present { value: RefinementNarrowsToDeclaredBrand } + } else if declared_chain |> any(d => produced_chain |> any(p => p == d)) { + Present { value: RefinementPeerChains } + } else { + none + } + } + } +} + // THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating // them: coproduct_payload_where_parent_required already peels transparent aliases through // transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the @@ -3332,16 +3520,26 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco 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) { - InhabitanceRefused { reason: RefusedKernelAtStructured } - } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { - InhabitanceRefused { reason: RefusedPayloadAtParent } } else { - match nominal_product_inhabitance_refusal(declared: declared, produced: produced, scope: scope) { - Present { value: r } => InhabitanceRefused { reason: r } - Absent => Inhabits + match refinement_inhabitance(declared: declared, produced: produced, scope: scope) { + Present { value: RefinementWidensToDeclaredBase } => Inhabits + Present { value: RefinementNarrowsToDeclaredBrand } => + InhabitanceUndecidable { reason: UndecidableRefinementIntroduction } + Present { value: RefinementPeerChains } => + InhabitanceUndecidable { reason: UndecidableRefinementPeerChains } + Absent => + if kernel_value_declared_type_mismatch( + formal: declared, actual: produced, + type_env: scope.type_env, source_indices: source_indices) { + InhabitanceRefused { reason: RefusedKernelAtStructured } + } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { + InhabitanceRefused { reason: RefusedPayloadAtParent } + } else { + match nominal_product_inhabitance_refusal(declared: declared, produced: produced, scope: scope) { + Present { value: r } => InhabitanceRefused { reason: r } + Absent => Inhabits + } + } } } } @@ -3545,6 +3743,26 @@ fn nominal_product_head_name(n: Node, scope: InferScope) -> String { } } +// A WHERE-REFINEMENT IS NOT A NOMINAL PRODUCT, and the Conj test alone cannot tell them apart. +// `type NonEmptyStr = String where non_empty` and `type HostIdentity = NonEmptyStr where +// brand("HostIdentity")` both carry connective Conj with one child, which is the shape a +// one-field record also has -- so the bare Conj-with-children test admitted them to the +// nominal-product arm, where two distinct refinement names disagree and the pair refuses. +// Measured on the corpus: HostIdentity flowing into a NonEmptyStr formal, which is WIDENING TO +// ITS OWN DECLARED BASE and is correct code, refused as RefusedDistinctProductConstructor. +// +// WHY THE EXCLUSION IS THE HONEST FIX RATHER THAN A WIDENING. This arm's own contract is +// "concrete named products and their transparent aliases", and it names the shapes it does not +// handle rather than implying coverage. A where-refinement is a fourth such shape: deciding it +// needs the refinement CHAIN and its direction -- widening to a base admits, narrowing to a +// brand must not -- which is a different judgment with a different authority +// (where_refinement_chain), not a case of this one. Refusing it here would fabricate a verdict +// from a name comparison that carries no direction at all. It reaches this arm only because the +// declared side used to be stamped a generic formal and declined before any arm ran. +// +// NEXT-RUNG TRIGGER: a refinement-inhabitance relation that consumes where_refinement_chain and +// decides the two directions separately, at which point brand narrowing becomes a refusal here +// rather than an abstention. fn nominal_product_head_name_if_declared_product(name: String, scope: InferScope) -> String { let representative = transparent_alias_representative( index: scope.type_env.symbol_index, name: name) @@ -3735,6 +3953,8 @@ fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason) -> UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape" UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against" UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam" + UndecidableRefinementPeerChains => "refinement peer chains: the declared and produced refinements MEET on a shared link with neither nesting inside the other -- PEER PREDICATES over one base, measured as FilePath, GcpProjectId and Sha512DigestHex at NonEmptyStr, which are not brands at all -- so this is neither an introduction nor a brand conflict, and neither this seam nor the brand wall decides the pair" + UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult" } } diff --git a/src/v1/04_lookup.dag b/src/v1/04_lookup.dag index f2213f91889..6d8423df90b 100644 --- a/src/v1/04_lookup.dag +++ b/src/v1/04_lookup.dag @@ -627,27 +627,14 @@ fn borrowed_census_callable_candidate(type_env: TypeEnv, name: String, candidate } } -// A global-bare hit still names one exact declaration and its completed census. Resolve each -// formal at that declaration's containment position, once while that authority is present, rather -// than reconstructing it later through the caller TypeEnv. -// SEED WALKER DISPOSITION (DESIGN section 6): v1's canonical traversal idiom is a purpose-specific -// self-recursive Node collector; importing v2 fold_node/node_query here would invert the bootstrap -// because v1 compiles v2. This collector walks only the finite declaration type tree and dissolves -// with the sibling v1 walkers at the v2 self-host cut. A one-off shared walker for this carrier -// would add a traversal representation rather than consolidate the seed's existing population. -fn declaration_unbound_leaf_names(n: Node, env: TypeEnv) -> List { - let name = authored_name_at(source_indices: env.source_indices, node: n) - let here = if n.connective == NoConnective - && (n.children |> count) == 0 - && name != "" - && !contains(name, ".") - && !is_kernel_type(name: name) - && lookup_binding_by_name_local(env: env, name: name) == none { - [name] - } else { [] } - concat(here, n.children |> flat_map(ch => declaration_unbound_leaf_names(n: ch, env: env))) -} - +// THE ROSTER IS THE UNION OF TWO FACTS AND NEITHER SUBSUMES THE OTHER. fn_type_param_names reads +// the DECLARED clause; borrowed_generic_param_names reads params whose type expression is a +// childless NoConnective leaf spelled as the parameter or its type name. The second is wider on one +// axis and NARROWER on two -- it drops any declared type param whose type expression is not such a +// leaf, and any with an empty name -- so passing it alone would reclassify such a param as a +// concrete unresolved name: the exact failure the negative control below exists to prevent, +// arriving through the other door. Review finding, tidy-lynx-804, 2026-09-07. The union is what the +// pre-repair code passed and it is what is passed here; only the ABSENCE disjunct is deleted. fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String, node: Node) -> List { let tp_names = fn_type_param_names(item: node, source_indices: type_env.source_indices) let declaration_env = census_declaration_type_env( @@ -656,20 +643,8 @@ fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String tp_names: tp_names, source_indices: type_env.source_indices ) - let return_type = match node.inferred { - Present { value: Resolved { node: resolved_return } } => resolved_return - _ => match node.type_annotation { - Present { value: annotated_return } => annotated_return - Absent => error_type - } - } - let declaration_generic_names = concat( - tp_names, - concat( - declaration_unbound_leaf_names(n: return_type, env: declaration_env), - node.params |> flat_map(p => declaration_unbound_leaf_names(n: param_node_type_expr(n: p), env: declaration_env)) - ) - ) + let declaration_generic_names = borrowed_generic_param_names( + params: node.params, source_indices: type_env.source_indices) node.params |> filter(p => !(tp_names |> any(tp => tp == param_node_name_at(n: p, source_indices: type_env.source_indices)))) |> map(p => { @@ -680,7 +655,9 @@ fn census_declaration_bound_formals(type_env: TypeEnv, owner_module_path: String declaration_bound_conformance: preserve_outer_optional_cardinality( outer: declared_type, inner: peel_nominal_alias_identity(n: declared_type, env: declaration_env, module_name: owner_module_path)), - substitution_basis: declaration_substitution_basis(n: declared_type, env: declaration_env, generic_names: declaration_generic_names) + substitution_basis: declaration_substitution_basis( + n: declared_type, env: declaration_env, + generic_names: concat(tp_names, map_keys(declaration_generic_names))) } }) } diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index aa756d07de4..02aaf22693c 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -9,6 +9,7 @@ use self::InhabitanceRefusalReason::*; use self::InhabitanceUndecidableReason::*; use self::InhabitanceVerdict::*; use self::LiteralBoundary::*; +use self::RefinementInhabitance::*; use self::ServiceConfigFieldJudgment::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, @@ -4584,6 +4585,8 @@ pub enum InhabitanceUndecidableReason { UndecidableOptionalCarrier, UndecidableFormalUnresolved, UndecidableProducedIdentityErased, + UndecidableRefinementIntroduction, + UndecidableRefinementPeerChains, } #[derive( @@ -4638,6 +4641,171 @@ pub fn declared_type_position_label(position: DeclaredTypePosition, subject: Str } } +pub fn refinement_chain_link_identity(link: Rc, type_env: Rc) -> Option { + match crate::v1_compiler_infer_env::lookup_type_for(type_env.clone(), link.clone()) { + Some(declaration) => where_refinement_brand_declaration_site( + declaration.clone(), + type_env.source_indices.clone(), + ), + std::option::Option::None => std::option::Option::None, + } +} + +pub fn refinement_chain_link_identities( + links: Rc>>, + type_env: Rc, +) -> Rc> { + { + let identified = Rc::new({ + let mut __result = Vec::new(); + for id in Rc::new({ + let mut __result = Vec::new(); + for site in Rc::new({ + let mut __result = Vec::new(); + for site in Rc::new({ + let mut __result = Vec::new(); + for link in links.iter().cloned() { + __result.push(refinement_chain_link_identity( + link.clone(), + type_env.clone(), + )); + } + __result + }) + .iter() + .cloned() + { + if (site.clone() != std::option::Option::None) { + __result.push(site); + } + } + __result + }) + .iter() + .cloned() + { + __result.push(match site.clone() { + Some(id) => id.clone(), + std::option::Option::None => "".to_string(), + }); + } + __result + }) + .iter() + .cloned() + { + if (id.clone() != "".to_string()) { + __result.push(id); + } + } + __result + }); + if ((identified.clone().len() as i64) == (links.clone().len() as i64)) { + identified.clone() + } else { + Rc::new(vec![]) + } + } +} + +pub fn refinement_chain_names(n: Rc, scope: Rc) -> Rc> { + match crate::v1_compiler_infer_env::lookup_type_for(scope.type_env.clone(), n.clone()) { + Some(declaration) => refinement_chain_link_identities( + where_refinement_chain(declaration.clone(), scope.type_env.clone()), + scope.type_env.clone(), + ), + std::option::Option::None => Rc::new(vec![]), + } +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum RefinementInhabitance { + RefinementWidensToDeclaredBase, + RefinementNarrowsToDeclaredBrand, + RefinementPeerChains, +} + +pub fn refinement_inhabitance( + declared: Rc, + produced: Rc, + scope: Rc, +) -> Option { + { + let declared_chain = refinement_chain_names(declared.clone(), scope.clone()); + let produced_chain = refinement_chain_names(produced.clone(), scope.clone()); + match declared_chain.clone().first().cloned() { + std::option::Option::None => std::option::Option::None, + Some(declared_head) => match produced_chain.clone().first().cloned() { + std::option::Option::None => std::option::Option::None, + Some(produced_head) => { + if (declared_head.clone() == produced_head.clone()) { + std::option::Option::None + } else { + if (((declared_chain.clone().len() as i64) <= 1) + && ((produced_chain.clone().len() as i64) <= 1)) + { + std::option::Option::None + } else { + if { + let mut __found = false; + for link in produced_chain.iter().cloned() { + if (link.clone() == declared_head.clone()) { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementWidensToDeclaredBase) + } else { + if { + let mut __found = false; + for link in declared_chain.iter().cloned() { + if (link.clone() == produced_head.clone()) { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementNarrowsToDeclaredBrand) + } else { + if { + let mut __found = false; + for d in declared_chain.iter().cloned() { + if { + let mut __found = false; + for p in produced_chain.iter().cloned() { + if (p.clone() == d.clone()) { + __found = true; + break; + } + } + __found + } { + __found = true; + break; + } + } + __found + } { + Some(RefinementInhabitance::RefinementPeerChains) + } else { + std::option::Option::None + } + } + } + } + } + } + }, + } + } +} + pub fn declared_type_inhabitance( obligation: Rc, scope: Rc, @@ -4712,41 +4880,33 @@ pub fn declared_type_inhabitance( InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - if kernel_value_declared_type_mismatch( - declared.clone(), - produced.clone(), - scope.type_env.clone(), - source_indices.clone(), - ) { + match refinement_inhabitance(declared.clone(), produced.clone(), scope.clone()) { + Some(RefinementInhabitance::RefinementWidensToDeclaredBase) => Rc::new(InhabitanceVerdict::Inhabits), + Some(RefinementInhabitance::RefinementNarrowsToDeclaredBrand) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableRefinementIntroduction, +}), + Some(RefinementInhabitance::RefinementPeerChains) => Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableRefinementPeerChains, +}), + std::option::Option::None => if kernel_value_declared_type_mismatch(declared.clone(), produced.clone(), scope.type_env.clone(), source_indices.clone()) { Rc::new(InhabitanceVerdict::InhabitanceRefused { reason: InhabitanceRefusalReason::RefusedKernelAtStructured, }) } else { - if coproduct_payload_where_parent_required( - declared.clone(), - produced.clone(), - scope.clone(), - ) { + 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(), - }, - ), - std::option::Option::None => { - Rc::new(InhabitanceVerdict::Inhabits) - } - } + match nominal_product_inhabitance_refusal(declared.clone(), produced.clone(), scope.clone()) { + Some(r) => Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: r.clone(), +}), + std::option::Option::None => Rc::new(InhabitanceVerdict::Inhabits), +} } - } + }, +} } } } @@ -5153,6 +5313,8 @@ pub fn inhabitance_undecidable_reason_label(reason: InhabitanceUndecidableReason InhabitanceUndecidableReason::UndecidableOptionalCarrier => "optional carrier: the language's own cardinality carrier, where a T standing in an Optional position is the declared spelling rather than a payload escape".to_string(), InhabitanceUndecidableReason::UndecidableFormalUnresolved => "formal unresolved: the declared type did not resolve to a declaration, so there is nothing to judge inhabitance against".to_string(), InhabitanceUndecidableReason::UndecidableProducedIdentityErased => "produced identity erased: the produced value's type identity is not recoverable at this seam".to_string(), + InhabitanceUndecidableReason::UndecidableRefinementPeerChains => "refinement peer chains: the declared and produced refinements MEET on a shared link with neither nesting inside the other -- PEER PREDICATES over one base, measured as FilePath, GcpProjectId and Sha512DigestHex at NonEmptyStr, which are not brands at all -- so this is neither an introduction nor a brand conflict, and neither this seam nor the brand wall decides the pair".to_string(), + InhabitanceUndecidableReason::UndecidableRefinementIntroduction => "refinement introduction: the produced value sits at or above the declared refinement on its own chain and carries no cast to it, so whether it was INTRODUCED at that refinement is the literal-elaboration verdict for its destination, which this seam does not consult".to_string(), } } @@ -26561,6 +26723,10 @@ pub struct UndecidableFormalUnresolved; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct UndecidableProducedIdentityErased; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableRefinementIntroduction; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableRefinementPeerChains; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedPayloadAtParent; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedKernelAtStructured; @@ -26568,3 +26734,9 @@ pub struct RefusedKernelAtStructured; pub struct RefusedDistinctProductConstructor; #[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] pub struct RefusedDistinctAppliedTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementWidensToDeclaredBase; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementNarrowsToDeclaredBrand; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefinementPeerChains; diff --git a/src/v1/stage0/src/v1_compiler_infer_env.rs b/src/v1/stage0/src/v1_compiler_infer_env.rs index ca167b72ba9..b950bd34fb7 100644 --- a/src/v1/stage0/src/v1_compiler_infer_env.rs +++ b/src/v1/stage0/src/v1_compiler_infer_env.rs @@ -1790,7 +1790,7 @@ pub fn declaration_substitution_basis( let generic_leaf = ((((n.connective.clone() == Connective::NoConnective) && ((n.children.clone().len() as i64) == 0)) && (name.clone() != "".to_string())) - && ({ + && { let mut __found = false; for g in generic_names.iter().cloned() { if (g.clone() == name.clone()) { @@ -1799,10 +1799,7 @@ pub fn declaration_substitution_basis( } } __found - } || ((!v1_rt::contains(name.clone(), ".".to_string()) - && !crate::std_types::is_kernel_type(name.clone())) - && (lookup_binding_by_name_local(env.clone(), name.clone()) - == std::option::Option::None)))); + }); if generic_leaf.clone() { node_with_inferred( with_children.clone(), diff --git a/src/v1/stage0/src/v1_compiler_infer_lookup.rs b/src/v1/stage0/src/v1_compiler_infer_lookup.rs index 2e1f41289d0..afbfb33e19e 100644 --- a/src/v1/stage0/src/v1_compiler_infer_lookup.rs +++ b/src/v1/stage0/src/v1_compiler_infer_lookup.rs @@ -684,40 +684,6 @@ pub fn borrowed_census_callable_candidate( } } -pub fn declaration_unbound_leaf_names(n: Rc, env: Rc) -> Rc> { - stacker::maybe_grow(512 * 1024, 2 * 1024 * 1024, || { - let name = crate::v1_std_core::authored_name_at(env.source_indices.clone(), n.clone()); - let here = if ((((((n.connective.clone() == Connective::NoConnective) - && ((n.children.clone().len() as i64) == 0)) - && (name.clone() != "".to_string())) - && !v1_rt::contains(name.clone(), ".".to_string())) - && !crate::std_types::is_kernel_type(name.clone())) - && (crate::v1_compiler_infer_env::lookup_binding_by_name_local( - env.clone(), - name.clone(), - ) == std::option::Option::None)) - { - Rc::new(vec![name.clone()]) - } else { - Rc::new(vec![]) - }; - v1_rt::concat( - here.clone(), - Rc::new({ - let mut __result = Vec::new(); - for ch in n.children.clone().iter().cloned() { - __result.extend( - (*declaration_unbound_leaf_names(ch.clone(), env.clone())) - .iter() - .cloned(), - ); - } - __result - }), - ) - }) -} - pub fn census_declaration_bound_formals( type_env: Rc, owner_module_path: String, @@ -734,35 +700,9 @@ pub fn census_declaration_bound_formals( tp_names.clone(), type_env.source_indices.clone(), ); - let return_type = match node.inferred.clone().as_deref().cloned() { - Some(InferredNode::Resolved { - node: resolved_return, - .. - }) => resolved_return.clone(), - _ => match node.type_annotation.clone() { - Some(annotated_return) => annotated_return.clone(), - std::option::Option::None => error_type(), - }, - }; - let declaration_generic_names = v1_rt::concat( - tp_names.clone(), - v1_rt::concat( - declaration_unbound_leaf_names(return_type.clone(), declaration_env.clone()), - Rc::new({ - let mut __result = Vec::new(); - for p in node.params.clone().iter().cloned() { - __result.extend( - (*declaration_unbound_leaf_names( - crate::v1_std_core::param_node_type_expr(p.clone()), - declaration_env.clone(), - )) - .iter() - .cloned(), - ); - } - __result - }), - ), + let declaration_generic_names = crate::v1_compiler_infer_env::borrowed_generic_param_names( + node.params.clone(), + type_env.source_indices.clone(), ); Rc::new({ let mut __result = Vec::new(); @@ -813,7 +753,10 @@ pub fn census_declaration_bound_formals( crate::v1_compiler_infer_env::declaration_substitution_basis( declared_type.clone(), declaration_env.clone(), - declaration_generic_names.clone(), + v1_rt::concat( + tp_names.clone(), + Rc::new(v1_rt::map_keys(&declaration_generic_names)), + ), ), }) });