Repository navigation
File the accepted-source-emits-uncompilable-target class: unit variant in non-applied type position (E0573 specimen from the Measure lane) — row only, no emitter edit - #9970
Closed
gunbai-bot[bot] wants to merge 11 commits into
Conversation
…ant in a non-applied type position
gunbc accepts a coproduct's unit variant standing in a field, parameter or
return type and emits a Rust program rustc refuses. That is section 5 silent
wrongness on the source-to-target path: the only wall that fires belongs to the
target's compiler, and section 7 makes that gunbc's floor rather than rustc's
problem.
The row carries both halves of the evidence. The field specimen (neat-otter-332)
is `type NonApplied { value: Time }` over `type Quantity = Time | Memory`,
refusing E0573 at the emitted field under the narrow emitter classifier; under
the broad classifier a phantom marker struct import made the same source COMPILE,
and extending it across its declared parent boundary refuses E0308 expected
Quantity found Time -- so the narrow classifier's E0573 is the class becoming
visible, not a regression. Independently reproduced here at parameter position
on baeabbb: `fn take(stamp: StampClass) -> StampMode` compiles with 0 blocking
errors and one import-hygiene advisory, and cargo check on the emitted crate
refuses E0308. One source defect, three target behaviours, so the rustc code is
not the class.
Rung found at: below the ladder, by execution at the emission boundary. Ceiling
4, because constructor identity and type identity are distinct modelled facts
with decidable membership from the declaration. Next-rung trigger is the
capability -- type-position resolution over the type namespace alone -- not a
fixture or either specimen's repair.
Row and ledger authorities only; no emitter edit. DESIGN.md and
docs/design-ledgers.md are the regenerated projections.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
…tory The row said the field specimen's measured tree lived in session-local /tmp and was gone. The lane that owns it (neat-otter-332) states its emitted artifacts are held by its own receipts, and its /tmp paths are unreadable from any other session -- so the original clause asserted a provenance fact this row cannot back, which is the unbacked_execution_claim shape the same ledger warns about. Replaced with what is true and resolvable: the fixture was never committed here, which is WHY the row carries the source and both diagnostics inline rather than citing them, and no external path is given because such a path is not a citation a later reader can resolve. The specimen content itself is unchanged and matches the lane's corrected inline strings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
Three ledger surfaces conflicted because sibling lanes are appending to them in parallel. Resolution: - dag/gunbc/recurring_failure_mode.dag: roster only. Kept BOTH appended identities, main's merge_region_excludes_shared_tail first and this branch's accepted_source_emits_uncompilable_target after it, preserving source order. The row declarations themselves auto-merged. - DESIGN.md and docs/design-ledgers.md: not resolved by hand. Both are generated projections and the merge driver correctly refused to pick a side, so they were regenerated from the merged authorities. Audited the result rather than trusting the absence of conflict markers, since a clean textual merge of two appended rows can still be defective: roster and data declarations are in exact bijection with no duplicates, this branch's class appears exactly once, and the carrier's whole diff against origin/main is the one added row plus its one roster line -- so no sibling correction was reverted and proud-moth-614's retracted instrument_reenters_its_own_build_tool did not come back (0 occurrences across the carrier and both projections). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
Same three ledger surfaces, same shape: sibling lanes appending in parallel. main brought sealing_property_erases_structure; both hunks of the carrier conflict were resolved by keeping BOTH identities, main's first and this branch's after, in the declarations and in the roster. DESIGN.md and docs/design-ledgers.md were regenerated from the merged authorities rather than hand-resolved. THE DECLARATION HUNK NEEDED MORE THAN KEEPING BOTH SIDES, and the row that landed on main this cycle is the one that names why. Git's conflict region excluded the shared `evidence: [], }` tail, so taking both sides verbatim left sealing_property_erases_structure unterminated and silently donated its closing lines to the row after it -- merge_region_excludes_shared_tail, exactly. Caught by auditing the resulting declarations rather than by the absence of conflict markers, and repaired by restoring the tail to the first block. Audited after resolving: roster and data declarations in exact bijection, no duplicates on either side, the carrier's whole diff against origin/main is this branch's one row plus its one roster line, and the retracted instrument_reenters_its_own_build_tool remains at zero occurrences. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
…orrect the sighting's own severity claim An independent instance of that class, produced by this lane while integrating main on a later merge base: sealing_property_erases_structure was severed and accepted_source_emits_uncompilable_target received its donated `evidence: [],` and `}` tail. Found by auditing the resulting declarations, not by any marker. THE RECEIPT CORRECTS ITSELF, which is why it is worth appending. This lane first reported that the fused file still parsed and nothing went red. That was an inference from reading the text, never an execution. Compiling the reconstructed fused shape refuses at `expected expression, found Eq` — the same diagnostic the row already measured — so the row's corrected reading holds and the reading it corrects is what a second reporter independently reinvented before measuring. The generalizable part is recorded with it: the misreport is the DEFAULT, not a lapse. Every signal available without executing — both rows present, no markers, no red — agrees with "parses fine". Auditing for the fusion and executing to establish its cost are two separate steps, and doing only the first produces a confident wrong report about severity. The class is not re-filed and its recognition rule is untouched; it held. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
main brought restoration_promise_names_a_route_that_does_not_exist, authored in the ONE-LINE form merge_region_excludes_shared_tail prescribes as the repair. So this integration had no shared tail to exclude: both sides of the conflict region were complete units, and keeping both was the whole resolution. Audited anyway, and executed rather than inferred this time: roster and data declarations in exact bijection, no duplicates, and the resolved carrier COMPILES (0 blocking errors). That last step is the one the previous integration's report skipped, which is how a false severity claim reached my manager; running it is cheap and is now part of resolving this file. Projections regenerated from the merged authorities, not hand-resolved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
Only the generated ledger conflicted; the .dag authorities auto-merged. Resolved by regenerating from the merged authorities, never by hand. Post-merge diff against main is exactly this branch's three files: the added row, its roster line, and the two projections. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
main brought admitted_module_without_judged_standing as a multi-line block, so this is merge_region_excludes_shared_tail again: both sides of the conflict region were four-line half-blocks with the shared `evidence: [],` / `}` tail factored out below the markers, where it would have terminated only the second row. Resolved by keeping both identities AND restoring the tail to the first, which is the resolution that row prescribes for the multi-line form. Third instance of that class in this session, and the second on this branch. It fires on every multi-line append and did not fire on the one-line append two integrations ago. Verified by EXECUTION, not by reading: the resolved carrier compiles with 0 blocking errors. Roster auto-merged carrying both identities; declarations and roster are in exact bijection with no duplicates; the diff against main is this branch's three files. Projections regenerated from the merged authorities, not hand-resolved. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
Roster only this time; main's two new rows auto-merged as declarations. Kept both incoming identities ahead of this branch's, source order preserved. Executed rather than read: resolved carrier compiles, 0 blocking errors. Roster and declarations bijective, no duplicates. Projections regenerated from the merged authorities. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AsNTMSgjX8EPvGHVNo2sNC
briansrls
marked this pull request as ready for review
September 1, 2026 23:04
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: e6572baaf8
ℹ️ 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".
Comment on lines
+169
to
+173
| data accepted_source_emits_uncompilable_target: RecurringFailureMode = RecurringFailureMode { | ||
| identity: "accepted_source_emits_uncompilable_target" as NonEmptyStr, | ||
| authored: "**accepted source emits uncompilable target** (INVALID STATE: a .dag construction the front end accepts with zero blocking diagnostics, whose emission is a target program the target compiler refuses. The instance filed here is a coproduct's UNIT VARIANT standing in a NON-APPLIED TYPE POSITION -- a field, parameter or return type spelled with a constructor rather than a type. HARM: section 5 silent wrongness on the source-to-target path. gunbc says Accepted and hands over a program that cannot build, so the only wall that fires belongs to the target's compiler; where a target has no such wall, or where the emitted artifact is never compiled, nothing fires at all. Section 7 makes this the seed's floor and not the target's problem: the .dag graph is the authority and Rust is one realization, so 'rustc catches it' is exactly the outsourcing this project exists to end. THE SPECIMEN IS CARRIED IN THIS ROW RATHER THAN CITED, because the fixture that produced it was never committed to this repository (neat-otter-332, 2026-09-01). Its emitted artifacts are held by that lane's own receipts; no path is given here, since a path outside this repository is not a citation a later reader can resolve. Authored source, two modules: `scope.provider` declares `type Quantity = Time | Memory`; `scope.consumer` does `import scope.provider \{ Quantity, Time \}`, `type NonApplied \{ value: Time \}`, `fn field_as_quantity(subject: NonApplied) -> Quantity \{ subject.value \}`. gunbc accepts it. DISTINGUISHING FACT, and the reason this class must not be read off the target's error code: WHAT rustc says is decided by what else the emitter minted, not by the source defect. Under the NARROW emitter classifier the consumer emits `pub use crate::scope_provider::\{Quantity\};` then `use crate::scope_provider::Quantity::\{Time\};` with no marker binding, and `pub struct NonApplied \{ pub value: Time \}` refuses `error[E0573]: expected type, found variant Time` at `src/scope_consumer.rs:15:16` on `pub value: Time,`, label `not a type`, help `consider importing this struct instead`. Under the BROAD classifier the consumer instead emits `pub use crate::scope_provider::\{Time\};` beside `\{Quantity\}` -- the provider having emitted `pub enum Quantity \{ Time, Memory \}` AND `pub struct Time;` -- so the field declaration COMPILES, and the refusal moves to the function: `error[E0308]: mismatched types` at `src/scope_consumer.rs:20:5` on `subject.value.clone()`, `expected Quantity, found Time`, against `expected Quantity because of return type`. INDEPENDENTLY REPRODUCED AT PARAMETER POSITION on this branch, 2026-09-01 on gunbc baeabbbf80, by a single-file source handed to the compiler: `type StampMode = StampClass | StampOther` with `fn take(stamp: StampClass) -> StampMode \{ stamp \}`. `gunbc compile --target rust` exits 0 with 0 blocking errors, emits `pub fn take(stamp: StampClass) -> StampMode` beside `pub struct StampClass;`, and `cargo check` on the emitted crate refuses `E0308 expected StampMode, found StampClass`. One source defect; E0573, E0308-at-the-parent, and E0308-at-the-body depending on emission. THE MASK IS THE SHARP HALF, and it is fabricated plausible output rather than a lucky green: the broad classifier's marker import made the FIELD-ONLY source compile by substituting a distinct struct for a variant. It never preserved the modelled meaning, and extending the SAME accepted source across its declared parent boundary -- the function returning `Quantity` -- is what exposes it. So the narrow classifier's E0573 is this class becoming VISIBLE, not a regression the narrowing introduced. GENERAL FORM: a green obtained because the emitter manufactured a target-only entity for a source name is not evidence the source is well-typed, and the discriminator is to extend the source past the boundary the manufactured entity does not model. THE ONE .dag-SIDE SIGNAL IS ABOUT THE WRONG QUESTION: on the parameter reproduction the compile printed the ADVISORY `unlisted import use 'StampClass' (referenced but not in any import's name list)`. It fires because the name was not found among types -- the front end reached the exact fact that decides this case and reported it as import hygiene. It is not a partial wall: it is advisory, it names listing rather than type position, and the field specimen above IMPORTS `Time` explicitly, so it does not fire there at all (see `diagnostic_name_mechanism_silent`). RUNG FOUND AT: below the ladder, established by execution at the emission boundary -- the compile accepts and the emitted crate refuses. Section 4b's rung-1 mitigations are absent: nothing at the .dag boundary is typed, located or countable about this construction. CEILING: 4, structurally impossible, and the reason is that constructor identity and type identity are two distinct modelled facts whose membership is decidable from the coproduct declaration -- a variant name is reachable from that declaration as an ARM and never as a type, so the type-position slot has no constructor that admits it. No undecidable predicate is involved, so this is a wall now and not a ratchet. NEXT-RUNG TRIGGER, phrased as the capability that retires the row rather than an artifact that would contribute to one: type-position name resolution that consults the TYPE namespace alone and refuses a name resolving to a constructor with a located diagnostic, sufficient that NO Accepted program contains a variant name in any non-applied type position -- field, parameter or return. Repairing either specimen, narrowing the emitter classifier, or adding a fixture satisfies less than that and does not retire this row. RECOGNITION RULE: when the target compiler names a symbol at a type position, check whether that symbol is declared as an ARM of a coproduct in the source; if it is, the defect is in accepted .dag and the target compiler is the only wall that fired. SCOPE STATED RATHER THAN GENERALISED: executed for a unit arm at a field type and at a parameter type, Rust target only. Record-shaped arms, applied positions such as `List<Time>`, and other targets were not measured and are not claimed.)", | ||
| evidence: [], | ||
| } |
There was a problem hiding this comment.
When this change is integrated alongside another roster append, this multi-line declaration recreates the shared evidence: [], / } tail that the carrier explicitly eliminates in dag/gunbc/recurring_failure_mode.dag:42-70. Git can factor that suffix out of the conflict region, and the natural additive resolution then produces a fused declaration that fails to parse—the exact failure documented by the adjacent merge_region_excludes_shared_tail row. Keep the complete RecurringFailureMode declaration on one physical line before landing it.
Useful? React with 👍 / 👎.
Contributor
Author
|
Closing without rebasing — this PR has nothing to land and resolving it would remove rows from main. Head e6572ba is the commit already squash-merged as #9909 (309c743). The branch's own row, accepted_source_emits_uncompilable_target, is present on main (4 occurrences) exactly as it is on the branch. It adds nothing. The conflict is not integration debt. Three rows landed on main after this branch's base — disagreement_census_blind_to_agreed_wrong, undecided_fraction_read_as_denominator, incidental_denominator_as_wall — and the branch side of each conflict region is EMPTY. Taking the naive both-sides resolution would delete all three from the authority. That is precisely the merge_region_excludes_shared_tail class rostered in this same file: rows are multi-line blocks sharing an 'evidence: [], }' tail, the three-way merge factors the shared suffix out of the conflict region, and the resolution that looks purely additive severs or drops rows. The rostered repair is the unit, not a check. Nothing to rebase. Closing. |
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
vivid-boar-481.Pushing to
session/vivid-boar-481advances 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