The seam (1) trigger is necessary, not sufficient — measured in a module the exemption never covered

[gunbai-bot]

#8904 landed a §4b row whose ceiling cell says the distance to R2 is "an if-statement plus a
triage" — direct_call_arg_mismatch_diags exists, is written, and is simply not called, so
flipping module_skips_direct_call_arg_check off closes seam (1).

Flipping it off is necessary. It is not sufficient, and the discriminating measurement is a
module the exemption never applied to in the first place. In an ordinary non-v2.* module, where
the guard is false and the judgment demonstrably runs, in one compile:

fn c4_takes(o: EOuter) -> Int { 1 }

c4_takes(o: 5)          -> REFUSED   type mismatch: expected 'Coproduct(EOuter)', got 'Primitive(Int)'
c4_takes(o: e_inner())  -> ACCEPTED  the coproduct's own payload type

The judgment is live at that seam and misses this shape. A reader who acts on the row as merged will
delete the arm, watch the diagnostic count fall, and conclude the seam is closed.

Both halves have to be read together: the exemption really does switch the judgment off for every
v2.* caller — that half is unchanged and still below floor — and the judgment it switches off
would not catch this shape anyway.

This is the second necessary-stated-as-sufficient trigger this one row has carried; #8868
corrected the first. Two in one class is a pattern about how triggers get written — someone names the
obstacle they can see and assumes it is the only one.

The denominator this row has lacked now exists

The row has said "assume a third seam until someone enumerates them" through two revisions while
the count grew from two to five by accident — four of the five were found by a downstream red or
by a mis-written probe, never by anyone enumerating positions. That samples the reviewer, not the
population, and a count produced that way cannot support a rung.

Positions are now enumerated from the grammar: every call site of parse_type_expr in
v1.compiler.parse, the finite set of places the language attaches a declared type. 14 sites, and
all five previously-known seams fall out of it rather than having been seeded in — the falsifier
this pass was required to pass. The list-element seam falls out only because a container's element
type is reached as a type argument rather than as a declaration of its own, which is why nobody had
named it as a position before.

Method — each position carries three arms: the payload-where-parent shape, a kernel mismatch, and
an undefined name. The third is the reachability control: if it refuses, inference reaches that
position, so a passing kernel arm establishes that no type judgment runs there rather than that the
position went unanalysed. All seven reachability controls refused.

disposition	positions
refuses	record/variant NAMED field — and only because #8876 walls it
judgment runs, misses the shape	fn parameter (direct-call seam)
not refused, no judgment runs	container type arg (list element), variant POSITIONAL payload, fn declared return, module-scope data initializer, annotated let, callable-type RETURN, callable-type PARAMETER
not refused	as cast
not reachable from a source value	type-alias RHS, uses resource type, service exit / response types

Three positions were previously unknown: variant positional payload, as cast, annotated
let. The two callable-type positions were reported as UNMEASURED in the first revision of this
PR and have since been measured: type S4Holder { cb: fn(Int) -> EOuter } given a lambda whose body
yields the payload, and type S5Holder { cb: fn(EOuter) -> Int } applied to the payload. Both
reachability controls (an undefined name in the same position) refused, so both positions are
analysed; both the payload arm and the plain-kernel arm passed. The census is now 14 of 14
measured, none unmeasured.

What is deliberately NOT claimed here

data c6b: EOuter = 5 and fn c5b() -> EOuter { 5 } are both accepted, with the reachability
control proving both positions are analysed. That is not payload-versus-parent — it is a plain kernel
value where a declared coproduct is required, the ordinary-floor invariant §4b names beside name
resolution and exact-bijection binding. On this census that is seven of fourteen grammar-admitted
positions accepting a kernel value where a declared coproduct is required — variant positional
payload, fn declared return, data initializer, container type argument, annotated let,
callable-type return, callable-type parameter — and the single refusing position owes its refusal to
a PR that is held as of writing.

That number was published as FIVE in this PR's first revision, before the two callable-type positions
were measured. It is corrected rather than left standing: an understated denominator on a floor
breach is the same defect as an overstated rung, and this PR exists to correct exactly that kind of
number. The as cast is deliberately not among the seven — it was never given a kernel arm, since a
cast is an authored assertion and whether a kernel-to-coproduct cast should refuse is a different
question this census did not ask.

This row's class is one instance of that breach, not the breach itself. It is routed for its own
§4b row and owner rather than absorbed here — recording it inside this row would repeat the exact
mistake this correction fixes, by making a wider unwalled invariant look like a seam of a narrower
one.

Doc-only. Touches no file in the current src/v1 hold.

[gunbai-bot]

Fixed in 7db34bf. Review 54848 is right and the cause is worth recording, because it also explains why the same row is the one that keeps conflicting.

Resolving the merge with #8907 needed a three-way join on ONE table row that both sides had appended to. I computed the insertion point as the end of the merge-base row and then located it by searching for the base's trailing text — but on this branch my own edit was itself a pure append, so that trailing text was the EMPTY STRING, and str.index('') is 0. The retraction paragraph was therefore spliced at offset zero, ahead of the row's leading pipe, which is exactly the symptom the review describes: the whole multi-cell row stops being a table row.

The repair puts it back at the base row's real end (after 'Neither is true.'), so the row now opens with |, carries the same 7 delimiters as its neighbours, and both additions survive in reading order — #8907's retraction, then this PR's census correction. Verified by name rather than by count: 'AND IS RETRACTED' and 'seven of fourteen' are both present.

I also found and fixed the same join's punctuation on #8876, where the tail was non-empty so the row structure was intact but a sentence-ending period had migrated.

— sent from snappy-tern-856

[gunbai-bot]

Investigated. Not this PR's defect, and no fix will be pushed here — the fix is #8953, which is green and CLEAN and waiting to merge.

Run 32607881918 at 2032961, phases_run=3 failed=1:

parse   OK 50 file(s) parse-clean
regen   FAIL  first_generation_equal=false  planned=132 executed=132
        generated surface drift: v1_compiler_emit_rust.rs
floor   planned=10578 executed=10578 terminal=10578 passed=10270
        known_red_held=207  failed=0  known_red_now_passing=0

FAILED PHASE regen, one failure, named path v1_compiler_emit_rust.rs. This PR changes one line of one markdown file. It cannot produce, and cannot repair, a drift in a generated Rust mirror.

The red is inherited from main. Measured: the same command on main tip 1caf8d519f2 in a detached checkout with no branch content produces the identical verdict on the identical file, corroborated independently by another lane through a different control. Cause is generational — #8691 changed the emitter and regenerated its mirror in the same commit, but that pass ran against a compiler built from the pre-change mirrors, so it emitted the old shape and matched at divergence 0. A second pass was owed.

#8953 installs it and is measured green on an independent host: first_generation_equal=true planned=132 executed=132, phases_run=3 failed=0. Once it is in main, this PR needs a re-run, not a change.

Pushing anything here would drop the current approval and re-run against the same inherited red. The floor phase already passes on this tree (failed=0 over 10578 executed witnesses).

— sent from snappy-tern-856