diff --git a/dag/std/decl_ref.dag b/dag/std/decl_ref.dag index ed01d19d040..43ccb965e80 100644 --- a/dag/std/decl_ref.dag +++ b/dag/std/decl_ref.dag @@ -18,6 +18,17 @@ type DeclarationRef { field: DeclField } +// WHETHER A REFERENCE NAMES A TYPE PARAMETER, read from the carrier and never from a spelling. It +// lives beside the type for the reason the constructors do: one authority for what the field arm +// means (DESIGN section 3). +fn declaration_ref_is_type_parameter(ref: DeclarationRef) -> Bool { + match ref.field { + TypeParameter { name: _ } => true + WholeDeclaration => false + NamedField { field_name: _ } => false + } +} + // The constructors live HERE, beside the type they construct — single authority (DESIGN section 3). // Two parallel lanes each minted an identical fn decl_ref/decl_field_ref pair // (std.primitive_identity and std.roster_frontier, both 2026-08-01), and because v1-seed fn names diff --git a/fixtures/generic_identity_census/a.dag b/fixtures/generic_identity_census/a.dag index 30976852997..5f57acc0a5a 100644 --- a/fixtures/generic_identity_census/a.dag +++ b/fixtures/generic_identity_census/a.dag @@ -46,3 +46,7 @@ fn boxed() -> Box { fn unbox(b: Box) -> Q { b.item } + +fn same_spelling_as_a_record_parameter(b: Box, q: Q) -> Q { + q +} diff --git a/src/v1/04_resolve.dag b/src/v1/04_resolve.dag index 7d9352925f0..20f347397da 100644 --- a/src/v1/04_resolve.dag +++ b/src/v1/04_resolve.dag @@ -1,6 +1,6 @@ module v1.compiler.infer_resolve -import std.decl_ref { DeclarationRef, decl_ref, decl_type_parameter_ref } +import std.decl_ref { DeclarationRef, decl_ref, decl_type_parameter_ref, declaration_ref_is_type_parameter } import std.occurrence_identity { OccurrenceSynthetic } import std.types { SourceSpan, container_param_name } @@ -295,7 +295,27 @@ fn preserve_nominal_brand_on_resolve( } else { preserve_outer_optional_cardinality(outer: identity, inner: structural) } } +// A TYPE-PARAMETER REFERENCE IS NOT A NOMINAL ALIAS, AND IT IS KNOWN BY ITS MARK, NOT ITS SPELLING +// (docs/plans/derived-node-identity-design.md, copy law L1; class gunbc.recurring_failure_mode +// generic_identity_decided_by_spelling). binder_marked_type records (owner, TypeParameter) on every +// reference to an item's own parameter. This function then looked the node up BY NAME and returned +// whatever the environment bound to that spelling, so a parameter spelled like some other binding in +// scope was replaced by that binding and its own identity was dropped: measured by +// //gunbc/instruments:generic-identity-census as formal_declaration_bound_conformance leaves carrying +// neither mark, where the signature they were read from carried both. There is nothing to peel +// beneath a parameter, so a node carrying the mark is returned as it was given. +fn node_is_type_parameter_reference(n: Node) -> Bool { + match n.declaration { + Present { value: ref } => declaration_ref_is_type_parameter(ref: ref) + Absent => false + } +} + fn peel_nominal_alias_identity(n: Node, env: TypeEnv, module_name: String) -> Node { + if node_is_type_parameter_reference(n: n) { n } else { peel_nominal_alias_identity_by_name(n: n, env: env, module_name: module_name) } +} + +fn peel_nominal_alias_identity_by_name(n: Node, env: TypeEnv, module_name: String) -> Node { let source_indices = env.source_indices let brand = authored_name_at(source_indices: source_indices, node: n) match lookup_type_for(env: env, node: n) { diff --git a/src/v1/stage0/src/std_decl_ref.rs b/src/v1/stage0/src/std_decl_ref.rs index 0c1312aced1..87c559a3131 100644 --- a/src/v1/stage0/src/std_decl_ref.rs +++ b/src/v1/stage0/src/std_decl_ref.rs @@ -26,6 +26,14 @@ pub struct DeclarationRef { pub field: Rc, } +pub fn declaration_ref_is_type_parameter(ref_: Rc) -> bool { + match (*ref_.field.clone()).clone() { + DeclField::TypeParameter { name: _, .. } => true, + DeclField::WholeDeclaration => false, + DeclField::NamedField { field_name: _, .. } => false, + } +} + #[derive( Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, )] diff --git a/src/v1/stage0/src/v1_compiler_infer_resolve.rs b/src/v1/stage0/src/v1_compiler_infer_resolve.rs index 8de8ce0e93f..aac5671d9cb 100644 --- a/src/v1/stage0/src/v1_compiler_infer_resolve.rs +++ b/src/v1/stage0/src/v1_compiler_infer_resolve.rs @@ -4,7 +4,9 @@ use self::AliasKind::*; use self::KindInhabitance::*; pub use crate::std_decl_ref::DeclarationRef; -pub use crate::std_decl_ref::{decl_ref, decl_type_parameter_ref}; +pub use crate::std_decl_ref::{ + decl_ref, decl_type_parameter_ref, declaration_ref_is_type_parameter, +}; pub use crate::std_induction::SubValueRelation; use crate::std_induction::SubValueRelation::SubValueUnknown; pub use crate::std_occurrence_identity::NodeOccurrenceIdentity; @@ -413,7 +415,26 @@ pub fn preserve_nominal_brand_on_resolve( } } +pub fn node_is_type_parameter_reference(n: Rc) -> bool { + match n.declaration.clone() { + Some(ref_) => crate::std_decl_ref::declaration_ref_is_type_parameter(ref_.clone()), + std::option::Option::None => false, + } +} + pub fn peel_nominal_alias_identity(n: Rc, env: Rc, module_name: String) -> Rc { + if node_is_type_parameter_reference(n.clone()) { + n.clone() + } else { + peel_nominal_alias_identity_by_name(n.clone(), env.clone(), module_name.clone()) + } +} + +pub fn peel_nominal_alias_identity_by_name( + n: Rc, + env: Rc, + module_name: String, +) -> Rc { { let source_indices = env.source_indices.clone(); let brand = crate::v1_std_core::authored_name_at(source_indices.clone(), n.clone()); diff --git a/src/v1/stage0/src/v1_tests_claim_generic_identity_census.rs b/src/v1/stage0/src/v1_tests_claim_generic_identity_census.rs index fea7bd46cd7..ccdf9df1572 100644 --- a/src/v1/stage0/src/v1_tests_claim_generic_identity_census.rs +++ b/src/v1/stage0/src/v1_tests_claim_generic_identity_census.rs @@ -9,7 +9,9 @@ pub use crate::std_decl_ref::{DeclField, DeclarationRef}; pub use crate::std_types::{Bool, List, Map}; pub use crate::v1_compiler_compile::compile_to_resolved; pub use crate::v1_compiler_compile::{ResolvedPipelineResult, SourceFile}; -pub use crate::v1_compiler_infer::{param_is_generic_decl, type_node_label}; +pub use crate::v1_compiler_infer::{ + param_is_generic_decl, substitute_generics_apply, type_node_label, unify_generics, +}; pub use crate::v1_compiler_infer_env::node_with_children; pub use crate::v1_compiler_infer_items::{ResolvedGraph, TypedModule}; use crate::v1_compiler_infer_sigs::ResolvedFormals::{ @@ -905,6 +907,223 @@ pub fn gi_rows_from_sources( } } +pub fn gi_formal_named(sig: Rc, parameter: String) -> Option> { + match (*sig.resolved_formals.clone()).clone() { + ResolvedFormals::DeclarationBoundFormals { formals: fs, .. } => Rc::new({ + let mut __result = Vec::new(); + for f in fs.iter().cloned() { + if (f.parameter_identity.clone() == parameter.clone()) { + __result.push(f); + } + } + __result + }) + .first() + .cloned(), + ResolvedFormals::KernelGroundedFormals { formals: fs, .. } => Rc::new({ + let mut __result = Vec::new(); + for f in fs.iter().cloned() { + if (f.parameter_identity.clone() == parameter.clone()) { + __result.push(f); + } + } + __result + }) + .first() + .cloned(), + ResolvedFormals::LocalFormalsAwaitingModuleContext => std::option::Option::None, + } +} + +pub fn gi_first_child(n: Rc) -> Option> { + n.children.clone().first().cloned() +} + +pub fn gi_reading_line(name: String, value: String) -> String { + v1_rt::concat( + v1_rt::concat( + v1_rt::concat("reading ".to_string(), name.clone()), + ": ".to_string(), + ), + value.clone(), + ) +} + +pub fn gi_supplied_node_readings( + sigs: Rc>>, + si: Rc>>, +) -> Rc> { + match v1_rt::map_get(&sigs, "gic.a::head_of".to_string()) { + std::option::Option::None => Rc::new(vec![ + "reading supplied_nodes: UNREACHED (no signature gic.a::head_of)".to_string(), + ]), + Some(head_of) => match v1_rt::map_get(&sigs, "gic.a::ints".to_string()) { + std::option::Option::None => Rc::new(vec![ + "reading supplied_nodes: UNREACHED (no signature gic.a::ints)".to_string(), + ]), + Some(ints) => match v1_rt::map_get(&sigs, "gic.a::rename_of".to_string()) { + std::option::Option::None => Rc::new(vec![ + "reading supplied_nodes: UNREACHED (no signature gic.a::rename_of)".to_string(), + ]), + Some(rename_of) => match gi_formal_named(head_of.clone(), "xs".to_string()) { + std::option::Option::None => Rc::new(vec![ + "reading supplied_nodes: UNREACHED (head_of has no bound formal xs)" + .to_string(), + ]), + Some(xs) => match gi_formal_named(rename_of.clone(), "xs".to_string()) { + std::option::Option::None => Rc::new(vec![ + "reading supplied_nodes: UNREACHED (rename_of has no bound formal xs)" + .to_string(), + ]), + Some(renamed_xs) => gi_supplied_node_reading_lines( + xs.clone(), + renamed_xs.clone(), + ints.inferred.clone(), + si.clone(), + ), + }, + }, + }, + }, + } +} + +pub fn gi_supplied_node_reading_lines( + xs: Rc, + renamed_xs: Rc, + list_of_int: Rc, + si: Rc>>, +) -> Rc> { + { + let int_node = match gi_first_child(list_of_int.clone()) { + Some(c) => c.clone(), + std::option::Option::None => list_of_int.clone(), + }; + let formal_child_key = match gi_first_child(xs.declared_type.clone()) { + Some(c) => gi_declaration_label(c.declaration.clone()), + std::option::Option::None => "no child".to_string(), + }; + let substituted = crate::v1_compiler_infer::substitute_generics_apply( + xs.declared_type.clone(), + v1_rt::rc_map_insert( + v1_rt::rc_empty_map::>(), + "T".to_string(), + int_node.clone(), + ), + si.clone(), + ); + let substituted_child = gi_first_child(substituted.clone()); + let substituted_child_label = match substituted_child.clone() { + Some(c) => crate::v1_compiler_infer::type_node_label(c.clone(), si.clone()), + std::option::Option::None => "no child".to_string(), + }; + let substituted_child_declaration = match substituted_child.clone() { + Some(c) => gi_declaration_label(c.declaration.clone()), + std::option::Option::None => "no child".to_string(), + }; + let copied = crate::v1_compiler_infer::substitute_generics_apply( + xs.declared_type.clone(), + v1_rt::rc_map_insert( + v1_rt::rc_empty_map::>(), + "gic_no_such_parameter".to_string(), + int_node.clone(), + ), + si.clone(), + ); + let copied_child_key = match gi_first_child(copied.clone()) { + Some(c) => gi_declaration_label(c.declaration.clone()), + std::option::Option::None => "no child".to_string(), + }; + let bound_from_basis = crate::v1_compiler_infer::unify_generics( + xs.substitution_basis.clone(), + list_of_int.clone(), + Rc::new(vec!["T".to_string()]), + si.clone(), + v1_rt::rc_empty_map::>(), + ); + let bound_by_name_alone = crate::v1_compiler_infer::unify_generics( + renamed_xs.substitution_basis.clone(), + list_of_int.clone(), + Rc::new(vec!["M".to_string()]), + si.clone(), + v1_rt::rc_empty_map::>(), + ); + let renamed_child_key = match gi_first_child(renamed_xs.substitution_basis.clone()) { + Some(c) => gi_declaration_label(c.declaration.clone()), + std::option::Option::None => "no child".to_string(), + }; + Rc::new(vec![ + gi_reading_line( + "substitute_keeps_outer_declaration".to_string(), + v1_rt::concat( + v1_rt::concat( + if (gi_declaration_label(substituted.declaration.clone()) + == gi_declaration_label(xs.declared_type.clone().declaration.clone())) + { + "kept ".to_string() + } else { + "CHANGED from ".to_string() + }, + gi_declaration_label(xs.declared_type.clone().declaration.clone()), + ), + if (gi_declaration_label(xs.declared_type.clone().declaration.clone()) + == "none".to_string()) + { + " (vacuous: the input carried no declaration to lose)".to_string() + } else { + "".to_string() + }, + ), + ), + gi_reading_line( + "substitute_child_becomes".to_string(), + v1_rt::concat( + v1_rt::concat(substituted_child_label.clone(), " carrying ".to_string()), + substituted_child_declaration.clone(), + ), + ), + gi_reading_line( + "substitute_copy_keeps_child_declaration".to_string(), + if (copied_child_key.clone() == formal_child_key.clone()) { + v1_rt::concat("kept ".to_string(), copied_child_key.clone()) + } else { + v1_rt::concat( + v1_rt::concat( + v1_rt::concat("CHANGED ".to_string(), formal_child_key.clone()), + " -> ".to_string(), + ), + copied_child_key.clone(), + ) + }, + ), + gi_reading_line( + "unify_binds_from_substitution_basis".to_string(), + match v1_rt::map_get(&bound_from_basis, "T".to_string()) { + Some(b) => v1_rt::concat( + "T := ".to_string(), + crate::v1_compiler_infer::type_node_label(b.clone(), si.clone()), + ), + std::option::Option::None => "T unbound".to_string(), + }, + ), + gi_reading_line( + "unify_formal_child_mark".to_string(), + renamed_child_key.clone(), + ), + gi_reading_line( + "unify_binds_a_name_with_no_owner_check".to_string(), + match v1_rt::map_get(&bound_by_name_alone, "M".to_string()) { + Some(b) => v1_rt::concat( + "M := ".to_string(), + crate::v1_compiler_infer::type_node_label(b.clone(), si.clone()), + ), + std::option::Option::None => "M unbound".to_string(), + }, + ), + ]) + } +} + pub fn gi_tally(keys: Rc>) -> Rc> { keys.iter().cloned().fold( v1_rt::rc_empty_map::(), @@ -1480,61 +1699,86 @@ pub fn generic_identity_fixture_standing(sources: Rc>>) -> St let unobserved_declared = ((generic_identity_unobserved().len() as i64) == 4); let owner_argument_arms = gi_owner_argument_arms_discriminate(g.clone(), si.clone(), sigs.clone()); + let conformance_keeps_mark = { + let mut __found = false; + for r in rows.iter().cloned() { + if ((((r.enclosing.clone() + == "same_spelling_as_a_record_parameter".to_string()) + && (r.carrier.clone() + == "formal_declaration_bound_conformance".to_string())) + && (r.path.clone() == "q".to_string())) + && (gi_declaration_label(r.declaration.clone()) + == "gic.a::same_spelling_as_a_record_parameter::".to_string())) + { + __found = true; + break; + } + } + __found + }; let missing_carriers = gi_missing_carriers_are_unobserved(g.clone(), si.clone(), sigs.clone()); - let held = (((((marked_signature_leaf.clone() + let held = ((((((marked_signature_leaf.clone() && minted_container_child.clone()) && bound_call_observed_clean.clone()) && unobserved_declared.clone()) && owner_argument_arms.clone()) - && missing_carriers.clone()); - Rc::new(vec![ - v1_rt::concat( - "STANDING ".to_string(), - if held.clone() { - "held".to_string() - } else { - "unmet".to_string() - }, - ), - gi_control_line( - "marked_signature_leaf".to_string(), - marked_signature_leaf.clone(), - ), - gi_control_line( - "minted_container_child".to_string(), - minted_container_child.clone(), - ), - gi_control_line( - "bound_call_observed_clean".to_string(), - bound_call_observed_clean.clone(), - ), - gi_control_line( - "unobserved_populations_declared".to_string(), - unobserved_declared.clone(), - ), - gi_control_line( - "owner_argument_arms_discriminate".to_string(), - owner_argument_arms.clone(), - ), - gi_control_line( - "missing_carriers_are_unobserved".to_string(), - missing_carriers.clone(), - ), - v1_rt::concat( - "reading bound_call: ".to_string(), - gi_collision_reading(bound_call.clone()), - ), - v1_rt::concat( - "reading spelling_collision_call: ".to_string(), - gi_collision_reading(gi_result_carrier_observation( - g.clone(), - si.clone(), - sigs.clone(), - "caller_literal".to_string(), - )), - ), - ]) + && missing_carriers.clone()) + && conformance_keeps_mark.clone()); + v1_rt::concat( + Rc::new(vec![ + v1_rt::concat( + "STANDING ".to_string(), + if held.clone() { + "held".to_string() + } else { + "unmet".to_string() + }, + ), + gi_control_line( + "marked_signature_leaf".to_string(), + marked_signature_leaf.clone(), + ), + gi_control_line( + "minted_container_child".to_string(), + minted_container_child.clone(), + ), + gi_control_line( + "bound_call_observed_clean".to_string(), + bound_call_observed_clean.clone(), + ), + gi_control_line( + "unobserved_populations_declared".to_string(), + unobserved_declared.clone(), + ), + gi_control_line( + "owner_argument_arms_discriminate".to_string(), + owner_argument_arms.clone(), + ), + gi_control_line( + "missing_carriers_are_unobserved".to_string(), + missing_carriers.clone(), + ), + gi_control_line( + "conformance_keeps_the_parameter_mark".to_string(), + conformance_keeps_mark.clone(), + ), + v1_rt::concat( + "reading bound_call: ".to_string(), + gi_collision_reading(bound_call.clone()), + ), + v1_rt::concat( + "reading spelling_collision_call: ".to_string(), + gi_collision_reading(gi_result_carrier_observation( + g.clone(), + si.clone(), + sigs.clone(), + "caller_literal".to_string(), + )), + ), + ]), + gi_supplied_node_readings(sigs.clone(), si.clone()), + ) .join(&"\n".to_string()) } } diff --git a/src/v1/tests/claim/generic_identity_census.dag b/src/v1/tests/claim/generic_identity_census.dag index 0e37dea2a2f..c474b22e3f8 100644 --- a/src/v1/tests/claim/generic_identity_census.dag +++ b/src/v1/tests/claim/generic_identity_census.dag @@ -3,7 +3,7 @@ module v1.tests.claim.generic_identity_census import v1.compiler.compile { SourceFile, ResolvedPipelineResult, compile_to_resolved } import v1.compiler.infer_items { ResolvedGraph, TypedModule } import v1.compiler.infer_sigs { ResolvedFuncSig, ResolvedFormals, DeclarationBoundFormals, KernelGroundedFormals, LocalFormalsAwaitingModuleContext } -import v1.compiler.infer { param_is_generic_decl, type_node_label } +import v1.compiler.infer { param_is_generic_decl, type_node_label, unify_generics, substitute_generics_apply } import v1.compiler.infer_env { node_with_children } import v1.std.core { Node, NewlineIndex, ResolvedFormal, authored_name_at, param_node_type_expr, param_node_name_at, Resolved, TypeVariable, Arrow } import std.decl_ref { DeclarationRef, TypeParameter, WholeDeclaration, NamedField, declaration_ref_display_key } @@ -480,6 +480,105 @@ fn gi_rows_from_sources(sources: List) -> List? } } +// THE TWO UNOBSERVED OPERATIONS, EXECUTED OVER SUPPLIED NODES (DESIGN section 3, a witness +// discriminates at one interface). The census cannot see inside unify_generics or +// substitute_generics_apply, so these call them directly. Every operand is a node the REAL producer +// emitted for the fixture -- a signature's formal, a declared return -- never a hand-built one, so +// the readings are about the shapes infer actually hands those functions. +fn gi_formal_named(sig: ResolvedFuncSig, parameter: String) -> ResolvedFormal? { + match sig.resolved_formals { + DeclarationBoundFormals { formals: fs } => fs |> filter(f => f.parameter_identity == parameter) |> first + KernelGroundedFormals { formals: fs } => fs |> filter(f => f.parameter_identity == parameter) |> first + LocalFormalsAwaitingModuleContext {} => none + } +} + +fn gi_first_child(n: Node) -> Node? { + n.children |> first +} + +fn gi_reading_line(name: String, value: String) -> String { + concat(concat(concat("reading ", name), ": "), value) +} + +fn gi_supplied_node_readings(sigs: Map, si: Map) -> List { + match map_get(sigs, "gic.a::head_of") { + Absent => ["reading supplied_nodes: UNREACHED (no signature gic.a::head_of)"] + Present { value: head_of } => + match map_get(sigs, "gic.a::ints") { + Absent => ["reading supplied_nodes: UNREACHED (no signature gic.a::ints)"] + Present { value: ints } => + match map_get(sigs, "gic.a::rename_of") { + Absent => ["reading supplied_nodes: UNREACHED (no signature gic.a::rename_of)"] + Present { value: rename_of } => + match gi_formal_named(sig: head_of, parameter: "xs") { + Absent => ["reading supplied_nodes: UNREACHED (head_of has no bound formal xs)"] + Present { value: xs } => + match gi_formal_named(sig: rename_of, parameter: "xs") { + Absent => ["reading supplied_nodes: UNREACHED (rename_of has no bound formal xs)"] + Present { value: renamed_xs } => + gi_supplied_node_reading_lines(xs: xs, renamed_xs: renamed_xs, list_of_int: ints.inferred, si: si) + } + } + } + } + } +} + +// WHAT EACH READING EXECUTES. +// substitute_*: bet 2. List under { T := Int } (the substituting arm), and the same node under +// a substitution naming no parameter of it (the copy arm, law L1). +// unify_binds_from_substitution_basis: bet 1's plan half -- what unify_generics binds from the +// field infer_call_arguments_generic_pass hands it. +// unify_binds_a_name_with_no_owner_check: the spelling decision, isolated. rename_of's formal is +// List, whose child carries the mark of rename_of's own M; asked to bind a parameter NAMED M +// with no owner supplied, unify_generics has only the name to go on. +fn gi_supplied_node_reading_lines(xs: ResolvedFormal, renamed_xs: ResolvedFormal, list_of_int: Node, si: Map) -> List { + let int_node = match gi_first_child(n: list_of_int) { + Present { value: c } => c + Absent => list_of_int + } + let formal_child_key = match gi_first_child(n: xs.declared_type) { + Present { value: c } => gi_declaration_label(d: c.declaration) + Absent => "no child" + } + let substituted = substitute_generics_apply(n: xs.declared_type, subst: map_insert(empty_map(), "T", int_node), source_indices: si) + let substituted_child = gi_first_child(n: substituted) + let substituted_child_label = match substituted_child { + Present { value: c } => type_node_label(n: c, source_indices: si) + Absent => "no child" + } + let substituted_child_declaration = match substituted_child { + Present { value: c } => gi_declaration_label(d: c.declaration) + Absent => "no child" + } + let copied = substitute_generics_apply(n: xs.declared_type, subst: map_insert(empty_map(), "gic_no_such_parameter", int_node), source_indices: si) + let copied_child_key = match gi_first_child(n: copied) { + Present { value: c } => gi_declaration_label(d: c.declaration) + Absent => "no child" + } + let bound_from_basis = unify_generics(formal: xs.substitution_basis, actual: list_of_int, generic_names: ["T"], source_indices: si, acc: empty_map()) + let bound_by_name_alone = unify_generics(formal: renamed_xs.substitution_basis, actual: list_of_int, generic_names: ["M"], source_indices: si, acc: empty_map()) + let renamed_child_key = match gi_first_child(n: renamed_xs.substitution_basis) { + Present { value: c } => gi_declaration_label(d: c.declaration) + Absent => "no child" + } + [ + gi_reading_line(name: "substitute_keeps_outer_declaration", value: concat(concat(if gi_declaration_label(d: substituted.declaration) == gi_declaration_label(d: xs.declared_type.declaration) { "kept " } else { "CHANGED from " }, gi_declaration_label(d: xs.declared_type.declaration)), if gi_declaration_label(d: xs.declared_type.declaration) == "none" { " (vacuous: the input carried no declaration to lose)" } else { "" })), + gi_reading_line(name: "substitute_child_becomes", value: concat(concat(substituted_child_label, " carrying "), substituted_child_declaration)), + gi_reading_line(name: "substitute_copy_keeps_child_declaration", value: if copied_child_key == formal_child_key { concat("kept ", copied_child_key) } else { concat(concat(concat("CHANGED ", formal_child_key), " -> "), copied_child_key) }), + gi_reading_line(name: "unify_binds_from_substitution_basis", value: match map_get(bound_from_basis, "T") { + Present { value: b } => concat("T := ", type_node_label(n: b, source_indices: si)) + Absent => "T unbound" + }), + gi_reading_line(name: "unify_formal_child_mark", value: renamed_child_key), + gi_reading_line(name: "unify_binds_a_name_with_no_owner_check", value: match map_get(bound_by_name_alone, "M") { + Present { value: b } => concat("M := ", type_node_label(n: b, source_indices: si)) + Absent => "M unbound" + }) + ] +} + fn gi_tally(keys: List) -> Map { fold(keys, init: empty_map(), f: (acc, k) => match map_get(acc, k) { @@ -592,6 +691,12 @@ type GenericIdentityContextItem { // argument does bind the parameter, OBSERVED typed Int and carrying no foreign parameter. None // depends on a defect staying unrepaired. The call the spelling collision leaves unsubstituted is a // three-valued READING beside them and never gates, because repairing it is the point of step 2. +// +// conformance_keeps_the_parameter_mark is the copy law (L1) at one stored carrier. The fixture's +// same_spelling_as_a_record_parameter declares a parameter spelled like the record Box's, and +// its formal q: Q must carry ITS OWN mark in declaration_bound_conformance. Before +// v1.compiler.infer_resolve peel_nominal_alias_identity read the mark, the name lookup replaced that +// leaf with whatever the module bound to the spelling Q, and this control was UNMET. fn gi_control_line(name: String, held: Bool) -> String { concat(concat(concat("control ", name), ": "), if held { "held" } else { "UNMET" }) } @@ -711,9 +816,12 @@ fn generic_identity_fixture_standing(sources: List) -> String { let bound_call_observed_clean = gi_bound_call_observed_clean(o: bound_call) let unobserved_declared = (generic_identity_unobserved() |> count) == 4 let owner_argument_arms = gi_owner_argument_arms_discriminate(g: g, si: si, sigs: sigs) + let conformance_keeps_mark = rows |> any(r => + r.enclosing == "same_spelling_as_a_record_parameter" && r.carrier == "formal_declaration_bound_conformance" && r.path == "q" + && gi_declaration_label(d: r.declaration) == "gic.a::same_spelling_as_a_record_parameter::") let missing_carriers = gi_missing_carriers_are_unobserved(g: g, si: si, sigs: sigs) - let held = marked_signature_leaf && minted_container_child && bound_call_observed_clean && unobserved_declared && owner_argument_arms && missing_carriers - [ + let held = marked_signature_leaf && minted_container_child && bound_call_observed_clean && unobserved_declared && owner_argument_arms && missing_carriers && conformance_keeps_mark + concat([ concat("STANDING ", if held { "held" } else { "unmet" }), gi_control_line(name: "marked_signature_leaf", held: marked_signature_leaf), gi_control_line(name: "minted_container_child", held: minted_container_child), @@ -721,9 +829,10 @@ fn generic_identity_fixture_standing(sources: List) -> String { gi_control_line(name: "unobserved_populations_declared", held: unobserved_declared), gi_control_line(name: "owner_argument_arms_discriminate", held: owner_argument_arms), gi_control_line(name: "missing_carriers_are_unobserved", held: missing_carriers), + gi_control_line(name: "conformance_keeps_the_parameter_mark", held: conformance_keeps_mark), concat("reading bound_call: ", gi_collision_reading(o: bound_call)), concat("reading spelling_collision_call: ", gi_collision_reading(o: gi_result_carrier_observation(g: g, si: si, sigs: sigs, function_name: "caller_literal"))) - ] |> join(separator: "\n") + ], gi_supplied_node_readings(sigs: sigs, si: si)) |> join(separator: "\n") } }