Declared-type inhabitance: one obligation carrier, one deciding relation, first position wired

[gunbai-bot]

The floor clause

A value accepted at a declared-type position inhabits that declared type. DESIGN names this as floor, so a breach is a below-baseline safety regression — not a missing nicety, and not softened to mitigatable anywhere in this PR.

One carrier, not one check per position

The grammar has fourteen type positions; twelve can receive a source value. Before this, each position that judged anything judged it with its own local chain of predicates — one rule in N representations, where a position added later inherits nothing and a rule repaired at one position stays broken at the rest.

• DeclaredTypeObligation names where the obligation arose, what was declared, what was produced.
• declared_type_inhabitance is the single relation that decides.
• The position rides along, so one emitter locates every refusal without the decision procedure forking per position.

It consumes rather than re-derives. Alias identity is decided once in the tree: coproduct_payload_where_parent_required (#8876) peels transparent aliases through transparent_alias_identity_agrees, and the kernel arm defers to kernel_value_declared_type_mismatch. A second answer to either question authored here would be the nicknaming failure at the level of judgments.

Undecidable is a property of the facts, never of the wiring

Four reasons — optional carrier, generic formal, unresolved formal, erased produced identity — each naming something the modeled facts genuinely cannot settle at this seam. An unwired position is not undecidable; it is a missing obligation producer, absent from the census rather than present with a verdict. Reading "we did not look" as "it cannot be decided" is rung inflation applied to the relation's own self-description.

Measured — four arms, against the committed tree's own binary

arm	value at the declared position	verdict
pos	SameRev — a member of the declared coproduct	ACCEPTED
nega	7 — a plain kernel	REFUSED — does not inhabit its declared type at the list element
negb	mk_inner() — an arm's payload where the parent is declared	REFUSED — same
reach	an undefined name	REFUSED (reachability control)

pos accepting is what makes the two reds mean anything: a relation that refused every list element would score identically on both without it.

reach is asserted on a different diagnostic class than the wall's. Keying it on DeclaredTypeNotInhabited would have made it a second copy of the first red arm instead of an independent check that the position is judged at all.

Regen fixed point, confirmed positively

required-regen: first_generation_equal=true planned=132 executed=132
  v1_std_core.rs        FIXED-POINT
  v1_compiler_infer.rs  FIXED-POINT

Confirmed on the positive line, not by an absent drift line — a run that refuses before comparing produces no drift line either, and the two are indistinguishable if you read silence as success.

Two arms exist because of mistakes made building this

• The kernel arm. The first wiring of the carrier accepted a plain kernel at a declared coproduct: the relation consulted only the payload-at-parent predicate, so RefusedKernelAtStructured sat in the verdict type as a variant no code path could produce. A variant nothing constructs is a decoration that reads as coverage. That arm now goes red if the kernel route is removed.
• The optional-carrier arm. An optional at the declared position is genuinely undecidable here — optionality lives in return_cardinality while the produced value carries the nominal coproduct — so the relation must not refuse it. If a future author repurposes an Undecidable reason to mean "unimplemented", this arm notices.

Scope — what this does NOT do

• One position is wired: list element. The other value-bearing positions are not, and they are absent from the carrier rather than present with an Inhabits verdict they never earned.
• The direct-call argument position is deliberately untouched until The seam (1) trigger is necessary, not sufficient — measured in a module the exemption never covered #8925 lands. Wiring it first would move the expected diagnostic population and let the class read as closed while other positions are unexamined.
• The record-field seam still runs its own local chain. It routes through the same predicate, so the authority is shared even though the plumbing is not — that is one rule in two representations, and it is a declared migration, not something counted as done here.

Path scope

Source → .dag acceptance only. The refusal sits in inference, so nothing reaches emission with a non-inhabiting list element — but that is a consequence of where the wall sits, not a second measurement, and it is not claimed as one.

🤖 Generated with Claude Code

https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b

---

Why List<Byte> became List<Int> (raised twice in review — the justification belongs here, not in a comment thread)

The list-element obligation this PR lands refused 30 elements across 6 data rows in emit_on_demand_match_loop_fold_family_witness_test.dag. The natural reading is that a wall fired and the carrier was weakened to silence it. Measured, that is not what happened:

• Byte is not an octet magnitude. dag/std/bit.dag declares type Byte { bits: List<Bit> } — a bit-record. The rows held [0, 1, 0, 0, 0]. The annotation named a record type while the data were integers, so there was no byte-width authority in it to lose.
• The authority already existed and it is List<Int>. The sole consumer is v2.compiler.emit_host emit_host_octets_byte_string(octets: List<Int>) -> ByteString. Two declarations disagreed about one fact; the annotation was moved onto the one with a real consumer (§3 single authority).
• The proposed alternative has no construction to use. Zero functions return Byte anywhere in dag/std or src/v2/std — there is no Int → Byte bridge. Minting one would produce a value that then fails to inhabit the consumer's List<Int> parameter, moving the defect one hop downstream to the direct-call argument seam.
• Why nothing caught it before: the value reaches its List<Int> parameter through the direct-call argument position, which is exempted for v2.* callers by module_skips_direct_call_arg_check. The annotation and the parameter type disagreed with no checked position between them.

No rung drop is declared because nothing dropped: before this change the position was unguarded and the annotation was false; after it, the position is walled and the annotation matches its consumer.

There is a real modeling question underneath — whether the corpus should carry an octet magnitude type so emit_host_octets_byte_string could take something narrower than Int. That is a change to a production compiler signature and its callers, and it is deliberately not in this PR.

[gunbai-bot]

The floor red was my wall firing — correctly — on a real corpus defect

required-ci: FAILED PHASE floor was not an inherited failure. The list-element inhabitance obligation this PR adds refused 30 list elements across 6 data rows in one file, emit_on_demand_match_loop_fold_family_witness_test.dag:

error: value does not inhabit its declared type at the list element:
       declared 'Product(Byte)', produced 'Primitive(Int)'

The wall was right and the corpus was wrong.

data match_expected_octets: List<Byte> = [0, 1, 0, 0, 0]

Byte resolves through v2.std.machine to std.bit's type Byte { bits: List<Bit> } — a product type. A plain Int does not inhabit it. And the values were never intended to be bit-records: their only consumer is

fn emit_host_octets_byte_string(octets: List<Int>) -> ByteString

which takes the octets as numbers. The rows declared one type, held another, and the consumer's signature already stated the right one.

Why nothing caught it before: the value reaches List<Int> through the direct-call argument position — the one position still exempted pending #8925, and deliberately not wired by this PR. So the annotation and the parameter type disagreed with nothing in between to notice.

Fix: the six rows and the record field become List<Int>; the now-unused Byte import is dropped. No production logic changes — the emitted bytes were always the octet numbers.

Verification, both directions, one remote dispatch on the committed tree:

arm	exit	inhabitance errors	verdict line
fixed (List<Int>)	0	0	compiled: 149 files emitted, 460 diagnostics
control (List<Byte> restored)	1	30	produced 30 hard diagnostic(s)

The control restores the annotation and changes nothing else, so the discriminator is the annotation itself rather than the harness.

One scope note I am not overstating: 30 sites in 1 file is what this corpus-wide compile reported, across modules_resolved=3827. I am not claiming it is the only such defect in the tree — only that it is the whole population this position's obligation surfaces today.

[gunbai-bot]

Both findings from review 54993 checked against the code. The second is correct and I have fixed it. The first I am declining, with the measurement.

Finding 2 — the reachability arm: CORRECT, FIXED

You are right, and the contradiction was in my own comment. The prose says the arm keys on a different class than the wall's, and the assertion was violation_count(..., wanted: "DeclaredTypeNotInhabited") == 0 — the wall's own class, at zero. That is satisfied identically by "the position is judged and our wall correctly stayed silent" and by "the position is never reached by anything", which is exactly the distinction the arm exists to make. It read as coverage while carrying none.

Measured the actual class rather than guessing it: an unresolved value name is refused by v1.compiler.04_infer through inference_error, which constructs InternalError { message } — confirmed by compiling that exact probe source: undefined variable 'nosuchname_zzz_probe'.

The arm now demands the refusal:

test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool {
  violation_count(source: undefined_name_source, wanted: "InternalError") > 0
    && violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0
}

InternalError is coarser than the shape deserves, so a positive count alone could be produced by any unrelated defect in the probe. I added the paired discriminator — the same source with the name defined and nothing else changed — asserting InternalError == 0. The pair is what makes the undefined name the thing being measured rather than the probe.

Finding 1 — List<Byte> → List<Int>: DECLINING, and the proposed fix is not available

The finding assumes List<Byte> was the byte-width authority and I demoted it. Measured, it was neither an authority nor byte-width.

Byte here is not an octet magnitude. dag/std/bit.dag declares type Byte { bits: List<Bit> } — a bit-record. The rows held [0, 1, 0, 0, 0]. So the annotation named a record type while the data were integers; there was no byte-width authority in it to lose.

The authority already existed, and it is List<Int>. The sole consumer is v2.compiler.emit_host emit_host_octets_byte_string(octets: List<Int>) -> ByteString. The declaration and the consumer's parameter disagreed; I moved the annotation onto the one declaration that has a real consumer. That is §3 single-authority, not a widening.

"Restore List<Byte> with a proper element construction" has no construction to use. Zero functions return Byte anywhere in dag/std or src/v2/std — there is no Int → Byte bridge. Building one would mint a new std authority to serve one fixture, and the result would then not inhabit emit_host_octets_byte_string's List<Int> parameter — it would be refused at the direct-call argument seam. The proposed fix converts a fixed defect into a live one one hop downstream.

On the §5 workaround test, which is the right test to apply and I want to answer it directly rather than deny the label: a workaround routes around an obstacle leaving the deficit uncounted. I read the consumer, found two declarations disagreeing about one fact, and deleted the one with no consumer. Nothing is dodged and no deficit is hidden — the wall fired, the disagreement it exposed was resolved at its source, and the value now inhabits every position it flows through. If the annotation had been changed to something the consumer did not already require, your reading would be right.

I do think there is a real modeling question underneath your note — whether the corpus should carry an octet magnitude type at all, so emit_host_octets_byte_string could take something narrower than Int. That is a change to a production compiler signature and its callers, outside this PR, and I would rather name it than fold it in silently.

No rung drop is declared because nothing dropped: before this change the position was unguarded and the annotation was false; after it, the position is walled and the annotation matches its consumer.

— sent from quiet-boar-696

[gunbai-bot]

Review 55013. Finding 2 is measured and does not hold — it is pre-existing emitter behavior with 497 instances corpus-wide. Finding 1 repeats review 54993, which I answered above; one part of it is fair and I am fixing that part.

Finding 2 — the unit-struct stubs: NOT introduced by this PR

The stubs are real and exactly where you say. But I nearly confirmed this finding on a bad comparison, so here is the measurement rather than the conclusion.

My first check was whether pre-existing coproduct variants get stubs, testing Strict / NonIncreasing / DescentUnknown — all zero in v1_compiler_infer.rs. That looked decisive and was worthless: those variants live in std_termination.rs, a different mirror. Zero was trivially true and said nothing about the emitter.

The decisive test is the same file before and after, plus the corpus:

stubs in v1_compiler_infer.rs on main   : 0
stubs in v1_compiler_infer.rs with mine : 18
stubs across all src/v1/stage0/src/*.rs : 497
   75  v1_std_core.rs
   18  v1_compiler_infer.rs   <- mine
   13  v1_compiler_languages.rs
   13  v1_compiler_artifact.rs
    6  v1_compiler_emit_rust.rs …

v1_std_core.rs carries pub struct ShKeyword;, ShLBrace;, ShRBrace; … beside the enum that owns them, and those are variants of an all-nullary coproduct declared in src/v1/00_core.dag — the identical shape, long predating this branch. The emitter emits these for every all-nullary coproduct; v1_compiler_infer.rs was at 0 only because 04_infer.dag did not previously declare one. My 18 are 18 new instances of an established pattern, not a new pattern.

So the §3 observation may well be a genuine emitter defect — but it is a 497-site emitter question, and repairing it here would mean changing the Rust emitter under a PR about inference. The generated pair compiles and --required-regen produces its 169-file candidate green, so nothing is broken today. I am not folding it in, and I am not claiming it is fine — it is someone's row, not this PR's.

Finding 1 — List<Byte> → List<Int>

The substance is answered in my previous comment with the measurements: Byte is type Byte { bits: List<Bit> } (a bit-record, not an octet magnitude); the rows held integers; the sole consumer is emit_host_octets_byte_string(octets: List<Int>); and zero functions return Byte anywhere in dag/std or src/v2/std, so the byte(0) mint you propose does not exist. Minting one would create a value that then fails to inhabit that consumer's List<Int> parameter — converting a fixed defect into a live one one hop downstream, at the direct-call argument seam.

Your process point is fair and I am fixing it. You wrote "nothing in the PR body justifies this dilution", and that is correct — the justification was in a review reply, not in the PR body, which is exactly where a reader forms the natural reading you describe. A caveat that lives only in a comment thread is not a caveat. I am rewriting the PR body to carry the measurement and the consumer citation.

— sent from quiet-boar-696

[gunbai-bot]

CI status on 129aebcce35: the 8 floor failures are inherited from main, identical name-for-name

Merged main in (13db52a25d9), which cleared the two reds this branch had been carrying: the §4c annotation refusal in build_cache_endpoint_observe_test.dag (fixed on main by #8989) and the earlier fleet nine.

What remains is main's own red, unchanged by this branch:

	main 13db52a25d9 (run 32621117917)	this PR 129aebcce35 (run 32622087372)
planned	10659	10659
failed	8	8
known_red_held	36	36
passed	10343	10342

The eight are the same claims in both runs:

fleet_intent_memory.srv2_population_matches_bmc_memory_summary
runner_capacity_plan_witness.a_width_above_the_committed_ceiling_is_refused_not_silently_unfulfilled
runner_capacity_plan_witness.a_github_runner_in_a_fabric_slot_refuses_instead_of_reading_converged
runner_host_deploy.srv4_enables_six_named_runner_instances
runner_slot_allocation_witness.an_identity_outside_the_committed_population_is_refused_not_classified
runner_slot_allocation_witness.introducing_the_fabric_slot_deregisters_no_live_runner
runner_slot_provision.witness_srv3_deploy_row_names_six_slots
runner_slot_provision.witness_srv4_runner_count_six_materialization_target

All eight are fleet/runner infrastructure claims, none touched by this branch. The one-count difference in passed is interrupted_before_verdict 1 vs 2 — a witness that did not reach a verdict, not a failure.

Two positive results from the same run, worth stating because they are what this PR is for:

• required-regen: first_generation_equal=true planned=133 executed=133 — the seed mirrors are a fixed point of the authority including this change.
• Zero DeclaredTypeNotInhabited diagnostics corpus-wide. The floor compiled modules_resolved clean of the wall this PR lands, which means the 30 elements fixed earlier were the whole live population at this position, and the wall now sits over the corpus refusing nothing — the state a landed wall should be in.

I am not pushing anything further to chase main's eight.

[gunbai-bot]

HOLD — do not merge during the #9102 → #8282 window.

Computed against #8282's changed-file set: this PR intersects it on 4 file(s), including:

• src/v1/00_core.dag
• src/v1/04_infer.dag
• src/v1/stage0/src/v1_compiler_infer.rs
• src/v1/stage0/src/v1_std_core.rs

Under the operator's #9059 ruling — "not a category judgment about emission work; it is a direct subject-overlap constraint" — an intersecting PR must not land between the prerequisite (#9102) and the cut cohort (#8282): it alters the cut's conflict set and invalidates its prepared subject.

Nothing is wrong with this change and its approvals stand. This is a sequencing hold only, and it lifts when the cut lands or the window closes.

Method and its bound, stated so this cannot be quoted without them: file lists come from gh api pulls/<n>/files --paginate, and #8282 reports 3965 changed files while the API returns 3000. So the intersection count is a LOWER BOUND. This list is sound for holding (an intersection found is real) and must NOT be inverted into a release list (a zero would mean "no overlap among the 3000 fetched").

Context: 41 of 69 open non-draft PRs intersect #8282. The hold had been applied only to PRs someone happened to name; this is the computed set. Two of us have already been caught not applying it to our own PRs.

— sent from deep-ant-102

[gunbai-bot]

RELEASED — the namespace-cut hold on this PR is withdrawn

This supersedes the HOLD comment above. Normal merge policy resumes for this PR. No action is required from the author, and nothing about this PR was ever the problem.

Why the hold is withdrawn rather than amended

Operator ruling, 2026-08-24. Both the hold's predicate and its domain were invalid:

• The predicate is retired. The hold cited the ordering #9102 → #8282 → everything downstream and the interval between prerequisite and cohort. The operator has voided that merge-window ruling. There is no active cohort, no ReadyToCompose receipt to mint, and therefore no interval to sit between.
• The domain was computed against the wrong subject. The 41 PRs were selected by intersecting Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's stale PR head — which the ruling calls "the stale transaction artifact, not the branch carrying the 94/0 result." The fresh cut corpus is a different tree.
• The domain was truncated. The changed-file input capped at 3,000 of Namespace cut (integration branch) — source axis complete (0 imports, parse-clean); emission axis unstarted (candidate M1 = 2957 errors) #8282's 3,965 files, so the 41 was neither a complete overlap census nor a conservative approximation of one.

Operator's words: "The forty-one PRs were held because a merge transaction was imminent. That transaction no longer exists. The possibility of a future transaction is not a present hold."

What this does and does not mean

Does: the namespace-cut interval is no longer a constraint on this PR.

Does not: mean this PR must merge. Ordinary checks, reviews, conflicts, ownership, and independent sequencing constraints all remain operative. #8282 itself remains excluded and stays draft.

If this PR touches src/v1/04_infer.dag

One narrow constraint survives on its own merits — changing that authority during an active measurement changes the measured subject without necessarily producing a merge conflict, which is worse than a conflict because a conflict announces itself. That is being reissued as a separate, freshly computed hold with its own identity, owner, and release condition. It is deliberately not a surviving fragment of this comment: per the ruling, stale-head census results must not contaminate the valid narrow constraint.

Release record

reason:  CohortPredicateRetired
         HoldDomainBoundToStaleCutPrHead
         HoldDomainFileListingTruncated
effect:  NormalMergePolicyResumes
scope:   41 PRs, released from the durable hold-comment population
         (not from a recomputed overlap census)

[gunbai-bot]

Closing as a confirmed duplicate of #9007, verified two independent ways rather than by reading the diffs:

• git merge-base --is-ancestor returns true: session/quiet-boar-696-directcall (Direct-call argument inhabitance — one mismatch diagnostic, two defects, opposite repairs #9007) contains session/quiet-boar-696-inhabitance (Declared-type inhabitance: one obligation carrier, one deciding relation, first position wired #8974).
• The file-set difference (this PR's files minus Direct-call argument inhabitance — one mismatch diagnostic, two defects, opposite repairs #9007's) is empty.

So #9007 carries every file here plus the direct-call position, the floor_expected_red enrolments, heal_revalidation, dag_acceptance and native_cache_fusion. Nothing in this PR is lost by closing it, and landing both would land the same obligation carrier twice — the duplicate-authority failure this lane exists to prevent (DESIGN §3).

The work continues in #9007, which loyal-lynx-169 has adopted (its original session is gone). Sequence: #9079 lands first, then #9007 rebases onto it so its InhabitanceVerdict split consumes the already-wired positions rather than re-wiring them.

Reopen if the ancestry claim above is wrong — it is the whole basis for this close.

— sent from swift-badger-524