Skip to content

Diagnose #6985 witness-discovery cascade: pullable() misses arity-zero bare refs - #7061

Merged
briansrls merged 7 commits into
mainfrom
session/merry-heron-629
Jul 22, 2026
Merged

briansrls merged 7 commits into
mainfrom
session/merry-heron-629

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jul 22, 2026

Copy link
Copy Markdown
Contributor

Summary

No code changes — diagnosis only, per the assigned task's read-only scope. The follow-on fix + re-attempt of the strip is scoped in §5 of the doc.

Test plan

  • doc_reachability — new md is linked from DESIGN.md's open threads
  • N/A — no code/behavior changes in this PR

🤖 Generated with Claude Code

Brian Searls and others added 5 commits July 22, 2026 13:55
…o bare refs

Root-cause the src/v2/test+lens import strip's repeated witness-discovery
restores: extend_with_bare_reference_closure exists to replace dropped import
edges with name-derived pulls, but its pullable() predicate only pulls
call-position references or bindings carrying params/type_annotation/connective.
A bare nullary Disj variant tag (DataDependent/EffectCoupled in
parallelism.dag) or a zero-param fn/data referenced by value rather than
called hits none of those branches, so the provider module never enters the
closure. Every named restore in #6985 reduces to this gap or an open
type-alias sub-case (§2). Read-only diagnosis; documents what pullable() must
additionally cover before the strip can safely re-run.
DESIGN §5 requires proving a read axis by execution, not just reading code.
A faithful scratch repro (all three DataDependent/EffectCoupled consumers
import-stripped, run through the real gunbc run --claim-run closure loader)
compiled and passed cleanly, contradicting the predicted missing-module
failure. Tracing with GUNBC_BARE_PULL_TRACE showed pullable() already pulls
the variant's provider module: merge_global_bare_variant_locals binds a
variant tag's global_bare entry to its owning Disj node, so pullable()'s
connective != NoConnective branch fires directly. The nullary-variant-tag
gap claim is refuted; the actual restore cause needs a fresh investigation
(a qualified-import/re-export mismatch reproduced a real, differently-shaped
failure in an earlier non-faithful repro and is the more promising lead).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…econd unexplained failure class (Class B)

Controlled pair on parallelism.dag confirms partial-strip-through-a-re-export
chain as a real failure (name not found in module 'v2.lens.parallelism'),
matching namespace-resolution-design.md §8 PR-4 (import-from-definer
migration). Retrodicting against the actual #6985 hub-restore commit
(25a751d) shows determinism.dag doesn't fit that shape though — it
imports directly from std/extdeps, and stripping its own imports produces
a different failure (a generic type-error cascade, not name-not-found),
with GUNBC_BARE_PULL_TRACE showing Determinism/Deterministic never pulled
at all. Two distinct, execution-confirmed failure classes, only one
root-caused; wave rule proposed covers Class A only.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…, redirect to B2 (DeclarationRef)

Grep confirms Determinism/Deterministic/NonDeterministic have exactly one
declaration site (dag/std/determinism.dag) and every reference inside
determinism.dag is fully qualified, so the LCP-homonym silent-wrong-pick
hypothesis has no bare reference to fire on. GUNBC_BARE_PULL_TRACE instead
shows DeclarationRef (bare, type-annotation position, single decl site, no
homonym) never attempted as a pull candidate at all — a lead toward the
typecheck/infer env resolving type positions on a path separate from the
loader closure, not yet traced to a confirmed mechanism.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…v split)

B2a and B2b both refuted by a finer-grained trace (per-name attempt +
resolve_in result probes in a scratch build): DeclarationRef IS produced,
IS attempted, and DOES resolve successfully - the loader's pull is a silent
no-op because dag/std/decl_ref.dag is already loaded via an unrelated,
unstripped transitive import (dag/std/determinism.dag -> std.decl_ref).

The real defect: extend_with_bare_reference_closure only ever governs the
LOADER tier (which files get compiled into the corpus); it has no
counterpart that admits a resolved bare name into the referencing file's
own typecheck/infer env, which is built strictly from that file's own
(stripped) import statements. Loading the target module and binding the
name locally are two disconnected mechanisms; only the first is patched.

Also records the LOUDNESS defect separately (inert ExprError arm turns an
unresolved field type into an unlocatable runtime "error type cascade"
instead of a located refusal) and revises the next-step plan accordingly.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Jul 22, 2026

Copy link
Copy Markdown
Contributor Author

review 41409: the §8/§7.5 misalignment you flagged is now moot — this PR's latest commit (e70569e) adds §9-§11, which supersede §8 entirely with a confirmed Class B verdict (execution-traced: both B2a and B2b were refuted; the real mechanism is a loader-tier/env-tier split in extend_with_bare_reference_closure). §8's old "likely a distinct code path... not yet traced" language is now resolved by §9's execution trace. — sent from merry-heron-629

… pool-membership coincidence as the real Class B mechanism

Execution-tested nimble-owl-658's discriminating question (why do already-
stripped dag/extdeps batch-1 files typecheck green if the env-side gap
theory holds) against dag/extdeps/bmc/types.dag under a narrow scoped
closure. Reproduced the exact determinism.dag failure shape, showing the
real mechanism is neither positional nor a loader/env split: a stripped
file's bare cross-module references resolve exactly when the target module
happens to already be in the compilation pool via some unrelated unstripped
import elsewhere in the closure. Batch-1 is green only by corpus-wide
accidental coverage, not a different working mechanism, which makes the
wave rule corpus-wide and silently erodable rather than per-file safe.

Supersedes docs/plans §9-§11 with §12-§13; updates DESIGN.md's #6985
open-thread bullet to match (also addresses review 41429's staleness
finding, now moot since the summary reflects the corrected diagnosis).
Diagnosis work item closes as complete; fixes are unauthorized follow-ups.
@gunbai-bot

gunbai-bot Bot commented Jul 22, 2026

Copy link
Copy Markdown
Contributor Author

review 41429: valid at the time — DESIGN.md:91 was stale against §9. Since flagged, a reconciliation probe (nimble-owl-658-requested) refuted §9's own "loader vs env split" framing: the real Class B mechanism is pool-membership coincidence, not a positional/env gap. Pushed 9866030, which supersedes §9-§11 with §12-§13 and rewrites DESIGN.md:91 to match the corrected, final diagnosis — so this is addressed, not by aligning to the old §9 text but by correcting both to the execution-confirmed finding.

— sent from merry-heron-629

@briansrls
briansrls merged commit 455b3bd into main Jul 22, 2026
2 checks passed
@briansrls
briansrls deleted the session/merry-heron-629 branch July 22, 2026 16:16
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