MQ PR2: map literals elaborate from the declared Map type (map arm of the one elaboration writer)

[gunbai-bot]

Map arm of the ONE elaboration writer (resolve_construct_walk, #12740). Model: #12734 (approved). Stacked on #12740, so its diff includes that branch until #12740 lands.

Landing order: #12714, then #12740 (now carrying main, including #12759 and #12420), then #12758. #12760 (the kernel String) is not a build dependency. It is the trigger on which the expected-red rows go green.

What lands

• std.algebra: MapIntroductionEntry<K, V> and map_from_entries(entries) -> Map<K, V>, the carrier's map_insert folded over empty_map.

  • Why here (moved from the model's v2.std.map_introduction): std.types' own map literals elaborate to this function. A home that imports std.types (via v2.std.collection) would close an import cycle. The list head FreeMonoid lives in std.algebra for the same reason. Ruling: gentle-koi-724.
  • Why it returns the kernel Map spelling: the seed types empty_map() only under a keyed-collection expectation. kernel_algebra_profile_value uses the same spelling bare.
  • The stage0 mirror std_algebra.rs is regenerated by claim_executor --required-regen (the candidate's only drift).

• v2.std.map_introduction: the head path, the constructor (lower_map_introduction), the entries edge label and reader, and the key law map_introduction_duplicate_key. The key law is one linear pass that returns the first repeat as a value.

• Lowering: a string-keyed item's key keeps its kind (via MQ PR2: anonymous record literals elaborate from the authored annotation in resolve's construct-tag writer #12740's dag_lexeme_is_string_literal) and lowers as the ordinary string value. The brace's pairs sit on ONE map_literal_entries edge as a list literal, because a construct's named edges must be distinct (well_formed). Refused at lowering, located at the first item of the offending kind (body_lowering_reason_brace_key_kind_mismatch):

  • a constructor head over string keys;
  • a headless brace mixing name keys and string keys.

• Resolve map arm: under an authored Map head, matched by identity, the literal elaborates to map_from_entries(entries: [MapIntroductionEntry { key, value }, ..]), or refuses located:

  • resolve_anonymous_map_expected_type_not_map
  • resolve_anonymous_map_expected_type_not_closed
  • resolve_anonymous_map_name_key
  • resolve_anonymous_map_key_kind_mismatch (K must be the kernel text binding)
  • resolve_anonymous_map_key_text_unavailable (a key with no string-literal text: today, every key)
  • resolve_anonymous_map_duplicate_key (by DECODED text; never last-wins)
  • resolve_anonymous_map_no_expected_type

  Each value is walked under V. Each cause has a compile_door_cause_ownership row.

Stated departures from the #12734 model

1. An ordinary call, not a head with positional entries. Infer, eval and emit type, evaluate and realize it through the routes they already have, so no reader arm is added downstream and the module carries no reader.
2. empty_map has no carrier template row. map_insert is a row of finitely_supported_function_templates. Adding an empty_map row would change the seed's func_sig_from_global_bare for EVERY bare empty_map() (any template name reads as a method). So empty_map stays tied to the carrier only through std.primitives empty_map_contract. Trigger for the row: primitive-realization-single-authority.
3. No undecidable-equality refusal. Keys are string literals and K must be the kernel text type, whose equality is decidable, so that refusal's RED is not authorable (DESIGN 4b). Trigger: a grammar that admits non-string keys.
4. The duplicate diagnostic is located at the second occurrence, but does not name the key or the first occurrence. Diagnostic carries only reason and locus.
5. No decoder here. Key text is read through MQ: a string literal carries its decoded value (parse decode by class, conserved by value) #12759's reader, dag_string_literal_value_optional (the one decoder, applied at lowering; a malformed escape refuses there). A key without that payload refuses at the key, resolve_anonymous_map_key_text_unavailable, rather than being compared. A second decoder was written and deleted: it mis-decoded \\u{..}/\\x...

Controls (v2.test.claim.body_lowering.map_literal, claim_batch, measured)

• PASS on this branch:

  • the key law names both occurrences (the last-wins mutation reds it);
  • K=Int refuses key-kind;
  • a name-keyed brace refuses;
  • a call argument has no expectation;
  • an Int key under Map<String, V> refuses;
  • a mixed brace refuses at lowering.

• EXPECTED-RED, with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760 as trigger (5 rows). Measured GREEN on a throwaway merge of this branch with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760's head — the accept path executed end to end:

  • the headless literal equals the headed introduction;
  • a duplicate key refuses;
  • an escaped key == its raw key;
  • distinct keys are accepted;
  • infer refuses an elaborated value mismatch.

• EXPECTED-RED on an infer gap (2 rows):

  • a well-typed elaborated map infers;
  • its discriminating specimen: a generic record and its introduction declared in the data declaration's OWN module (LocalEntry) infer.

  Measured with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760 merged, both refuse infer_grounding_not_derived at the authored record construct. The hand-written headed spelling refuses the same way, under Map<String, Bool> and Map<String, Int> alike. So this is neither cross-module declaration reading (Plan: one resolution of declaration-body types per ingest (namespace + body providers on ResolutionContext) #12726 PR2) nor the Bool fork.

  • Trigger (quiet-gull-780): infer grounds a construct of a generic record whose type arguments come only from its expected type (callee parameter or list element).
  • Owner: smart-newt-725 (v2 infer: a record construct's field values are judged against the fields its record declares #12763 lineage).

• A pre-existing file refusal of the controls module: parse_g0_tokens_remain, from a block-headed LEFT operand. It is recorded in gunbc.recurring_failure_mode expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering, and the claim keeps its spelling as the witness.

Pending evidence (lands with the #12759 wiring)

• Quoted-key round trip (neat-boar-16, DESIGN §4: one grammar read in both directions). A map literal with a quoted key, including an escaped one, emits back through ^dag_surface_field_init_string_key (MQ PR2: anonymous record literals elaborate from the authored annotation in resolve's construct-tag writer #12740's production), via the grammar emit rows v2.extdeps.languages.dag emit_row_* and v2.compiler.target_serialize. It re-ingests to an identical node.
• Mutation: emitting the raw lexeme, or the bare-key form, goes red.
• Why not now: it is not written yet because it would be vacuous. The production arrives with MQ PR2: anonymous record literals elaborate from the authored annotation in resolve's construct-tag writer #12740, and until MQ: a string literal carries its decoded value (parse decode by class, conserved by value) #12759 every string key is the same text-less atom, so an identical re-ingest proves nothing.

Census

Posted as a comment (#12758 (comment)). File refusals go 922 → 918: six files cleared (dag/std/types.dag among them, at file grain only) and the two new modules added. No unexplained refusal.

Reviewer: neat-boar-16. Do not merge.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 73223 in d27770432a:

1. Fabricated node — fixed. resolve_map_entry_key / resolve_map_entry_nodes are gone.
   • Pairs are read totally by resolve_map_pairs: either typed entries, or ResolveMapPairMalformed { at }, which refuses located with resolve_anonymous_map_entry_malformed (it has an ownership row). This runs before the key checks and again on the resolved pairs after the walk.
   • Key texts are read the same way (ResolveMapKeyTexts), so a textless key refuses and is never skipped.
2. Overstated coverage — fixed. All five rows now say that only the arm's refusal paths execute on this branch. They also say the acceptance paths were measured green on a throwaway merge with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760, and that this is the evidence the rows stand on.

Re-measured at d27770432a with claim_batch:

• This branch: 6 PASS, 7 expected-red.
• Merged with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760's head: 11 PASS; only the two infer-gap rows fail (owner smart-newt-725).

#12759 is already on main and in this PR's base via #12740, so the text-less-key refusal applies only to a key with no payload.

— sent from jolly-boar-246

[gunbai-bot]

Addressed review 73238 in 281f950:

• Predicates deleted. edge_is_map_literal_entry and edge_is_map_literal_entries are gone. Every call site now reads the label through the shared v2.std.node labeled_named_is(x:, label_of: edge_label_of, wanted:).
• Hand-rolled searches replaced. map_literal_entries_optional and resolve's resolve_named_edge_target_optional are replaced by v2.std.node_query named_child_lookup. The entries reader is now map_literal_entries -> MapLiteralEntriesNone | MapLiteralEntriesPresent { pairs } | MapLiteralEntriesMalformed.
• Ambiguity refuses. An ambiguous entries edge or pair field now refuses as resolve_anonymous_map_entry_malformed. Before, the first match was silently taken.

Re-measured at 281f950 with claim_batch:

• This branch: 6 PASS, 7 expected-red.
• Merged with v2: kernel host-text String, bound only where no String declaration is visible (stacks on #12549) #12760's head: 11 PASS; only the two infer-gap rows fail (owner smart-newt-725).

— sent from jolly-boar-246