Climb import-less UniqueBare from proximity to lexical on-chain binding

[gunbai-bot]

Summary

• Import-less UniqueBare no longer ranks by longest shared prefix among homonyms. Unique on-chain → UniqueBare; census-unique off-chain GlobalBareUniqueBinding → UniqueBare (kept; dropping the reader edge alone would undercount); two-or-more on-chain → AmbiguousBare; homonyms with no unique binder → no UniqueBare.
• Discriminating RED on dependency_resolution_facts: sibling plant vs ancestor. Captured on merge-base ranking (entry_resolve.rs identical at 17ebbde83b and 82a3edfea3): proximity UniqueBare bound the sibling plant: ["frontier.child.plant"].
• Two populations in the RFM: (a) LCP ranking climb is rung 2 on the producer; (b) GlobalBareUniqueBinding residual stays outside the lexical guarantee. The row's minimum is (b). Ceiling 3. Trigger: canonical acceptance and this producer change together (forbid bindings without lexical authority, not off-chain references in general).
• Homonym compile control greps Debug text for blocking diagnostics containing shared plus not-found/undefined/AMBIGUOUS/unresolved — not a typed variant plus file/span.
• Env-gated dump test deleted; corpus delta is a one-off receipt on this PR.

1) Fail-open

UniqueBinding still accepts a census-unique off-chain name (unique_off_chain_bare_name_compiles_and_keeps_its_uniquebare_edge). The producer therefore emits that UniqueBare. Do not drop those edges from the reader alone.

Drop of a UniqueBare is only for homonyms with no unique on-chain binder. Path: load_sources_for_entry_with_pool → compile_sources (not resolve_entry_with_index). Evidence: Debug-rendered blocking diagnostics; not a typed-and-located diagnostic identity.

2) Corpus dependency_resolution_facts delta (dag+src/v2)

One-off measurement at sha 6a56a0a215090cea40205e5a5a66b9a92a0f0fb0. Command:

GUNBC_DUMP_DEP_FACTS=1 cargo test --release -p v1-compiler --lib cli_run::reference_edge_producer_tests::dump_dependency_resolution_facts_when_env_set -- --nocapture --exact

DEPFACT_DELTA union_before=55085 union_after=55085 union_dropped=0 union_added=0 uniquebare_dropped=0 uniquebare_added=0

3) Rung

(a) LCP ranking among homonyms: mechanically preventable (2) on the UniqueBare producer. (b) GlobalBareUniqueBinding: outside the lexical guarantee until resolver and producer change together. Row minimum is (b). Ceiling 3.

4) RED sha

Failing line: proximity UniqueBare bound the sibling plant: ["frontier.child.plant"]
Remote checkout sha: 17ebbde83bec38c472a436ff05251c1422dc4334. Merge base: 82a3edfea341b64e160ac9e49bac4d73682912e4.

Rust controls (not PR CI)

rust-unit-tests is skipped on pull_request. RED, positive, and loader inhabitance were run on exact head 19f6a5b14a via ctrl-build (remote BuildBuddy runner docker://ghcr.io/gunb-ai/ctrl-session:latest), invocation https://app.buildbuddy.io/invocation/d26a11c1-fee2-4c73-9432-bd70db7e2e8c :

cargo test --release -p v1-compiler --lib -- proximity_must_not_bind_an_importless_bare_name_to_a_sibling_homonym an_importless_bare_name_on_the_ancestor_chain_still_resolves load_sources_binds_the_on_chain_ancestor_not_the_sibling_plant -- --nocapture

Names:

• RED: cli_run::reference_edge_producer_tests::proximity_must_not_bind_an_importless_bare_name_to_a_sibling_homonym
• positive: cli_run::reference_edge_producer_tests::an_importless_bare_name_on_the_ancestor_chain_still_resolves
• inhabitance: cli_run::closure_edge_demand_tests::load_sources_binds_the_on_chain_ancestor_not_the_sibling_plant

test result: ok. 3 passed; 0 failed; 0 ignored; 0 measured; 1170 filtered out; finished in 0.01s.

Test plan

• RED + positive + inhabitance on ctrl-build as above
• Corpus dump recorded
• PR witnesses on 19f6a5b14a (37782059414)

Do not merge.

[briansrls]

REQUEST_CHANGES at exact head 8d84e04133b6d2d227aa19a8322abbd56ad6080e. One P2 in the committed rung account. The proximity-ranking removal itself is a useful, bounded repair; I am not requesting that its surviving resolver fallback be removed from the dependency reader alone.

P2 — The stated minimum rung 2 does not hold for this row's whole invalid-state population

The row defines its invalid state as a dependency edge to a declarer the source does not lexically bind, and its review tell explicitly includes an edge justified only by one pool declarer. The new row then states The minimum across in-scope paths is 2 while documenting—and positively testing—the continued acceptance of exactly that off-chain case.

pick_importless_bare's mods.len() == 1 arm is NOT a lexical-scope proof. In the pinned canonical v1.compiler.infer_env::global_bare_lookup_candidates, GlobalBareUniqueBinding returns the binding without checking the referencing module's ancestor chain. The new unique_off_chain_bare_name_compiles_and_keeps_its_uniquebare_edge deliberately proves that test.user can call test.decl.shared_fn without an import or ancestor relationship. There is still no refusal or wrong-binding discriminator for that part of the row's declared class. It remains outside the ladder under the lexical contract the row states, not mechanically prevented merely because the more specific sibling-ranking bug has a regression test.

Distinguish these two populations in the committed account: (a) the removed longest-common-prefix ranking mismatch, with its producer RED/ancestor positive and the actual tested boundary; (b) the surviving off-chain census-unique acceptance, explicitly still outside the lexical guarantee until the canonical resolver and graph producer change together. Keep ceiling 3 at source -> accepted graph and retain the capability trigger and permanent controls. A written import is a legitimate lexical binding even when its target is not an ancestor; phrase the guarantee as 'no binding without lexical authority', not a blanket ban on off-chain references. No new row, broad census, new test lane or complete resolver rewrite is required to land the honest bounded improvement.

Answer to the binding question

At the dependency-reader boundary this is not a newly invented second fallback: it intentionally mirrors the existing resolver's UniqueBinding acceptance. At the language-scope boundary, census uniqueness is still not lexical binding. The distinction is important: dropping that edge while the compiler still accepts the call would undercount a real accepted dependency and make affected-set selection fail open. Repair the canonical acceptance policy and edge derivation together when closing that residual; do not make this reader look lexically clean by hiding it.

The on-chain predicate is containment, not similarity: equality or a full module-segment prefix. It avoids the sibling plant, and both reference_edges_for_file_on_demand and reference_targets_of use the shared pick. Two on-chain candidates remain ambiguous rather than silently choosing one. The retained unique-off-chain edge is openly accounted for.

Refusal and controls: exact scope

The wrong-edge RED drives dependency_resolution_facts itself, asserts that the planted sibling is absent AND that the ancestor is present. The ancestor-only positive and loader inhabitance are useful; an always-empty answer fails them. The off-chain-homonym test loads the fixture then calls v1_compiler_compile::compile_sources, filters interpreter-blocking diagnostics, and checks the missing-call text. The producer itself returns no edge for this unresolved case; it does not mint a typed refusal there.

Do not call that test a verification of a particular diagnostic class and source locus: it joins Debug-rendered messages and accepts several substrings, without asserting a diagnostic variant, file or span. It demonstrates blocking compile failure on that fixture, not independently verified typed-and-located identity. Also correct the RFM's resolve_entry_with_index refuses description to the actual load_sources_for_entry_with_pool -> compile_sources path it invokes. Strengthening that existing assertion to the diagnostic's own kind/name/location would make the location claim falsifiable; no claim of a missing location in the actual compiler is made by this review.

Verification

The commit-filtered workflow is 37743729232, successful. Seed, generated, floor, emit-build and witnesses succeeded; Rust unit tests were skipped on this PR run. All-target lint and one-emission mirror checking succeeded. The new tests are ordinary cfg(test) library controls, but this PR run is not evidence they executed. The main RED, post-fix targeted runs and 55,085 -> 55,085 corpus edge comparison remain author-run evidence; I did not independently execute them or certify the global delta. An unchanged corpus delta also says nothing about the invalid fixture population.

Reviewed the complete three-file diff, pinned RFM, canonical binding code, relevant host reader source, DESIGN §4b/§5, and exact-head CI metadata. No local compiler build, new mutant, merge or enqueue. Preserve the code repair; correct the durable scope/rung account before landing.

[gunbai-bot]

review 77933: the fork was real. module_path_is_containment_ancestor is deleted. on_chain_declarers now filters through v1_compiler_infer_env::type_ref_module_path_is_containment_prefix (segment LCP), the same predicate global_bare_chain_candidates applies per candidate. Did not wrap census paths as dummy GlobalBareCandidates — that would mint a TypeBinding the edge producer does not have.

Head 3bafc5c2a0. Sibling RED + ancestor positive + UniqueBinding keep + homonym refuse still green.

— sent from loyal-boar-448

[gunbai-bot]

review 5454183451 (P2 rung account at 8d84e04): the row now splits the two populations. (a) LCP ranking among homonyms: producer RED enrolled, rung 2 on that producer path. (b) census-unique off-chain UniqueBinding: still outside the ladder under the lexical contract; UniqueBare kept so the reader does not undercount an accepted call. The row's minimum is that residual, not 2. Homonym control is described as compile_sources over load_sources_for_entry_with_pool, blocking compile failure, not typed diagnostic identity. Ceiling 3 and the capability trigger kept; lexical authority includes a written import.

review 77933: containment fork deleted on 3bafc5c2a0 (type_ref_module_path_is_containment_prefix).

Head e5b5539a2c. Not merging.

— sent from loyal-boar-448

[gunbai-bot]

review 77937: the copy-destination declared-gap comment is restored to destination is new-at-path by the same argument as \rename to`. It was mangled in 6a56a0a215 (unrelated UniqueBare edit). Head 1b44bf6`.

Advisory (seed growth): no census/deferral row added. This is admitted v1-maintenance — close silent UniqueBare wrongness on the producer the v2 build path consumes. The proximity ranker (module_prefix_shared_len and both callers) is deleted at the root; pick_importless_bare is that replacement, not a second path beside it. A seed-census ledger for this one function would be a parallel authority for a fact the diff already shows.

— sent from loyal-boar-448

[briansrls]

APPROVE at exact head 19f6a5b14aa5a79e7b5e62a12c09fb2e0dd19e1a, re-reviewing 5454183451. The blocking P2 is resolved. No new blocking code finding.

The committed RFM now gives rung 2 only to the removed longest-common-prefix ranking among homonyms at the UniqueBare producer boundary. It explicitly leaves census-unique off-chain GlobalBareUniqueBinding outside the lexical guarantee and makes that residual, not 2, the row's minimum. Ceiling 3 is the future source -> accepted-graph guarantee, not a claim already achieved. The trigger couples canonical acceptance with edge derivation, and correctly permits written imports as lexical authority. Keeping the currently accepted unique-off-chain dependency visible is correct; dropping only that reader edge would undercount.

The producer RED is discriminating: proximity_must_not_bind_an_importless_bare_name_to_a_sibling_homonym calls the real dependency_resolution_facts union, rejects frontier.child.plant, AND requires frontier. An always-empty answer fails. The ancestor-only positive requires the exact target set ["frontier"]. The old ranker chooses the sibling on this fixture; I verified that entry_resolve.rs at the reported RED checkout 17ebbde83b and merge base 82a3edfea3 has the same blob SHA, 8e3b7850e61221bbcdd6660607dd0c3bcfe97a9c. The current reader uses the shared pick instead, retaining explicit Unique/Ambiguous/None outcomes and the canonical containment predicate. This supports the bounded producer claim, not a universal lexical-binding guarantee.

Execution attribution: the body names BuildBuddy invocation d920b80a-3893-4169-9fa9-421ebee90a67, its four selected lib controls and reported 4-pass result. Comparing tested checkout 1b44bf6438 with this head yields only the RFM edit, so the Rust implementation and controls are unchanged. These are author-run receipts: I could not open the raw BuildBuddy log, and did not independently replay either the pre-fix RED or the passing controls. The listed four-test command does NOT include the separate load_sources_binds_the_on_chain_ancestor_not_the_sibling_plant inhabitance test; its source is present, but that command is not execution evidence for it. Likewise, the zero corpus delta is the dated one-off receipt on 6a56a0a215, not a new measurement of this head or evidence closing the invalid fixture population.

The refusal route is now correctly named load_sources_for_entry_with_pool -> compile_sources, and no typed diagnostic variant/file/span guarantee is claimed. One non-blocking wording nit remains: the RFM says the control asserts the full sentence function 'shared' not found in scope; the actual assertion accepts shared plus one of several diagnostic fragments. The PR body already describes that accurately. Describe the RFM assertion the same way; no stronger test or new lane is required for this repair.

Exact-head workflow 37782059414 succeeded, including generated/all-target lint, floor and emit-build; rust-unit-tests was skipped. I do not credit that PR workflow as execution of the Rust controls. No merge or enqueue performed.

[gunbai-bot]

review 77950: already on head 19f6a5b14a (receipt-only, UniqueBare keep-arm unchanged).

The row no longer says the minimum is 2. RUNG NOW splits (a) LCP-among-homonyms ranking (rung 2 on the UniqueBare producer) from (b) GlobalBareUniqueBinding off-chain UniqueBare, still outside the lexical guarantee; the row's minimum is (b). Ceiling 3 and the joint resolver+producer trigger stay. pick_importless_bare's mods.len() == 1 arm is still there on purpose.

EVIDENCE no longer says resolve_entry_with_index refuses. The homonym control is named as load_sources_for_entry_with_pool → compile_sources, Debug-joined blocking text, not typed-and-located diagnostic identity.

— sent from loyal-boar-448

[gunbai-bot]

review 77980: the copy-destination declared-gap line is already restored on this head. parse_unified_diff_added_paths reads destination is new-at-path by the same argument as \rename to` (1b44bf6, still in 19f6a5b`). No further hunk to revert.

Advisory (hand-Rust / no seed census): no census or deferral row. The change is admitted v1-maintenance (close silent UniqueBare wrongness on the producer the v2 path consumes). module_prefix_shared_len and both callers are deleted; pick_importless_bare is that replacement, not a second path.

— sent from loyal-boar-448

[gunbai-bot]

Superseded by #13641 (v1 closeout): this head is an ancestor of integration/v1-closeout.