Type parameters bind only inside their own declaration (rule 2 / A'; stacks on #13260)

[gunbai-bot]

Native broker 1C, rule 2 (ruling A' by gentle-dove-36). Stacks on #13260: its commits appear in this diff until it lands. Held behind #13164, since it is an emitter/infer-mirror PR.

Root cause (§6b)

A generic function was emitted without its type parameters because v1.compiler.infer build_type_env param_bindings inserted every generic type declaration's parameters into the module environment:

• type Box<Q> made a bare Q resolve anywhere in that module, and in its importers.
• fn f(x: Int) -> Q was then accepted with no <Q>, and even returned an Int as a Q.
• is_type_variable_name, a hard-coded list of T, K, V, MappedElement, FoldAccumulator, was the patch that stripped those names from import surfaces again.

Two controls ran before any change:

• An undeclared T with no generic type in the module was already refused.
• A non-listed Q was accepted after type Box<Q>.

So the defect was the scope leak, not the list.

Change

• A declaration's type parameters bind only while that declaration is resolved. v1.compiler.infer_resolve declaration_type_param_names serves both item resolution and topo_resolve_types, which now uses declaration_body_env. The body keeps the nominal-leaf shape it always resolved against; only the scope changed. v1.compiler.infer_env env_with_type_parameter_bindings is the one scoped insert, and the type-variable shape calls it too.
• Deleted with no residue: param_bindings, is_type_variable_name, its std.types import filter (type_env_for_import collapses away), the import-all export filter, and the record-field conv arm.
• Census. The CI floor on this draft refused exactly at the first affected module. The whole-corpus textual census (all fn signatures in dag, src/v2, src/v1 and examples, every listed name) finds the same population. Every site gets an explicit <T>, and each T is the fresh parameter of the reading type it consumes:
  • extdeps.languages.json.parse json_field_value, json_field_cause
  • extdeps.docker.container_inspect nested_value, nested_causes
  • gunbc.machine_intake.mtjade1_access_observation read_cause
  • gunbc.machine_intake.mtcollins1_boot_diagnostic_bundle members_channel

Evidence

• Regen is a fixed point. With emit_rust: a type parameter carries its own cardinality (K? emits Option<K>) #13260 underneath, the only generated changes are this PR's own three infer mirrors. emit_rust: a type parameter carries its own cardinality (K? emits Option<K>) #13260 was split out because, without it, std.algebra PartialFunction lost Option<V>: a pre-existing defect that this leak had masked.
• test.claim.type_parameter_declaration_scope_witness runs on tools.multi_module_compile_fixture (the real acceptance path):
  • same-module RED: a sibling's Q refuses UnresolvedType;
  • cross-import RED: an imported type's Q refuses in the importer;
  • positive control: a declared <Q> compiles clean.
  • With the new seed all three hold. With main's seed both REDs fail and the control holds.

🤖 Generated with Claude Code

[briansrls]

NO-LAND at this exact head. The declaration-local type-parameter model and the two leak REDs look right, but the whole-tree consequence is not closed: the exact-head floor failed in extdeps.dns.domain_name::parse_dns_label_list. At labels |> list_push(label), the receiver is now inferred as Product(ServeWireResponse) rather than List<DnsLabel>, so list_push is unresolved; the existing frontier row simultaneously reports that its former Primitive(ok) occurrence disappeared. This must not be repaired by merely changing the frontier identity/count—the new receiver is semantically wrong. Restore/establish the binder's List<DnsLabel> type (or land the upstream identity fix that actually does so), then lower/delete the old frontier row from measured ground and rerun the exact-head floor. Run 31519's required CI receipt records both blocking diagnostics.

[gunbai-bot]

Held behind derived-node-identity step 2 (docs/plans/derived-node-identity-design.md; class gunbc.recurring_failure_mode generic_identity_decided_by_spelling), per gentle-dove-36. The note's owner session (clever-lynx-801) no longer exists, so step-2 evidence and its RED are recorded here, where step 2 has to find this PR.

What the floor found on head 2d5645a. extdeps.dns.domain_name parse_dns_label_list folds over an accumulator of std.error_primitives type Result<ok, err> = Ok { value: ok } | Err { value: err }. In the arm Ok { value: labels }, the binder labels is typed from the variant field value: ok, and the consumer resolves that parameter leaf by name in its own scope.

• On main: the lookup hits the leaked module and import binding of ok, which is Primitive(ok), an honest unknown admitted by a declared frontier row.
• With this PR's scoping: the same lookup falls through to the global bare name and binds an unrelated fn ok(..) -> ServeWireResponse (gunbc.fabric.fabric_storage_serve). That is a silent wrong type, which the floor reports as list_push cannot be resolved: receiver type Product(ServeWireResponse).

So scoping exposes the name-keyed instantiation; it does not cause it. This PR lands only after step 2 substitutes by binder identity. That is the RED step 2 needs. Caveat: a standalone two-module reduction (generic Res<ok, err> plus an unrelated fn ok in another module) did not reproduce, so the RED needs the real dns shape or a closer reduction.

— sent from snappy-wolf-524

[gunbai-bot]

Step-2 evidence from native broker lane 2L (gentle-gull-189), posted here beside 1C's at gentle-dove-36's request. Lane 2L is held and closed: instantiating a generic record literal from its field payloads is the move docs/plans/derived-node-identity-design.md §6 ("Residue admitted to step 2") leaves to step 2. Nothing was committed or pushed.

Everything under "Measured" was observed by emitting Rust with a seed built from main (gunbc compile --entry <fixture> --target rust), with no change of mine applied. The patch at the bottom was never executed: its remote run was restarted twice by log-stream errors and had not reached the "after" arm when the lane closed.

The std.list shape

std.list duplicated_by_key<T> folds from init: DuplicatedScan { firsts: empty_map(), reported: empty_map(), kept_reversed: [] }, where type DuplicatedScan<T> { firsts: Map<String, T>, .. kept_reversed: List<T> }.

• The init has no payload that binds T: empty_map() and [] carry nothing. v1.compiler.infer infer_record_lit_structural types the literal as the unapplied declaration (raw_resolved), and the sibling empty_map() is inferred against Map<String, TypeVariable T>.
• Measured emission: firsts: v1_rt::rc_empty_map::<String, compile_error!("UNRESOLVED_CompilerError")>(). (Native broker 2C/C3: an erased empty-map type argument defers to the target's inference (std_list, −3 broker errors) #13238 defers that turbofish to rustc; that deferral stays.)

Why name-keyed unify_generics is right there only by coincidence of spelling

Inside the step, the accumulator is the unapplied declaration, so every read of it returns the declaration's own formal as a bare name. Measured with a record whose param is renamed (type Scan<E> { firsts: Map<String, E>, kept: List<E> }, used inside fn f<T>(xs: List<T>, key: fn(T) -> String)), reading each expression's type off a closure annotation:

expression in the step	type printed
acc.kept	List<E> (rendered _)
map_insert(acc.firsts, key(x), x)	Rc<HashMap<String, E>> — the receiver's formal, not x's T
concat([x], acc.kept)	Rc<Vec<T>> — first argument wins
concat(acc.kept, [x])	List<E> (rendered _)

In the real duplicated_by_key, every list payload in the step's literals is read back out of acc (acc.kept_reversed, concat([first], acc.kept_reversed) with first from map_get(acc.firsts, ..)). The only genuine evidence for the function's T is the value argument x of map_insert, and that call is typed from its receiver. So a payload-to-formal unify_generics over those fields binds T := T, where the right-hand T is the record's leaked formal. It reads as the function's T only because both are spelled T; today's emitter already leans on the same coincidence (|acc: Rc<DuplicatedScan<T>>, ..|). Rename the record's param and nothing binds.

The same leak with no enclosing generic at all: Same<T> folded over List<Int> prints e: Rc<HashMap<String, T>> in a function that declares no T.

Three more specimens (all on main)

1. Formal leaks out of a payload-determined literal. let s = Scan { firsts: empty_map(), kept: [1] } then fold(s.kept, init: 0, f: (acc, n) => acc + n) emits |acc: i64, n: E| in fn() -> i64, and the sibling empty_map() is erased, although kept: [1] determines E.
2. Valid code refused. Pair { left: Scan { firsts: empty_map(), kept: ["x"] }, right: [Scan { firsts: empty_map(), kept: [2] }] } (type Pair<A, B> { left: A, right: List<B> }), then fold(outer.right, .., f: (acc, inner) => acc + count(inner.kept)): blocking no field 'kept' on type 'B'.
3. Arithmetic falls off the typed path. Pair { left: 1, .. } then q.left + n emits a raw (q.left.clone() + ..) instead of v1_rt::int_add, because q.left is typed A.

What a name-keyed rule cannot decide (for the step-2 design)

• An owner formal leaked back out of an uninstantiated value vs. the enclosing declaration's parameter of the same spelling. The only discriminator available today is the declared roster by name (scope.enclosing_declared_type_param_names).
• The kernel container slot name: every List<M> has a child spelled T, so a "does this type mention the owner's param" walk must read slots through child_type_node, never by the child's own name.
• unify_generics descends only single-child applications, so a formal Map<String, E> never binds E.
• An application minted for a struct literal reaches the emitter's Rc-carrier decision (v1.compiler.emit_rust emit_rust_expr_record_lit, rc_name). Inference: a variant literal of a generic coproduct takes the expected application (native broker dns E0599) #13243 measured a qualified-name struct literal losing its Rc::new( there (v2.std.artifact generated_artifact_validation, E0308); neither lane traced the arm.
• The fold init is inferred before the step; once the step names an application the init must be inferred again under it, or its fields stay uninstantiated while the fold's type is instantiated.

2D (#13243) and I agree a generic literal is one fact — an application of its owner, args from the expected type else from payloads — and should have one instantiation authority; #13243's coproduct-only restriction exists only because of that carrier decision.

Unexecuted 2L patch to src/v1/04_infer.dag (typechecks under an older seed; never run)

diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag
index 0482917b3e..2492c5852d 100644
--- a/src/v1/04_infer.dag
+++ b/src/v1/04_infer.dag
@@ -361,6 +361,8 @@ type FieldInferResult {
   typed_field: Node
   infer_result: InferResult
   diagnostics: List<ErrorNode>
+  authored: Node
+  position_diagnostics: List<ErrorNode>
 }
 
 type BuildTypeEnvResult {
@@ -7409,7 +7411,7 @@ fn derive_element_provenance(coll_expr: Node, elem_type: Node, scope: InferScope
 // type is unknown expects nothing, as before.
 fn infer_method_args_with_fold(method_name: String?, method_args: List<Node>, fold_info: ArgInferResult?, fold_acc_type: Node, element_type: Node, elem_provenance: SubValueRelation, arg_contract: DeclaredArgContract, scope: InferScope) -> List<ArgInferResult> {
   let is_fold = method_name_is(opt: method_name, expected: "fold")
-  method_args |> enumerate |> map(idx_pair =>
+  let step_blind_results = method_args |> enumerate |> map(idx_pair =>
     let a = idx_pair.second
     let idx = idx_pair.first
     let is_init_arg = arg_has_name(arg: a, name: "init", source_indices: scope.type_env.source_indices) || (arg_name_at(n: a, source_indices: scope.type_env.source_indices) == none && idx == 0)
@@ -7490,6 +7492,52 @@ fn infer_method_args_with_fold(method_name: String?, method_args: List<Node>, fo
       }
     }
   )
+  if is_fold && fold_info != none {
+    fold_record_init_under_step_application(results: step_blind_results, method_args: method_args, fold_acc_type: fold_acc_type, scope: scope)
+  } else { step_blind_results }
+}
+
+// A RECORD-LITERAL INIT OF A GENERIC DECLARATION IS INFERRED AGAIN ONCE THE STEP NAMES THE
+// APPLICATION. The init is inferred before the step, so `init: Scan { firsts: empty_map(), kept: [] }`
+// has no payload that binds E and types as the declaration; the step's return is where E is
+// established (record_lit_payload_application, over a body that conses an element). The fold call
+// already refines its ACCUMULATOR from that return (fold_accumulator_is_unapplied_generic) and
+// never went back to the init, so the fold's type was instantiated while the init's own fields
+// were not: its `empty_map()` reached the emitter with an erased value type (std.list
+// duplicated_by_key). The second inference is the ordinary expected-type route --
+// record_lit_instantiated_fields under the step's application -- admitted only when that
+// application's head resolves to the SAME declaration the init typed as (rc identity), so a step
+// that returns some other type leaves the init as it was. One extra inference of the init, of a
+// literal whose first inference bound nothing.
+fn fold_record_init_under_step_application(results: List<ArgInferResult>, method_args: List<Node>, fold_acc_type: Node, scope: InferScope) -> List<ArgInferResult> {
+  if fold_acc_type.connective != Conj || !fold_accumulator_is_unapplied_generic(n: fold_acc_type) { results } else {
+    match results |> filter(r => is_lambda_expr(e: arg_value(n: r.typed_arg))) |> first {
+      Absent => results
+      Present { value: step } =>
+        let step_return = resolved_type(n: arg_value(n: step.typed_arg))
+        let step_names_the_declaration = step_return.connective == NoConnective
+          && (step_return.children |> count) > 0
+          && (step_return.children |> count) == (fold_acc_type.params |> count)
+          && match lookup_type_for(env: scope.type_env, node: step_return) {
+            Present { value: head } => rc_ptr_eq(head, fold_acc_type)
+            Absent => false
+          }
+        let si = scope.type_env.source_indices
+        let authored_init = match method_args |> filter(a => arg_has_name(arg: a, name: "init", source_indices: si)) |> first {
+          Present { value: a } => Present { value: a }
+          Absent => method_args |> first
+        }
+        match authored_init {
+          Absent => results
+          Present { value: ia } =>
+            if !step_names_the_declaration || record_lit_expr_optional(expr: arg_value(n: ia)) == none { results } else {
+              let again = infer_expr(texpr: arg_value(n: ia), scope: scope, expected: Present { value: step_return })
+              let init_under_application = ArgInferResult { typed_arg: make_arg_node(occurrence_identity: ia.occurrence_identity, name: arg_name_at(n: ia, source_indices: si), value: again.typed, span: ia.span, name_span: ia.span), diagnostics: again.diagnostics }
+              results |> map(r => if r.typed_arg.span == ia.span { init_under_application } else { r })
+            }
+        }
+    }
+  }
 }
 
 fn is_lambda_expr(e: Node) -> Bool {
@@ -10335,7 +10383,9 @@ fn infer_map_literal(occurrence_identity: NodeOccurrenceIdentity, map_node: Node
         name_span: node_name_span(n: fi)
       ),
       infer_result: ar,
-      diagnostics: ar.diagnostics
+      diagnostics: ar.diagnostics,
+      authored: fi,
+      position_diagnostics: []
     }
   )
   InferResult {
@@ -10519,6 +10569,187 @@ fn present_value_expected_from_optional(type_name: String, field_name: String, v
 // declares no fields, so `SingleAuthority { reason: "..." }` supplies one that does not exist. The
 // ambiguity guard is shared with MissingField for the same reason it exists there -- an ambiguous
 // name has not been resolved to a type, so neither half may judge its fields.
+// A GENERIC RECORD LITERAL IS AN APPLICATION OF ITS DECLARATION WHEN ITS OWN PAYLOADS SAY WHICH.
+// `Scan { firsts: empty_map(), kept: [1] }` of `type Scan<E> { firsts: Map<String, E>, kept: List<E> }`
+// typed as the DECLARATION -- the expansion still carrying `E` as a param -- so every reader of the
+// value saw the formal: `s.kept` was List<E>, a lambda over it annotated `n: E` into a function with
+// no E, and the sibling `empty_map()` was inferred against Map<String, TypeVariable E> and reached
+// the emitter with its value type erased (std.list duplicated_by_key, native broker lane 2C/2L).
+// The literal is the earliest link holding the instantiating fact: its field payloads. The call path
+// already reads them -- unify_record_lit_generics walks a literal ARGUMENT's fields to bind the
+// CALLEE's generics, a consumer compensating for a literal that did not carry its own application.
+// This is the same payload-to-formal unification (unify_generics over each declared field type and
+// its payload type), asked once at the literal for the OWNER's params.
+//
+// IT ANSWERS ONLY WHEN EVERY OWNER PARAM IS BOUND BY ADMISSIBLE, AGREEING EVIDENCE; otherwise the
+// literal keeps the declaration exactly as before. A payload type is not evidence when it is
+// unresolved, carries an error, is optional, or mentions one of the owner's own formals that the
+// enclosing declaration does not declare -- that last is the formal LEAKED back out of an
+// uninstantiated value (`acc.kept` of an accumulator typed as the declaration is List<E>), and
+// binding E to it instantiates nothing. Two payloads that bind one param to incompatible types
+// decline rather than letting the first win: a literal typed Pair<Int> over a String payload would
+// be this stage asserting a type its own evidence contradicts.
+//
+// THE ADMISSION IS NAME-KEYED, AND THAT IS THE ROSTERED FORK, NOT A NEW ONE. unify_generics binds a
+// formal by its label, and an owner param spelled like an enclosing declared type parameter
+// (`type Scan<T>` built inside `fn f<T>`) cannot be told from it here, so a leaked formal spelled T
+// is admitted as the function's T. gunbc.recurring_failure_mode generic_identity_decided_by_spelling
+// owns that class and its trigger (declaration identity carried through infer's node-copying
+// constructors); this arm reads the declared roster the way name_is_enclosing_declared_type_parameter
+// does and adds no identity scheme of its own.
+//
+// AN EXPECTED APPLICATION STILL OUTRANKS THE PAYLOADS: record_lit_instantiated_fields instantiates
+// the fields from it and this arm is not asked. The literal's own type on that route stays the
+// declaration (v1.compiler.infer variant_literal_expected_application takes the coproduct half), so
+// one instantiation authority for both halves is still owed.
+type PayloadOwnerBindings {
+  bound: Map<String, Node>
+  conflicted: Bool
+}
+
+fn record_field_declared_type(sf: Node) -> Node {
+  match sf.inferred {
+    Present { value: Resolved { node: rt } } => rt
+    _ => field_node_type_expr(n: sf)
+  }
+}
+
+fn payload_type_carries_error(n: Node, fuel: Int) -> Bool {
+  if fuel <= 0 { false } else {
+    let own = match n.inferred {
+      Present { value: inf } => is_compiler_error(inferred: inf)
+      Absent => false
+    }
+    own || (n.children |> any(ch => payload_type_carries_error(n: child_type_node(ch: ch), fuel: fuel - 1)))
+  }
+}
+
+// A kernel container names its argument SLOT after its own template parameter -- every List<M>
+// carries a child spelled T and resolved to M (make_container_type) -- so a walk that reads a child's
+// own name finds an owner param spelled T inside every list. The slot is read through to what it
+// resolves to (child_type_node); only a bare leaf or a type variable that IS the name counts.
+fn payload_type_mentions_formal(n: Node, names: List<String>, source_indices: Map<String, NewlineIndex>, fuel: Int) -> Bool {
+  if fuel <= 0 || (names |> count) == 0 { false } else {
+    let is_variable = match n.inferred {
+      Present { value: TypeVariable { id: id } } => names |> any(g => g == id)
+      _ => false
+    }
+    let t = match n.inferred {
+      Present { value: Resolved { node: _ } } => child_type_node(ch: n)
+      _ => n
+    }
+    let is_bare_leaf = (t.children |> count) == 0 && t.connective == NoConnective
+      && (names |> any(g => g == authored_name_at(source_indices: source_indices, node: t)))
+    is_variable || is_bare_leaf
+      || (t.children |> any(ch => payload_type_mentions_formal(n: ch, names: names, source_indices: source_indices, fuel: fuel - 1)))
+  }
+}
+
+fn payload_type_is_instantiating_evidence(candidate: Node, leaked_formal_names: List<String>, source_indices: Map<String, NewlineIndex>) -> Bool {
+  candidate.return_cardinality != CardOptional
+    && !payload_type_carries_error(n: candidate, fuel: 16)
+    && is_fully_resolved(n: candidate, source_indices: source_indices)
+    && !payload_type_mentions_formal(n: candidate, names: leaked_formal_names, source_indices: source_indices, fuel: 16)
+}
+
+fn record_lit_payload_owner_bindings(owner_param_names: List<String>, struct_fields: List<Node>, typed_fields: List<Node>, scope: InferScope) -> Map<String, Node>? {
+  let si = scope.type_env.source_indices
+  let leaked_formal_names = owner_param_names |> filter(g => !name_is_enclosing_declared_type_parameter(name: g, scope: scope))
+  let walked = fold(struct_fields, init: PayloadOwnerBindings { bound: empty_map(), conflicted: false }, f: (st, sf) =>
+    let field_name = authored_name_at(source_indices: si, node: sf)
+    match typed_fields |> filter(fi => field_init_node_name_at(n: fi, source_indices: si) == field_name) |> first {
+      Absent => st
+      Present { value: fi } =>
+        let field_formal = record_field_declared_type(sf: sf)
+        if sf.return_cardinality == CardOptional || field_formal.return_cardinality == CardOptional { st } else {
+          let field_evidence = unify_generics(formal: field_formal, actual: resolved_type(n: field_init_node_value(n: fi)), generic_names: owner_param_names, source_indices: si, acc: empty_map())
+          fold(owner_param_names, init: st, f: (inner, g) =>
+            match map_get(field_evidence, g) {
+              Absent => inner
+              Present { value: raw } =>
+                let candidate = child_type_node(ch: raw)
+                if !payload_type_is_instantiating_evidence(candidate: candidate, leaked_formal_names: leaked_formal_names, source_indices: si) { inner } else {
+                  match map_get(inner.bound, g) {
+                    Absent => PayloadOwnerBindings { bound: map_insert(inner.bound, g, candidate), conflicted: inner.conflicted }
+                    Present { value: earlier } =>
+                      if node_type_compatible(left: earlier, right: candidate, source_indices: si, text: TextJudgedIn { env: scope.type_env }) { inner }
+                      else { PayloadOwnerBindings { bound: inner.bound, conflicted: true } }
+                  }
+                }
+            }
+          )
+        }
+    }
+  )
+  if walked.conflicted || (owner_param_names |> any(g => map_get(walked.bound, g) == none)) { none } else { Present { value: walked.bound } }
+}
+
+fn record_lit_payload_application(type_name: String, name_span: SourceSpan, owner_param_names: List<String>, struct_fields: List<Node>, typed_fields: List<Node>, scope: InferScope) -> Node? {
+  match lookup_type_by_name(env: scope.type_env, name: type_name) {
+    Absent => none
+    Present { value: owner } =>
+      if owner.connective != Conj || (owner.params |> count) != (owner_param_names |> count) { none } else {
+        match record_lit_payload_owner_bindings(owner_param_names: owner_param_names, struct_fields: struct_fields, typed_fields: typed_fields, scope: scope) {
+          Absent => none
+          Present { value: bindings } =>
+            let application = Node {
+              occurrence_identity: OccurrenceSynthetic, name: type_name, span: name_span, ident_span: Present { value: name_span },
+              children: owner_param_names |> map(g => match map_get(bindings, g) {
+                Present { value: bound } => bound
+                Absent => error_type
+              }),
+              connective: NoConnective, params: [], inferred: none, return_cardinality: Required, uses: [],
+              body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false,
+              has_non_tail_self_call: false, match_pattern: none, module_item_kind: NotAModuleItem, declaration_marker: Unmarked, declaration: none, expr_data: NoExprData
+            }
+            match lookup_type_for(env: scope.type_env, node: application) {
+              Present { value: head } =>
+                if rc_ptr_eq(head, owner) && record_lit_instantiated_fields(type_name: Present { value: type_name }, expected: Present { value: application }, scope: scope) != none {
+                  Present { value: application }
+                } else { none }
+              Absent => none
+            }
+        }
+      }
+  }
+}
+
+// THE SIBLINGS THE PAYLOADS COULD NOT TYPE ARE INFERRED AGAIN UNDER THE APPLICATION, and only those:
+// a field whose declared type mentions an owner param and whose payload came back unresolved under
+// the declaration's formals (`empty_map()` against Map<String, E>, `[]` against List<E>). The
+// instantiated field types are the ones record_lit_instantiated_fields answers for an EXPECTED
+// application, so both routes instantiate a field through one function. A field that was already
+// evidence is not inferred twice.
+fn record_lit_fields_settled_under_application(type_name: String?, application: Node, owner_param_names: List<String>, struct_fields: List<Node>, first_pass: List<FieldInferResult>, scope: InferScope) -> List<FieldInferResult> {
+  let si = scope.type_env.source_indices
+  match record_lit_instantiated_fields(type_name: type_name, expected: Present { value: application }, scope: scope) {
+    Absent => first_pass
+    Present { value: instantiated_fields } =>
+      first_pass |> map(fir =>
+        let fi_name = field_init_node_name_at(n: fir.typed_field, source_indices: si)
+        let payload_type = resolved_type(n: field_init_node_value(n: fir.typed_field))
+        let payload_is_settled = is_fully_resolved(n: payload_type, source_indices: si) && !payload_type_carries_error(n: payload_type, fuel: 16)
+        let declared_mentions_owner_param = struct_fields
+          |> filter(sf => authored_name_at(source_indices: si, node: sf) == fi_name)
+          |> any(sf => type_node_mentions_any_name(n: record_field_declared_type(sf: sf), names: owner_param_names, source_indices: si, fuel: 16))
+        if payload_is_settled || !declared_mentions_owner_param { fir } else {
+          match instantiated_fields |> filter(sf => authored_name_at(source_indices: si, node: sf) == fi_name) |> first {
+            Absent => fir
+            Present { value: instantiated } =>
+              let again = infer_expr(texpr: field_init_node_value(n: fir.authored), scope: scope, expected: Present { value: preserve_outer_optional_cardinality(outer: instantiated, inner: resolved_type(n: instantiated)) })
+              FieldInferResult {
+                typed_field: make_field_init_node(occurrence_identity: fir.authored.occurrence_identity, name: fi_name, value: again.typed, span: fir.authored.span, name_span: node_name_span(n: fir.authored)),
+                infer_result: again,
+                diagnostics: concat(again.diagnostics, fir.position_diagnostics),
+                authored: fir.authored,
+                position_diagnostics: fir.position_diagnostics
+              }
+          }
+        }
+      )
+  }
+}
+
 fn infer_record_lit_structural(occurrence_identity: NodeOccurrenceIdentity, type_name: String?, field_inits: List<Node>, span: SourceSpan, name_span: SourceSpan, scope: InferScope, expected: Node?) -> InferResult {
   let instantiated_struct_fields = record_lit_instantiated_fields(type_name: type_name, expected: expected, scope: scope)
   let expected_struct_fields = if instantiated_struct_fields == none {
@@ -10657,7 +10888,7 @@ fn infer_record_lit_structural(occurrence_identity: NodeOccurrenceIdentity, type
   let unbound_owner_param_variables = fold(uninstantiated_owner_param_names, init: empty_map(), f: (acc, g) =>
     map_insert(acc, g, type_variable_node(id: g))
   )
-  let fi_infer_results = map(field_inits, fi =>
+  let declared_formal_fi_results = map(field_inits, fi =>
     let fi_name = field_init_node_name_at(n: fi, source_indices: scope.type_env.source_indices)
 
     let unknown_field_diags = match construction_field_names {
@@ -10796,18 +11027,43 @@ fn infer_record_lit_structural(occurrence_identity: NodeOccurrenceIdentity, type
         }
       Absent => []
     }
+    let position_diags = concat(concat(field_type_diags, unknown_field_diags), bare_none_field_construction_diags(
+      fi: fi,
+      fi_name: fi_name,
+      field_declared_type: field_declared_type,
+      type_name_for_message: tn_str,
+      scope: scope
+    ))
     FieldInferResult {
       typed_field: make_field_init_node(occurrence_identity: fi.occurrence_identity, name: fi_name, value: ar_typed, span: fi.span, name_span: node_name_span(n: fi)),
       infer_result: ar,
-      diagnostics: concat(concat(concat(ar_diags, field_type_diags), unknown_field_diags), bare_none_field_construction_diags(
-        fi: fi,
-        fi_name: fi_name,
-        field_declared_type: field_declared_type,
-        type_name_for_message: tn_str,
-        scope: scope
-      ))
+      diagnostics: concat(ar_diags, position_diags),
+      authored: fi,
+      position_diagnostics: position_diags
     }
   )
+  let payload_application = if tn_str == "" || presence_variant_owner != none || expected_variant_node != none || (uninstantiated_owner_param_names |> count) == 0 { none } else {
+    record_lit_payload_application(
+      type_name: tn_str,
+      name_span: name_span,
+      owner_param_names: uninstantiated_owner_param_names,
+      struct_fields: struct_fields,
+      typed_fields: declared_formal_fi_results |> map(fir => fir.typed_field),
+      scope: scope
+    )
+  }
+  let fi_infer_results = match payload_application {
+    Absent => declared_formal_fi_results
+    Present { value: application } =>
+      record_lit_fields_settled_under_application(
+        type_name: type_name,
+        application: application,
+        owner_param_names: uninstantiated_owner_param_names,
+        struct_fields: struct_fields,
+        first_pass: declared_formal_fi_results,
+        scope: scope
+      )
+  }
   let typed_fields = fi_infer_results |> map(fir => fir.typed_field)
   let fi_own_diags = flat_map(fi_infer_results, fir => fir.diagnostics)
   let record_effectful_fields = flat_map(typed_fields, tf =>
@@ -10938,7 +11194,9 @@ fn infer_record_lit_structural(occurrence_identity: NodeOccurrenceIdentity, type
     }
     let expected_optional_parent = Present { value: "Optional" }
     let is_present_ctor = type_name.value == "Present" && local_variant_parent == expected_optional_parent
-    let resolved_node = if is_present_ctor {
+    let resolved_node = if payload_application != none {
+      payload_application.value
+    } else if is_present_ctor {
       let val_field = fi_infer_results |> filter(fir => field_init_node_name_at(n: fir.typed_field, source_indices: scope.type_env.source_indices) == "value") |> first
       match val_field {
         Present { value: val_fir } => with_optional_cardinality(n: resolved_type(n: val_fir.infer_result.typed))

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-09T18:29:15.145189Z	2d5645a	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[gunbai-bot]

Closed without folding in the v1 closeout bankruptcy (#13641). REQUEST_CHANGES (review 78367): it would bind Result's ok to an unrelated fn ok (fabricated type). Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604