Skip to content

Delete the keys/values/has algebra nicknames: the emit refusal was a three-row family, not one method - #8726

Merged
gunbai-bot[bot] merged 5 commits into
mainfrom
session/snappy-ferret-99
Aug 21, 2026
Merged

gunbai-bot[bot] merged 5 commits into
mainfrom
session/snappy-ferret-99

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor

Delete the keys/values/has algebra nicknames: emit's refusal was a three-row family, not one method (five call sites, four of them silent)

The brief asked whether the emit refusal on keys was one method or a
population. It is a family of three, and the count of compile_error!
literals in the emitted tree undercounts it in both directions.

WHAT WAS MEASURED. Emitting the 03_ingest closure
(gunbc compile --entry src/v2/compiler/03_ingest.dag --source-root dag --source-root src/v2 --target rust --dependency-pool-index primary-precedence, 176 files) produced ONE compile_error!("method keys is neither a resolved callable receiver field nor a registered v1_rt bridge function"), at src/v2/std/compilers/target_model.dag
target_derive_supplemental_generic_bound_requirement_nodes_for_contract.
But .keys() has FIVE production call sites in that closure, and the
other four did not refuse -- they emitted (m.clone().keys)(), a field
access on a HashMap, from rust_receiver_has_callable_method_field.
That probe answers yes because std.algebra PartialFunction declares a
callable field literally named keys, so the emitter read a Map receiver
as a record with a keys closure field. Four of five sites therefore
FABRICATED rather than refused; only rustc would have caught them. A
histogram over emitted compile_error! literals cannot see them.

THE ROOT CAUSE IS SS3 NICKNAMING, FORKED ACROSS TWO REALIZATIONS.
partial_function_templates declared both keys and map_keys, both
values and map_values, and has beside map_has -- one concept, two
names. v1_interpreter.rs carried method_call.keys and
method_call.values arms byte-identical to their map_* siblings, and
has as a spelling alternate on method_call.contains. The Rust emitter
registered only the map_* half. So the interpreter accepted a spelling
the emitter could not emit: a path divergence, not an emit-surface gap.

THE CUT (delete-first, SS3): the three nickname rows are gone from
partial_function_templates; the PartialFunction interface fields are
renamed to the surviving canonical spelling (map_keys / map_values /
map_has), which is what removes the callable-field collision; the two
duplicate interpreter arms and the "has" alternate are deleted, and
v1_interpreter_dispatch_generated.rs regenerated from the roster; the
dead std.methods rows are dropped. All 11 .keys() call sites (5
production, 6 test) are rewritten to map_keys(...). values and has
had zero call sites.

WHY THIS IS ADMISSIBLE UNDER THE v1 FREEZE: it is deletion in direct
service of the v2 self-host emission, not growth.

EVIDENCE, BY EXECUTION.

  • Re-emit of the same closure: RC=0, 176 files, 502 advisory (unchanged
    from before the cut), 0 compile_error!("method ..., 0 .keys)().
    The one production keys call now emits
    Rc::new(v1_rt::map_keys(&incoming.entries.clone())).
  • DISCRIMINATING RED, post-cut binary: m.keys() on a Map is now
    refused at resolve with a located diagnostic -- probe.dag:4:40: error: method 'keys' not found on receiver type 'Map(...)'. Before
    the cut the same input compiled with "0 diagnostics" and emitted the
    compile_error! macro. The class climbed from a rustc-visible emit
    marker to a refusal on the source->.dag-acceptance path.
  • POSITIVE CONTROL: count(map_keys(map_insert(empty_map(), "a", 1)))
    evaluates to 1 through the interpreter.
  • claim_executor --required-regen: FAIL on std_algebra.rs drift
    (the candidate diff was exactly this change and nothing else), mirror
    installed, re-run first_generation_equal=true planned=128 executed=128.
  • cargo build --release --bins green (the deleted arms redded E0004
    until the generated dispatch enum was regenerated -- the closed
    vocabulary did its job).

WHAT IS NOT CLOSED, NAMED RATHER THAN LEFT TO BE REDISCOVERED. get /
map_get is the same nickname pair and survives, because both halves are
routable today so it produces no refusal; closing it is a 547-site
rewrite that this diff does not attempt. No witness is enrolled for
"no algebra template name has a map_-prefixed twin", because such a
witness would red on get/map_get on its first run and would need an
exception list -- a second roster beside the algebra authority, which is
the violation it is meant to police. The next-rung trigger for the class
is the get/map_get consolidation, not a lens.

Co-Authored-By: Claude Opus 5 noreply@anthropic.com

…ree-row family, not one method (five call sites, four of them silent)

The brief asked whether the emit refusal on `keys` was one method or a
population. It is a family of three, and the count of `compile_error!`
literals in the emitted tree undercounts it in both directions.

WHAT WAS MEASURED. Emitting the 03_ingest closure
(`gunbc compile --entry src/v2/compiler/03_ingest.dag --source-root dag
--source-root src/v2 --target rust --dependency-pool-index
primary-precedence`, 176 files) produced ONE `compile_error!("method keys
is neither a resolved callable receiver field nor a registered v1_rt
bridge function")`, at src/v2/std/compilers/target_model.dag
`target_derive_supplemental_generic_bound_requirement_nodes_for_contract`.
But `.keys()` has FIVE production call sites in that closure, and the
other four did not refuse -- they emitted `(m.clone().keys)()`, a field
access on a `HashMap`, from `rust_receiver_has_callable_method_field`.
That probe answers yes because `std.algebra` `PartialFunction` declares a
callable field literally named `keys`, so the emitter read a Map receiver
as a record with a `keys` closure field. Four of five sites therefore
FABRICATED rather than refused; only rustc would have caught them. A
histogram over emitted `compile_error!` literals cannot see them.

THE ROOT CAUSE IS SS3 NICKNAMING, FORKED ACROSS TWO REALIZATIONS.
`partial_function_templates` declared both `keys` and `map_keys`, both
`values` and `map_values`, and `has` beside `map_has` -- one concept, two
names. `v1_interpreter.rs` carried `method_call.keys` and
`method_call.values` arms byte-identical to their `map_*` siblings, and
`has` as a spelling alternate on `method_call.contains`. The Rust emitter
registered only the `map_*` half. So the interpreter accepted a spelling
the emitter could not emit: a path divergence, not an emit-surface gap.

THE CUT (delete-first, SS3): the three nickname rows are gone from
`partial_function_templates`; the `PartialFunction` interface fields are
renamed to the surviving canonical spelling (`map_keys` / `map_values` /
`map_has`), which is what removes the callable-field collision; the two
duplicate interpreter arms and the `"has"` alternate are deleted, and
`v1_interpreter_dispatch_generated.rs` regenerated from the roster; the
dead `std.methods` rows are dropped. All 11 `.keys()` call sites (5
production, 6 test) are rewritten to `map_keys(...)`. `values` and `has`
had zero call sites.

WHY THIS IS ADMISSIBLE UNDER THE v1 FREEZE: it is deletion in direct
service of the v2 self-host emission, not growth.

EVIDENCE, BY EXECUTION.
  - Re-emit of the same closure: RC=0, 176 files, 502 advisory (unchanged
    from before the cut), 0 `compile_error!("method ...`, 0 `.keys)()`.
    The one production `keys` call now emits
    `Rc::new(v1_rt::map_keys(&incoming.entries.clone()))`.
  - DISCRIMINATING RED, post-cut binary: `m.keys()` on a `Map` is now
    refused at resolve with a located diagnostic -- `probe.dag:4:40:
    error: method 'keys' not found on receiver type 'Map(...)'`. Before
    the cut the same input compiled with "0 diagnostics" and emitted the
    `compile_error!` macro. The class climbed from a rustc-visible emit
    marker to a refusal on the source->.dag-acceptance path.
  - POSITIVE CONTROL: `count(map_keys(map_insert(empty_map(), "a", 1)))`
    evaluates to 1 through the interpreter.
  - `claim_executor --required-regen`: FAIL on `std_algebra.rs` drift
    (the candidate diff was exactly this change and nothing else), mirror
    installed, re-run `first_generation_equal=true planned=128
    executed=128`.
  - `cargo build --release --bins` green (the deleted arms redded E0004
    until the generated dispatch enum was regenerated -- the closed
    vocabulary did its job).

WHAT IS NOT CLOSED, NAMED RATHER THAN LEFT TO BE REDISCOVERED. `get` /
`map_get` is the same nickname pair and survives, because both halves are
routable today so it produces no refusal; closing it is a 547-site
rewrite that this diff does not attempt. No witness is enrolled for
"no algebra template name has a `map_`-prefixed twin", because such a
witness would red on `get`/`map_get` on its first run and would need an
exception list -- a second roster beside the algebra authority, which is
the violation it is meant to police. The next-rung trigger for the class
is the `get`/`map_get` consolidation, not a lens.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor Author

The red on this PR is a pre-existing defect in the receipt phase, not this change

Recording it here rather than only in chat, because whoever merges this will see a red check.

This PR's own content is green. From run 32448150852:

  • floor: planned=9914 executed=9914 terminal=9914 passed=9607 known_red_held=206 failed=0
  • required-ci: parse OK 50 file(s) parse-clean
  • required-ci: regen first_generation_equal=true
  • required-ci: regen-fixed-point fixed_point_equal=true

The failing phase is receipt, and it fails for two causes, neither of which is a behavioral change introduced here.

Cause 1 — the gate reports DIVERGENT over a byte-identical file

In that same run, regen established that the emitted std_algebra.rs is byte-identical to the committed mirror. The behavioral receipt then installed that candidate over the mirror and reported DIVERGENT. It compared a file against itself and could not answer EQUIVALENT.

The first_difference it printed is kernel_algebra_profile_value() — a function this PR does not touch — with the same seven entries in a different order.

generate_receipt_driver renders every derived call as println!("... = {:?}", call), and that function returns Rc<HashMap<String, AlgebraProfile>>. The two halves of the differential are produced by two separate driver processes, and Rust's HashMap iterates in per-process randomized order.

Proved by execution, independent of how CI scored any run. A one-line driver built against the committed libv1_compiler.rlib, printing that call through {:?}, run 20 times on an unchanged tree:

20 distinct transcripts out of 20 runs

So this is the normal outcome for a map-returning function in a selected authority, not a bad night. The gate does not fail open here — it fails wrong.

Cause 2 — an authority whose mirror this emit cannot produce

behavioral-receipt: gunbc.v1_interpreter_primitive_surface REFUSED — the emit produced no
v1_interpreter_dispatch_generated.rs, so there is no candidate to compare.
Not equivalence: a missing candidate is ignorance

That artifact is produced by main_wet on tools/generated_artifact_gate.dag, not by the stage0 mirror emit, so no candidate can ever exist for that authority. The refusal is correct as written — ignorance is not equivalence — but it means any PR touching that roster reds this phase by construction.

Disposition

Both are being handled in a separate PR, coordinated with the session already editing this phase (#8699), so the per-cause counter vocabulary is shared rather than forked. Not fixed here: riding a CI-gate repair in under an algebra-nickname review is how a green PR becomes a red one.

Noting one limit on the fix I proposed, so it is not read as more than it is: keying the exclusion on the outermost return type is a proxy for the real property, which is the value's transitive shape — a record containing a HashMap renders nondeterministically and would pass a return-type check cleanly, and HashSet has the same property. The higher rung is deterministic emission (BTreeMap), which makes the nondeterminism unwritable rather than detected and excluded.

— sent from snappy-ferret-99

@gunbai-bot

gunbai-bot Bot commented Aug 21, 2026

Copy link
Copy Markdown
Contributor Author

Correction and current status, on green main

My earlier comment on this PR is now partly superseded, and one prediction I made about this run was wrong. Correcting both here rather than leaving the stale version as the record.

What changed since that comment

Main was red for about an hour on dag/gunbc/fleet_desired_admission.dag:169 (a non-exhaustive match; FleetDesiredRevision grew from two variants to four in #8701 and this consumer was not updated in the same commit). That is fixed by #8744, main is green again, and this branch has merged it. The floor now passes on this PR: planned=9921 executed=9921 terminal=9921 passed=9614 known_red_held=206 failed=0.

I had also attributed that defect to #8643. That was wrong — #8643 merely last-touched the file and its two-arm match was exhaustive and correct when written. #8701 grew the type. For a type/consumer mismatch the owner is whichever side landed second, not whoever last edited the file with the match in it.

The prediction I got wrong

I predicted this run would fail on the missing-candidate cause alone. It failed on both receipt causes:

behavioral-receipt: gunbc.v1_interpreter_primitive_surface REFUSED — the emit produced no
  v1_interpreter_dispatch_generated.rs, so there is no candidate to compare
behavioral-receipt: std.algebra DIVERGENT over 31 derived calls — seed:
  kernel_algebra_profile_value() = {...}

The reason is simple and I should have caught it: the fix for the DIVERGENT cause is in #8743, a different PR. This branch carries the unpatched gate, so that cause still fires here. I had "that cause is fixed" in mind without asking which tree carries the fix — the same class of error as reading a green from a merge ref that predates the change you care about.

Where this actually stands

Everything this diff owns is clean:

required-ci: parse OK 50 file(s) parse-clean
required-ci: regen first_generation_equal=true
required-ci: regen-fixed-point fixed_point_equal=true
required-ci: receipt-selftest OK both arms discriminate
required-floor: ... failed=0
required-ci: phases_run=6 failed=1   (FAILED PHASE receipt)

Two gate causes remain, neither in this diff:

  1. std.algebra DIVERGENT — the receipt renders every derived call through {:?}, and kernel_algebra_profile_value returns Rc<HashMap<..>>, which iterates in per-process random order. Measured: 20 distinct transcripts over 20 runs of one unchanged binary. In the run before this one, required-regen reported first_generation_equal=true for std_algebra.rs and the receipt then reported DIVERGENT over that byte-identical file. Fixed by The behavioral receipt reported DIVERGENT over a byte-identical file: measure instability instead of rendering it as a difference #8743, which is green and approved; verified end-to-end against this exact tree, where the verdict becomes EQUIVALENT over 30 derived calls, with 1 EXCLUDED as nondeterministically rendered — kernel_algebra_profile_value.

  2. the missing candidate — v1_interpreter_dispatch_generated.rs is produced by gunbc.generated_artifact_emit through main_wet, not by the mirror emit, so this fragment asks the wrong generator. The refusal is correct as written (ignorance is not equivalence). Not fixed, and deliberately not worked around: the clean fix routes through the single artifact→content authority, and calling the per-artifact emitter directly would be a second dispatch beside the real one.

So this PR needs #8743 merged, then cause 2 resolved. I am not re-running before #8743 lands, since a re-run would reproduce both failures.

— sent from snappy-ferret-99

@gunbai-bot
gunbai-bot Bot merged commit dd1ac18 into main Aug 21, 2026
1 check passed
@gunbai-bot
gunbai-bot Bot deleted the session/snappy-ferret-99 branch August 21, 2026 14:31
gunbai-bot Bot pushed a commit that referenced this pull request Aug 21, 2026
…etions, which is exactly what the merge driver refused to guess

Nine .dag files recut (0 refused; target_model 4456, scm_merge_witness 199,
scm/merge 141). Regen holds at 0 hard diagnostics.

THE INTERESTING CONFLICT was v1_interpreter_dispatch_generated.rs, and neither
side's file was correct:

  main deleted   MethodCallKeys / MethodCallValues        (#8726, algebra nicknames)
  this branch deleted  the two import-closure builtin arms (the cut)

Taking main's file reintroduced the import-closure arms and broke exhaustiveness
against this branch's v1_builtin_arms! macro. Taking the branch's file kept the
keys/values arms that main's interpreter no longer handles, breaking
exhaustiveness the other way. The resolution is both deletions applied to one
file -- a merge no single side contains.

That is precisely why the generated-artifact merge driver REFUSED rather than
answering: it left the ours side in the worktree, marked the path unmerged, and
printed the regeneration recipe. Its refusal was correct and taking either side
whole would have been wrong in a way that compiles on exactly one of the two
possible builds. The seed rebuild is what established it, twice, in both
directions.

I MISREAD THE DIFF DIRECTION ONCE ON THE WAY: `git diff origin/main -- <file>`
shows main on the `-` side, so the import-closure arms I read as "main deleted
these" are main HAVING them and the branch having deleted them. I acted on the
wrong reading first, took main's file, and the build refused. Recorded because
the wrong reading is self-consistent and produces a confident, wrong resolution.

FALSE POSITIVES CHECKED, NOT COUNTED: grepping for surviving calls to the deleted
keys/values/has nicknames returned 5 hits. All five are prose or unrelated code --
three CSS `:has()` selectors inside string literals and two LOCAL `fn has(s, p)`
definitions in witness files. Zero real orphans. The count alone would have read
as five call sites needing repair.

Also forced to one side rather than trusted: std_algebra.rs auto-merged CLEANLY
and is generated, which is the hybrid case that appears in no conflict list.
v1_interpreter.rs also auto-merged but is HAND-maintained per
HAND_MAINTAINED_STAGE0_FILES, so its text merge is legitimate and was kept.

Sole remaining blocker is unchanged: the emitter, std.types._list from to_snake
over a dotted address.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 21, 2026
… floor named it before I did

CI floor refused with `variant 'Empty'/'Cons' not found in type 'FreeMonoid'`
(dag/std/algebra.dag). Cause: taking main's .dag and recutting it DE-QUALIFIED
SELF-REFERENCES. The recut tool subtracts the file's own module from the
candidate declarer set, so a name declared in the same module is never qualified
-- correct while main's imports supply local scope, wrong on this branch, where
bare names do not resolve in the floor's whole-pool frame.

  dag/std/algebra.dag                      6 self-references lost
  src/v2/std/compilers/target_model.dag  756 self-references lost

THE BRANCH ALREADY LEARNED THIS ONCE. Commit 0594b34 is "revert dag/std/types.dag
de-qualification: bare NonEmptyStr is unresolved in the floor's whole-pool frame
(floor preparation refused, 3739 modules)" -- same mechanism, sibling file, and
the recut re-introduced it on two more files because the fix lived in the file
rather than in the tool.

RESOLVED AS A 3-WAY MERGE, NOT A REVERT, because both sides had real changes:
main renamed the algebra nicknames (keys/values/has -> map_keys/map_values/
map_has, and `.keys()` method calls -> `map_keys(..)` free calls, #8726) while
the branch carries the qualification. Taking either side whole loses the other's
work. Merged with git merge-file against the true base and resolved the 3 hunks
to main's semantics PLUS the branch's qualification -- the same union the
dispatch table needed in the previous commit.

Verified by count rather than by inspection: self-qualified references now equal
the pre-merge branch exactly (algebra 5, target_model 786), main's rename is
present (4 map_keys free calls) and no `.keys()` method call survives.

A CHECK THAT LIED, FIXED: my first sweep for this regression across all 9 recut
files printed "no REGRESSED lines" while silently erroring on 6 of them -- `grep -c`
returns 0 both for no-match and no-file, and the shell comparison then failed on
"0\n0". Re-run properly, 9 files: 3 new, 6 compared, 0 regressed.

NOT FIXED HERE, and confirmed pre-existing rather than merge-introduced: CI's
merge-admission-stamp refusal (src/v2/compiler/02_parse.dag `no field
'expression' on type 'C'`). That file is untouched by this merge, last modified
by earlier branch commits, and differs from main by 1211 lines.

Regen still 0 hard diagnostics. The emitter blocker now has a THIRD observed
position -- a Rust type-alias RHS, `pub type SemVerIdentity = std.types.NonEmptyStr;`
-- beside the generic argument and the struct literal. One root: qualified type
references are never translated into Rust paths.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Aug 21, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Aug 21, 2026
…not #8597's

Commit bbf4350 in this branch blamed #8597 for the two surviving `.keys()`
call sites. That is wrong, and a commit repairing a main-wide red while
misattributing it puts a false fact in the durable record beside a true fix.

Verified per-commit on the file rather than taken on trust:

  #8726  dd1ac18   +6 map_keys lines,  +0 .keys() lines
  #8749  8077603   +0 map_keys lines,  +2 .keys() lines   <- introduced both
  #8597  aa8a65e   +0 in either direction, touched neither

THE MECHANISM IS ALSO NOT WHAT bbf4350 SAID. It described an incomplete
conversion -- six done, two missed. It was not. #8726's sweep was COMPLETE when
it ran: it converted every site that existed at that point. #8749 then
introduced NEW uses of the retired spelling, from a branch that predated the
deletion. No census over #8726's tree could have found them, because they did
not exist yet.

So the class is REINTRODUCTION AFTER A SWEEP, not a missed census, and it is a
merge-time question rather than a branch-time one: neither branch is wrong on
its own, and the defect exists only in their union. Nothing guards that today.

This two-line repair is therefore the right SCOPE and explicitly NOT the root.
It clears a main-wide red; what stops the next reintroduction is unbuilt.

Caught by quick-lynx-620 pushing back on the attribution I was given.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 21, 2026
…eted (composition break, #8726 + #8749) (#8780)

Main has been red since 15:48 on the witness floor's preparation phase:

  required-ci: FAILED PHASE floor refused: subject=e8feaa4cce2b2557 modules_resolved=3775
  src/v2/test/claim/emit/trait_derive_supplemental_generic_bound_contract_test.dag:486:30
    error: method 'keys' not found on receiver type 'Map(...)'
  src/v2/test/claim/emit/trait_derive_supplemental_generic_bound_contract_test.dag:490:27
    error: method 'keys' not found on receiver type 'Map(...)'

NEITHER CONTRIBUTING PR IS DEFECTIVE. #8726 (merged 14:31:10Z) deleted the keys/values/has
algebra nicknames, converting six sites in this very file to map_keys. #8749 (merged 15:48:08Z)
added two NEW .keys() sites to the same file. #8749's last CI ran at 11:30 -- three hours before
#8726 landed -- and nothing recompiles a sibling before merge, so no PR-head gate could observe
the pair. Green alone, red on contact.

THE FIX is the spelling #8726 already established in this file for its other six sites: the free
function map_keys(m), not a method on the receiver. Two lines.

VERIFICATION, both arms executed on the real acceptance path
(gunbc compile --source-root dag --source-root src/v2 --entry <this file>):

  AFTER  (map_keys)  exit=0  'method keys not found'=0  hard diagnostics=0  annotations=0
  BEFORE (.keys())   exit=1  'method keys not found'=2

The BEFORE arm asserts the REASON, not merely that the tree builds: it reproduces the literal
diagnostic, twice, at the two sites. A green that came from the witness no longer being
discovered would not produce that. The revert arm printed its own site count (2) before running,
so a silently no-opped edit could not have passed as a red -- an earlier attempt at this arm DID
produce a false zero (it reconstructed the pre-fix file via `git show origin/main:<path>` on a
shallow runner, which failed, emptied the file, and refused for an unrelated 'no provenance'
cause while scoring 0 on the keys grep). The count guard is what caught it.

SCOPE. Exactly two sites corpus-wide under dag/ and src/v2. src/v1/runtime_rust.dag:179 also
matches a bare grep for .keys() but is a Rust STRING LITERAL emitting m.keys().cloned().collect()
for HashMap; it is correct emitted Rust and is deliberately untouched. A mechanical sed over the
corpus would have rewritten it.

NOT SETTLED HERE: map_keys exists in both a free-function and a method spelling. That is a
single-authority question and does not belong in a main-red repair.

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>
briansrls pushed a commit that referenced this pull request Aug 21, 2026
… spelling with no arity row is a third state, not "not a container" (#8778)

`container_expected_arity` returning Absent meant two different things and the
callers could only read one of them. For `String`, `Bool`, and every user record,
Absent is the correct answer: not a container, no arity expectation. For a
container spelling with no row — a qualified `std.types.List`, anything the arity
table does not carry — Absent is ignorance, and three call sites rendered it as
the first meaning:

  04_types  is_fully_resolved      "not under-parameterized"  -> claims RESOLVED
  trait_derive_emit  v1_type_expr_is_keyed_map  "not a keyed map"
  03_normalize  check_bare_containers          no diagnostic at all

The first is the one that hurts: a resolution claim about a name whose arity the
compiler does not know, and the wrong answer produces no evidence of itself
(DESIGN section 5, the empty-observation narrow).

WHAT LANDS

`v1.std.core` `container_spelling_verdict` gives the lookup its third answer:
ContainerSpellingDeclared / NotAContainerSpelling / ContainerSpellingUnknown. Its
known-container roster is read from `container_type_arity` itself, so this is not
a third table. `authored_container_spelling_verdict` adds the authorship guard.

`v1.compiler.normalize` `check_bare_containers` is where the class becomes LOUD:
it already walks every node of every module and already owns a diagnostics
channel, so the new `ContainerSpellingUnrecognized` diagnostic is emitted there —
typed, located, counted, once per authored occurrence. Missing rows now announce
themselves instead of having to be guessed at.

`v1.compiler.infer_types` `type_resolution_verdict` is the threaded refusal:
FullyResolved | UnderResolved | ContainerSpellingUnresolvable. `is_fully_resolved`
survives as a NAMED collapse over it for its thirteen call sites, all of which sit
in boolean conditions with no channel to carry a diagnostic; a refusal reads as
NOT fully resolved, which is the conservative arm and never widens to the resolved
answer the old Absent arm gave. Reporting from the query instead of from the
normalize walk would emit one diagnostic per node per asking walk.

`v1_type_expr_keyed_map_verdict` does the same for the derive walk. Its algebra
lookup deliberately keeps the FULL authored name: matching a leaf to REFUSE is
conservative, matching a leaf to DECIDE would collapse a qualified spelling onto
the kernel row and select the wrong template.

THE DISCRIMINATOR, AND THE SIX FALSE-REFUSALS

Refusing every name whose leaf is a container name would refuse real code:
`check_service_field_access_node` renders a service operation as a LEAF TYPE NODE
via `nominal_type_ref`, so `cron.Tab.List`, `Filesystem.List`, `github.Pulls.List`,
`tmux.Session.List`, `os.Hostname.Set` and `req.Header.Set` all reach this walk
and none is a container. They are excluded by AUTHORSHIP — a synthesized node
carries a `<kernel:...>` span that is in no source index — so a seventh service
operation named after a container needs no edit and no exception list.

EVIDENCE

Eleven fixtures in `infer_semantics_witness`, including the six false-refusals
asserted NOT refused and the same spelling asserted REFUSED when authored, which
is what keeps the first six from passing for a walk that simply stopped refusing.
Confirmed by execution: witness green; a perturbed expectation reds with
ContainerSpellingUnresolvable { name: "std.types.List" }; `--required-regen`
first_generation_equal=true and `--required-regen-fixed-point` fixed_point_equal=true
over the 129-file seed closure, so the wall refuses nothing that compiles today.

Also repaired in passing: this witness asserted `has`/`keys`/`values` on Map,
three nicknames #8726 deleted, so it panicked on main before reaching anything
new. Renamed to the surviving `map_has`/`map_keys`/`map_values`; no assertion
dropped.

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Aug 21, 2026
…lta, so #8758's carrier gets a corrected cause (two roots, per-site) and the four-name roster goes as cleanup (#8772)

* wip: lambda_argument_scope (roster removal + per-arg lambda scope)

* Correct #8758's carrier: the mechanism it names is refuted, the sites and the derivation stand

The row asserted a cause -- emit_typed_call's four-name collection_scope gate
produces the three E0282 sites. Two-arm emission over three closures, from two
binaries whose difference was confirmed before either arm ran, is byte-identical:
258 files per arm, 0 differing files, 0 differing lines. A third arm deleting the
binding entirely is also identical, which is what separates "refuted" from "my
replacement happens to agree with the roster".

The mechanism cannot reach emitted bytes: scope.locals has exactly one reader in
the Rust emitter (is_already_optional) on the arm taken only when a node carries
no resolved type, and the declared parameter types the gate was meant to supply
are already bound onto the lambda's param nodes one stage earlier by infer_expr's
ExprCall/ExprLambda path.

THE DISSOLUTION TRIGGER WAS THE DANGEROUS HALF. It keyed on repairing that gate,
so it was exactly satisfiable by a change that fixes nothing -- delete the roster,
retire the row, three sites still red. A false cause misleads a reader; a false
trigger disposes of the evidence. The replacement keys on the three sites emitting
and compiling without an inference failure, and says outright that no repair to
the gate satisfies it.

Not over-retracted: the three sites, the E0282 x E0061 intersection that derived
them, and UpperBoundPendingResidueCheck with its standing prediction all survive
untouched -- none depended on the cause. The surface is still a bare-name-keying
shape, now at the honest strength: syntactic, with no observable consequence.

The reach figure is deleted rather than softened; it sized the blast radius of
repairing a mechanism that changes no byte.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Per-site cause on the lambda-typing-gate row, and finish #8597's map_keys conversion

CARRIER: cause becomes a PER-SITE field, because the sites and the causes were
established by different instruments with different groupings. The three sites
were derived together by one intersection over one subject; the causes were
established one site at a time by three cargo probes over three emitted
closures. A single row-level CauseAttributed would force one instrument's
grouping onto the other's -- the same collapse this row was already corrected
for once.

  parse/parse_lexeme_digest        StringDeclarationSiteAlias   (help annotates ch)
  target_model/...apply_callee     UntypedFoldInitAccumulator   (help annotates acc)
  tokenize/lex_match_prefix        StringDeclarationSiteAlias   (help annotates a)

Three real reds, TWO causes. Row-level CauseUnlocated is retired rather than
answered, replaced by CauseGrouping = CausePerSite. The dissolution trigger now
states that no single repair can fire it.

The discriminator is free and sits in output everyone reads past: rustc's help
names WHICH parameter it wants annotated. Element means the collection could not
supply T; accumulator means the fold's init could not supply its own type.

Also recorded: a pre-registered hunch that was REFUTED (field access on the
lambda parameter was named in advance as the first place to look, and rustc's
caret is on acc, never on row), and a warning that four E0282s in the parse
crate belong to the held contains class so a count there is not a population.

MAP_KEYS, NOT MINE AND SAID SO: the witness floor refuses on
trait_derive_supplemental_generic_bound_contract_test.dag with "method 'keys'
not found on receiver type 'Map(...)'". Confirmed pre-existing on main at
c603c06 -- same file, same two lines, same message, on a commit unrelated to
this branch. #8597 converted six sites in that file to map_keys and left two
behind. This applies the same conversion to the stragglers; it repairs a
main-wide red, not a defect this branch introduced.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Retract 'closes a real leak' in the emitter comment: the same null refutes it

The per-argument narrowing was described as closing a real leak -- one lambda's
parameter names visible while emitting sibling arguments and filled defaults.
That is a mechanism claim, and the measurement in this PR refutes it exactly as
it refutes the roster: scope.locals is read once in the whole Rust emitter, on
an arm taken only when a node carries no resolved type, so nothing measured
shows the leak producing a wrong byte.

It is now stated as construction cleanup with no measured current consequence --
narrowed because the narrow form is the correct construction, not because a
defect was observed, and unearned as a repair until a fixture makes it
observable.

A change whose whole point is that an unmeasured mechanism claim was wrong must
not carry a second unmeasured mechanism claim in its own text. Same defect, one
level down. Caught by external review, not by me.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* Correct the map_keys attribution: the two .keys() lines are #8749's, not #8597's

Commit bbf4350 in this branch blamed #8597 for the two surviving `.keys()`
call sites. That is wrong, and a commit repairing a main-wide red while
misattributing it puts a false fact in the durable record beside a true fix.

Verified per-commit on the file rather than taken on trust:

  #8726  dd1ac18   +6 map_keys lines,  +0 .keys() lines
  #8749  8077603   +0 map_keys lines,  +2 .keys() lines   <- introduced both
  #8597  aa8a65e   +0 in either direction, touched neither

THE MECHANISM IS ALSO NOT WHAT bbf4350 SAID. It described an incomplete
conversion -- six done, two missed. It was not. #8726's sweep was COMPLETE when
it ran: it converted every site that existed at that point. #8749 then
introduced NEW uses of the retired spelling, from a branch that predated the
deletion. No census over #8726's tree could have found them, because they did
not exist yet.

So the class is REINTRODUCTION AFTER A SWEEP, not a missed census, and it is a
merge-time question rather than a branch-time one: neither branch is wrong on
its own, and the defect exists only in their union. Nothing guards that today.

This two-line repair is therefore the right SCOPE and explicitly NOT the root.
It clears a main-wide red; what stops the next reintroduction is unbuilt.

Caught by quick-lynx-620 pushing back on the attribution I was given.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* File the second cause as its own row: untyped fold-init accumulator

The target_model site in lambda_typing_gate_sites has a distinct cause with a
distinct repair, so it gets a row. empty_map() in a fold's `empty:` position
emits as v1_rt::rc_empty_map::<_, _>(); the only thing that could close those
type parameters is the fold's own closure, which RECEIVES the accumulator -- so
the target compiler is asked to infer a parameter's type from a body that uses
it, and refuses.

What rules out the neighbours, since this site was first filed under one: the
collection is a genuine List<TargetEffectCalleeRow>, rustc never asks about
`row`, and `acc` traces to the init rather than to the collection or the
callee's spelling. The discriminator is rustc's own help text naming which
parameter it wants annotated -- |acc: Type, row| here, |acc, ch: Type| for the
collection-realization class.

POPULATION IS ObservedSitesOnly. One measured site is not a census: this one was
found only because it sat in a partition being probed member by member, and no
sweep for untyped empty-collection literals in fold-init position has been run.
The sweep is named rather than performed so the absence is a stated gap, not an
implied zero.

The site STAYS LISTED in lambda_typing_gate_sites with a cross-reference, because
that row records that the three were derived TOGETHER by one intersection over
one subject. Removing a member because its cause turned out to differ would
destroy the only artifact of that derivation.

Trigger is keyed to the site compiling, not to any repair -- the sibling row
learned that the expensive way. It also refuses the cheap escape: annotating the
closure at the call site moves the obligation to the author instead of deriving
it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* The census refused a synthetic control literal: give it the honest cause, not a copied one

Adding per-site `cause` and `cause_receipt` to LambdaTypingGateSite made every
existing literal incomplete, and the floor refused exactly one:
dag/test/claim/long/cited_symbol_resolution_witness_test.dag's planted red
control, landed by #8775 after this branch's type change was authored. That
refusal is the fail-closed census working -- the widened type surfaced its one
real dependent loudly rather than silently defaulting it.

The planted site is SYNTHETIC: it names a declaration that does not exist, so no
probe can have measured why it fails to type and there is nothing for a receipt
to point at. It therefore carries SiteCauseUnmeasured / NotYetProbed, and an
annotation says why it must stay that way -- copying a real site's cause here to
make the literal look complete would put a measured attribution on a specimen no
run produced, which is the fabricated-receipt failure the receipt field exists to
prevent.

Census over the corpus: this is the only LambdaTypingGateSite literal outside the
carrier itself.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants