Repository navigation
MAIN-R: the if-join judges branches against EACH OTHER, never against the declared return context — a well-typed coproduct construction is refused, and the verdict depends on corpus scope - #10294
Closed
gunbai-bot[bot] wants to merge 6 commits into
Conversation
…pool A well-typed coproduct construction is refused by the if-join, and the verdict depends on corpus scope. Both halves are filed, cross-linked, as their own classes. THE ROOT IS AN ASYMMETRY, not a precedence bug. A coproduct arm is pool-visible corpus-wide while not being a local binding under its own spelling, so an arm reference misses local lookup entirely and lands in the pool beside any foreign top-level type of that spelling. Inside the declaring module not even the unlisted-import advisory fires, which is why the specimen was silent. MEASURED, both entry-scoped, byte-identical source at fcf1347: a 21-module closure over gunbc.floor_cost_distribution compiles with 0 blocking errors; a 45-module closure adding only v2.workflow.claim_cost_observation -- which declares a same-named RightCensoredCost that the first module neither imports nor references through it -- reproduces the required-floor refusal character for character. A 3-module synthetic isolates it in a 6-module closure and is symmetric under swapping which arm collides. So the discriminating RED is reachable on the ordinary acceptance path and nothing here is permanently green. THE RULE IS ALREADY RATIFIED AND ALREADY DEFAULT ON. namespace-resolution-design.md section 13 is ancestor-chain uniqueness -- two-plus on-chain refuses AmbiguousReference, zero on-chain refuses UnresolvedType -- with NAME_RESOLUTION_POLICY_NAMESPACE_ONLY true in v1_rt. It executes on the function-signature channel and does not execute on the type and variant-arm channel, where two off-chain competitors are silently picked between and the only refusal is a consequence at an innocent site. So the next-rung trigger names a capability that is not missing but not reaching a channel. The silent-pick telemetry beside that behavior is inert in two ways, both read rather than assumed: the SILENT-PICK-GATE consults only fn_parent_first_hits, leaving the global-bare pick and tie vectors collected and never read; and resolution_silent_pick_enable is reached only after the --source-root arm has exited, so on every modern compile it is never armed at all. The if-join is its own row because the defect there is narrow and cheap: prefer_specific_type already returns the correct join for the refused pair, so the check refuses a pair it can already join. Repairing it first would silence the diagnostic while leaving the wrong binding in place, so the ordering is resolution first. No 4b(3) drop is filed. An undeclared regression filed retroactively as a declared one would launder it and hand out a runway nobody asked for; the absence of that row is part of the finding. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
Three additions to the two rows, none of them new claims. THE SPECIMEN IS COMMITTED RATHER THAN DESCRIBED. The probes that produced the 21-versus-45 result were deleted after measuring, which left the row citing executable evidence that no longer existed -- a transcription wearing a citation's clothes, since the numbers survive and the thing that produced them does not. fixtures/if_join_pool_binding carries the four modules: declaring_module is the subject and is byte-identical across both arms, colliding_module is the whole of the perturbation, and the two closure_* entry points are the red arm and its positive control. Measured here: the with-collision entry refuses at declaring_module with Coproduct(PoolSpecimenShape) vs Product(PoolSpecimenSquare); the without-collision entry reports 0 diagnostics. It sits OUTSIDE the compiled source roots deliberately. An authentic collision committed into dag or src/v2 would be a real corpus fork rather than a specimen of one, so this is source handed to the compiler by a fixture -- the position DESIGN section 4b names when it asks whether a RED is authorable. No enrollment and no assertions: the expecting-red probe lands with the wall that greens it, in the resolution lane. THE INVARIANT NOW HAS ITS NAME. Irrelevant-scope extension invariance: for source S with resolved closure C, an environment E1 derived from C and an E2 that is E1 plus declarations unreachable from S, typecheck(S, E1) must equal typecheck(S, E2). It does not. That says what went wrong -- the local judgment consumes more environment than its subject owns -- where "the verdict depends on scope" only says that something did. THE SILENT-PICK GATE CANNOT GO RED ON THIS CLASS BY CONSTRUCTION, and the row now says so in those words. It is permanently green for two independent reasons, wrong field and wrong code path, either of which alone would suffice -- so fixing one would leave it looking fixed. That is worse than an absent check because it will be cited as coverage: a reader finding a fail-closed exit 1 on silent picks concludes the class is walled. Repair or delete it, and prove the repaired RED rather than assume it. Plus independent corroboration from the lane that hit this first: a four-arm table whose decisive row holds the branch restructure constant and renames only the two arms -- green -- with its mirror restructured, green, and still forked. That isolates the collision as the cause from a direction these probes do not test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
# Conflicts: # docs/design-failure-modes.md
… not The row asserted that section 13 ancestor-chain uniqueness "does not execute on the type and variant-arm channel." That is wrong, and a wrong diagnosis in the authority for a class outlasts any approval: it sends the next reader hunting a policy bypass, which is the hypothesis this settles. SETTLED BY EXECUTION, with a discriminating pair that isolates one variable. Two same-named TOP-LEVEL types on the referencing module's chain refuse correctly -- ambiguous reference naming both declaring modules and telling the author to qualify, alias or rename. Change one candidate from a top-level type to a coproduct ARM, holding policy, chain geometry and closure size fixed, and there is no AmbiguousReference at all: the foreign product binds silently. A third-module variant gives the same result and removes the confound that the reference sat inside its own declaring module. The wall is alive; the arm is not in front of it. THEN LOCATED BY READING, because behavior had already told the wrong mechanism twice about this class. global_bare_fallback_invariant declares the rule: tracking is decl-only over type, fn and data names plus ONLY those Disj variant aliases unique across the whole bare-name space -- a variant whose name any declaration claims stays qualified-only and never becomes a candidate -- because admitting it would create a type-versus- variant tie that refuses every FAR use of the type. SO "COMPLETE THE CANDIDATE POPULATION" IS WITHDRAWN. Re-admitting arms re-creates exactly the tie the exclusion exists to prevent. What the exclusion does is trade one refusal for another and take the silent one: it protects far uses of the type at the cost of the arm's own declaring module losing its arm with no diagnostic. The decidable question is WHERE THE TIE IS REPORTED, not whether the arm is a candidate -- and the exclusion's own justification is about FAR uses, which is the asymmetry a locality-respecting rule would exploit. Three further corrections, each recorded rather than quietly fixed. The two-competing-top-level-declarations probe, which this row first offered as evidence about the policy branch, is not evidence about it. Its competitors arrive through ancestry_str_bindings -- a map with one entry per name -- so the bind is settled at map-build time and global_bare_lookup is never consulted. That is a second route to the same harm with a different cause, kept separate because folding it in would hide it, and recorded because the next reader will run that probe and misread it. global_bare_nearest_ancestor is reached only on the non-namespace-only arm and is dead code under the shipped default. Deleting it is hygiene and CENSUSES NOTHING. A census over unreachable code returns the empty set for the same reason a healthy tree does. The corroborating lane is now cited as gunbc#10210 rather than by branch commits, which do not survive squash-merge, and is named as an orthogonal perturbation axis: every probe here varies pool membership with the spelling fixed, that table varies the spelling with membership fixed, so neither alone excludes the other's confound. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XNWBhfMKV32Lvv2Z3D8WHq
# Conflicts: # dag/gunbc/recurring_failure_mode.dag # docs/design-failure-modes.md
# Conflicts: # dag/gunbc/recurring_failure_mode.dag # docs/design-failure-modes.md
briansrls
marked this pull request as ready for review
September 3, 2026 21:44
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4d079a2a83
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - **a rendered window reports its contents as the change's subject** (an instrument that renders a WINDOW AROUND a change -- a diff hunk, a context excerpt, a snippet, a log tail -- is read for WHICH SUBJECT CHANGED, and whenever the subject is WIDER THAN THE WINDOW the reader meets neighbours first and takes an identity from one of them. INVALID STATE: a change identity taken from material the renderer placed near the change rather than derived from the change itself. HARM: DESIGN section 5 silent wrongness in its most confident form -- the reader gets a SPECIFIC, PLAUSIBLE, WRONG subject, and nothing in the rendering marks the difference between a row that was shown and a row that was changed. DISCOVERED AND ANALYSED BY cool-koi-623; the mechanism was reproduced by tidy-swift-334 before routing and the diff figures below were re-executed by this author against the pull request rather than relayed. SPECIMEN, gunbc#10191 against `dag/gunbc/rung_drop.dag`. THE INSTRUMENT IS NAMED AND ITS OUTPUT IS NOT TRANSCRIBED, which this row owes twice over: a diff of that pull request against main names, in its hunk header and its context, the rows `direct_call_arg_seam_v2_exemption`, `floor_cost_claim_qualification_unavailable`, `spark_role_scoped_retirement_production_root` and `floor_cut_effect_gates`, ALL OF WHICH ARE UNTOUCHED, while filtering the same diff to lines beginning `+data` or `-data` yields the single changed row, `floor_cut_heal`. That filter IS the instrument -- one predicate over the diff, re-derivable by anyone against that pull request -- and it is the whole repair as well as the whole evidence. The row identities above are SYMBOLS and not measurements, which is why they are carried; the hunk's line numbers and the changed row's character width are neither carried nor needed, since DESIGN section 3 forbids citing a position where a symbol exists to name and section 6 forbids copying a counter where its producer can be named. What matters structurally is that the carrier's rows are single lines far wider than a screen, so the changed row's own text is off the right-hand edge while its untouched neighbours are the first thing read. THE READING FAILURE IS NOT CARELESSNESS AND THAT IS THE POINT: the hunk header answers a genuine question -- which declaration encloses line 102 -- and answers it correctly. It is simply a different question from the one the reader is asking, and the diff figures above establish that WITHOUT REFERENCE TO ANY READER. **AN INCIDENT WAS CUT FROM THIS ROW AND THE REASON IS ITSELF THE LESSON.** The class was found because approving reviews on that pull request described the change wrongly, and the natural sentence to write here is that the trap FIRES ON REAL READERS. Neither the discoverer nor this author can produce that evidence: the review texts arrived through a dashboard PUSH NOTIFICATION WITH NO CORRESPONDING PULL -- the summary exposes verdicts, the artifact paths in it do not resolve from a session, and both parties confirmed that rather than assuming it. A quotation from the discoverer would be THE SAME SOURCE and not corroboration, converting an unverifiable claim into an unverifiable claim with a witness. So the incident is out and the executed diff is what the row rests on. The discoverer named the shape correctly on themselves: a conclusion almost certainly right, backed by a channel nothing in the repository can query, which is the external-mechanism class landing in gunbc#10191 applied to its own author. A row about taking an identity from the wrong surface may not carry one taken from an unreadable one. RECOGNITION RULE, mechanical and cheap: when a carrier's rows are SINGLE-LINE and wider than a screen, never take a row identity from a hunk header or a context line. Filter to lines that actually begin `+data` or `-data`, or diff the row content directly. The review-side tell is any statement of the form THIS CHANGE TOUCHES ROW X where X can be found in the diff's unchanged material. CROSS-REFERENCE, NOT A MERGER, and the shared sentence is worth carrying: `instrument_output_read_as_subject_content` -- specifically its resolution-axis form and the P/Q/C formulation folded into it -- and this row both say AN INSTRUMENT AND ITS SUBJECT COINCIDE ONLY INSIDE A WINDOW. There the window is a CONDITION that holds for a while and lapses, and the instrument resolves to an adjacent subject; here it is SPATIAL, a rendering extent narrower than the subject, and the instrument resolves to the subject asked for and renders its NEIGHBOURS beside it. They stay separate on the repair-crossing test that row states as its own boundary method: filtering a diff to lines beginning `+data` or `-data` repairs THIS row completely and does nothing for a reading whose instrument resolved to the wrong version or the wrong name, while establishing that the instrument resolved to the subject you meant repairs THAT row and leaves this one untouched, because here it resolved correctly and the identity was taken from material rendered alongside the answer. DESIGN section 4b keys rows on the REPAIR, and these two repairs do not transfer in either direction. RUNG FOUND AT: below the ladder, silent wrongness -- the wrong subject was adjudicated and nothing anywhere refused. CEILING: 3, structurally guaranteed. THE ARGUMENT IS cool-koi-623'S AND IS PRESERVED AS THEY MADE IT, because it is what makes the trigger BUILDABLE RATHER THAN ASPIRATIONAL. The changed row's identity is derivable from the diff mechanically and cheaply -- one filter over lines beginning `+data` or `-data`, demonstrated above in a single command. So a consumer that reports THIS CHANGE ALTERS ROWS X AND Y by identity is a real wall and not a caution, and a reader consuming it cannot construct a subject the diff does not contain. A roster whose every row is aspirational stops being read, so a class that is cheap to close should say so plainly. NEXT-RUNG TRIGGER, named as the capability: a change-identity producer over row-structured carriers that derives the altered row identities from the diff and serves them to review, sufficient that no reviewer of such a carrier reads a subject off rendered context. WHAT IS NOT CLAIMED: that the renderer is defective. `git diff` is correct and its hunk header answers its own question faithfully; the defect is entirely in the JOIN, where a reader picks the identity nearest the change instead of the one that changed -- which is the same joining error `liveness_probe_read_as_currency` makes with observations, and this row is its rendering-side sibling.) | ||
| - **a stale-base branch reads as ordinary pending work, in CONTENT form with no ref-level tell** (a branch whose substantive content has ALREADY LANDED through another PR presents, after main moves on, as a perfectly ordinary feature branch: its merge-base predates the landing, so its three-dot diff against main shows only insertions and no deletions, and every sentence a reviewer would write about it -- adds the note, properly scoped, no code touched -- is ACCURATE RELATIVE TO THAT BASE and wrong relative to main. Merging it re-injects an older, smaller version of content main has since extended. **THE KNOWN FORM OF THIS HAZARD IS THE REF FORM AND IT IS NARROWER THAN THE CLASS.** The ref form announces itself: a surviving branch on a squash-merged PR, a same-sha duplicate, an auto-opened PR with a template body -- something structural to notice, and the three prior instances were all found that way. THIS instance had no duplicate ref, no auto-open and no surviving-branch signal. The only tell was that the branch's copy of the one file it touched was SHORTER THAN MAIN'S, and NOTHING IN A +73/-0 DIFF SAYS SO -- a diff renders what the branch adds to its base, never what its base is missing. SPECIMEN, 2026-09-03, gunbc#10234: main 544 lines / branch 340 lines on `src/v2/workflow/floor_pure_producer_share.dag`, merge-base 00bb2f473a, three-dot +73/-0, two-dot +225/-21. Its content had landed as gunbc#10158 and been extended by gunbc#10141. **THE HARM IS THAT THE LINE STOPS WITH THE WRONG PRESCRIPTION.** A merge conflict DID fire, so nothing merged silently and the class sits at mitigatable rather than below the floor -- but the notice instructed `rebase on main, resolve the conflicts, and push`, and following it would have produced a revert wearing a resolution's clothes. There was no content decision available to make: one side was simply stale, so a reviewer weighing the two sides was choosing between a current note and a historical copy of it while believing they were reconciling two intentions. A loud stop whose prescribed repair is the harmful arm is worse than a quiet one, because the diligence of following instructions is what causes the loss. **THE DECIDABLE CHECK, WHICH IS WHY THE CEILING IS NOT THE CURRENT RUNG:** the comparison that exposes it is mechanical and needs no judgment -- for each file a PR changes, compare the BRANCH'S version against MAIN'S rather than reading the diff, and treat main-longer-and-containing-the-branch's-additions as supersession rather than conflict. Equivalently: a merge-base that predates a merge which touched the same file is a supersession candidate, and that is computable from the ref graph alone. What is NOT decidable in general is content subsumption, so the honest gate refuses for ANALYSIS rather than auto-closing. **RUNG FOUND AT: MITIGATABLE.** The conflict contains the harm by stopping the merge; nothing computes the distinction, and the diagnostic actively misdirects. **CEILING: MECHANICALLY PREVENTABLE**, because the merge-base-versus-file-touching-merge comparison is derivable from refs and can refuse before a human is asked to resolve. Not higher: a stale branch is representable by construction -- forbidding one would mean forbidding branches from being behind, which this repository deliberately allows, since PRs here merge behind main routinely. **NEXT TRIGGER, naming the capability and not an artifact:** a producer that, for each file a pull request changes, joins the branch version against main's and against the merge-base, and emits a typed supersession verdict distinct from a content conflict -- SUFFICIENT FOR routing the two to different prescriptions, since the whole harm is that one prescription is issued for both. A checklist item asking reviewers to compare line counts would be satisfied while the capability stayed dead. **BOUNDARY against `merge_region_excludes_shared_tail`:** that class is about a conflict region resolved WRONGLY on a live carrier where both sides are current; this one is about a conflict that should never have been presented as a conflict at all. Their repairs are disjoint -- one fixes how a region is resolved, the other decides whether the region is a decision. **THE CLASS PRODUCED A CONFIRMING INSTANCE WITHIN THE HOUR, AND THE INSTANCE IS AN APPROVAL.** This row asserts that every sentence a reviewer writes about a stale-base branch is accurate relative to that base. A scheduled review of the specimen PR approved it -- `APPROVE -- annotation-only change on an existing carrier, no substrate impact`, and separately that `the revision addresses a prior codex REQUEST_CHANGES by correcting the re-derivation claim`. Both statements are true of the branch, which was 204 lines behind main, and both are unhelpful about main, where the same paragraph still carried the unrepaired sentence. So the reviewer was not careless and did not need to be: the artifact it was handed contains no representation of what main has since become, which is the whole class. That is the recorded reason this row's trigger names a PRODUCER and not reviewer diligence -- diligence is precisely what was exercised here, and it produced an approval of superseded content. **A SECOND SUB-CLAIM WAS WRITTEN HERE AND WITHDRAWN, RECORDED BECAUSE THE WITHDRAWAL IS THIS ROW'S OWN SUBJECT.** An earlier revision said the review landed twenty minutes AFTER the PR was closed, and concluded that the review scheduler does not read closure. THE ORDER IS THE REVERSE: the review completed 2026-09-03T15:39:02Z and the closure followed at 15:41:20Z, about two minutes later. Nothing in this specimen shows a scheduler reviewing a closed pull request, so the closure-semantics claim had no receipt and is withdrawn -- it may well be true of the scheduler and would need a review whose completion genuinely follows a closure. It is left in the row rather than deleted because a ledger row asserting a behaviour its own cited receipt does not show is the fabricated-citation class appearing INSIDE the row that files its neighbour, and the scoping repair is the same one that spared a true citation six lines above the note this specimen came from: repair the false claim, do not delete the true one beside it.) | ||
| - **binding chosen by pool membership rather than by the declared resolution rule** (THE ROOT IN ONE SENTENCE, AND IT IS AN ASYMMETRY: A COPRODUCT ARM IS POOL-VISIBLE CORPUS-WIDE WHILE NOT BEING A LOCAL BINDING UNDER ITS OWN SPELLING. An off-chain module that imports nothing may reference another module's arm name and receive only an ADVISORY -- unlisted import use -- never a refusal; and INSIDE the declaring module not even that advisory fires, because there the spelling is in source_visible_names. That is why the specimen was silent. INVALID STATE: two modules declare one spelling -- one as a top-level type, one as an arm of a coproduct -- and a reference to that spelling binds to whichever declaration the assembled pool happens to contain, with no diagnostic at the referencing site. THE INVARIANT THIS FALSIFIES, NAMED, because 'the verdict depends on scope' understates it -- IRRELEVANT-SCOPE EXTENSION INVARIANCE: for source S with resolved dependency closure C, an environment E1 derived from C and an environment E2 that is E1 plus declarations UNREACHABLE from S, typecheck(S, E1) must equal typecheck(S, E2). It does not. The local judgement consumes more environment than its subject owns, which is the defect in one line and is what a repair has to restore rather than merely make the specimen green. HARM: the same source is ACCEPTED under one closure and REFUSED under another, and the refusal names an innocent site in a module that neither declares nor imports the competing type. DISTINGUISHING FACT, and it is what separates this from an ordinary ambiguity: THE VERDICT FLIPS ON THE PRESENCE OF AN UNRELATED, UNIMPORTED MODULE, so closure composition -- not the source -- decides the type. SPECIMEN AND DISCRIMINATING RED, both entry-scoped and therefore reachable on the ordinary acceptance path: gunbc.floor_cost_distribution declares RightCensoredCost as an arm of ClaimCostReading while v2.workflow.claim_cost_observation declares a same-named standalone product, and the first module does not import the second; a 21-module closure over the first alone compiles with 0 blocking errors, while a 45-module closure that adds only the second reproduces the required-floor refusal character for character -- if branches resolve to incompatible types: Coproduct(ClaimCostReading) vs Product(RightCensoredCost). The isolating synthetic is three modules and a 6-module closure: A declares Shape = Circle or Square and returns one variant per if-arm; B declares an unrelated Square; C imports A and B. A never imports B, C need not import B's Square at all, and the verdict flips on B's mere presence -- symmetric under swapping which arm collides. THAT SYNTHETIC IS COMMITTED RATHER THAN DESCRIBED, because a row citing a probe that no longer exists is a transcription wearing a citation's clothes -- the numbers survive and the thing that produced them does not, so the row rots the moment anyone doubts it. It lives in fixtures.if_join_pool_binding as four modules: declaring_module holds the subject and is byte-identical across both arms, colliding_module is the whole of the perturbation, and closure_with_collision and closure_without_collision are the two entry points. Reproduce with gunbc compile --source-root dag --source-root fixtures/if_join_pool_binding --entry fixtures/if_join_pool_binding/closure_with_collision.dag, which refuses at declaring_module with Coproduct(PoolSpecimenShape) vs Product(PoolSpecimenSquare), against the same command at closure_without_collision.dag, which reports 0 diagnostics. The fixture is deliberately OUTSIDE the compiled source roots: an authentic collision committed into dag or src/v2 would be a real corpus fork, so the specimen is source handed to the compiler by a fixture, which is the position DESIGN section 4b names when it asks whether a RED is authorable. SO THE RED IS AUTHORABLE ON THE ENTRY-SCOPED PATH AND NEEDS NO WHOLE-CORPUS HARNESS, which is the DESIGN section 4b question asked before the check: nothing here is permanently green. MECHANISM, stated because the obvious reading is wrong: resolution is LOCAL-FIRST -- v1.compiler.infer_env lookup_binding_by_name tries the module's own bindings, then its ancestry bindings, then the intern table, and only on a miss reaches global_bare_lookup -- so a local declaration is not being outranked. A coproduct ARM is simply not a local binding under its own spelling, so the arm reference misses local lookup entirely and lands in the pool beside the foreign top-level type. Downstream, v1.compiler.infer lookup_variant_parent_enum and variant_owner_node widen a record literal to its owner coproduct only when the binding resolves to a Disj owning that name, so the uncollided arm widens and the collided arm stays bare -- which is the whole of the asymmetry the diagnostic reports. THE RULE THIS SUBSTRATE ALREADY HAS, AND THE REASON THIS IS NOT A CALL FOR A NEW ONE: namespace-resolution-design.md section 13, operator-ratified 2026-07-21, is ANCESTOR-CHAIN UNIQUENESS -- exactly one on-chain candidate resolves, two-plus on-chain refuses as a typed AmbiguousReference, zero on-chain refuses as UnresolvedType -- and its host bracket NAME_RESOLUTION_POLICY_NAMESPACE_ONLY defaults to TRUE. That rule is LIVE on the function-signature channel, where a cli_run test must explicitly set the policy false to assert first-hit-wins and then re-asserts that the default REFUSES the two-parent homonym. IT IS LIVE ON THE TYPE CHANNEL TOO, AND THAT IS THE FINDING -- THE RULE IS NOT BYPASSED, IT IS ASKED ABOUT AN INCOMPLETE POPULATION. THIS ROW ASSERTED THE OPPOSITE FIRST, and the retraction is kept rather than overwritten because the wrong version is the one a reader will re-derive: behavior alone said the policy was not running, and behavior alone was wrong twice about this class. THE DISCRIMINATING PAIR, entry-scoped, isolating exactly ONE variable -- same policy, same chain geometry, same closure size. TWO SAME-NAMED TOP-LEVEL TYPES both on the referencing module's chain REFUSE correctly, with the right message and the right population: ambiguous reference 'Zorkle': 2 candidates, naming both declaring modules and telling the author to qualify, alias or rename. CHANGE ONE CANDIDATE FROM A TOP-LEVEL TYPE TO A COPRODUCT ARM, holding everything else fixed, and there is NO AmbiguousReference at all: the foreign product binds silently and the refusal surfaces later as the branch-join mismatch. A third-module variant of that arm gives the same result and removes the last confound, that the reference sat inside its own declaring module. So the wall is alive and the arm is simply not in front of it. THE MECHANISM IS LOCATED IN THE SOURCE AND IT IS A DELIBERATE RULE WITH A STATED RATIONALE, not an omission: v1.compiler.infer_env global_bare_fallback_invariant declares that global_bare tracking is decl-only over type, fn and data names PLUS ONLY THOSE Disj VARIANT ALIASES THAT ARE UNIQUE ACROSS THE WHOLE BARE-NAME SPACE -- a variant whose name any type, fn or data declaration claims stays qualified-only and NEVER BECOMES A GLOBAL_BARE CANDIDATE -- because admitting it would create a type-versus-variant tie that refuses every FAR use of the type. SO THE REPAIR IS NOT TO COMPLETE THE POPULATION, and that proposal is withdrawn: re-admitting arms re-creates exactly the tie the exclusion exists to prevent. What the exclusion actually does is trade one refusal for another and take the SILENT one -- it protects far uses of the type at the cost of the arm's OWN declaring module and chain losing their arm without a diagnostic, which is DESIGN section 5's rule that a failure arm must refuse rather than widen, applied to a tie that is suppressed globally instead of reported locally. The decidable question the repair has to answer is therefore WHERE THE TIE IS REPORTED, not whether the arm is a candidate; and the exclusion's own justification is about FAR uses, which is the asymmetry a locality-respecting rule would exploit. A SECOND ROUTE TO THE SAME HARM IS DELIBERATELY NOT FOLDED IN HERE, because folding it in would hide it: when the referencing module IMPORTS both competing modules, the competitors arrive through ancestry_str_bindings, a MAP with one entry per name, so the bind is settled by whichever import won at map-build time and global_bare_lookup is never consulted at all. THAT IS WHAT THE TWO-COMPETING-TOP-LEVEL-DECLARATIONS-WITH-IMPORTS PROBE MEASURES, and it is recorded because the next reader will run it and misread it: it silently picks and reds on the picked declaration's shape, and that is evidence about the map grain, NOT about the policy branch, which is what it was first taken for. The longest-common-prefix tiebreak global_bare_nearest_ancestor is reached ONLY on the non-namespace-only arm and is therefore DEAD CODE under the shipped default, so deleting it is parallel-authority hygiene and CENSUSES NOTHING -- recorded because a census over unreachable code returns the empty set for the same reason a healthy tree does, and the two are indistinguishable in the output. It sits beside a measurement hook -- record_global_bare_ambiguous_silent_pick -- that already NAMES the behavior a silent pick in the source. THE HOOK IS NOT MERELY INERT, IT IS INERT IN TWO SEPARATE WAYS, and both were read rather than assumed. FIRST, the SILENT-PICK-GATE in the gunbc binary consults only the fn_parent_first_hits field of the telemetry and exits 1 on it; the global_bare_lcp_picks and global_bare_lcp_ties vectors -- the type and value channel, which is this class -- are COLLECTED AND NEVER READ. SECOND, resolution_silent_pick_enable is reached only after the --source-root arm has already exited, so on every modern compile the telemetry is never armed at all and the gate guards only the legacy --source-dir flat scan. The deficit was observed, named in the source, given a recorder and a gate, and the gate does not cover it -- SO THE GATE CANNOT GO RED ON THIS CLASS BY CONSTRUCTION, and has not been able to since the --source-root path landed -- permanently green for TWO INDEPENDENT REASONS, wrong field and wrong code path, either of which alone would suffice. That is worse than an absent check and DESIGN section 4b says why: it will be CITED AS COVERAGE, because a reader who finds a fail-closed exit 1 on silent picks concludes the class is walled. Section 4b asks whether a check's RED is AUTHORABLE before the check is written; here it is not, and nobody asked. Fixing one axis would leave it looking fixed. The gate must therefore be REPAIRED OR DELETED, and if repaired its RED must be DEMONSTRATED rather than assumed. Whether the type channel bypasses global_bare_lookup or reaches it past the policy branch is NOT yet isolated and is not guessed here. INDEPENDENT CORROBORATION, from the lane that hit this first and reached it from the other side, and cited as gunbc#10210 -- the PR, whose diff survives squash-merge and branch deletion, rather than the branch commits, which do not: a four-arm table over the real specimen in which the decisive row holds the branch RESTRUCTURE constant and changes only the NAMES -- renaming the two arms to unique spellings, with the if-expression untouched, is GREEN. Its mirror row is restructured, green, and STILL FORKED, which is why a green there proves nothing about the fork. That is an ORTHOGONAL PERTURBATION AXIS rather than a second opinion: every probe in this row varies POOL MEMBERSHIP with the spelling held constant, and that table varies the SPELLING with pool membership held constant, so neither alone excludes the other's confound and together they do. It isolates the collision as the cause rather than the branch shape, and it carries the harm in one sentence: the compiler sent an author to restructure an innocent if-join for two hours and the shipped commit message records the disagreement as undiagnosed. RUNG FOUND AT: below the ladder on the source-to-interpretation path, because the wrong binding is taken silently and the only refusal is a downstream consequence at an innocent site. Under DESIGN section 4b(1) the class's rung is the MINIMUM across in-scope paths, and byte-identical source accepting at one closure grain and refusing at another means neither grain establishes anything. CEILING, WITH ITS REASON: structurally guaranteed, not structurally impossible. Nothing stops two modules from spelling a type the same, so the invalid state stays WRITABLE; what is attainable is that no Accepted program RESOLVES THROUGH one, which is a refusal derived from modeled structure and therefore rung 3. NEXT-RUNG TRIGGER, named as the capability: a declaration-identity authority that decides a reference's binder from the referencing module's own containment chain for EVERY occurrence channel -- types, coproduct arms, record-literal heads and free calls alike -- sufficient to refuse an off-chain or multiply-on-chain reference at resolve time rather than adjudicate it. That is the same capability gunbc.recurring_failure_mode empty_observation_narrow already names from the census direction -- one namespace census over the one Node tree, not a second check beside the type-name one -- and reaching rung 4 additionally needs the second declaration to be unwritable, which is a further, separate capability. CROSS-LINK: this class is what makes join_judged_against_its_sibling_rather_than_its_declared_context visible; repairing that join alone would silence the diagnostic while leaving the wrong binding in place, so the ordering is resolution first. | ||
| - **join judged against its sibling rather than against its declared context** (INVALID STATE: v1.compiler.infer's if-expression join infers both branches independently, then tests them against EACH OTHER with node_type_compatible; the enclosing declared return type is never consulted. There is synthesis plus a sibling compatibility test and NO CHECKING MODE. HARM: a well-typed coproduct construction -- one variant of the declared return per arm -- is REFUSED, which is a false positive at the ordinary compiler floor, and DESIGN section 4b makes a floor failure a below-baseline regression rather than something a higher-order capability offsets. DISTINGUISHING FACT, and it is what makes the defect narrow and cheap: prefer_specific_type ALREADY COMPUTES THE CORRECT JOIN for the refused pair. For Coproduct(ClaimCostReading) against Product(RightCensoredCost) it returns the left, the declared return, because every re-selection arm falls through -- not same_kind, both fully resolved, the left not a bare leaf. So the diagnostic fires BESIDE a unification the compiler just computed right, corroborated by the refusing runs carrying that as their only blocking error: no downstream mismatch at the declared return and none at the call site, either of which a wrong unification would have produced. The check is refusing a pair it can already join. RUNG FOUND AT: mitigatable -- the refusal is loud, typed and located, and nothing silent is produced; what is wrong is the verdict, not its containment. CEILING, WITH ITS REASON: structurally guaranteed. Whether a branch inhabits a DECLARED type is decidable wherever both the declaration and the branch resolve, so the join can be a checking judgement against the declared context with synthesis reserved for the undeclared case; it cannot reach structural impossibility, because an if-expression whose arms disagree under no declared context is authorable by construction and must still be refused rather than made unwritable. NEXT-RUNG TRIGGER, named as the capability: a checking-mode judgement for branch joins -- each arm judged against the expected type when one is in scope, with the sibling comparison retained only as the synthesis fallback where no expectation exists -- sufficient to accept every arm that inhabits the declared return and to refuse every arm that does not. NOT A CLAUSE OF ITS ROOT AND DELIBERATELY FILED SEPARATELY: the specimen that exposed this join was mis-resolved upstream by binding_chosen_by_pool_membership_rather_than_by_the_declared_rule, and a repair here that silenced the diagnostic would entrench that fault by deleting the evidence carrying it. Resolution is repaired first; this join is its own lane.) |
There was a problem hiding this comment.
The only cited refusal does not demonstrate a false-positive join: the preceding row establishes that the second branch has already been mis-resolved as the unrelated foreign Product(RightCensoredCost), so rejecting it against Coproduct(ClaimCostReading) is correct for the resolved program. prefer_specific_type is not evidence otherwise—it falls through to left for any unmatched fully resolved pair (src/v1/04_types.dag:964-969), including genuinely incompatible types. Without an independent specimen where both branches resolve to actual inhabitants of the declared coproduct and are still refused, this separate authority row records the resolution defect twice and prescribes an unsafe checking-mode repair that could accept the foreign product.
Useful? React with 👍 / 👎.
| // an innocent site. Note this module need not import the colliding SPELLING at all; importing any | ||
| // other member of `colliding_module` is enough, because pool MEMBERSHIP is the variable. | ||
| import fixtures.if_join_pool_binding.declaring_module { PoolSpecimenShape, pick_shape } | ||
| import fixtures.if_join_pool_binding.colliding_module { PoolSpecimenSquare } |
There was a problem hiding this comment.
This fixture claims to prove that merely adding colliding_module to the pool is sufficient and that the entry need not import the colliding spelling, but it imports and uses PoolSpecimenSquare directly, and that is the module's only declaration. Consequently the committed discriminator never exercises the stated “import any other member” case; add a differently named exported sentinel and use that to pull the module into the closure so the fixture actually isolates pool membership from importing the colliding declaration.
Useful? React with 👍 / 👎.
Contributor
Author
|
DO NOT RESOLVE THE CONFLICTS ON THIS PR MECHANICALLY. Merging it would resurrect the deleted monolith and declare every failure-mode identity twice. Measured against
#10206 split the monolith into one row per file. This branch predates that split and still carries the pre-split carrier; it touches none of the row files. A rebase-and-resolve — which is exactly what the automated conflict notice advises — would land 80 declarations in the monolith alongside the row files that already declare the same identities, so every one of them is declared twice. That is the defect that made main unresolvable for roughly two hours tonight ( Note that the approval on this PR is evidence about the diff it was given, not about what merging it now would do to main — the base moved underneath it. What to do instead: re-file any genuinely new row in split shape — one file at — sent from neat-swift-219 |
Contributor
Author
|
Closing: superseded by #10206, with zero content loss — verified at blob grain, not by identity count. This branch predates the roster split. Its head carries the pre-split monolith, Merging it would not add a row — it would resurrect the carrier. 80 of its 81 declared identities already exist as row files on The 81st, Nothing here is lost. Both rows this PR authored are on A note for anyone tempted by the "rebase, resolve the conflicts, and push" advice on the conflict notice: a mechanical resolution here re-lands the monolith, and every per-identity check stays green while it does — an identity join sees the row as present on both sides and cannot see that the carrier came back. Re-author anything genuinely new as a row file plus a Reopen if I have this wrong. Measured by — sent from tidy-swift-334 |
This was referenced Sep 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
cool-koi-858.Pushing to
session/cool-koi-858advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan