Type a let-bound lambda at its arrow; bind a CallableOf return to an arrow's return (#12143 items 5+6)

dag/gunbc/recurring_failure_mode/function_typed_argument_mismatch_accepted.dag

@@ -26,11 +26,11 @@ data function_typed_argument_mismatch_accepted: RecurringFailureMode = Recurring
 
     "REPAIRED BY gunbc#12143, at the direct-call argument position (`v1.compiler.infer` `direct_call_arg_type_mismatch`) and at every position `declared_type_conformance_diags` serves (an annotated `let`, a fn body against its declared return, an early `return`, a `data` annotation): (a) ARROW PAIRS through `callable_signature_mismatch` -- arity must agree, and parameters and return are compared EXACTLY (the language has no subtype relation, so no variance is modeled); a leaf refuses where both sides are ground and `node_type_compatible` denies them, and a nested arrow is compared recursively with no depth cutoff, the walk being bounded by the finite acyclic Node it is handed. (b) POLYMORPHIC ACTUALS through ONE substitution over the whole arrow: the actual's generic declarations bind at their first occurrence by `unify_generics` and every later occurrence, return included, must agree, so `same<T>(x: T, y: T) -> T` refuses at `fn(Int, String) -> Int` and at `fn(Int) -> String`, while `ident<T>` at `fn(Int) -> Int` and `pair<T, U>` at `fn(Int, String) -> Int` are accepted. (c) ONE-SIDED CASES through `one_sided_callable_mismatch` -- a value that is positively not a function (a ground kernel type, or a name resolving to a product or coproduct) at a function boundary, and a function value at such a boundary. (d) NULLARY VALUES: `expected_type_is_arrow` makes a bare nullary name a function value where an arrow is expected, minted from its signature as a unary one is, instead of applying it. (e) LAMBDAS: a lambda expression is declaration-shaped -- its parameters are its children after the body and its `inferred` is its BODY type -- so `expression_value_type` mints its arrow at every position that judges a produced expression. (f) CALLABILITY BY THE ARROW, NOT BY `params`: `type_node_is_callable` also answers true for a generic TYPE declaration, which carries its type parameters in `params`, and the one-sided arm asked of it refused eight correct corpus sites (a `List<String>` at a `List<T>` formal among them); the new relations decide by `type_node_is_arrow`.",
 
-    "A LATENT MIS-INFERENCE THE NEW JUDGMENT SURFACED, NOT REPAIRED HERE AND WHY. `xs |> map(nm)` with `fn nm(p: String) -> String` types its ELEMENTS as the function itself: `v1.compiler.infer_types` `unify_template` binds a `CallableOf` return variable to the whole argument type -- right for a lambda, which is typed as its body, wrong for a named function value, which is typed as its arrow. An intermediate state of gunbc#12143 that judged LOCAL values one-sided refused a correct use of such a list in `v1.compiler.emit_rust` `emit_lib_rs_from_paths` (the lambda parameter `n` arrived typed as the function). A one-line repair at unify_template was written and then withdrawn: once locals are not judged (remaining population (6) below), no refusal observes the element type -- a generic `T` bound from the list reads it through child_type_node, which collapses an arrow to its return -- so the repair had no discriminating RED and would have landed as unevidenced. It is a separate class (method-callback return inference), recorded here with its trigger: typing let-bound lambdas at their arrow, which re-admits locals to the one-sided arm and makes the emit_lib_rs_from_paths site the discriminating RED.",
+    "METHOD-CALLBACK RETURN INFERENCE, repaired with its trigger (gunbc#12143 open items 5 and 6). `xs |> map(nm)` with `fn nm(p: String) -> String` typed its ELEMENTS as the function itself: `v1.compiler.infer_types` `unify_template` bound a `CallableOf` return variable to the whole argument type -- right for a lambda, typed as its body, wrong for a function value, typed as its arrow. It had no discriminating RED while locals were unjudged; typing an unannotated let-bound lambda at its arrow (`v1.compiler.infer` ExprLet binds at `expression_value_type`) re-admits locals to the one-sided arm, so both land together: `unify_template` reads an arrow argument at its return. Its discriminating RED is `map_named_function_wrong_elements_refuses` (a `List<Int>` bound from `xs |> map(nm)` with `nm` returning String, accepted before the repair because the elements were the arrow and went unjudged); `map_named_function_elements_accepted` and `map_local_lambda_elements_accepted` are its controls, and the gen-2 regen compiles `v1.compiler.emit_rust` `emit_lib_rs_from_paths` with no refusal.",
 
     "EXECUTED EVIDENCE, named rather than transcribed: `test.claim.infer_function_value_argument_arrow_witness_test`, admitted to the required floor by the `test.claim.infer_` prefix. Its RED cells -- parameter, arity, return, annotated let, nullary direct and let, both polymorphic mismatches, both one-sided directions, and a ground mismatch nested past depth eight -- refuse; its matching unary, matching nullary, `ident`, `pair`, lambda and deep matching cells are the accepted controls.",
 
-    "RUNG NOW, FOR THE CLASS: still below the ladder (silent wrongness), because a class rung is the minimum across its in-scope paths (DESIGN section 4b(1)) and paths (1), (4) and (6) below remain silent. PER PATH, as a path rung and not a class rung: 3, structurally guaranteed, on the direct-call argument path and the annotated-let path for the populations the repair names, and for arrow pairs at the fn-return, early-return and `data` positions. The class climbs to 3 only when every in-scope path does. THE PATHS STILL BELOW THE LADDER, stated rather than implied: (1) the RECORD-FIELD specimen above -- `Cfg { cb: 7 }` against `cb: fn() -> Int` -- is not repaired; record-literal field checks do not consult these relations. (2) An arrow leaf that is a brand, a nominal record or coproduct, or a keyed collection is unjudged by the arrow relation. (3) A one-sided case whose non-function side is a type variable, an unresolved name or an Optional is unjudged. (4) Method and pipe argument positions do not pass through `direct_call_arg_type_mismatch`. (5) A generic FORMAL (`f: fn(T) -> U` inside a generic callee) leaves its type-variable leaves unjudged. (6) A LOCAL VALUE is not judged by the one-sided arm, at either the direct-call or the annotated-let position: an unannotated `let f = fn(x) { .. }` binds its local at the lambda's BODY type, so a local holding a function can arrive typed as `Bool` (measured at `gunbc.primitive_egress.census`, a correct call refused). Its trigger is typing an unannotated let-bound lambda at its arrow. (7) The one-sided arm does not run at the fn-return or `data` positions, whose produced value is a block rather than an expression in hand.",
+    "RUNG NOW, FOR THE CLASS: still below the ladder (silent wrongness), because a class rung is the minimum across its in-scope paths (DESIGN section 4b(1)) and paths (1) and (4) below remain silent. PER PATH, as a path rung and not a class rung: 3, structurally guaranteed, on the direct-call argument path and the annotated-let path for the populations the repair names, and for arrow pairs at the fn-return, early-return and `data` positions. The class climbs to 3 only when every in-scope path does. THE PATHS STILL BELOW THE LADDER, stated rather than implied: (1) the RECORD-FIELD specimen above -- `Cfg { cb: 7 }` against `cb: fn() -> Int` -- is not repaired; record-literal field checks do not consult these relations. (2) An arrow leaf that is a brand, a nominal record or coproduct, or a keyed collection is unjudged by the arrow relation. (3) A one-sided case whose non-function side is a type variable, an unresolved name or an Optional is unjudged. (4) Method and pipe argument positions do not pass through `direct_call_arg_type_mismatch`. (5) A generic FORMAL (`f: fn(T) -> U` inside a generic callee) leaves its type-variable leaves unjudged against an arrow actual; a NON-function actual at such a formal is judged one-sided (`generic_formal_non_function_refuses`), because function-ness is the arrow connective and not its leaves. (6) [REPAIRED] A LOCAL VALUE bound by an unannotated `let f = fn(x) { .. }` is typed at its arrow and judged by the one-sided and arrow-pair arms at both positions (REDs `local_lambda_at_kernel_formal_refuses`, `local_lambda_return_mismatch_refuses`). (7) The one-sided arm does not run at the fn-return or `data` positions, whose produced value is a block rather than an expression in hand.",
 
     "OUTSIDE THIS CLASS, found beside it: a nullary function value, now correctly typed, is still EMITTED to Rust as a bare `seven` where the formal renders `Rc<dyn Fn() -> i64>`, so the emitted crate does not compile (the unary formal renders `impl Fn` and compiles). The interpreter path executes it correctly. That is an emission-realization gap, not a checker gap, and it is reported to the owning lane rather than folded in here.",
 

dag/test/claim/infer_function_value_argument_arrow_witness_test.dag

@@ -59,6 +59,29 @@ data qualified_matching_source: String = "module test.claim.tmp_fn_value_arrow_p
 data qualified_mismatched_parameter_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn convert(s: String) -> String { s }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int { apply(f: test.claim.tmp_fn_value_arrow_probe.convert) }\n"
 
 
+// LET-BOUND LAMBDAS AND METHOD CALLBACKS. An unannotated `let f = fn(x) { .. }` binds its local at
+// the lambda's ARROW, so the one-sided and arrow-pair arms judge a local like any function value;
+// and `xs |> map(nm)` binds the callback's return variable to what a CALL of `nm` produces, not to
+// the arrow itself. The `_local_` REDs were accepted while the local was typed as the lambda's body;
+// the `map_` controls were refused while a function-value callback typed the elements as its arrow.
+
+data local_lambda_at_kernel_formal_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn take(n: Int) -> Int { n }\nfn host() -> Int {\n  let f = fn(x) { 1 }\n  take(n: f)\n}\n"
+
+data local_lambda_return_mismatch_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int {\n  let g = fn(x) { \"s\" }\n  apply(f: g)\n}\n"
+
+data local_lambda_matching_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int {\n  let g = fn(x) { 1 }\n  apply(f: g)\n}\n"
+
+data local_lambda_called_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn host() -> Int {\n  let g = fn(x) { 1 }\n  let n: Int = g(2)\n  n\n}\n"
+
+data map_named_function_elements_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn nm(p: String) -> String { p }\nfn host(xs: List<String>) -> List<String> {\n  let ys: List<String> = xs |> map(nm)\n  ys\n}\n"
+
+data map_local_lambda_elements_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn host(xs: List<String>) -> List<String> {\n  let g = fn(p) { \"a\" }\n  let ys: List<String> = xs |> map(g)\n  ys\n}\n"
+
+data map_named_function_wrong_elements_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn nm(p: String) -> String { p }\nfn host(xs: List<String>) -> List<Int> {\n  let ys: List<Int> = xs |> map(nm)\n  ys\n}\n"
+
+
+data generic_formal_non_function_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn apply<T>(f: fn(T) -> T) -> Int { 0 }\nfn host() -> Int { apply(f: 7) }\n"
+
 fn refuses_as_type_mismatch(source: String) -> Bool {
   any_class_count_for(source: source, wanted_class: "TypeMismatch") > 0
 }
@@ -131,6 +154,38 @@ test fn deep_nested_matching_accepted() -> Bool {
   total_blocking_count_for(source: deep_nested_matching_source) == 0
 }
 
+test fn local_lambda_at_kernel_formal_refuses() -> Bool {
+  refuses_as_type_mismatch(source: local_lambda_at_kernel_formal_source)
+}
+
+test fn local_lambda_return_mismatch_refuses() -> Bool {
+  refuses_as_type_mismatch(source: local_lambda_return_mismatch_source)
+}
+
+test fn map_named_function_wrong_elements_refuses() -> Bool {
+  refuses_as_type_mismatch(source: map_named_function_wrong_elements_source)
+}
+
+test fn local_lambda_matching_accepted() -> Bool {
+  total_blocking_count_for(source: local_lambda_matching_source) == 0
+}
+
+test fn local_lambda_called_accepted() -> Bool {
+  total_blocking_count_for(source: local_lambda_called_source) == 0
+}
+
+test fn map_named_function_elements_accepted() -> Bool {
+  total_blocking_count_for(source: map_named_function_elements_source) == 0
+}
+
+test fn map_local_lambda_elements_accepted() -> Bool {
+  total_blocking_count_for(source: map_local_lambda_elements_source) == 0
+}
+
+test fn generic_formal_non_function_refuses() -> Bool {
+  refuses_as_type_mismatch(source: generic_formal_non_function_source)
+}
+
 test fn qualified_matching_accepted() -> Bool {
   total_blocking_count_for(source: qualified_matching_source) == 0
 }

src/v1/04_infer.dag

@@ -5319,7 +5319,8 @@ fn type_node_positively_not_callable(n: Node, type_env: TypeEnv) -> Bool {
 // formal (dag/std/materialization_ladder.dag first_provider_where callers, the std.algebra
 // fold_list callers). The lambda's value is the arrow over its own parameters and body type, minted
 // by the same constructor a named function value's arrow is. Every other expression's value type is
-// its resolved type.
+// its resolved type. An unannotated `let` binds its local at this value type too, so a let-bound
+// lambda's local is its ARROW and every argument seam judges it like any other function value.
 //
 // A LAMBDA'S PARAMETERS ARE ITS CHILDREN AFTER THE BODY (lambda_body, lambda_param_names_at), each
 // carrying its type in `inferred`, and its `params` is empty -- so the arrow is minted over those
@@ -5352,11 +5353,20 @@ fn lambda_arrow_param(lambda_param: Node) -> Node {
 // an unbound type variable is not established.
 fn one_sided_callable_value_mismatch(declared: Node, produced: Node, type_env: TypeEnv) -> Bool {
   (type_node_is_arrow(n: declared) != type_node_is_arrow(n: produced))
-    && !direct_call_formal_has_unbound_type_variable(n: declared)
-    && !direct_call_formal_has_unbound_type_variable(n: produced)
+    && !one_sided_non_arrow_side_is_open(formal: declared, formal_basis: declared, actual: produced)
     && one_sided_callable_mismatch(formal: declared, actual: produced, type_env: type_env)
 }
 
+// WHETHER A VALUE IS A FUNCTION AT ALL IS THE ARROW CONNECTIVE, NOT THE ARROW'S LEAVES. A lambda
+// with an unannotated parameter (`let f = fn(x) { 1 }`) is an arrow whose parameter is a fresh type
+// variable; that leaf leaves its parameter type open and its function-ness closed, so it cannot hide
+// a function standing where an `Int` is declared. What keeps the one-sided arm from judging is an
+// open NON-arrow side -- a type variable there may yet be a function -- and that case stays unjudged.
+fn one_sided_non_arrow_side_is_open(formal: Node, formal_basis: Node, actual: Node) -> Bool {
+  if type_node_is_arrow(n: formal) { direct_call_formal_has_unbound_type_variable(n: actual) }
+  else { direct_call_formal_has_unbound_type_variable(n: formal_basis) }
+}
+
 fn one_sided_callable_mismatch(formal: Node, actual: Node, type_env: TypeEnv) -> Bool {
   (type_node_is_arrow(n: formal) && type_node_positively_not_callable(n: actual, type_env: type_env))
     || (type_node_is_arrow(n: actual) && type_node_positively_not_callable(n: formal, type_env: type_env))
@@ -5376,28 +5386,6 @@ fn type_node_is_arrow(n: Node) -> Bool {
   n.connective == Arrow
 }
 
-// A LOCAL VALUE'S RECORDED TYPE MAY BE A LAMBDA'S BODY, not its arrow: an unannotated
-// `let on_surface = fn(id) { .. }` binds the local at the lambda's resolved type, which is its body
-// type (expression_value_type states why). So a local passed where a function type is declared can
-// arrive typed as `Bool` while holding a function, and the one-sided arm cannot tell that apart from
-// a genuine Bool. Measured at dag/gunbc/primitive_egress/census.dag, a correct call refused. The arm
-// therefore does not judge a local value; that population is recorded on
-// gunbc.recurring_failure_mode function_typed_argument_mismatch_accepted with its trigger, typing an
-// unannotated let-bound lambda at its arrow.
-fn expression_is_local_value(e: Node) -> Bool {
-  match e.expr_data {
-    ExprVar { binding_kind: kind } => binding_kind_is_local_value(kind: kind)
-    _ => false
-  }
-}
-
-fn binding_kind_is_local_value(kind: VarBindingKind?) -> Bool {
-  match kind {
-    Present { value: LocalValueBinding } => true
-    _ => false
-  }
-}
-
 fn direct_call_arg_type_mismatch(
   formal: Node,
   substitution_basis: Node,
@@ -5413,11 +5401,12 @@ fn direct_call_arg_type_mismatch(
   else if type_node_is_arrow(n: formal) && type_node_is_arrow(n: actual) {
     callable_signature_mismatch(formal: formal, actual: actual, source_indices: source_indices)
   }
-  else if direct_call_formal_has_unbound_type_variable(n: substitution_basis) || direct_call_formal_has_unbound_type_variable(n: actual) { false }
   else if type_node_is_arrow(n: formal) || type_node_is_arrow(n: actual) {
-    one_sided_callable_mismatch(formal: formal, actual: actual, type_env: type_env)
-      && !expression_is_local_value(e: actual_expr)
+    !one_sided_non_arrow_side_is_open(
+      formal: formal, formal_basis: substitution_basis, actual: actual)
+      && one_sided_callable_mismatch(formal: formal, actual: actual, type_env: type_env)
   }
+  else if direct_call_formal_has_unbound_type_variable(n: substitution_basis) || direct_call_formal_has_unbound_type_variable(n: actual) { false }
   else if type_node_is_callable(n: formal) || type_node_is_callable(n: actual) { false }
   else {
     nominal_call_arg_brand_mismatch(formal: formal, actual: actual, type_env: type_env, source_indices: source_indices)
@@ -8291,7 +8280,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu
       }
       let val_result = infer_expr(texpr: val_expr, scope: scope, expected: val_expected)
       let val_typed = val_result.typed
-      let val_type = resolved_type(n: val_typed)
+      let val_type = expression_value_type(e: val_typed)
       let val_annotation_diags = match declared_let_type {
         Present { value: declared } =>
           let produced_value_type = expression_value_type(e: val_typed)
@@ -8301,8 +8290,7 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu
             span: val_expr.span,
             scope: scope)
           if (conformance |> count) > 0 { conformance }
-          else if one_sided_callable_value_mismatch(declared: declared, produced: produced_value_type, type_env: scope.type_env)
-              && !expression_is_local_value(e: val_typed) {
+          else if one_sided_callable_value_mismatch(declared: declared, produced: produced_value_type, type_env: scope.type_env) {
             [type_mismatch_error(
               expected: node_type_shape(n: declared, source_indices: scope.type_env.source_indices),
               got: node_type_shape(n: produced_value_type, source_indices: scope.type_env.source_indices),