Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -28,12 +28,21 @@ data arity_proxy_for_callability_misroutes_a_found_local: RecurringFailureMode =

"WHAT IS NOT CLOSED, and it is a DIFFERENT CLASS sharing this one's fall-through: a body local the seam rejects because it genuinely is not callable is also retried as a global name. `fn host(pick: Int) -> Int { pick() }` still refuses with the same misdirected `function 'pick' not found in scope`, and with a global `fn pick()` beside it the call silently binds past the shadowing parameter. That is filed separately as `gunbc.recurring_failure_mode` `shadowing_body_local_bypassed_by_global_call_fallback`, because its invalid state, harm and recognition rule differ from this row's.",

"RESIDUE ONE LINK EARLIER, 2026-09-25 (a type ARGUMENT, not a binding's own type): a function type written inside a type argument -- `List<fn() -> R>`, `List<fn(Int) -> Int>` -- reached the call seam already stripped of its arrow, so the repaired `type_node_is_callable` was never asked about an Arrow. `v1.compiler.infer_types` `child_type_node` read a child's `inferred` field as the type the child denotes, but an Arrow stores its CODOMAIN there (`make_callable_type`, `parse_callable_type_expr`), so the element of `List<fn() -> Int>` became `Int`. Same harm, same misdirected diagnostic: `function 'r' not found in scope` for a fold or map lambda's parameter and for a match arm over `first`. It broke gunbc-private CI through `extdeps.apple.app_attest` `first_assertion_refusal` (a fold over `List<fn() -> AssertionRefusal?>`) under --target dag; the refusal is raised in inference, so --target rust refused identically, and public CI stayed green only because no required lane compiles that module. The repair is at that earliest boundary: an Arrow child denotes itself. A second candidate -- teaching `type_node_is_established` that a nullary arrow is established -- was built and MEASURED UNNECESSARY once the arrow survived (every specimen green without it), so it was withdrawn rather than shipped as a guard. Executed evidence: `test.claim.infer_callable_type_argument_witness_test` -- three discriminating cells (fold over nullary thunks, map over unary callables, match arm over `first`), each refused by the pre-repair seed, plus a control that an unbound callee inside the same lambda still refuses with that callee as the subject. Corpus sweep for a function type inside a type argument: `extdeps.apple.app_attest` is the only production site; it now compiles clean under --target dag.",

"KEEPING THE ARROW MOVED THE QUESTION DOWNSTREAM, AND THE RELATIONS THERE HAD NEVER BEEN ASKED IT (merge review of gunbc#12295). Once `child_type_node` returned the Arrow, every relation it feeds met a function type where it used to meet the codomain, and none of them read an Arrow's signature -- which lives in params and inferred, never children. `v1.compiler.infer_types` `node_type_equals_core` compared two Arrows as childless structural nodes by the name Callable, so `List<fn() -> Int>` and `List<fn() -> String>` compared EQUAL and `v1.compiler.infer_emit_info` `enum_field_type_consistent` could admit them as one common coproduct field; `node_type_compatible` fell through to name compatibility; `type_resolution_verdict` walked only children, so an Arrow with an unresolved signature read as resolved. And one REFUSAL had been supplied by the erasure itself: a declared `List<fn() -> String>` return given a `List<fn() -> Int>` refused on main only because the pair read as List<Int> against List<String>. The repair is one signature relation, `callable_signatures_agree` (arity, parameter types, codomain, parameterised by the component relation so equality and compatibility cannot drift), which the equality arm that already compared params now also routes through; an Arrow arm in the resolution verdict and the shape renderer; and in `v1.compiler.infer` `declared_type_conformance_diags` a one-peel element arm, `callable_element_signature_mismatch`, that hands two function-typed elements to the existing arrow authority `callable_signature_mismatch` rather than minting a second conformance relation. So the codomain refusal is preserved on purpose, and the parameter and arity mismatches -- accepted on main -- now refuse. Evidence: the four declared-return cells of `test.claim.infer_callable_type_argument_witness_test` (floor-admitted) and its emitted-accessor cells over a coproduct common field.",

"NEXT-RUNG TRIGGER: none for this class on the path named above -- it sits at its ceiling there. What would move the ceiling itself is a call seam that receives a callable-typed carrier from binding resolution by construction rather than a binding by spelling it then interrogates.",
],

evidence: [
DeclarationRef { module_path: "v1.compiler.infer", decl_name: "type_node_is_callable", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.infer_nullary_local_callable_witness_test", decl_name: "nullary_parameter_callable_resolves", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.infer_nullary_local_callable_witness_test", decl_name: "nullary_local_refuses_a_surplus_argument", field: WholeDeclaration },
DeclarationRef { module_path: "v1.compiler.infer_types", decl_name: "child_type_node", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.infer_callable_type_argument_witness_test", decl_name: "fold_lambda_calls_a_nullary_element_parameter", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.infer_callable_type_argument_witness_test", decl_name: "unbound_callee_in_the_same_lambda_still_refuses", field: WholeDeclaration },
DeclarationRef { module_path: "v1.compiler.infer_types", decl_name: "callable_signatures_agree", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.infer_callable_type_argument_witness_test", decl_name: "element_codomain_mismatch_refuses_at_the_declared_return", field: WholeDeclaration },
],
}
114 changes: 114 additions & 0 deletions dag/test/claim/infer_callable_type_argument_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
module test.claim.infer_callable_type_argument_witness_test

import std.types { Bool, Int, String }
import gunbc.compile_census_probe { blocking_subject_count_for, total_blocking_count_for, blocking_class_count_for }

// EXECUTING EVIDENCE FOR THE TYPE-ARGUMENT RESIDUE OF gunbc.recurring_failure_mode
// arity_proxy_for_callability_misroutes_a_found_local.
//
// A function type written as a TYPE ARGUMENT -- `List<fn() -> R>` -- lost its arrow when
// v1.compiler.infer_types child_type_node read the child's `inferred` field as the type it denotes: an
// Arrow stores its RETURN type there, so the element of `List<fn() -> Int>` became `Int`. Every
// binding drawn from that element then refused at the call seam as `function 'r' not found in
// scope` (class InternalError, subject function:r): a fold or map lambda's parameter, a match arm
// over `first`. It surfaced on extdeps.apple.app_attest first_assertion_refusal, a fold over
// `List<fn() -> AssertionRefusal?>`. The refusal is raised in inference, which every emission
// target runs, so it refused under --target dag and --target rust alike.
//
// Each cell is a source string compiled by the seed through gunbc.compile_census_probe, so the
// REDs assert zero blocking rows (a repair that swapped the misdirected refusal for another would
// still fail), and the control asserts a genuinely unbound callee inside the same lambda still
// refuses with that callee as the subject -- the repair admits the bound parameter, not any name.

data fold_thunk_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn first_some(rs: List<fn() -> Int?>) -> Int? {\n fold(rs, init: none, f: (acc, r) => match acc {\n Present { value: a } => Present { value: a }\n Absent => r()\n })\n}\n"

data map_unary_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn apply_all(rs: List<fn(Int) -> Int>) -> List<Int> { rs |> map(r => r(1)) }\n"

data match_arm_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn head_value(rs: List<fn() -> Int>) -> Int {\n match rs |> first {\n Present { value: r } => r()\n Absent => 0\n }\n}\n"

data unbound_callee_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn apply_all(rs: List<fn() -> Int>) -> List<Int> { rs |> map(r => unbound_callee_zzz()) }\n"

fn resolves_clean(source: String) -> Bool {
blocking_subject_count_for(source: source, wanted_class: "InternalError", wanted_subject: "function:r") == 0
&& total_blocking_count_for(source: source) == 0
}

test fn fold_lambda_calls_a_nullary_element_parameter() -> Bool {
resolves_clean(source: fold_thunk_source)
}

test fn map_lambda_calls_a_unary_element_parameter() -> Bool {
resolves_clean(source: map_unary_source)
}

test fn match_arm_calls_a_callable_element() -> Bool {
resolves_clean(source: match_arm_source)
}

test fn unbound_callee_in_the_same_lambda_still_refuses() -> Bool {
blocking_subject_count_for(source: unbound_callee_source, wanted_class: "InternalError", wanted_subject: "function:unbound_callee_zzz") > 0
}

// KEEPING THE ARROW MUST NOT LOSE A REFUSAL THE ERASURE HAD. While child_type_node erased an Arrow
// type argument to its codomain, returning `List<fn() -> Int>` where `List<fn() -> String>` is
// declared refused -- by accident, as List<Int> against List<String>. With the arrow kept the pair
// reaches v1.compiler.infer declared_type_conformance_diags as two function-typed elements, which
// it now hands to callable_signature_mismatch one element peel deep. So the codomain cell is the
// preserved refusal, the parameter and arity cells are refusals the erasure never had (both were
// accepted on main), and the same-signature cell is the accepted control that keeps the wall from
// being a blanket refusal of function-typed elements.

data codomain_mismatch_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, String, List }\nfn widen(xs: List<fn() -> Int>) -> List<fn() -> String> { xs }\n"

data parameter_mismatch_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, String, List }\nfn widen(xs: List<fn(Int) -> Int>) -> List<fn(String) -> Int> { xs }\n"

data arity_mismatch_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn widen(xs: List<fn() -> Int>) -> List<fn(Int) -> Int> { xs }\n"

data same_signature_source: String = "module test.claim.tmp_callable_type_argument_probe\nimport std.types { Int, List }\nfn keep(xs: List<fn(Int) -> Int>) -> List<fn(Int) -> Int> { xs }\n"

test fn element_codomain_mismatch_refuses_at_the_declared_return() -> Bool {
blocking_class_count_for(source: codomain_mismatch_source, wanted_class: "TypeMismatch") > 0
}

test fn element_parameter_mismatch_refuses_at_the_declared_return() -> Bool {
blocking_class_count_for(source: parameter_mismatch_source, wanted_class: "TypeMismatch") > 0
}

test fn element_arity_mismatch_refuses_at_the_declared_return() -> Bool {
blocking_class_count_for(source: arity_mismatch_source, wanted_class: "TypeMismatch") > 0
}

test fn element_same_signature_is_accepted_at_the_declared_return() -> Bool {
total_blocking_count_for(source: same_signature_source) == 0
}

// THE COMMON-FIELD CONSUMER. v1.compiler.infer_emit_info enum_field_type_consistent decides whether
// a field every variant carries is ONE common field, judging with node_type_equals over
// child_type_node, and the Rust emitter renders an access to a common field as an accessor call.
// Before the signature relation, two Arrow elements compared equal by the name Callable, so
// `List<fn() -> Int>` against `List<fn() -> String>` was admitted as common and `m.callbacks`
// rendered `m.callbacks()` -- a call to an accessor the emitter never generates, because the two
// arms carry different types. The negative cell asserts that call is gone; the control asserts the
// same access over one shared signature still renders through the accessor.

data mixed_callbacks_source: String = "module test.claim.callable_common_field_mixed_probe\nimport std.types { Int, String, List }\ntype MixedCallbacks = IntCallbacks { callbacks: List<fn() -> Int> } | StringCallbacks { callbacks: List<fn() -> String> }\nfn count_mixed(m: MixedCallbacks) -> Int { m.callbacks |> count }\n"

data same_callbacks_source: String = "module test.claim.callable_common_field_same_probe\nimport std.types { Int, List }\ntype SameCallbacks = LeftCallbacks { callbacks: List<fn(Int) -> Int> } | RightCallbacks { callbacks: List<fn(Int) -> Int> }\nfn count_same(s: SameCallbacks) -> Int { s.callbacks |> count }\n"

test fn callbacks_differing_in_codomain_are_not_one_common_field() -> Bool {
compile_dag_rust_emit_check(
mixed_callbacks_source,
"src/test_claim_callable_common_field_mixed_probe.rs",
[],
["m.callbacks()", "impl MixedCallbacks"]
)
}

test fn callbacks_with_one_signature_are_one_common_field() -> Bool {
compile_dag_rust_emit_check(
same_callbacks_source,
"src/test_claim_callable_common_field_same_probe.rs",
["impl SameCallbacks", "s.callbacks()"],
[]
)
}
40 changes: 40 additions & 0 deletions src/v1/04_infer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1416,6 +1416,38 @@ fn declared_type_kernel_inhabitance_mismatch_at_element(
}
}

// A FUNCTION TYPE AT THE ELEMENT POSITION IS JUDGED BY THE ARROW AUTHORITY, one peel deep like the
// kernel check above. `List<fn() -> Int>` returned where `List<fn() -> String>` is declared was
// refused only BY ACCIDENT while v1.compiler.infer_types child_type_node erased an Arrow type
// argument to its codomain -- the pair read as List<Int> against List<String>, both ground. With the
// arrow kept, neither side is ground and the pair fell to the unjudged arm. The judgment is
// callable_signature_mismatch, the same relation the top-level arrow arm consults, so a parameter
// or arity difference now refuses too, where before it was accepted under the erasure.
fn callable_element_signature_mismatch(declared: Node, produced: Node, source_indices: Map<String, NewlineIndex>) -> Bool {
let both_element_collections = node_is_element_collection(n: declared, source_indices: source_indices)
&& node_is_element_collection(n: produced, source_indices: source_indices)
&& node_is_keyed_collection(n: declared, source_indices: source_indices) == false
&& node_is_keyed_collection(n: produced, source_indices: source_indices) == false
&& declared.return_cardinality == Required
&& produced.return_cardinality == Required
if both_element_collections == false {
false
} else {
match declared.children |> first {
Absent => false
Present { value: dl } =>
match produced.children |> first {
Absent => false
Present { value: pr } =>
let declared_element = child_type_node(ch: dl)
let produced_element = child_type_node(ch: pr)
type_node_is_arrow(n: declared_element) && type_node_is_arrow(n: produced_element)
&& callable_signature_mismatch(formal: declared_element, actual: produced_element, source_indices: source_indices)
}
}
}
}

fn declared_type_kernel_inhabitance_mismatch_here_or_at_element(
declared: Node,
produced: Node,
Expand Down Expand Up @@ -1476,6 +1508,14 @@ fn declared_type_conformance_diags(declared: Node, produced: Node, span: SourceS
module_name: scope.module_name
)]
}
else if callable_element_signature_mismatch(declared: declared, produced: produced, source_indices: si) {
[type_mismatch_error(
expected: node_type_shape(n: declared, source_indices: si),
got: node_type_shape(n: produced, source_indices: si),
span: span,
module_name: scope.module_name
)]
}
else if !both_ground { [] }
else if node_type_compatible(left: declared, right: produced, source_indices: si) { [] }
else {
Expand Down
Loading