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..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 @@ -23,7 +23,9 @@ 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.", - "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.", + "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: 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 new file mode 100644 index 00000000000..e5acd0c65ce --- /dev/null +++ b/dag/test/claim/lambda_return_solves_generic_witness_test.dag @@ -0,0 +1,60 @@ +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 +} + +// 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/04_infer.dag b/src/v1/04_infer.dag index 65685e1b258..a795de05852 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 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 -- 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))) } @@ -7762,8 +7771,16 @@ fn infer_call_arguments_generic_pass(call_args: List, value_params: List, sourc Absent => map_insert(acc, bind_name, actual) 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) } else if formal.children |> count == 1 && actual.children |> count == 1 { match formal.children |> first { Present { value: fc } => @@ -13685,6 +13704,82 @@ 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 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) { + 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: _ } => 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 } + } +} + 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 diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 1bafe0dd5d2..0745da949e0 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 { @@ -23659,39 +23675,207 @@ pub fn unify_generics( } } } 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(_) => 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 should_unify_record_lit_generics( formal: Rc, arg_expr: Rc,