File the third inhabitance seam: a bodyless declared type admits any argument by gunbai-bot[bot] · Pull Request #9879 · gunb-ai/gunbc

gunbai-bot · 2026-09-01T03:56:17Z

What this is

A §4b row, not a fix. DESIGN §4b obliges every newly discovered error class to file or update one row. The row "a value that does not inhabit its declared type is accepted — seam-split, enumeration UNFINISHED" already says "Assume a third seam exists until someone enumerates them". This is one, so it updates that row rather than opening a second authority for the same class.

The finding

The seam is not a position. The three open positions that row already names — variant positional payload, callable return, callable parameter — all vary the POSITION while holding the declared type ordinary. Here the position is the already-covered direct-call parameter and the declared type is bodyless: any type X declared with no body admits any argument, silently.

Four fixtures in an ordinary (non-v2.*) module, so seam (1)'s module_skips_direct_call_arg_check exemption is not in play:

fixture	result
`fn takes(x: Compose<Int, MachineWidth<8>>) -> Int` given a `String`	ACCEPTED, zero diagnostics naming the file
bare `Phantom` as the parameter type	ACCEPTED
locally declared `type Opaque`, no `Phantom` anywhere	ACCEPTED
control: `type MyRec = Word8` (alias to a record)	REFUSES — type mismatch + the paired inhabitance diagnostic

The control is what makes this a finding rather than a silence. The judgment RUNS in that module and admits — a different mechanism from seam (1), where the judgment never runs. The third fixture refutes both obvious readings: it is neither Phantom-specific nor Compose-specific.

Ceiling R2: membership is decidable from the declaration, and the refusing control proves the comparison seam already reaches this position with both types in hand.

Population, stated as syntactic

69 bodyless declarations corpus-wide, including std.constructors Phantom/Product/Coproduct and std.machine_constraints MachineWidth/PointerWidth. The row records that this is the syntactic population and that the exposed subset — bodyless types actually used in parameter position — is smaller and unmeasured, so the number cannot be read as an exposure count.

A naive line-oriented count returns 5227, because the multi-line coproduct spelling (type X then = A | B on the following line) reads as bodyless. The row says to re-derive rather than quote either number.

Second, independent defect recorded in the same row

tools.opaque_realization_census declaration_body_standing_in decides opacity from the type X line alone, and carries the annotation "No such spelling occurs in this corpus today, so the reading is exact for the corpus it is run over" about exactly that multi-line form.

The premise is false by 5269 declarations, every one classified DeclaredOpaque. Separately, it matches the declaration by bare prefix with no name-boundary check, so a longer same-prefix name declared earlier in the same file decides a shorter name's standing — 304 such pairs (e.g. Userset shadowing User in extdeps.access.zanzibar).

Both are read from the function, not from its annotation. It gates nothing today, so this is a wrong instrument rather than a wrong wall — but it is the instrument this row's population question would be handed to, which is why it is recorded beside the row rather than filed elsewhere.

What this does NOT do

Not enrolled. No probe asserts any of this; nothing reds if it changes. The row says so explicitly and names the next trigger at capability grain per §4b(3), with the four fixtures as the discriminating REDs and the alias-to-record case as the no-fork control.
No compiler change, no census change. Filing the row is the whole diff.
Provenance: measured against a byte-pinned binary carrying main's semantics (verified by symbol presence, not by assumption). Fixtures were deleted with the worktree and are reconstructable from the row.

🤖 Generated with Claude Code

https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox

…them, and correct their prose Follow-on to #9858. Five annotations asserted that a deleted cadence executes them; std.witness_admission witness_cadence_has_scheduled_route reports all three named arms routeless. SAME SUBJECT, ANSWERED AGAINST THE CENSUS'S OWN DECLARATION RATHER THAN BY RESEMBLANCE. gunbc.deleted_cadence_reference_census's twelve rows are authority rows that RELIED on the cadence for a coverage claim; these five are witness tests whose annotations asserted the cadence EXECUTES them. That is the same subject reached from the other side — the row's coverage rests on a dark cadence either way — and the precedent is already in the census: tools.namespace_import_closure_behavioral_transport nic_doc is a wet-receipt transport doc censused there, carrying the exact correction these five now match. So this is enrollment in an existing subject, not a widening of it, and no new authority is minted. THE CENSUS'S VOCABULARY CORRECTED MY OWN READING TWICE, which is the argument for using it rather than editing prose beside it. 1. NONE OF THE FIVE IS ReboundToExecutingConsumer, INCLUDING THE TWO CARRYING A LOCAL RECIPE. I had recorded on #9858 that instrument_sandbox's live half genuinely executes via its local recipe and should be corrected rather than past-tensed. Too generous: std.witness_admission answers OfflineLocalRecipe true, which is a statement about ROUTES, while this census asks the stricter question and its own note answers it — a command with no workflow is a local recipe, not a scheduled entry point. Two authorities, two questions; reading the looser answer into the stricter one would have manufactured coverage. The recipes are recorded as MANUAL routes instead. 2. The site is the DECLARATION THE ANNOTATION IS ATTACHED TO, because §4c annotations have no symbol of their own for a DeclarationRef to name. WHAT LANDS: - five PremiseInvalidated rows, plus substrate_long_lane_coverage for the third cadence (the other two coverage rows already existed and are reused). - the census's own arithmetic brought into agreement with itself: "THE TWELVE SITES … two more than the ten" becomes seventeen and fifteen, and the five are added to the drop population, because a PremiseInvalidated row IS one a re-add restores — which is the distinction that comment already spells out. - five prose corrections, one remedy arm each per gunbc.recurring_failure_mode unbacked_execution_claim, MATCHING THE TWO EXISTING EXEMPLARS rather than inventing a style beside them: nic_doc's "classification is membership, not execution" for the two self-host receipts, and ci_layer_roots bin_witness_wet_note's "THE JUSTIFYING HALF OF THAT SENTENCE IS PAST TENSE" for self_host_logic, which is the strongest instance. The perturb line keeps its true "Enrolled on" and loses only the false "nightly". NOT VERIFIED LOCALLY, DELIBERATELY: the census witness runs deleted_cadence_reference_census_live_holds over the live rows, so it checks every new row's cadence is genuinely routeless. Two remote attempts refused fail-closed with HostBudgetUnreadable — the BuildBuddy runner exposes no cgroup memory limit, so the corpus resolve cannot bound itself and refuses rather than defaulting. That is the runner, not this change, and it never reached the witness. CI's floor job is the executing evidence, as it was for #9858. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Li6e7cEDFodeBV7uPi3yTz

…le-item grain only The parse phase refused 14 times, once per line of a `//` block I placed INSIDE `deleted_cadence_references()` between the census rows: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration. Moved verbatim to module scope, joining the existing header comment above that fn, where it reads better anyway because it now sits beside the "THE SEVENTEEN SITES" arithmetic it elaborates. WHAT THE FAILING RUN ACTUALLY ESTABLISHED, since it is easy to read a red job as a red change: the floor was CLEAN — verdict=FloorClean, planned=3349 executed=3349 failed=0, with 19 known-reds held and none newly passing. So `deleted_cadence_reference_census_live_holds` DID run over the five new rows and DID pass, which is the executing evidence this PR was waiting on: each new row's cadence is genuinely routeless. The two failing phases were parse (this defect) and namespace-wave-admission, which did not run at all because parse produced no index. One authoring defect, no modeling defect. Checked the same class across all six files this PR touches with a brace-depth scan rather than by eye: no `//` inside any body remains. This is a repeat of a class I had already been bitten by and had written down. Recording it here rather than only in the commit that fixes it, because the recurrence is the useful part: annotation grain is a rule the author must apply at authoring time, and a long explanatory block is exactly where the temptation to sit it beside the rows it explains is strongest. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Li6e7cEDFodeBV7uPi3yTz

…argument DESIGN §4b obliges every newly discovered error class to file or update one row. The row "a value that does not inhabit its declared type is accepted" already says its enumeration is unfinished and to assume a third seam exists until someone enumerates them. This is one, so it updates that row rather than opening a second authority for the same class. The seam is not a position. (a)/(b)/(c) all vary the position while holding the declared type ordinary; here the position is the already-covered direct-call parameter and the DECLARED TYPE is bodyless. Any `type X` with no body admits any argument, silently. Measured in an ordinary non-v2 module, so seam (1)'s exemption is not in play: a String is accepted against `Compose<Int, MachineWidth<8>>`, against a bare `Phantom`, and against a locally declared `type Opaque` with no Phantom involved -- while the control `type MyRec = Word8` refuses with both a type mismatch and an inhabitance diagnostic. The control is what makes this a finding: the judgment RUNS here and admits, which is a different mechanism from seam (1), where the judgment never runs. It is neither Phantom-specific nor Compose-specific; both were the obvious readings and the third fixture refutes them. The population is recorded as syntactic and not as an exposure count, and the row says why 5227 is the wrong number for it. Also recorded: `tools.opaque_realization_census` decides opacity from the declaration line alone and carries an annotation asserting the multi-line body spelling does not occur in this corpus. It occurs 5269 times, and the function classifies every one of them DeclaredOpaque. Separately it matches by bare prefix with no name boundary, so a longer same-prefix name declared earlier in a file decides a shorter name's standing (304 pairs). Both read from the function rather than its annotation. It gates nothing, so it is a wrong instrument rather than a wrong wall -- but it is the instrument this row's population question would be handed to. Not enrolled: no probe asserts any of this, and the row says so and names the next trigger at capability grain. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox

…rank the two census defects bold-carp-449's reading, adopted. The census annotation asserting "No such spelling occurs in this corpus today" is not merely a rotted comment: it certifies the exact trap its own function falls into, so a reader checking whether the author considered the continuation form finds a sentence saying yes. DESIGN §4c already names that shape -- an annotation is never evidence that a machine claim holds, because no Accepted program can read one -- so this belongs to that rule as a receipt, not only to this census as a defect. Also records which of the two defects ranks first for repair, and why they are not one defect: the continuation misclassification is systematic and one control exposes it, while the bare-prefix match is silent, name-dependent, and changes its answer with declaration order -- so it survives a fix of the continuation reading alone, and 304 pairs is enough that such a fix would look correct on a spot check. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox

…6-cadence

…d is a choice test.claim.declared_type_expected_type_path_witness landed on main tonight and compiles caller-authored source strings through gunbc.compile_diagnostic_census, asserting on census_ran plus a blocking refusing-count rather than on a diagnostic spelling. The four fixtures in this row are ordinary source strings, so that harness can express them. §4b says declining enrollment where the RED is authorable is specification-without-execution, so the row may not simply say NOT ENROLLED and stop. It now says why: the seam ADMITS today, so the assertion is red on main and enrollment needs a floor_expected_red row -- a roster another lane edited the same night, and a decision about the required gate rather than about this class. Named as the immediate next step with an owner, so the gap stays countable instead of quietly permanent. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013wJU7jqGAEk8rj4UwpHdox

gunbai-bot · 2026-09-01T04:12:39Z

The diff the last review saw was not this PR's content, and that is now fixed.

Review 58051 described five witness-test cadence annotations and a deleted_cadence_reference_census enrolment, and flagged that the title ("third inhabitance seam") did not match. The reviewer was reading the diff correctly — the diff was wrong.

Cause: this branch's earlier work landed as #9866 by squash merge, so those commits are not ancestors of main even though their content is. The merge-base was therefore still 83fe4399d04, and main...HEAD re-presented six already-merged files. All six were byte-identical to main (verified per file by blob hash), so nothing was at risk of being re-applied differently — but the diff was noise, and it cost a reviewer their attention.

Merged origin/main in. The diff is now exactly one file:

docs/plans/compiler-guarantee-recovery-gap-analysis.md

The title and body describe what is actually here.

One substantive change while integrating main. test.claim.declared_type_expected_type_path_witness landed on main tonight, and it compiles caller-authored source strings through gunbc.compile_diagnostic_census, asserting on census_ran plus a blocking refusing-count rather than on a diagnostic spelling. The four fixtures in this row are ordinary source strings, so that harness can express them — which means the RED is authorable, and DESIGN §4b says declining enrollment where the RED is authorable is specification-without-execution.

So the row no longer just says NOT ENROLLED. It now says why it is a choice rather than a constraint: the seam admits today, so the assertion is red on main, and enrollment needs a v2.workflow.floor_expected_red row — a roster another lane edited the same night, and a decision about the required gate rather than about this class. Named as the immediate next step with an owner, so the gap stays countable instead of quietly permanent.

I did not add that roster row myself: enrolling an expected red is a decision about the required gate, not about this finding.

— sent from eager-hawk-376

… nullary-alias-applied-argument class TWO CHANGES TO docs/plans/compiler-guarantee-recovery-gap-analysis.md, both building on the third-inhabitance-seam row landed by #9879 rather than beside it. 1. THE EXPOSED SUBSET, which #9879's row explicitly left unmeasured. Re-derived independently over dag/, src/v1/ and src/v2/ at origin/main 6741a39, per that row's own instruction to re-derive rather than quote: 69 bodyless declarations / 66 distinct names -- JOINING #9879's 69 at identity grain, not merely at count. A first pass matching ^type X$ found 62; the missing 7 are the PARAMETERIZED bodyless declarations (Compose<carrier, dimension>, MachineWidth<bits> twice, ReferenceModel<T>, CppTargetDataModel<...>, CppTargetProfile<...>, ConfigPatchRecord<Config>). 62 + 7 = 69, so the two censuses agree on membership. Reachability in PARAMETER position -- where a non-inhabiting value can actually flow in: Symbol (v2.std.node) 1045 parameter sites SourceSpan (v2.lens.application) 129 Bytes (std.types) 4 ConfigPatchRecord (v2.std.patch) 1 and nothing else. 33 names appear only in field position; 27 appear in no parameter, field or return position at all. Compose and MachineWidth are among the unexposed -- type CONSTRUCTORS applied as type arguments, never parameter types. So the headline is not 69: the exposure is dominated by ONE declaration, Symbol, the substrate's own identity field, by an order of magnitude. CEILING SPLIT THREE WAYS, because one value would overstate the row: (a) declared-abstract by ruling (Symbol, Unit) -- construction discipline at the boundary through a minting authority, NOT arms. R3 at such sites, R2 corpus-wide. (b) the 27 type-level tags -- hole unreachable, no climb needed. Filing them as exposure would inflate the class and bury the member that matters. (c) SourceSpan and Bytes -- genuinely exposed, unruled, recorded so they are countable. Class rung is the minimum across parts: below floor. Trigger names the CAPABILITY per 4b(3) -- a bodyless declared type inhabitable only through a declared minting authority, AND the direct-call inhabitance judgment consulting it. #9854's witness is a wall for ONE SITE and does not retire the row. METHOD LIMITS carried in the row: single-line fn matching undercounts multi-line signatures; field position over-counts. Bounds, not exact counts; the shape is robust. 2. A NEW CLASS: a nullary alias rendered with its body's type argument applied to it. Two instances, different aliases, one shape: a refusal at a LexText-declared parameter printed expected 'Node(LexText<Product(Char)>)' though type LexText = FreeMonoid<Char> is nullary; and a repair to is_host_text_carrier_type emitted pub fn string_is_empty(s: String<i64>), which is not valid Rust. The harm is that a malformed type READS AS A REAL REFUSAL: the LexText arm produced 129 refusals against the qualified spelling's 30, and the 129 was reported and endorsed as a stricter wall over a larger population before the diagnostic text was read closely enough to notice the alias cannot take an argument. A population inflated by a printer defect is worse than a missing measurement, because it gets quoted. Both instances reproduced on a binary built from a pristine origin/main export with the is_host_text_carrier_type repair verified absent from the compiled mirror, each arm carrying a firing positive control. The row deliberately does NOT name a repair site -- three lanes are converging on 05_emit_rust.dag. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019o3436yxdGdYZa53YopdQH

…ol — and a nullary alias rendered with an applied type argument (#9888) * Measure the bodyless-type exposed subset (4 names of 66) and file the nullary-alias-applied-argument class TWO CHANGES TO docs/plans/compiler-guarantee-recovery-gap-analysis.md, both building on the third-inhabitance-seam row landed by #9879 rather than beside it. 1. THE EXPOSED SUBSET, which #9879's row explicitly left unmeasured. Re-derived independently over dag/, src/v1/ and src/v2/ at origin/main 6741a39, per that row's own instruction to re-derive rather than quote: 69 bodyless declarations / 66 distinct names -- JOINING #9879's 69 at identity grain, not merely at count. A first pass matching ^type X$ found 62; the missing 7 are the PARAMETERIZED bodyless declarations (Compose<carrier, dimension>, MachineWidth<bits> twice, ReferenceModel<T>, CppTargetDataModel<...>, CppTargetProfile<...>, ConfigPatchRecord<Config>). 62 + 7 = 69, so the two censuses agree on membership. Reachability in PARAMETER position -- where a non-inhabiting value can actually flow in: Symbol (v2.std.node) 1045 parameter sites SourceSpan (v2.lens.application) 129 Bytes (std.types) 4 ConfigPatchRecord (v2.std.patch) 1 and nothing else. 33 names appear only in field position; 27 appear in no parameter, field or return position at all. Compose and MachineWidth are among the unexposed -- type CONSTRUCTORS applied as type arguments, never parameter types. So the headline is not 69: the exposure is dominated by ONE declaration, Symbol, the substrate's own identity field, by an order of magnitude. CEILING SPLIT THREE WAYS, because one value would overstate the row: (a) declared-abstract by ruling (Symbol, Unit) -- construction discipline at the boundary through a minting authority, NOT arms. R3 at such sites, R2 corpus-wide. (b) the 27 type-level tags -- hole unreachable, no climb needed. Filing them as exposure would inflate the class and bury the member that matters. (c) SourceSpan and Bytes -- genuinely exposed, unruled, recorded so they are countable. Class rung is the minimum across parts: below floor. Trigger names the CAPABILITY per 4b(3) -- a bodyless declared type inhabitable only through a declared minting authority, AND the direct-call inhabitance judgment consulting it. #9854's witness is a wall for ONE SITE and does not retire the row. METHOD LIMITS carried in the row: single-line fn matching undercounts multi-line signatures; field position over-counts. Bounds, not exact counts; the shape is robust. 2. A NEW CLASS: a nullary alias rendered with its body's type argument applied to it. Two instances, different aliases, one shape: a refusal at a LexText-declared parameter printed expected 'Node(LexText<Product(Char)>)' though type LexText = FreeMonoid<Char> is nullary; and a repair to is_host_text_carrier_type emitted pub fn string_is_empty(s: String<i64>), which is not valid Rust. The harm is that a malformed type READS AS A REAL REFUSAL: the LexText arm produced 129 refusals against the qualified spelling's 30, and the 129 was reported and endorsed as a stricter wall over a larger population before the diagnostic text was read closely enough to notice the alias cannot take an argument. A population inflated by a printer defect is worse than a missing measurement, because it gets quoted. Both instances reproduced on a binary built from a pristine origin/main export with the is_host_text_carrier_type repair verified absent from the compiled mirror, each arm carrying a firing positive control. The row deliberately does NOT name a repair site -- three lanes are converging on 05_emit_rust.dag. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019o3436yxdGdYZa53YopdQH * Correct category (b): the 27 are exposure-on-first-use, not inert -- proven by execution eager-hawk-376 challenged the exclusion and they were right. DESIGN 4b judges reachability BY WHAT A FIXTURE MAY AUTHOR, not by what the accepted corpus contains, so "never used in parameter position in the corpus" is not grammar-absence. Measured in an ordinary (non-v2.*) module, so seam (1)'s exemption is not in play, against the pristine origin/main binary: fn vd_takes_phantom(x: Phantom) -> Int fed "abc" -> resolves clean, EXECUTES, returns 1 fn vd_takes_persecond(x: PerSecond) -> Int fed 7 -> resolves clean, EXECUTES, returns 2 planted positive control length(xs: n) on Int -> REFUSES The control is what makes the silence a measurement rather than a judgment that never ran, and reaching the body makes this admission proven by execution rather than by a silent compile. So the 27 are CORPUS-UNOCCUPIED, not grammar-absent: exposure-on-first-use, acquiring exposure the moment anyone writes the construct with nothing to refuse them. Filing them as inert was the bounded-population-reads-as-progress trap. Two of the 27 are measured, from two different declaring modules; the other 25 are the same shape and are recorded by class rather than each by receipt, which the row says. The exposure split is now three-way: exposed now (4 names, Symbol dominating), exposure-on-first-use (27), grammar-absent (none found). Population, Symbol concentration, below-floor rung and capability-grain trigger all unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019o3436yxdGdYZa53YopdQH --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbc-ci-auto-heal and others added 6 commits September 1, 2026 02:01

Merge remote-tracking branch 'origin/main' into session/eager-hawk-37…

e53166b

…6-cadence

gunbai-bot Bot merged commit d696040 into main Sep 1, 2026
6 checks passed

gunbai-bot Bot deleted the session/eager-hawk-376-cadence branch September 1, 2026 04:45

briansrls restored the session/eager-hawk-376-cadence branch September 1, 2026 04:50

This was referenced Sep 1, 2026

The bodyless-type exposed subset is four names of 66, 1045 of it Symbol — and a nullary alias rendered with an applied type argument #9888

Merged

Census the obligation scope gap: ten of twelve grammar positions have no producer #9889

Merged

Navigation Menu

Repository navigation

File the third inhabitance seam: a bodyless declared type admits any argument - #9879

File the third inhabitance seam: a bodyless declared type admits any argument#9879
gunbai-bot[bot] merged 6 commits into
mainfrom
session/eager-hawk-376-cadence

gunbai-bot Bot commented Sep 1, 2026

Uh oh!

gunbai-bot Bot commented Sep 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

Conversation

gunbai-bot Bot commented Sep 1, 2026

What this is

The finding

Population, stated as syntactic

Second, independent defect recorded in the same row

What this does NOT do

Uh oh!

gunbai-bot Bot commented Sep 1, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants