MQ-1: list literals lower whole as their free-monoid construction, through the one value reader

[gunbai-bot]

MQ-1 (work item adhoc-6c4a2f19-afa). The base is main.

What changes

A list literal is the flat free-monoid introduction. List<T> is std.algebra FreeMonoid<T> (dag/std/algebra.dag). [e1, .., en] lowers to one Transform. Its head is the resolved reference to std.algebra.FreeMonoid, and its remaining positional children are the elements in order. [] is the Transform with the head alone.

• Authority for the shape: std.literal_elaboration UnicodeScalarSequenceUnfold. It names the flat list-literal node as "the language's canonical FreeMonoid introduction" and rejects a cons^n nesting for two reasons: it is O(n²) under a sequence-backed carrier, and n-deep it exceeds the emitter's bounded recursion fuel.
• Recorded reversal. This PR first lowered to a right-nested list_append over freemonoid_singleton calls. That forked the authority above. Reading std.literal_elaboration for the caret slice surfaced it, and the gentle-koi-724 / neat-boar-16 ruling reversed it to the flat form before landing. The nested lowering and freemonoid_singleton (left with no consumer, §3c) are deleted.
• One producer, body_lower_list_literal, reached from body_lower_primary_expr. Every value position reads through body_lower_value_lowered, so all of them get it: call args, field inits, let values, operands and scrutinees. There are no per-position fixes.
  • Each element is lowered whole. One that can't be lowered refuses at the element (body_lowering_reason_list_element_unlowered).
  • An unreadable literal shape refuses as body_lowering_reason_list_literal_shape_unread.
• One infer introduction case in v2.compiler.infer, infer_transform_freemonoid_introduction. It runs before application inhabitance, because the head is a type and not a function.
  • All elements must unify to one T, compared with provenance stripped. The first element that differs refuses located at that element (infer_list_element_type_mismatch).
  • The result type is FreeMonoid<T>.
  • [] derives no T here: it stays on the counted GroundingNotDerived frontier rather than receiving a guessed T.
• The head names std.algebra, not v2.std.algebra. v2.std.algebra imports v2.std.node, so the list literals in v2.std.node itself would otherwise close a node → algebra → node cycle.
  • freemonoid_empty, list_append and list_snoc_item moved into std.algebra next to FreeMonoid, delete-first with no re-export.
  • Every consumer is repointed: ~200 import lines, the complexity lens's dotted calls, two embedded fixture programs and the census citations.
  • The self-host behavioral shims now use one bridge std_algebra.rs (review 70892).
• Deleted: the call-argument-only refusal (body_lowering_reason_list_literal_unlowered and its route).
• The RFM row list_literal_has_no_lowered_form records the climb, the form and the reversal.

Evidence

• v2.test.claim.namespace_xl0.list_literal_value_lowering is production-fed through module_roots_from_source_root_ingest. Its reader decodes only the flat form. It covers:
  • a list of calls;
  • a nested list;
  • an empty list in argument position;
  • a three-element list in argument position;
  • a depth control: a 200-element literal lowers to one flat node with 200 operands;
  • a mutation control: the first-only, drop-tail and reversed readings are absent;
  • self-reference: a std.algebra module's own list literals should resolve to its own FreeMonoid, and its twin without FreeMonoid must refuse located at the std.algebra.FreeMonoid head.
    • The twin is green.
    • The positive is enrolled expected-red, owner v2 type binders: a type declaration's <T> rides on its member under one unauthorable edge (trigger 1) #12240. The fixture keeps the real generic type FreeMonoid<T> = Empty | Cons { head: T, tail: FreeMonoid<T> }, and v2 resolve refuses it unbound at T. v2 type-parameter binders: <T> lowers onto an Arrow type-binder edge, resolve scopes it, infer instantiates it #12217 scoped <T> for fn signatures only. A type declaration's binders are trigger (1) of generic_type_parameter_resolved_as_an_ordinary_atom_in_v2, which v2 type binders: a type declaration's <T> rides on its member under one unauthorable edge (trigger 1) #12240 lands. This is not a list-lowering defect: the twin shows the head is located and bound. The same gap means the real dag/std/algebra.dag refuses at resolve on its own generic types until v2 type binders: a type declaration's <T> rides on its member under one unauthorable edge (trigger 1) #12240 lands.
• v2.test.claim.infer_list_introduction (supplied inputs at the infer interface; the head is supplied in resolved form via declaration_reference_node, per Resolver-minted declaration references carry an unauthorable marker; the reader never keys on the spine shape a literal also has #12220's marked references): [1, 1] infers to FreeMonoid<Int>; [1, true] refuses at the true; [] derives no type.
• reference_conservation: the list-argument control conserves every element.
• call_argument_value_resolve_refusal: the list arguments reach resolve.
• srv1:
  • At the nested head 54d56d5 (baseline): the claims passed and the first-only mutant reddened them. 0 of 35 paths refused on list_literal_unlowered. The next layer is function literals in value position (MQ-1: function values in value position (lambdas and fn literals) lower to the generic fn Arrow; unwritten types are fresh type parameters #12210).
  • The flat head needs a re-run (neat-boar-16).
• Emission within fuel for the 200-element literal is claimed here only at lowering depth (one flat node). v2 translate/eval consuming list values end to end is the declared follow-on frontier.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed review 70892 in 6350074. The finding was right. The emitted 03_normalize, 03_body_producer and use_site_verdict all import list_snoc_item from std.algebra after the move, but the only Rust shim for it was the v2_std_algebra.rs bridge, and normalize had a second std_algebra.rs stub that held only FreeMonoid.

What changed:

• One bridge, dag/gunbc/instruments/self_host_std_bridge_shims/std_algebra.rs, now holds FreeMonoid and list_snoc_item.
• The v2_std_algebra.rs bridge and normalize's stub are deleted, so there is no second copy.
• The transport rows (self_host_module_behavioral_transport_roster), the three shim lib.rs files, and normalize's declared_source_refs all point at the new bridge.
• No other shim or witness file referenced crate::v2_std_algebra.

Rung: this is consistent by inspection, not by execution. I haven't built these instruments; the build that exercises them is the self-host behavioral run.

— sent from lively-koi-275

[briansrls]

Exact-head re-review of 56a00a6b7765aad1d78889cac502bc4ae06350ae: APPROVE.

Review 5311185213 is closed.

1. Element-type equality is now structural rather than atom-only. infer_type_equal_ignoring_provenance delegates to the existing exact structural equality fold; the supplied nested-equal case establishes FreeMonoid<FreeMonoid<Int>>, and the nested-mismatch case refuses at the differing inner list.

2. The positive inference contract now reads the exact FreeMonoid argument. The Int claim requires FreeMonoid<Int>, and the Bool twin both establishes FreeMonoid<Bool> and rejects FreeMonoid<Int>.

3. The std.algebra bridge transition has executed rather than remaining source inspection. use_site_verdict passes on both the PR and the main control; body_producer passes here while main stops at its independently stale claim-run path; 03_normalize reaches the same unrelated emitted-crate E0308 on both. The shared bridge itself remains unchanged at this exact head, and the former count literal is now an identity join. That closes the pairing concern without over-reading the unrelated normalize failure as a successful behavioral receipt.

The #12202 integration is also complete: the canonical list-introduction reader recognizes the exact std.algebra.FreeMonoid head in both the pre-resolve qualified-spine form and post-resolve declaration-reference form; application_head_read returns NotApplicationHead before ordinary application classification. Controls establish that a lowered list argument and a resolved list introduction are not applications, while the call enclosing a list remains an application.

The flat representation, whole-element ordering controls, 200-element depth control, first-only/drop-head/reversal mutations, self-reference qualification after #12240, and the 0/35 list_literal_unlowered result are mutually consistent. All five exact-head checks are green, including the floor and emitted build.

The stated residuals are honest and do not block this slice: the seven-test canary remains downstream of #12210, and target emission of the 200-element value within fuel remains a separate frontier rather than being claimed here.

Non-blocking documentation cleanup: the PR body still contains the older wording that the std.algebra self-reference is expected-red and that the flat head needs a re-run. Both are superseded by the evidence at this head and should be refreshed before merge, but they do not reopen source review.