Skip to content

Namespace PR-4d: v1 global-unique bare fallback in lookup_binding_by_name — unblocks src/v1 import strip; witnesses + regen - #6595

Merged
briansrls merged 20 commits into
mainfrom
session/sleek-crab-599
Jul 14, 2026
Merged

briansrls merged 20 commits into
mainfrom
session/sleek-crab-599

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jul 14, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Namespace PR-4d: adds a corpus-wide global-unique bare-name fallback to v1 lookup_binding_by_name, unblocking the upcoming src/v1 import strip.

  • TypeEnv.global_bare carries a precomputed census (build_global_bare_census) built once over graph.modules before typecheck — order-independent, mirrors v2 symbol_index_global_bare.
  • lookup_binding_by_name consults it only after str_bindings / ancestry_str_bindings / intern+bindings all miss; GlobalBareUniqueBinding resolves, GlobalBareAmbiguousBinding stays absent (fail-closed per §5).
  • Rust seed + .dag authority updated in lockstep; regen_stage0 --verify green (regen_divergence_count=0).
  • Follow-on commit fixes compile-clean gate blockers inherited from main (fleet_converge_cli exhaustive HostEffect match; expressions.dag if-branch split for v2 unification).

Test plan

  • regen_stage0 --verify — regen_divergence_count=0
  • cargo test -p v1-compiler-tests global_bare — 2/2 passed
  • CI floor (dag_compile_clean_gate + full witness corpus) — green on 431b45910 (build / ci / emit_determinism)

briansrls and others added 15 commits July 14, 2026 06:44
Optional<T> literals in this dialect are constructed via `none`; a bare
Absent expression (unprecedented outside match arms) tripped the
checker into inferring one if-branch as Product(TypeBinding) instead
of Coproduct(Optional).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@briansrls
briansrls marked this pull request as ready for review July 14, 2026 10:12
…tch in fleet_converge_cli and split parse_atom_with for v2 if-branch unification.

Co-authored-by: Cursor <cursoragent@cursor.com>

@gunbai-bot gunbai-bot Bot left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review — Namespace PR-4d: global-unique bare fallback

Reviewed as coordinator-requested help toward merge readiness (Wave-0 step b). Design is sound; approving with two minor, non-blocking notes.

What it does

Adds a corpus-wide bare-name census (global_bare: Map<String, GlobalBareLookupState>, GlobalBareUniqueBinding | GlobalBareAmbiguousBinding) built once over graph.modules, consulted by lookup_binding_by_name only after str_bindings / ancestry_str_bindings / intern+bindings all miss. A globally-unique bare name resolves; an ambiguous one stays Absent. This is what lets a bare reference whose disambiguating import was stripped still resolve — iff its name is globally unique.

Strengths

  • Single-authority classification (the standout). local_binding_for_item is extracted from the prior inlined build_type_env local-bindings fold and now feeds both the per-module local bindings and build_global_bare_census. The census therefore cannot drift from the real binding construction — a §2/§3 correct-by-construction move, and it makes the refactor behavior-preserving for local bindings.
  • Fail-closed (§5). GlobalBareAmbiguousBinding => Absent — never guesses. Correct.
  • Correct precedence. Local/ancestry/intern scope always wins; the global fallback is strictly last. No shadowing regressions.
  • Collision-honest, order-independent census. census_insert_binding is idempotent for a structurally-identical re-sighting and promotes to Ambiguous on a structural difference; built once before any module typechecks, so it's fold-order-independent.
  • Coverage. New type_env_scope_chain_test, variant_export_surface_witness, transitive_interface_binding, and the reworked union_resolve_receipts exercise the path.

Notes (non-blocking)

  1. PR body is still the template TODO. The attestation checklist (what/why summary, test command + result) is unfilled — worth completing before merge since reviewers read it first.
  2. census_insert_binding dedup semantics. Two same-named declarations in different modules with structurally identical resolved nodes stay Unique (treated as one authority — the benign re-export / v1-seed-dup case). That matches the co-residence pattern and is the right call, but it does mean a genuine two-authority fork that happens to be structurally identical would resolve rather than refuse. Given the census's job (unblock unique bare refs) this is acceptable; flagging so it's a conscious choice, not an accident.

Verdict

Correct, conventional, fail-closed, well-tested, and CI-green. Approving.

briansrls and others added 2 commits July 14, 2026 17:43
…e_cli HostEffect match (take main's _ => fallback arm).

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Jul 14, 2026

Copy link
Copy Markdown
Contributor Author

Dashboard relayed two APPROVE review artifacts for #6587 (P5b srv3 host_effect_apply migration), including a non-blocking note about SshShell string concat in host_effect_realize.dag.

Verified against current #6595 head (947a63ace8): this PR does not touch host_effect_realize.dag, srv3_*, or host_effect_apply — scope is v1 namespace PR-4d (global_bare census + lookup_binding_by_name fallback, witnesses, compile-clean). The #6587 finding is valid on that PR but out of scope here; no fix commit on this branch.

Merge readiness for #6595: claude + cursor APPROVE on latest head, no REQUEST_CHANGES on latest head, mergeable=MERGEABLE; awaiting CI on post-conflict-resolve push.

— sent from snappy-swift-211

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant