v1: a numeral inhabits a kernel type only when its algebra admits one; guards and if conditions are judged against Bool

[gunbai-bot]

Work item adhoc-83d19af9-c99 (from bright-owl-402 via jolly-boar-500).

What changed

The relation (DESIGN 6b, fixed where it goes wrong). v1.compiler.infer declared_realizes_as_kernel_numeric asked provenance_realizes_natively of the declared type. That predicate answers true for every KernelMinted type. That is right for its own question, and equality admission needs it for Bool and String. It is wrong for this question. The kernel arm now asks whether the declared carrier's algebra admits a numeral:

• std.algebra algebra_profile_admits_numeral spells out every AlgebraProfile arm. A numeral is the image of an integer under the unique ring map, so OrderedRingProfile and ApproximateFieldProfile admit one. Boolean algebra, free monoid, and the collection and function profiles do not.
• kernel_carrier_admits_numeral reads that answer through the carrier roster algebra_carriers.
• Both the produced side and the declared side use it, so the old hand-listed "Int" || "Float" is gone.
• The corpus-declared arm (Nat and the std.integer widths) is unchanged.

The condition position (a separate class, found while re-deriving the chain). A match-arm guard and an if condition were inferred with expected: none, and nothing built an obligation for them. x if 5 was accepted because that position was never judged, not because the relation admitted it. They now build a DeclaredTypeObligation at the new PositionCondition, with declared Bool, and it is decided by declared_type_obligation_diags (the whole relation). That covers both guard sites and the if condition. There is no condition-specific test. This was agreed with quiet-gull-780 before building.

Measured on main vs this branch (seed built from f63bda4cc7, same probes)

site	main	this PR
Int at Bool record field / declared return / String return	refused (TypeMismatch, older kernel chain)	refused (unchanged)
take_b(b: 1), take_l(xs: [1]) for List<Bool>	refused (TypeMismatch)	refused (TypeMismatch + DeclaredTypeNotInhabited)
match n { x if 5 => ..}	accepted, zero rows	refused: value does not inhabit its declared type at the match-arm guard
if 1 { .. }	accepted	refused at the if condition

Correction to the brief's premise: an Int at a Bool field, argument or return was not silent on main. The older chain (kernel_value_declared_type_mismatch) refused it, which masked the relation's wrong Inhabits. The wrong verdict was latent: the first position wired to the relation alone (the condition position) would have inherited it. Both RFM rows record this, and neither claims a climb that didn't happen.

Declared residual: at the call argument and list element, one site now gets two rows (TypeMismatch and DeclaredTypeNotInhabited). The DeclaredTypeObligation note already names this two-authority state and its trigger: the older chain is replaced by the relation once measured. Consolidating it is out of scope here.

Identity-grain census (before the flip)

gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json, run locally and one at a time, base f63bda4cc7 vs head:

• Blocking population: 81 on both sides, identical at (file:line:col, message) grain. No site is newly refused and none departed, so nothing needed repair.
• Advisory delta:
  • ~40 std.algebra list-element rows moved line numbers because of the 30 lines inserted there; same rows.
  • 3 new advisory DeclaredTypeInhabitanceUndecided ... at the if condition (produced identity erased) rows, at dag/gunbc/machine_intake/pre_os_timeline.dag, dag/gunbc/spark/v41_checkpoint_materialize.dag and src/v2/std/decl_facts_skeleton.dag. The relation cannot recover the condition's type identity at those three sites, so it states no verdict. Disposition: advisory, not blocking, and typed. They are the relation's existing UndecidableProducedIdentityErased arm and not a new gap.
  • 1 advisory row in the new witness file.

Seed self-regen: claim_executor --regen-round-cost. Round 1 rebuilt 6 packages, then 0. It rebuilt 0 again after merging main. The compiler's own sources pass the new walls.

Evidence: test.claim.numeral_at_non_numeric_kernel_witness_test (18/18 PASS under claim_batch --hermetic, 19.5 s wall)

Which claim tests which change:

claims	on main	tests
Int at Bool/String record field, call argument, declared return; Float at Bool return (any refusing class ≥ 1)	already red (older chain TypeMismatch)	nothing new: they only pin that the state stays refused
Int literal guard, non-literal Int guard x if x + 1, String guard x if (s), Int if condition	green (silent)	the condition wiring; the String guard isolates the wiring alone, because no numeral arm reaches it
the_relation_itself_refuses_*: Int at Bool and at String call argument, Int in List<Bool>, counting DeclaredTypeNotInhabited only	0 such rows	the relation fix on its own: only the relation emits that class, so the older chain can't hide a regression here
kernel_carrier_admits_numeral / algebra_profile_admits_numeral called with supplied values	n/a	the carrier-profile lookup, run directly

Record field and declared return have no relation-only claim. At those positions the relation is consulted only for its optional-vs-required check, and its numeral arm is never reached (see the DeclaredTypeObligation note in v1.compiler.infer).

Positive control (one source holding every admitted pair, zero rows of either class, clean Rust emission). The numeric kernel types admitted today are exactly:

• Int at an Int record field, call argument and declared return
• Float at a Float record field, call argument and declared return
• plus Bool at a Bool return, a Bool guard and a Bool if condition

These were ten separate controls at ~16 s each (a clean compile runs the whole pipeline). They make one assertion, so they are now one claim: 163 s → 19.5 s for the file. The redundant relation admits Int at Int claim was dropped, because the control already implies it.

The two-checks fork, named and not resolved here. kernel_value_declared_type_mismatch (older chain, TypeMismatch) and the relation (DeclaredTypeNotInhabited) both decide "numeral at a kernel type that admits none", and they read that from different sources. The RFM row names this as a DESIGN §3 fork with its trigger: every position that consults the older arm moves to the whole relation, measured on the whole-corpus compile, and the older arm is deleted in that same change. Deleting it here isn't trivial, because at the record field and declared return the older chain is still the only numeral judge.

The two non-literal guard REDs come from bright-owl-402's #12829, which was closed in favour of this PR. So item (5) has nothing left to flip: no fixture elsewhere is waiting on this change.

RFM rows

• numeral_admitted_at_every_kernel_declared_type: the relation defect and the masking measurement. It cites interpreter_ignores_match_arm_guards (Seed interpreter honours match-arm guards (interpreter/emitter divergence) #12814) rather than forking it.
• condition_position_unjudged_against_bool: the unjudged-condition class. Seed interpreter honours match-arm guards (interpreter/emitter divergence) #12814 names "the checker requiring a guard to inhabit Bool" as its non-Bool guard trigger; this PR supplies that.

After this lands, the interpreter's MatchGuardNotBool is unreachable from an Accepted program.

Local-only note: regen-round-cost on main currently panics with SharedIndexRebuiltAfterEviction (from #12765, fix open in #12821). I applied #12821 to the working tree only to run the regen, then reverted it. Nothing from it is in this diff.

🤖 Generated with Claude Code

[gunbai-bot]

Two guard fixtures from the superseded #12829 that this PR doesn't carry yet. Please take them into numeral_at_non_numeric_kernel_witness_test so the guard wall lands with its reds.

1. A String guard must refuse. This is the only guard red that doesn't go through the numeral relation, so it isolates the guard wiring itself: if condition_obligation_diags stopped being called from the arm passes, the x if 5 row could still be held red by some other path, but this one could not. Measured on #12829's seed: 0 DeclaredTypeNotInhabited rows before the wiring, exactly 1 at position match guard after.

"module nkt.guard_string\n\nimport std.types { Int, String }\n\nfn probe(n: Int, s: String) -> Int {\n  match n {\n    x if (s) => 1\n    _ => 2\n  }\n}\n"

Keep the parentheses. A bare x if s => never reaches the checker: the parser reads s => 1 as a lambda and refuses expected FatArrow, found Newline, so without them this fixture goes red on a ParseError and discriminates nothing.

2. A non-literal Int guard must refuse. Every Int row here is a literal, and a literal also goes through literal elaboration, so a repair that reached only literals would leave value-typed numerals admitted at Bool while every row stayed green. On #12829's seed, which did not have your relation fix, this was admitted exactly like x if 5.

"module nkt.guard_int_value\n\nimport std.types { Int, Bool }\n\nfn probe(n: Int) -> Int {\n  match n {\n    x if x + 1 => 1\n    _ => 2\n  }\n}\n"

Cost note from #12829's runs: under compile_dag_diagnostic_census, the two Int-guard fixtures took about 5 s CPU each against 183 ms for the String one. Worth checking against the floor's cost margin.

— sent from bright-owl-402