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

[gunbai-bot]

What

v1's checker accepted function-typed mismatches at the ordinary floor (DESIGN §4b: values inhabit declared types). Specimen: apply(f: convert) against fn apply(f: fn(Int) -> Int) with fn convert(s: String) -> String. This PR repairs the class rostered as gunbc.recurring_failure_mode function_typed_argument_mismatch_accepted. That existing row is updated with what was repaired and what remains. It is not a new row.

It covers the direct-call argument position (direct_call_arg_type_mismatch) and the positions declared_type_conformance_diags serves: annotated let, fn return, early return, data.

The walls (review 5291730200) and how each closed

1. Exact arrows. callable_signature_mismatch requires the arity to agree, then compares parameters and return exactly. The language has no subtype relation, so no variance is modeled. Leaves are judged only where both sides are ground, so brands and nominal records are unjudged, never falsely refused.
2. Nullary. A bare nullary name was read as a call: apply(f: seven) typed the argument as Int, and the Rust emitter wrote apply(seven()). expected_type_is_arrow now makes it a function value where an arrow is expected. It is minted from its signature, not decided by parameter count.
3. Polymorphism. One substitution is built over the whole actual arrow with unify_generics (first binding wins, never rebinds), then leaves are compared. same<T> refuses at fn(Int, String) -> Int and at fn(Int) -> String. ident<T> and pair<T, U> are accepted.
4. Depth. There is no limit and no visited set. The walk descends only through the two arrow nodes it was handed, never through a lookup, and a Node is a finite acyclic value, so recursion is bounded by input size.
5. One-sided cases. A value that is positively not a function at a function formal refuses, and so does a function value at a kernel or nominal formal. This applies at the direct call and at the annotated let.

What the corpus sweep found, and how each case was judged

Every sweep was run, not assumed. Intermediate states surfaced these cases, and each was root-caused rather than silenced:

• 8 over-refusals, fixed in the checker. type_node_is_callable answers true for a generic type declaration, which carries type params in params. Examples: List<String> at a List<T> formal, let l: List<Int> = Cons {..}, FilePath at a parametric permit. The new relations now decide by the Arrow connective (type_node_is_arrow).
• Lambdas typed as their body, fixed. A lambda node is declaration-shaped: its params are its children after the body, and its inferred is its body type. expression_value_type mints a lambda's arrow. This fixed refusals across the std.algebra fold_list and std.materialization_ladder callers.
• Parameter reading, fixed. child_type_node collapses an arrow parameter to its return and turns a type variable into error_type. That hid the nested and polymorphic mismatches, so callable_param_type reads the parameter type directly.
• 1 over-refusal, recorded as remaining (6). At gunbc.primitive_egress.census, an unannotated let f = fn(..) {..} local is typed as the lambda's body. The one-sided arm therefore does not judge local values. Trigger: type let-bound lambdas at their arrow.
• 1 real latent bug, recorded in the row and not repaired here. xs |> map(named_fn) types its elements as the function, because unify_template binds a CallableOf return to the whole argument. A one-line repair was written and then withdrawn. Once locals are unjudged, no refusal observes it, so the fix would have had no discriminating RED. The row names the trigger that makes v1.compiler.emit_rust emit_lib_rs_from_paths its RED.

Final sweep, on the merged head (gunbc compile --source-root dag --source-root src/v2 --target dag --repository gunbc --measured-root-demands tools/whole_corpus_compile_measured_root_demands.json): the only two type mismatch rows are pre-existing and non-callable, so zero new refusals. The src/v1 self-compile (claim_executor --required-regen) has no hard diagnostics either.

Evidence

test.claim.infer_function_value_argument_arrow_witness_test (floor-enrolled via test.claim.infer_) has 17 cells, all PASS at the head. Mutations used one mutant build with env-gated knockouts, run through claim_batch:

mutation	cells that flip to FAIL
arrow judgment → false	9 arrow REDs (parameter, arity, return, let, both nullary, both polymorphic, deep)
no substitution (generic names empty)	the 2 polymorphic REDs
one-sided → false	the 2 one-sided REDs
depth ≥ 8 ⇒ false restored	deep_nested_ground_mismatch_refuses
nullary value off	nullary_matching_accepted. The nullary mismatch REDs still refuse, via the one-sided arm (a String at a function formal), so the matching control is the nullary change's discriminator.

All 6 controls stay PASS under every mutation. They are: matching unary, matching nullary, ident, pair, lambda, and deep matching.

Mirror

src/v1/stage0/src/v1_compiler_infer.rs is byte-identical to the claim_executor --required-regen candidate at this head, minus two unrelated pre-existing pub use lines. No other mirror file is touched. The remaining regen drift (emitted_population.rs, std_integer.rs, …) is pre-existing on main and not mine.

Why v1 (gunbc.v1_maintenance_standing purpose test)

v1 is the checker that type-checks v2's own sources. src/v2 compiles through v1.compiler.infer, so the v2 self-host program's higher-order code has been unchecked at function boundaries. This is a floor repair on that gate.

Remaining (in the row)

• The record-field seam (Cfg { cb: 7 }).
• Brand, nominal and keyed arrow leaves.
• Method and pipe arguments.
• Generic formals' type-variable leaves.
• Local values at the one-sided arm.
• The one-sided arm at return and data positions.
• Outside this class: the Rust emitter writes a now-correct nullary function value as bare seven into an Rc<dyn Fn()> slot. The interpreter executes it correctly.

🤖 Generated with Claude Code

[briansrls]

SOURCE HOLD at exact head bdd8ef5dd49588ac831be55ad7fe503afac1317a.

The central placement is right, and the parameter-variance choice is right for the language as modeled today, but the relation still has three fail-open populations and the new recurring-failure row forks an existing authority.

Ruling on the placement

direct_call_arg_type_mismatch's callable exemption was DELIBERATE only in the narrow sense that nominal-brand, element and kernel-scalar relations cannot interpret a callable's params as ordinary type arguments. It was never a justified acceptance rule. Main already records exactly that in gunbc.recurring_failure_mode function_typed_argument_mismatch_accepted: exempting callables from the wrong relations is correct; accepting them without a callable relation is the defect.

A shared callable-conformance relation in v1.compiler.infer, consumed by both direct_call_arg_type_mismatch and declared_type_conformance_diags, is therefore the correct earliest seam. I do not ask for this to move later into emission or earlier into generic nominal comparison.

Ruling on variance

Do NOT add contravariant parameter checking in this PR. The current language authority says applications bind in an exact bijection of modeled types and carries no directional subtype relation. At ground leaves, symmetric node_type_compatible comparison in parameter and result positions is the coherent present rule. Contravariance/covariance becomes meaningful only if a separate subtype judgment exists; inventing it here would add semantics rather than repair the floor.

1. The recurring-failure authority is forked, and its unrepaired population remains live

The new function_value_argument_arrow_never_compared row is a narrower second authority for a class already owned by function_typed_argument_mismatch_accepted. The existing row explicitly includes:

• nullary and non-nullary arrows;
• a non-function value supplied to a function-typed formal or record field;
• a function value supplied where a nominal type is declared;
• the missing arrow-pair comparison this PR repairs.

This head still preserves:

else if type_node_is_callable(formal) || type_node_is_callable(actual) { false }

so the one-sided callable cases remain silently accepted. A new row over the repaired subset makes two authorities answer the same failure mode and makes the older row's next-rung trigger appear satisfied when most of its specimen population is not.

Required disposition: delete the new row and update the existing function_typed_argument_mismatch_accepted authority to record this exact partial climb and its remaining population, OR close the existing row's one-sided callable specimens in this PR. A partial repair is acceptable; a second authority is not.

2. Nullary named function values still fall through

callable_signature_view delegates a non-Arrow node to callable_inferred. But callable_inferred synthesizes an Arrow only when n.params |> count > 0; a named nullary declaration is returned unchanged. If the produced node is the declaration rather than an already-materialized Arrow, the new relation sees a.connective != Arrow and answers false -- accepted.

That is the exact nullary population the existing failure-mode receipt names. The current witness has no nullary cell.

Required REDs and control:

fn pick() -> String { "x" }
fn apply(f: fn() -> Int) -> Int { f() }
fn host() -> Int { apply(f: pick) }

and the annotated-let twin must refuse; fn good() -> Int at fn() -> Int must remain accepted. Fix the view so zero-parameter named declarations materialize their declared Arrow rather than depending on positive arity as a callability proxy.

3. The polymorphic control proves non-refusal, not valid instantiation

Preserving ident<T>(T) -> T at fn(Int) -> Int is correct. The implementation achieves it by declining every generic judgment:

• direct_call_arg_type_mismatch returns false before the new relation whenever the actual contains an unbound type variable;
• the shared relation treats every non-ground component as no mismatch.

That accepts arrows for which no single instantiation exists. Counterexample:

fn same<T>(x: T, y: T) -> T { x }
fn apply(f: fn(Int, String) -> Int) -> Int { f(1, "x") }
fn host() -> Int { apply(f: same) }

No one substitution for T satisfies the two parameter positions, but this head accepts the function value. The annotated-let form has the same problem. This is under-refusal, not the requested protection against over-refusal.

The callable judgment needs one substitution environment across the WHOLE actual arrow: bind each actual type variable from the expected monomorphic component, require every repeated occurrence to agree, then compare the instantiated result. Keep ident<T> as the positive control and add at least:

• same<T>(T,T)->T against fn(Int,String)->Int -- refuse;
• same<T>(T)->T against fn(Int)->String -- refuse;
• a two-variable arrow with a consistent substitution -- accept.

Do not blanket-refuse generic functions; instantiate them consistently.

4. Depth eight is a silent acceptance boundary

callable_signature_mismatch returns false at depth >= 8. A mismatched arrow nested beyond that point is therefore accepted as conforming. The failure-mode row even describes the guarantee as holding only "up to the relation's bound", but no language rule bounds function-type nesting at eight.

Remove the arbitrary fail-open limit. If recursive type graphs require cycle protection, use a visited identity relation and return a typed unestablished/refusal state on an actual cycle; do not translate resource protection into no mismatch. Add a nested-arrow RED just beyond the old bound and a matching deep-arrow control.

Evidence disposition

The four current REDs and three controls are useful and discriminating for unary ground arrows. The 5,433-source sweep is useful regression evidence for the population the corpus happens to instantiate; it cannot establish the nullary, inconsistent-generic or depth-nine counterexamples above because none is in that sweep's judged source population.

At review time the exact-head witnesses workflow is running. This hold is source-scoped and independent of its eventual result.

[gunbai-bot]

Addressed review 70637 (rung inflation) in db859d1. The class rung in function_typed_argument_mismatch_accepted now stays below the ladder, because it is the minimum across in-scope paths (DESIGN §4b(1)) and the record-field seam, method/pipe arguments and local values are still silent. Rung 3 is stated as a path rung only: the direct-call argument and annotated-let paths, plus arrow pairs at the fn-return, early-return and data positions. The class climbs only when every in-scope path does. Checker code is unchanged. — sent from neat-ibex-861

[briansrls]

APPROVE-SOURCE at exact head db859d11ec4978e719071f6554f4c5f6554e64b6.

The source hold at bdd8ef5d… is discharged:

• The repair updates the existing function_typed_argument_mismatch_accepted authority instead of retaining the forked narrower row, and it explicitly records both the repaired paths and the still-unrepaired population.
• Nullary named functions are preserved as function values when an arrow is expected; the direct and annotated-let mismatches refuse, and a matching nullary function remains the discriminating control.
• Polymorphic actual arrows are instantiated through one substitution over the whole arrow, so repeated type variables must agree while ident<T> and the consistent two-variable case remain accepted.
• The arbitrary depth-eight fail-open is gone; the deep mismatch and matching control cover the former boundary.
• One-sided callable/non-callable mismatches are judged where established, while the unannotated local-lambda population that cannot yet be judged is excluded narrowly and recorded with its trigger rather than guessed.

All five required jobs are green at this exact head. No further source repair is requested. A head move requires a delta rebind.