From 2e7ff59002343163fb8f210604bf6b2b5a2009b6 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 10:27:55 +0000 Subject: [PATCH 1/7] Lambda-return solves: unify a lambda argument's callable (built by make_callable_type) against its formal in round 1; empty-literal placeholder solved by a later actual; #9416 note rewritten (mirrors pending regen round) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v1/04_infer.dag | 136 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 127 insertions(+), 9 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 7d6a55323ed..a9e74d7bc34 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -7596,12 +7596,21 @@ fn is_lambda_expr(e: Node) -> Bool { // again from the substitution the first round ended with, so every argument sees every // binding derivable in one forward pass regardless of authored order. Re-running is // sound rather than merely convenient because the substitution is a fixed point of the -// second round: lambda arguments are skipped for unification, so deferring what they -// would have contributed cannot change the result, and a formal whose generic slot is -// already bound is substituted to a concrete node that unify_generics no longer binds. -// It is bounded at two rounds and says so: a binding that is only derivable FROM a -// substituted expected type -- a lambda return feeding a later formal -- is still out -// of reach, and that is a narrowing stated rather than implied. +// second round: a lambda argument contributes to the substitution in ROUND 1 ONLY +// (unify_lambda_solves), and only informative bindings that solve an Absent slot or the +// minted empty-literal placeholder; in round 2 lambdas are skipped, so deferring what they +// would contribute cannot change the result, and a formal whose generic slot is already +// bound is substituted to a concrete node that unify_generics no longer binds. +// The narrowing this note used to state -- a binding derivable only from a lambda's +// A round-2 MISMATCH between a lambda's return and its substituted formal return is ALREADY +// judged: the lambda is inferred against the substituted expected callable, and +// `ap(f: fn(v) { v }, x: 1, r: 's')` refuses `expected Callable(Int->String), got +// Callable(Int->Int)` on main ed68b557. No second check belongs here; the open gap is the +// UNSOLVED case (gunbc.recurring_failure_mode unbound_generic_reaches_conformance_unjudged). +// return, such as fold_list's accumulator when `empty` is an empty literal -- is LIFTED by +// that round-1 contribution (unify_callable_generics unifies the callable's params and +// return). It stays bounded at two rounds: a round-2 return is not fed back again, and a +// return that depends on a binding only round 2 supplies contributes nothing. fn expr_contains_lambda(n: Node) -> Bool { is_lambda_expr(e: n) || (n.children |> any(c => expr_contains_lambda(n: c))) } @@ -7762,8 +7771,16 @@ fn infer_call_arguments_generic_pass(call_args: List, value_params: List InferResu Absent => unit_type } } else { unit_type } - Absent => type_variable_node(id: "empty_list_element") + Absent => type_variable_node(id: empty_list_element_variable_id) } } } @@ -13671,8 +13688,13 @@ fn unify_generics(formal: Node, actual: Node, generic_names: List, sourc match map_get(acc, bind_name) { Absent => map_insert(acc, bind_name, actual) - Present { value: _ } => acc + Present { value: existing } => + if unify_binding_is_placeholder(n: existing) && !unify_binding_is_placeholder(n: actual) { + map_insert(acc, bind_name, actual) + } else { acc } } + } else if (formal.connective == Arrow && actual.connective == Arrow) { + unify_callable_generics(formal: formal, actual: actual, generic_names: generic_names, source_indices: source_indices, acc: acc) } else if formal.children |> count == 1 && actual.children |> count == 1 { match formal.children |> first { Present { value: fc } => @@ -13685,6 +13707,102 @@ fn unify_generics(formal: Node, actual: Node, generic_names: List, sourc } else { acc } } +// A callable denotes its parameters in params and its return in inferred (make_callable_type), so +// it has no children for the descent below to walk. Its parameters unify positionally and its +// return unifies return, each read through child_type_node, the total read of a type position. +fn unify_callable_generics(formal: Node, actual: Node, generic_names: List, source_indices: Map, acc: Map) -> Map { + let with_params = unify_callable_param_pairs(formals: formal.params, actuals: actual.params, generic_names: generic_names, source_indices: source_indices, acc: acc) + match formal.inferred { + Present { value: Resolved { node: formal_ret } } => + match actual.inferred { + Present { value: Resolved { node: actual_ret } } => unify_generics(formal: formal_ret, actual: actual_ret, generic_names: generic_names, source_indices: source_indices, acc: with_params) + _ => with_params + } + _ => with_params + } +} + +// A typed lambda carries its BODY'S RETURN in inferred (infer_expr ExprLambda), not a callable +// type, and its parameter types on its param children (the children after the body). Unify needs +// the callable, so it is built here with make_callable_type, the existing authority for one. +fn lambda_callable_type(lambda: Node) -> Node { + make_callable_type(func_params: lambda.children |> skip(1), ret: resolved_type(n: lambda)) +} + +fn unify_callable_param_pairs(formals: List, actuals: List, generic_names: List, source_indices: Map, acc: Map) -> Map { + match formals |> first { + Present { value: f } => + match actuals |> first { + Present { value: a } => + unify_callable_param_pairs( + formals: formals |> skip(1), + actuals: actuals |> skip(1), + generic_names: generic_names, + source_indices: source_indices, + acc: unify_generics(formal: child_type_node(ch: f), actual: child_type_node(ch: a), generic_names: generic_names, source_indices: source_indices, acc: acc) + ) + Absent => acc + } + Absent => acc + } +} + +// What a lambda argument may contribute in round 1: only a binding that carries information. Its +// return is computed under a substitution that may not yet bind its own parameters, so it can be +// an unresolved type variable (callable_param), and binding a parameter to that would fix it first +// and keep it against the informative argument that follows. Such an entry is dropped, so a later +// argument or round 2 decides it. An entry solves only an Absent binding or the minted placeholder. +fn unify_lambda_solves(solved: Map, generic_names: List, acc: Map) -> Map { + fold(generic_names, init: acc, f: (st, g) => + match map_get(solved, g) { + Present { value: candidate } => + if unify_binding_is_uninformative(n: candidate) { + st + } else { + match map_get(st, g) { + Absent => map_insert(st, g, candidate) + Present { value: existing } => if unify_binding_is_placeholder(n: existing) { map_insert(st, g, candidate) } else { st } + } + } + Absent => st + } + ) +} + +// A type that is, or holds as its single element, any unresolved type variable. +fn unify_binding_is_uninformative(n: Node) -> Bool { + match n.inferred { + Present { value: TypeVariable { id: _ } } => true + _ => + if n.children |> count == 1 { + match n.children |> first { + Present { value: c } => unify_binding_is_uninformative(n: child_type_node(ch: c)) + Absent => false + } + } else { false } + } +} + +// The type variable an empty list literal with no expected type mints for its element: one +// authority for the mint in infer_expr ExprListLit and the check in unify_binding_is_placeholder. +data empty_list_element_variable_id: String = "empty_list_element" + +// That placeholder is an unsolved variable, not a binding: it carries no information about the +// parameter, so a later informative actual solves it. Only the minted placeholder yields; a type +// parameter in scope is a TypeVariable too and is information, so it never yields. +fn unify_binding_is_placeholder(n: Node) -> Bool { + match n.inferred { + Present { value: TypeVariable { id: tv } } => tv == empty_list_element_variable_id + _ => + if n.children |> count == 1 { + match n.children |> first { + Present { value: c } => unify_binding_is_placeholder(n: child_type_node(ch: c)) + Absent => false + } + } else { false } + } +} + fn should_unify_record_lit_generics(formal: Node, arg_expr: Node, generic_names: List, source_indices: Map) -> Bool { match record_lit_expr_optional(expr: arg_expr) { Absent => false From 48e090bdef67efc56395b9e62b9a17a831c50740 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:22:31 +0000 Subject: [PATCH 2/7] Regenerate the infer mirror for lambda-return solves (regen round converges: first_generation_equal=true, rebuild_packages=0, in a fresh tree at 864c9ce0c9) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v1/stage0/src/v1_compiler_infer.rs | 322 +++++++++++++++++++++---- 1 file changed, 278 insertions(+), 44 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 5a89bbe34e9..e7828d5eeab 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -11876,32 +11876,48 @@ pub fn infer_call_arguments_generic_pass( } else { ar_inferred.clone() }; - let next_subst = if (is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) - || !has_formal.clone()) - { + let next_subst = if !has_formal.clone() { st.subst.clone() } else { - if should_unify_record_lit_generics( - formal_raw.clone(), - crate::v1_std_core::arg_value(a.clone()), - generic_names.clone(), - scope.type_env.clone().source_indices.clone(), - ) { - unify_record_lit_generics( - formal_raw.clone(), - ar.typed.clone(), - generic_names.clone(), - scope.clone(), - st.subst.clone(), - ) + if is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) { + if v1_rt::map_is_empty(&init_subst) { + unify_lambda_solves( + unify_generics( + formal_raw.clone(), + lambda_callable_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + v1_rt::rc_empty_map::>(), + ), + generic_names.clone(), + st.subst.clone(), + ) + } else { + st.subst.clone() + } } else { - unify_generics( + if should_unify_record_lit_generics( formal_raw.clone(), - crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + crate::v1_std_core::arg_value(a.clone()), generic_names.clone(), scope.type_env.clone().source_indices.clone(), - st.subst.clone(), - ) + ) { + unify_record_lit_generics( + formal_raw.clone(), + ar.typed.clone(), + generic_names.clone(), + scope.clone(), + st.subst.clone(), + ) + } else { + unify_generics( + formal_raw.clone(), + crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + st.subst.clone(), + ) + } } }; Rc::new(ArgGenericFoldState { @@ -14993,7 +15009,7 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), } } std::option::Option::None => { - type_variable_node("empty_list_element".to_string()) + type_variable_node(empty_list_element_variable_id()) } } } @@ -23654,44 +23670,262 @@ pub fn unify_generics( std::option::Option::None => { break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); } - Some(_) => { - break acc.clone(); + Some(existing) => { + if (unify_binding_is_placeholder(existing.clone()) + && !unify_binding_is_placeholder(actual.clone())) + { + break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); + } else { + break acc.clone(); + } } } } else { - if (((formal.children.clone().len() as i64) == 1) - && ((actual.children.clone().len() as i64) == 1)) + if ((formal.connective.clone() == Connective::Arrow) + && (actual.connective.clone() == Connective::Arrow)) { - match formal.children.clone().first().cloned() { - Some(fc) => match actual.children.clone().first().cloned() { - Some(ac) => { - let __tco_0 = fc.clone(); - let __tco_1 = ac.clone(); - let __tco_2 = generic_names; - let __tco_3 = source_indices; - let __tco_4 = acc; - __tco_loop_formal = __tco_0; - __tco_loop_actual = __tco_1; - __tco_loop_generic_names = __tco_2; - __tco_loop_source_indices = __tco_3; - __tco_loop_acc = __tco_4; - continue; - } + break unify_callable_generics( + formal.clone(), + actual.clone(), + generic_names.clone(), + source_indices.clone(), + acc.clone(), + ); + } else { + if (((formal.children.clone().len() as i64) == 1) + && ((actual.children.clone().len() as i64) == 1)) + { + match formal.children.clone().first().cloned() { + Some(fc) => match actual.children.clone().first().cloned() { + Some(ac) => { + let __tco_0 = fc.clone(); + let __tco_1 = ac.clone(); + let __tco_2 = generic_names; + let __tco_3 = source_indices; + let __tco_4 = acc; + __tco_loop_formal = __tco_0; + __tco_loop_actual = __tco_1; + __tco_loop_generic_names = __tco_2; + __tco_loop_source_indices = __tco_3; + __tco_loop_acc = __tco_4; + continue; + } + std::option::Option::None => { + break acc.clone(); + } + }, std::option::Option::None => { break acc.clone(); } - }, - std::option::Option::None => { - break acc.clone(); } + } else { + break acc.clone(); } - } else { + } + } + } +} + +pub fn unify_callable_generics( + formal: Rc, + actual: Rc, + generic_names: Rc>, + source_indices: Rc>>, + acc: Rc>>, +) -> Rc>> { + { + let with_params = unify_callable_param_pairs( + formal.params.clone(), + actual.params.clone(), + generic_names.clone(), + source_indices.clone(), + acc.clone(), + ); + match formal.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: formal_ret, .. + }) => match actual.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: actual_ret, .. + }) => unify_generics( + formal_ret.clone(), + actual_ret.clone(), + generic_names.clone(), + source_indices.clone(), + with_params.clone(), + ), + _ => with_params.clone(), + }, + _ => with_params.clone(), + } + } +} + +pub fn lambda_callable_type(lambda: Rc) -> Rc { + crate::v1_compiler_infer_types::make_callable_type( + Rc::new( + lambda + .children + .clone() + .iter() + .cloned() + .skip(1 as usize) + .collect::>(), + ), + crate::v1_compiler_infer_types::resolved_type(lambda.clone()), + ) +} + +pub fn unify_callable_param_pairs( + mut __tco_loop_formals: Rc>>, + mut __tco_loop_actuals: Rc>>, + mut __tco_loop_generic_names: Rc>, + mut __tco_loop_source_indices: Rc>>, + mut __tco_loop_acc: Rc>>, +) -> Rc>> { + loop { + #[allow(unused_mut)] + let mut formals = __tco_loop_formals; + #[allow(unused_mut)] + let mut actuals = __tco_loop_actuals; + #[allow(unused_mut)] + let mut generic_names = __tco_loop_generic_names; + #[allow(unused_mut)] + let mut source_indices = __tco_loop_source_indices; + #[allow(unused_mut)] + let mut acc = __tco_loop_acc; + match formals.clone().first().cloned() { + Some(f) => match actuals.clone().first().cloned() { + Some(a) => { + let __tco_0 = + Rc::new(formals.iter().cloned().skip(1 as usize).collect::>()); + let __tco_1 = + Rc::new(actuals.iter().cloned().skip(1 as usize).collect::>()); + let __tco_2 = generic_names.clone(); + let __tco_3 = source_indices.clone(); + let __tco_4 = unify_generics( + crate::v1_compiler_infer_types::child_type_node(f.clone()), + crate::v1_compiler_infer_types::child_type_node(a.clone()), + generic_names.clone(), + source_indices.clone(), + acc, + ); + __tco_loop_formals = __tco_0; + __tco_loop_actuals = __tco_1; + __tco_loop_generic_names = __tco_2; + __tco_loop_source_indices = __tco_3; + __tco_loop_acc = __tco_4; + continue; + } + std::option::Option::None => { + break acc.clone(); + } + }, + std::option::Option::None => { break acc.clone(); } } } } +pub fn unify_lambda_solves( + solved: Rc>>, + generic_names: Rc>, + acc: Rc>>, +) -> Rc>> { + generic_names.iter().cloned().fold( + acc.clone(), + |st: Rc>>, g: String| match v1_rt::map_get(&solved, g.clone()) { + Some(candidate) => { + if unify_binding_is_uninformative(candidate.clone()) { + st.clone() + } else { + match v1_rt::map_get(&st, g.clone()) { + std::option::Option::None => { + v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) + } + Some(existing) => { + if unify_binding_is_placeholder(existing.clone()) { + v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) + } else { + st.clone() + } + } + } + } + } + std::option::Option::None => st.clone(), + }, + ) +} + +pub fn unify_binding_is_uninformative(mut __tco_loop_n: Rc) -> bool { + loop { + #[allow(unused_mut)] + let mut n = __tco_loop_n; + match n.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: _, .. }) => { + break true; + } + _ => { + if ((n.children.clone().len() as i64) == 1) { + match n.children.clone().first().cloned() { + Some(c) => { + let __tco_0 = + crate::v1_compiler_infer_types::child_type_node(c.clone()); + __tco_loop_n = __tco_0; + continue; + } + std::option::Option::None => { + break false; + } + } + } else { + break false; + } + } + } + } +} + +pub fn empty_list_element_variable_id() -> String { + thread_local! { + static CACHED: String = { + "empty_list_element".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +pub fn unify_binding_is_placeholder(mut __tco_loop_n: Rc) -> bool { + loop { + #[allow(unused_mut)] + let mut n = __tco_loop_n; + match n.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: tv, .. }) => { + break (tv.clone() == empty_list_element_variable_id()); + } + _ => { + if ((n.children.clone().len() as i64) == 1) { + match n.children.clone().first().cloned() { + Some(c) => { + let __tco_0 = + crate::v1_compiler_infer_types::child_type_node(c.clone()); + __tco_loop_n = __tco_0; + continue; + } + std::option::Option::None => { + break false; + } + } + } else { + break false; + } + } + } + } +} + pub fn should_unify_record_lit_generics( formal: Rc, arg_expr: Rc, From 0f9a55aaf5153eb4bdf86ab1d09445f1fb0bb6c0 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:56:34 +0000 Subject: [PATCH 3/7] Row unbound_generic_reaches_conformance_unjudged: the lambda-return member closes with this PR; p7b stays open Co-Authored-By: Claude Opus 5.5 (1M context) --- .../unbound_generic_reaches_conformance_unjudged.dag | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag b/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag index 2c8407fbecf..b530d1b7d22 100644 --- a/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag +++ b/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag @@ -23,6 +23,8 @@ data unbound_generic_reaches_conformance_unjudged: RecurringFailureMode = Recurr "NOT FIXED BY MORE BINDING: lifting particular routes (a lambda's return feeding a parameter, the #9416 narrowing in v1.compiler.infer above expr_contains_lambda) shrinks the population but leaves it open, because some parameters are genuinely not inferable from a call site. A round-2 MISMATCH is already judged on main: `ap(f: fn(T) -> R, x: T, r: R)` with `ap(f: fn(v) { v }, x: 1, r: 's')` refuses `expected Callable(Int->String), got Callable(Int->Int)`. The gap is the UNSOLVED case, not the disagreeing one.", + "PARTIAL CLOSURE, gunbc#13418: the LAMBDA-RETURN member closes. A generic fixed only by a lambda argument's return is now solved from it (v1.compiler.infer infer_call_arguments_generic_pass, lambda_callable_type and unify_callable_generics), so p8, p8b and p9 REFUSE `expected Primitive(String), got Primitive(Int)` at the located position instead of being Accepted. p7b STAYS OPEN: its lambda comes BEFORE the argument that fixes T, so in round 1 the lambda's return is still the unresolved callable_param and is dropped, round 2 contributes nothing, and R stays unbound and passes conformance unjudged. That is the stated two-round bound, and this row's wall (refuse an unresolved generic at a declared-type position) is what closes it, not more rounds.", + "RUNG FOUND AT: below the floor (silent acceptance). CEILING: 3 -- an unresolved type parameter at a declared-type position is a modeled state, decidable at the conformance site. NEXT TRIGGER: a call whose result type is an unresolved generic parameter, reaching a declared-type position, refuses with a typed located 'cannot infer here; annotate' diagnostic. Evidence: p8, p8b and p7b refuse with that cause; `apply2(f: fn(v) { v }, x: 1)` under a declared -> Int is the accepted control. That wall refuses some code main accepts today, by design, and lands as its own step with its own census of the sites that newly refuse.", ], From a361b1e608a325543eb9736febe0b87ee9f15f4b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 14:58:41 +0000 Subject: [PATCH 4/7] Reorder the #9416 note so its sentence is whole; cite the row that records the specimens, not a commit (review 76610) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v1/04_infer.dag | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index 6e62819b4c1..b9c65f0b680 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -7602,15 +7602,15 @@ fn is_lambda_expr(e: Node) -> Bool { // would contribute cannot change the result, and a formal whose generic slot is already // bound is substituted to a concrete node that unify_generics no longer binds. // The narrowing this note used to state -- a binding derivable only from a lambda's -// A round-2 MISMATCH between a lambda's return and its substituted formal return is ALREADY -// judged: the lambda is inferred against the substituted expected callable, and -// `ap(f: fn(v) { v }, x: 1, r: 's')` refuses `expected Callable(Int->String), got -// Callable(Int->Int)` on main ed68b557. No second check belongs here; the open gap is the -// UNSOLVED case (gunbc.recurring_failure_mode unbound_generic_reaches_conformance_unjudged). // return, such as fold_list's accumulator when `empty` is an empty literal -- is LIFTED by // that round-1 contribution (unify_callable_generics unifies the callable's params and // return). It stays bounded at two rounds: a round-2 return is not fed back again, and a // return that depends on a binding only round 2 supplies contributes nothing. +// A round-2 MISMATCH between a lambda's return and its substituted formal return is ALREADY +// judged, because the lambda is inferred against the substituted expected callable: a call +// such as `ap(f: fn(v) { v }, x: 1, r: 's')` refuses the callable mismatch. No second check +// belongs here. The open gap is the UNSOLVED case, whose specimens and wall are recorded in +// gunbc.recurring_failure_mode unbound_generic_reaches_conformance_unjudged. fn expr_contains_lambda(n: Node) -> Bool { is_lambda_expr(e: n) || (n.children |> any(c => expr_contains_lambda(n: c))) } From 2ece97ecbcbe9b48d6828b117f6312d53786a38e Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 15:43:35 +0000 Subject: [PATCH 5/7] Regenerate the infer mirror after merging main (fresh checkout: round 3 first_generation_equal=true, convergence_stages=0, rebuild_packages=0) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v1/stage0/src/v1_compiler_infer.rs | 322 +++++++++++++++++++++---- 1 file changed, 278 insertions(+), 44 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 1bafe0dd5d2..1049cf79e6a 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -11876,32 +11876,48 @@ pub fn infer_call_arguments_generic_pass( } else { ar_inferred.clone() }; - let next_subst = if (is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) - || !has_formal.clone()) - { + let next_subst = if !has_formal.clone() { st.subst.clone() } else { - if should_unify_record_lit_generics( - formal_raw.clone(), - crate::v1_std_core::arg_value(a.clone()), - generic_names.clone(), - scope.type_env.clone().source_indices.clone(), - ) { - unify_record_lit_generics( - formal_raw.clone(), - ar.typed.clone(), - generic_names.clone(), - scope.clone(), - st.subst.clone(), - ) + if is_lambda_expr(crate::v1_std_core::arg_value(a.clone())) { + if v1_rt::map_is_empty(&init_subst) { + unify_lambda_solves( + unify_generics( + formal_raw.clone(), + lambda_callable_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + v1_rt::rc_empty_map::>(), + ), + generic_names.clone(), + st.subst.clone(), + ) + } else { + st.subst.clone() + } } else { - unify_generics( + if should_unify_record_lit_generics( formal_raw.clone(), - crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + crate::v1_std_core::arg_value(a.clone()), generic_names.clone(), scope.type_env.clone().source_indices.clone(), - st.subst.clone(), - ) + ) { + unify_record_lit_generics( + formal_raw.clone(), + ar.typed.clone(), + generic_names.clone(), + scope.clone(), + st.subst.clone(), + ) + } else { + unify_generics( + formal_raw.clone(), + crate::v1_compiler_infer_types::resolved_type(ar.typed.clone()), + generic_names.clone(), + scope.type_env.clone().source_indices.clone(), + st.subst.clone(), + ) + } } }; Rc::new(ArgGenericFoldState { @@ -14993,7 +15009,7 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), } } std::option::Option::None => { - type_variable_node("empty_list_element".to_string()) + type_variable_node(empty_list_element_variable_id()) } } } @@ -23654,44 +23670,262 @@ pub fn unify_generics( std::option::Option::None => { break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); } - Some(_) => { - break acc.clone(); + Some(existing) => { + if (unify_binding_is_placeholder(existing.clone()) + && !unify_binding_is_placeholder(actual.clone())) + { + break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); + } else { + break acc.clone(); + } } } } else { - if (((formal.children.clone().len() as i64) == 1) - && ((actual.children.clone().len() as i64) == 1)) + if ((formal.connective.clone() == Connective::Arrow) + && (actual.connective.clone() == Connective::Arrow)) { - match formal.children.clone().first().cloned() { - Some(fc) => match actual.children.clone().first().cloned() { - Some(ac) => { - let __tco_0 = fc.clone(); - let __tco_1 = ac.clone(); - let __tco_2 = generic_names; - let __tco_3 = source_indices; - let __tco_4 = acc; - __tco_loop_formal = __tco_0; - __tco_loop_actual = __tco_1; - __tco_loop_generic_names = __tco_2; - __tco_loop_source_indices = __tco_3; - __tco_loop_acc = __tco_4; - continue; - } + break unify_callable_generics( + formal.clone(), + actual.clone(), + generic_names.clone(), + source_indices.clone(), + acc.clone(), + ); + } else { + if (((formal.children.clone().len() as i64) == 1) + && ((actual.children.clone().len() as i64) == 1)) + { + match formal.children.clone().first().cloned() { + Some(fc) => match actual.children.clone().first().cloned() { + Some(ac) => { + let __tco_0 = fc.clone(); + let __tco_1 = ac.clone(); + let __tco_2 = generic_names; + let __tco_3 = source_indices; + let __tco_4 = acc; + __tco_loop_formal = __tco_0; + __tco_loop_actual = __tco_1; + __tco_loop_generic_names = __tco_2; + __tco_loop_source_indices = __tco_3; + __tco_loop_acc = __tco_4; + continue; + } + std::option::Option::None => { + break acc.clone(); + } + }, std::option::Option::None => { break acc.clone(); } - }, - std::option::Option::None => { - break acc.clone(); } + } else { + break acc.clone(); } - } else { + } + } + } +} + +pub fn unify_callable_generics( + formal: Rc, + actual: Rc, + generic_names: Rc>, + source_indices: Rc>>, + acc: Rc>>, +) -> Rc>> { + { + let with_params = unify_callable_param_pairs( + formal.params.clone(), + actual.params.clone(), + generic_names.clone(), + source_indices.clone(), + acc.clone(), + ); + match formal.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: formal_ret, .. + }) => match actual.inferred.clone().as_deref().cloned() { + Some(InferredNode::Resolved { + node: actual_ret, .. + }) => unify_generics( + formal_ret.clone(), + actual_ret.clone(), + generic_names.clone(), + source_indices.clone(), + with_params.clone(), + ), + _ => with_params.clone(), + }, + _ => with_params.clone(), + } + } +} + +pub fn lambda_callable_type(lambda: Rc) -> Rc { + crate::v1_compiler_infer_types::make_callable_type( + Rc::new( + lambda + .children + .clone() + .iter() + .cloned() + .skip(1 as usize) + .collect::>(), + ), + crate::v1_compiler_infer_types::resolved_type(lambda.clone()), + ) +} + +pub fn unify_callable_param_pairs( + mut __tco_loop_formals: Rc>>, + mut __tco_loop_actuals: Rc>>, + mut __tco_loop_generic_names: Rc>, + mut __tco_loop_source_indices: Rc>>, + mut __tco_loop_acc: Rc>>, +) -> Rc>> { + loop { + #[allow(unused_mut)] + let mut formals = __tco_loop_formals; + #[allow(unused_mut)] + let mut actuals = __tco_loop_actuals; + #[allow(unused_mut)] + let mut generic_names = __tco_loop_generic_names; + #[allow(unused_mut)] + let mut source_indices = __tco_loop_source_indices; + #[allow(unused_mut)] + let mut acc = __tco_loop_acc; + match formals.clone().first().cloned() { + Some(f) => match actuals.clone().first().cloned() { + Some(a) => { + let __tco_0 = + Rc::new(formals.iter().cloned().skip(1 as usize).collect::>()); + let __tco_1 = + Rc::new(actuals.iter().cloned().skip(1 as usize).collect::>()); + let __tco_2 = generic_names.clone(); + let __tco_3 = source_indices.clone(); + let __tco_4 = unify_generics( + crate::v1_compiler_infer_types::child_type_node(f.clone()), + crate::v1_compiler_infer_types::child_type_node(a.clone()), + generic_names.clone(), + source_indices.clone(), + acc, + ); + __tco_loop_formals = __tco_0; + __tco_loop_actuals = __tco_1; + __tco_loop_generic_names = __tco_2; + __tco_loop_source_indices = __tco_3; + __tco_loop_acc = __tco_4; + continue; + } + std::option::Option::None => { + break acc.clone(); + } + }, + std::option::Option::None => { break acc.clone(); } } } } +pub fn unify_lambda_solves( + solved: Rc>>, + generic_names: Rc>, + acc: Rc>>, +) -> Rc>> { + generic_names.iter().cloned().fold( + acc.clone(), + |st: Rc>>, g: String| match v1_rt::map_get(&solved, g.clone()) { + Some(candidate) => { + if unify_binding_is_uninformative(candidate.clone()) { + st.clone() + } else { + match v1_rt::map_get(&st, g.clone()) { + std::option::Option::None => { + v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) + } + Some(existing) => { + if unify_binding_is_placeholder(existing.clone()) { + v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) + } else { + st.clone() + } + } + } + } + } + std::option::Option::None => st.clone(), + }, + ) +} + +pub fn unify_binding_is_uninformative(mut __tco_loop_n: Rc) -> bool { + loop { + #[allow(unused_mut)] + let mut n = __tco_loop_n; + match n.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: _, .. }) => { + break true; + } + _ => { + if ((n.children.clone().len() as i64) == 1) { + match n.children.clone().first().cloned() { + Some(c) => { + let __tco_0 = + crate::v1_compiler_infer_types::child_type_node(c.clone()); + __tco_loop_n = __tco_0; + continue; + } + std::option::Option::None => { + break false; + } + } + } else { + break false; + } + } + } + } +} + +pub fn empty_list_element_variable_id() -> String { + thread_local! { + static CACHED: String = { + "empty_list_element".to_string() + }; + } + CACHED.with(|c: &String| c.clone()) +} + +pub fn unify_binding_is_placeholder(mut __tco_loop_n: Rc) -> bool { + loop { + #[allow(unused_mut)] + let mut n = __tco_loop_n; + match n.inferred.clone().as_deref().cloned() { + Some(InferredNode::TypeVariable { id: tv, .. }) => { + break (tv.clone() == empty_list_element_variable_id()); + } + _ => { + if ((n.children.clone().len() as i64) == 1) { + match n.children.clone().first().cloned() { + Some(c) => { + let __tco_0 = + crate::v1_compiler_infer_types::child_type_node(c.clone()); + __tco_loop_n = __tco_0; + continue; + } + std::option::Option::None => { + break false; + } + } + } else { + break false; + } + } + } + } +} + pub fn should_unify_record_lit_generics( formal: Rc, arg_expr: Rc, From f84c29d54cf68e6bdcc2f0b4c0e0136737c5dbe8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 15:55:25 +0000 Subject: [PATCH 6/7] Drop the empty-literal placeholder rule (no measurable effect); enroll the lambda-return witness: three reds and an accepted control (review 76646). Mirror pending regen Co-Authored-By: Claude Opus 5.5 (1M context) --- ...bda_return_solves_generic_witness_test.dag | 38 +++++++++++++++++++ src/v1/04_infer.dag | 37 ++++-------------- 2 files changed, 45 insertions(+), 30 deletions(-) create mode 100644 dag/test/claim/lambda_return_solves_generic_witness_test.dag diff --git a/dag/test/claim/lambda_return_solves_generic_witness_test.dag b/dag/test/claim/lambda_return_solves_generic_witness_test.dag new file mode 100644 index 00000000000..03941d396ab --- /dev/null +++ b/dag/test/claim/lambda_return_solves_generic_witness_test.dag @@ -0,0 +1,38 @@ +module test.claim.lambda_return_solves_generic_witness_test + +import std.types { Bool, Int, String } +import gunbc.compile_census_probe { blocking_class_count_for, total_blocking_count_for } + +// THE EXECUTING EVIDENCE for the lambda-return member of gunbc.recurring_failure_mode +// unbound_generic_reaches_conformance_unjudged, closed by solving a generic from a lambda +// argument's return (v1.compiler.infer infer_call_arguments_generic_pass, lambda_callable_type, +// unify_callable_generics). Before that, each red source below was Accepted with zero blocking +// diagnostics: R stayed unbound and the wrong value reached a Bool position unjudged. The reds +// assert the refusal on the real acceptance path; the control asserts that the same calls at +// the type the lambda actually returns are still accepted, so a compiler that refused every +// lambda-fed generic would fail it. Both helpers return -1 when the census cannot run, so a +// broken harness fails the reds (>= 1) and the control (== 0) alike. + +data lambda_return_into_argument_source: String = "module test.claim.lrs_into_argument\nimport std.types { Bool, Int }\nfn lrs_idf(f: fn() -> R) -> R { f() }\nfn lrs_take(b: Bool) -> Bool { b }\nfn probe() -> Bool { lrs_take(b: lrs_idf(f: fn() { 5 })) }\n" + +data lambda_return_into_declared_return_source: String = "module test.claim.lrs_into_declared_return\nimport std.types { Bool, Int }\nfn lrs_idf(f: fn() -> R) -> R { f() }\nfn probe() -> Bool { lrs_idf(f: fn() { 5 }) }\n" + +data lambda_return_after_its_argument_source: String = "module test.claim.lrs_after_argument\nimport std.types { Bool, Int }\nfn lrs_app(x: T, f: fn(T) -> R) -> R { f(x) }\nfn lrs_take(b: Bool) -> Bool { b }\nfn probe() -> Bool { lrs_take(b: lrs_app(x: 1, f: fn(v) { v })) }\n" + +data lambda_return_at_its_own_type_source: String = "module test.claim.lrs_own_type\nimport std.types { Int }\nfn lrs_idf(f: fn() -> R) -> R { f() }\nfn lrs_app(x: T, f: fn(T) -> R) -> R { f(x) }\nfn probe() -> Int { lrs_idf(f: fn() { 5 }) }\nfn probe_after() -> Int { lrs_app(x: 1, f: fn(v) { v }) }\n" + +test fn a_generic_fixed_by_a_lambda_return_refuses_a_wrong_argument_position() -> Bool { + blocking_class_count_for(source: lambda_return_into_argument_source, wanted_class: "TypeMismatch") >= 1 +} + +test fn a_generic_fixed_by_a_lambda_return_refuses_a_wrong_declared_return() -> Bool { + blocking_class_count_for(source: lambda_return_into_declared_return_source, wanted_class: "TypeMismatch") >= 1 +} + +test fn a_lambda_after_the_argument_that_fixes_its_parameter_solves_the_result() -> Bool { + blocking_class_count_for(source: lambda_return_after_its_argument_source, wanted_class: "TypeMismatch") >= 1 +} + +test fn the_same_calls_at_the_type_the_lambda_returns_are_accepted() -> Bool { + total_blocking_count_for(source: lambda_return_at_its_own_type_source) == 0 +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index b9c65f0b680..a795de05852 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -7597,12 +7597,12 @@ fn is_lambda_expr(e: Node) -> Bool { // binding derivable in one forward pass regardless of authored order. Re-running is // sound rather than merely convenient because the substitution is a fixed point of the // second round: a lambda argument contributes to the substitution in ROUND 1 ONLY -// (unify_lambda_solves), and only informative bindings that solve an Absent slot or the -// minted empty-literal placeholder; in round 2 lambdas are skipped, so deferring what they +// (unify_lambda_solves), and only informative bindings that fill an Absent slot; in +// round 2 lambdas are skipped, so deferring what they // would contribute cannot change the result, and a formal whose generic slot is already // bound is substituted to a concrete node that unify_generics no longer binds. // The narrowing this note used to state -- a binding derivable only from a lambda's -// return, such as fold_list's accumulator when `empty` is an empty literal -- is LIFTED by +// return -- is LIFTED by // that round-1 contribution (unify_callable_generics unifies the callable's params and // return). It stays bounded at two rounds: a round-2 return is not fed back again, and a // return that depends on a binding only round 2 supplies contributes nothing. @@ -9487,7 +9487,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu Absent => unit_type } } else { unit_type } - Absent => type_variable_node(id: empty_list_element_variable_id) + Absent => type_variable_node(id: "empty_list_element") } } } @@ -13688,10 +13688,7 @@ fn unify_generics(formal: Node, actual: Node, generic_names: List, sourc match map_get(acc, bind_name) { Absent => map_insert(acc, bind_name, actual) - Present { value: existing } => - if unify_binding_is_placeholder(n: existing) && !unify_binding_is_placeholder(n: actual) { - map_insert(acc, bind_name, actual) - } else { acc } + Present { value: _ } => acc } } else if (formal.connective == Arrow && actual.connective == Arrow) { unify_callable_generics(formal: formal, actual: actual, generic_names: generic_names, source_indices: source_indices, acc: acc) @@ -13751,7 +13748,7 @@ fn unify_callable_param_pairs(formals: List, actuals: List, generic_ // return is computed under a substitution that may not yet bind its own parameters, so it can be // an unresolved type variable (callable_param), and binding a parameter to that would fix it first // and keep it against the informative argument that follows. Such an entry is dropped, so a later -// argument or round 2 decides it. An entry solves only an Absent binding or the minted placeholder. +// argument or round 2 decides it. An entry fills only an Absent binding; it never overrides one. fn unify_lambda_solves(solved: Map, generic_names: List, acc: Map) -> Map { fold(generic_names, init: acc, f: (st, g) => match map_get(solved, g) { @@ -13761,7 +13758,7 @@ fn unify_lambda_solves(solved: Map, generic_names: List, a } else { match map_get(st, g) { Absent => map_insert(st, g, candidate) - Present { value: existing } => if unify_binding_is_placeholder(n: existing) { map_insert(st, g, candidate) } else { st } + Present { value: _ } => st } } Absent => st @@ -13783,26 +13780,6 @@ fn unify_binding_is_uninformative(n: Node) -> Bool { } } -// The type variable an empty list literal with no expected type mints for its element: one -// authority for the mint in infer_expr ExprListLit and the check in unify_binding_is_placeholder. -data empty_list_element_variable_id: String = "empty_list_element" - -// That placeholder is an unsolved variable, not a binding: it carries no information about the -// parameter, so a later informative actual solves it. Only the minted placeholder yields; a type -// parameter in scope is a TypeVariable too and is information, so it never yields. -fn unify_binding_is_placeholder(n: Node) -> Bool { - match n.inferred { - Present { value: TypeVariable { id: tv } } => tv == empty_list_element_variable_id - _ => - if n.children |> count == 1 { - match n.children |> first { - Present { value: c } => unify_binding_is_placeholder(n: child_type_node(ch: c)) - Absent => false - } - } else { false } - } -} - fn should_unify_record_lit_generics(formal: Node, arg_expr: Node, generic_names: List, source_indices: Map) -> Bool { match record_lit_expr_optional(expr: arg_expr) { Absent => false From c431ac6ec0f331af8771f694178234adb51bfc43 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 5 Oct 2026 18:17:27 +0000 Subject: [PATCH 7/7] Witness: round-2 mismatch control and the p7b two-round boundary pin; the class row's trigger names p7b as the wall's discriminating member and p8/p8b/p9 as closure controls; regenerate the infer mirror (fresh checkout: round 2 first_generation_equal=true, rebuild_packages=0) Co-Authored-By: Claude Opus 5.5 (1M context) --- ...d_generic_reaches_conformance_unjudged.dag | 2 +- ...bda_return_solves_generic_witness_test.dag | 22 +++++++ src/v1/stage0/src/v1_compiler_infer.rs | 58 ++----------------- 3 files changed, 27 insertions(+), 55 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag b/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag index b530d1b7d22..c8e917b8742 100644 --- a/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag +++ b/dag/gunbc/recurring_failure_mode/unbound_generic_reaches_conformance_unjudged.dag @@ -25,7 +25,7 @@ data unbound_generic_reaches_conformance_unjudged: RecurringFailureMode = Recurr "PARTIAL CLOSURE, gunbc#13418: the LAMBDA-RETURN member closes. A generic fixed only by a lambda argument's return is now solved from it (v1.compiler.infer infer_call_arguments_generic_pass, lambda_callable_type and unify_callable_generics), so p8, p8b and p9 REFUSE `expected Primitive(String), got Primitive(Int)` at the located position instead of being Accepted. p7b STAYS OPEN: its lambda comes BEFORE the argument that fixes T, so in round 1 the lambda's return is still the unresolved callable_param and is dropped, round 2 contributes nothing, and R stays unbound and passes conformance unjudged. That is the stated two-round bound, and this row's wall (refuse an unresolved generic at a declared-type position) is what closes it, not more rounds.", - "RUNG FOUND AT: below the floor (silent acceptance). CEILING: 3 -- an unresolved type parameter at a declared-type position is a modeled state, decidable at the conformance site. NEXT TRIGGER: a call whose result type is an unresolved generic parameter, reaching a declared-type position, refuses with a typed located 'cannot infer here; annotate' diagnostic. Evidence: p8, p8b and p7b refuse with that cause; `apply2(f: fn(v) { v }, x: 1)` under a declared -> Int is the accepted control. That wall refuses some code main accepts today, by design, and lands as its own step with its own census of the sites that newly refuse.", + "RUNG FOUND AT: below the floor (silent acceptance). CEILING: 3 -- an unresolved type parameter at a declared-type position is a modeled state, decidable at the conformance site. NEXT TRIGGER: a call whose result type is an unresolved generic parameter, reaching a declared-type position, refuses with a typed located 'cannot infer here; annotate' diagnostic. Evidence: p7b, the lambda before the argument that fixes its parameter, refuses with that cause; it is the wall's discriminating member, enrolled today as the boundary pin in test.claim.lambda_return_solves_generic_witness_test. `apply2(f: fn(v) { v }, x: 1)` under a declared -> Int is the accepted control. p8, p8b and p9 are no longer members: since gunbc#13418 they refuse the concrete Int-vs-String mismatch, and they stay enrolled in that witness as closure controls. That wall refuses some code main accepts today, by design, and lands as its own step with its own census of the sites that newly refuse.", ], evidence: [], diff --git a/dag/test/claim/lambda_return_solves_generic_witness_test.dag b/dag/test/claim/lambda_return_solves_generic_witness_test.dag index 03941d396ab..e5acd0c65ce 100644 --- a/dag/test/claim/lambda_return_solves_generic_witness_test.dag +++ b/dag/test/claim/lambda_return_solves_generic_witness_test.dag @@ -36,3 +36,25 @@ test fn a_lambda_after_the_argument_that_fixes_its_parameter_solves_the_result() test fn the_same_calls_at_the_type_the_lambda_returns_are_accepted() -> Bool { total_blocking_count_for(source: lambda_return_at_its_own_type_source) == 0 } + +// THE ROUND-2 MISMATCH IS ALREADY JUDGED, AND THIS PINS IT. R is fixed by `r: true`, so the +// lambda is inferred against the substituted callable fn(Int) -> Bool and its Int return is a +// located mismatch. This held before the lambda-return solve and must keep holding beside it. +data lambda_return_disagrees_with_a_fixed_parameter_source: String = "module test.claim.lrs_round_two_mismatch\nimport std.types { Bool, Int }\nfn lrs_ap(f: fn(T) -> R, x: T, r: R) -> R { r }\nfn probe() -> Bool { lrs_ap(f: fn(v) { v }, x: 1, r: true) }\n" + +// THE TWO-ROUND BOUNDARY, PINNED AS WHAT IT IS. The lambda comes BEFORE the argument that fixes +// T, so in round 1 its return is the unresolved callable_param and is not bound, round 2 does not +// contribute, and R reaches the Bool position unsolved and unjudged: Accepted with zero blocking. +// That is the open member of gunbc.recurring_failure_mode unbound_generic_reaches_conformance_unjudged, +// whose wall (refuse an unresolved generic at a declared-type position) closes it. This test is +// EXPECTED to go red when that wall lands, and is then rewritten to assert the refusal: it pins the +// boundary so that neither a wider bound nor the wall can arrive unannounced. +data lambda_before_the_fixing_argument_source: String = "module test.claim.lrs_two_round_boundary\nimport std.types { Bool, Int }\nfn lrs_apply2(f: fn(T) -> R, x: T) -> R { f(x) }\nfn lrs_take(b: Bool) -> Bool { b }\nfn probe() -> Bool { lrs_take(b: lrs_apply2(f: fn(v) { v }, x: 1)) }\n" + +test fn a_lambda_return_that_disagrees_with_a_fixed_parameter_refuses() -> Bool { + blocking_class_count_for(source: lambda_return_disagrees_with_a_fixed_parameter_source, wanted_class: "TypeMismatch") >= 1 +} + +test fn a_lambda_before_the_argument_that_fixes_its_parameter_stays_unsolved_at_the_two_round_bound() -> Bool { + total_blocking_count_for(source: lambda_before_the_fixing_argument_source) == 0 +} diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 1049cf79e6a..0745da949e0 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -15009,7 +15009,7 @@ crate::v1_compiler_infer_types::resolve_type_variables_from_template(t.clone(), } } std::option::Option::None => { - type_variable_node(empty_list_element_variable_id()) + type_variable_node("empty_list_element".to_string()) } } } @@ -23670,14 +23670,8 @@ pub fn unify_generics( std::option::Option::None => { break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); } - Some(existing) => { - if (unify_binding_is_placeholder(existing.clone()) - && !unify_binding_is_placeholder(actual.clone())) - { - break v1_rt::rc_map_insert(acc.clone(), bind_name.clone(), actual.clone()); - } else { - break acc.clone(); - } + Some(_) => { + break acc.clone(); } } } else { @@ -23844,13 +23838,7 @@ pub fn unify_lambda_solves( std::option::Option::None => { v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) } - Some(existing) => { - if unify_binding_is_placeholder(existing.clone()) { - v1_rt::rc_map_insert(st.clone(), g.clone(), candidate.clone()) - } else { - st.clone() - } - } + Some(_) => st.clone(), } } } @@ -23888,44 +23876,6 @@ pub fn unify_binding_is_uninformative(mut __tco_loop_n: Rc) -> bool { } } -pub fn empty_list_element_variable_id() -> String { - thread_local! { - static CACHED: String = { - "empty_list_element".to_string() - }; - } - CACHED.with(|c: &String| c.clone()) -} - -pub fn unify_binding_is_placeholder(mut __tco_loop_n: Rc) -> bool { - loop { - #[allow(unused_mut)] - let mut n = __tco_loop_n; - match n.inferred.clone().as_deref().cloned() { - Some(InferredNode::TypeVariable { id: tv, .. }) => { - break (tv.clone() == empty_list_element_variable_id()); - } - _ => { - if ((n.children.clone().len() as i64) == 1) { - match n.children.clone().first().cloned() { - Some(c) => { - let __tco_0 = - crate::v1_compiler_infer_types::child_type_node(c.clone()); - __tco_loop_n = __tco_0; - continue; - } - std::option::Option::None => { - break false; - } - } - } else { - break false; - } - } - } - } -} - pub fn should_unify_record_lit_generics( formal: Rc, arg_expr: Rc,