v1 infer: a function value is judged against a declared function type (arrow arm)

dag/gunbc/recurring_failure_mode/function_typed_argument_mismatch_accepted.dag

@@ -20,12 +20,33 @@ data function_typed_argument_mismatch_accepted: RecurringFailureMode = Recurring
 
     "RUNG FOUND AT: below the ladder (silent wrongness).",
 
+    "A SECOND SPECIMEN, AND A CORRECTION TO HOW IT WAS REPORTED. eager-pike-297, repairing gunbc#12130, found `apply(f: convert)` accepted with `fn apply(f: fn(Int) -> Int)` and `fn convert(s: String) -> String`, and reported that the annotated-let form `let g: fn(Int) -> Int = convert` WAS refused. Executed against the seed at `7caa4c9b092`, it was not: both compiled with zero blocking rows. The declared-type relation `declared_type_conformance_diags` judged only ground kernel scalars and element collections, so no position compared two arrows.",
+
+    "A THIRD FACT FOUND WHILE REPAIRING THE NULLARY ARITY: a bare nullary function name is read as a CALL. `apply(f: seven)` with `fn seven() -> Int` was inferred as `apply(f: seven())`, typing the argument as the RETURN, so the matching nullary case was not correct either -- the Rust emitter wrote `apply(seven())` into an `Rc<dyn Fn() -> i64>` slot. The mismatching nullary specimen (`fn pick() -> String` at `fn() -> Int`) was therefore a one-sided case, a String at a function boundary, not an arrow pair.",
+
+    "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.",
+
+    "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.",
+
+    "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.",
+
     "CEILING: 3, structurally guaranteed -- arrow inhabitance (parameter count, parameter and return types) is decidable from the modeled types.",
 
-    "NEXT-RUNG TRIGGER, named as the capability: a declared-type judgment for function types at every site `type_node_is_callable` exempts, sufficient that each specimen above refuses located, with a passed function of matching arrow type as its accepted positive control.",
+    "NEXT-RUNG TRIGGER, named as the capability: the same judgment consulted at the record-literal field seam and the method/pipe argument seam, and a peeling conformance relation that grounds brands and nominal identities so arrow leaves of those kinds are judged -- sufficient that the record-field specimen above refuses located with a matching-arrow field as its control.",
   ],
 
   evidence: [
     DeclarationRef { module_path: "v1.compiler.infer", decl_name: "type_node_is_callable", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "callable_signature_mismatch", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "one_sided_callable_mismatch", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "expected_type_is_arrow", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "expression_value_type", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer", decl_name: "type_node_is_arrow", field: WholeDeclaration },
+    DeclarationRef { module_path: "v1.compiler.infer_types", decl_name: "unify_template", field: WholeDeclaration },
+    DeclarationRef { module_path: "test.claim.infer_function_value_argument_arrow_witness_test", decl_name: "polymorphic_repeated_variable_mismatch_refuses", field: WholeDeclaration },
   ],
 }

dag/test/claim/infer_function_value_argument_arrow_witness_test.dag

@@ -0,0 +1,123 @@
+module test.claim.infer_function_value_argument_arrow_witness_test
+
+import std.types { Bool, Int, String }
+import gunbc.compile_census_probe { total_blocking_count_for, any_class_count_for }
+
+// THE EXECUTING EVIDENCE FOR gunbc.recurring_failure_mode function_typed_argument_mismatch_accepted,
+// for the population gunbc#12143 repaired.
+//
+// Every cell is a source string compiled by the seed through gunbc.compile_census_probe. Each
+// `_refuses` cell is a program the seed accepted before the repair; each `_accepted` cell is a
+// control the repair must not refuse. They are paired by wall: exact arrow comparison (parameter,
+// arity, return, annotated let), the nullary arity (a mismatching nullary function refuses in both
+// positions, a matching one is accepted as a function value), polymorphism (one substitution over
+// the whole arrow: a repeated variable must agree, distinct variables need not), the one-sided
+// cases in both directions, and depth (a ground mismatch nested nine arrows deep refuses, where a
+// depth cutoff answering `false` would accept it; the identical matching nesting is accepted).
+
+data 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: convert) }\n"
+
+data mismatched_arity_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn add(x: Int, y: Int) -> Int { x + y }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int { apply(f: add) }\n"
+
+data mismatched_return_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn show(x: Int) -> String { \"n\" }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int { apply(f: show) }\n"
+
+data mismatched_let_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn convert(s: String) -> String { s }\nfn host() -> Int {\n  let g: fn(Int) -> Int = convert\n  g(1)\n}\n"
+
+data nullary_mismatch_direct_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn pick() -> String { \"a\" }\nfn apply(f: fn() -> Int) -> Int { f() }\nfn host() -> Int { apply(f: pick) }\n"
+
+data nullary_mismatch_let_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn pick() -> String { \"a\" }\nfn host() -> Int {\n  let g: fn() -> Int = pick\n  g()\n}\n"
+
+data polymorphic_repeated_variable_mismatch_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn same<T>(x: T, y: T) -> T { x }\nfn apply(f: fn(Int, String) -> Int) -> Int { 0 }\nfn host() -> Int { apply(f: same) }\n"
+
+data polymorphic_return_variable_mismatch_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn same<T>(x: T) -> T { x }\nfn apply(f: fn(Int) -> String) -> Int { 0 }\nfn host() -> Int { apply(f: same) }\n"
+
+data non_function_value_at_function_formal_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 { apply(f: 7) }\n"
+
+data function_value_at_kernel_formal_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn inc(x: Int) -> Int { x + 1 }\nfn take(n: Int) -> Int { n }\nfn host() -> Int { take(n: inc) }\n"
+
+data deep_nested_ground_mismatch_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn deep(g: fn(fn(fn(fn(fn(fn(fn(fn(fn(String) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int { 0 }\nfn apply(f: fn(fn(fn(fn(fn(fn(fn(fn(fn(fn(Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int { 0 }\nfn host() -> Int { apply(f: deep) }\n"
+
+data matching_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn inc(x: Int) -> Int { x + 1 }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int { apply(f: inc) }\n"
+
+data nullary_matching_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn seven() -> Int { 7 }\nfn apply(f: fn() -> Int) -> Int { f() }\nfn host() -> Int { apply(f: seven) }\n"
+
+data polymorphic_identity_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn ident<T>(x: T) -> T { x }\nfn apply(f: fn(Int) -> Int) -> Int { f(1) }\nfn host() -> Int { apply(f: ident) }\n"
+
+data polymorphic_two_variables_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn pair<T, U>(x: T, y: U) -> T { x }\nfn apply(f: fn(Int, String) -> Int) -> Int { 0 }\nfn host() -> Int { apply(f: pair) }\n"
+
+data lambda_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 { apply(f: x => x + 1) }\n"
+
+data deep_nested_matching_source: String = "module test.claim.tmp_fn_value_arrow_probe\nimport std.types { Int, String }\nfn deep(g: fn(fn(fn(fn(fn(fn(fn(fn(fn(Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int { 0 }\nfn apply(f: fn(fn(fn(fn(fn(fn(fn(fn(fn(fn(Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int) -> Int { 0 }\nfn host() -> Int { apply(f: deep) }\n"
+
+
+fn refuses_as_type_mismatch(source: String) -> Bool {
+  any_class_count_for(source: source, wanted_class: "TypeMismatch") > 0
+}
+
+test fn mismatched_parameter_refuses() -> Bool {
+  refuses_as_type_mismatch(source: mismatched_parameter_source)
+}
+
+test fn mismatched_arity_refuses() -> Bool {
+  refuses_as_type_mismatch(source: mismatched_arity_source)
+}
+
+test fn mismatched_return_refuses() -> Bool {
+  refuses_as_type_mismatch(source: mismatched_return_source)
+}
+
+test fn mismatched_let_refuses() -> Bool {
+  refuses_as_type_mismatch(source: mismatched_let_source)
+}
+
+test fn nullary_mismatch_direct_refuses() -> Bool {
+  refuses_as_type_mismatch(source: nullary_mismatch_direct_source)
+}
+
+test fn nullary_mismatch_let_refuses() -> Bool {
+  refuses_as_type_mismatch(source: nullary_mismatch_let_source)
+}
+
+test fn polymorphic_repeated_variable_mismatch_refuses() -> Bool {
+  refuses_as_type_mismatch(source: polymorphic_repeated_variable_mismatch_source)
+}
+
+test fn polymorphic_return_variable_mismatch_refuses() -> Bool {
+  refuses_as_type_mismatch(source: polymorphic_return_variable_mismatch_source)
+}
+
+test fn non_function_value_at_function_formal_refuses() -> Bool {
+  refuses_as_type_mismatch(source: non_function_value_at_function_formal_source)
+}
+
+test fn function_value_at_kernel_formal_refuses() -> Bool {
+  refuses_as_type_mismatch(source: function_value_at_kernel_formal_source)
+}
+
+test fn deep_nested_ground_mismatch_refuses() -> Bool {
+  refuses_as_type_mismatch(source: deep_nested_ground_mismatch_source)
+}
+
+test fn matching_accepted() -> Bool {
+  total_blocking_count_for(source: matching_source) == 0
+}
+
+test fn nullary_matching_accepted() -> Bool {
+  total_blocking_count_for(source: nullary_matching_source) == 0
+}
+
+test fn polymorphic_identity_accepted() -> Bool {
+  total_blocking_count_for(source: polymorphic_identity_source) == 0
+}
+
+test fn polymorphic_two_variables_accepted() -> Bool {
+  total_blocking_count_for(source: polymorphic_two_variables_source) == 0
+}
+
+test fn lambda_accepted() -> Bool {
+  total_blocking_count_for(source: lambda_source) == 0
+}
+
+test fn deep_nested_matching_accepted() -> Bool {
+  total_blocking_count_for(source: deep_nested_matching_source) == 0
+}