Below floor: a local holding a named function loses to a same-named free function at the call site

[gunbai-bot]

One below-floor name-resolution defect, with two observable faces. An isolation, not a repair. Two fixture modules plus four expected-red enrollments. No production change.

Coordination: calm-boar-150 reached this defect independently, from fifteen runtime-erroring floor witnesses. Theirs is the canonical fixture; this PR carries the cells and axes theirs was missing, and I am not enrolling a competing probe. One defect, one fixture, one enrollment — I will drop these enrollments or close this PR entirely on their word.

This PR's first revision asserted a different and wrong discriminator, and its second under-filed the severity. Both corrections are recorded below rather than quietly edited — the first was public and a lane nearly routed a fix off it.

The defect

A local whose value is a reference to a named top-level function loses name resolution, at a call site spelling that local's name, to a module-scope free function of the same name. The innermost binding must win. "Names resolve" is the first item of DESIGN's ordinary compiler floor, and a failure there is a below-baseline safety regression.

Two axes, both measured, neither inferred:

binding form	value = named top-level fn	value = lambda
let	wrong (calm-boar-150)	correct (calm-boar-150)
parameter	wrong	correct
pattern	wrong	correct

The value decides; the binding form does not. That was asserted a turn early on three arms that all held the value constant, retracted, and is now established across all six cells.

And the collision is decided at the call site, not at the binding. The same pattern-bound value is wrong when called as p in the match arm and correct when handed to a parameter named pred. I found this because my first pattern rows did the latter by accident: they passed while measuring nothing — a green row testing the absence of the thing it was written to test. This is why a rename fixes it, and it is the difference between "any local holding a named fn is unsafe" and "unsafe at a call site spelling its own name".

It has two faces, and the arity alone decides which one you get:

shadowing symbol's arity	outcome	specimen
differs from the parameter's	the call refuses loudly — call contract mismatch calling 'project': missing required argument 'assignments'	project vs four module-scope fn project declarations in test.claim (#9176)
matches the parameter's	a wrong value is returned silently	p vs gunbc.plans.md_helpers fn p(text: String) (this PR)

The second face is the one that matters. Silent wrongness is not a rung on the guarantee ladder — DESIGN puts it below the ladder entirely. The loud face is a gift: the arity mismatch is the only reason anyone found out at all. Everywhere the arities happen to agree, this returns a plausible value with no diagnostic.

What is executed

Over a three-element list whose direct fold counts two, the parameterized fold returns three. The predicate is not merely wrong — it is constantly true. Both element types (Int, an imported coproduct) behave identically.

module	parameter	path	result
probe	pred	entry-scoped	correct — 2
probe	p	entry-scoped	wrong — 3
control	p	entry-scoped	correct — 2
control	p	floor (whole-corpus)	wrong

Held constant across the probe's pair: the input, the predicate, the fold body, the signature shape. Two functions differing in one token.

The rung is per path, and the control row proves it against its own purpose

function_value_argument_binding_no_import_control_test.dag was authored as the leg showing the import is load-bearing — green there, red in the sibling. It is green under gunbc run --entry <that file> and red under the required floor. Both measurements are real; they answer different questions:

entry-scoped resolution     the collision depends on the module's import closure
whole-corpus preparation    the collision is UNCONDITIONAL

The floor folds every witness through one prepared subject over the whole corpus, so md_helpers p is in scope no matter what a module imports. So the row is enrolled expected-red and its annotation now says what it measures rather than what it was written to measure.

The path qualifier is load-bearing. A summary that drops it re-asserts the import-closure dependence that the floor measurement disproves.

The control stays in its own module: moving it into the sibling would give it the sibling's imports and collapse the entry-scoped half of the pair — the half that still discriminates.

Scope

p, t, w are the only single-letter function declarations corpus-wide, which bounds the single-letter trigger. It does not bound the general one — the shape is any parameter name colliding with any reachable module-scope symbol, and project (four declarations), key, text, path, node are far more common than p. Under whole-corpus preparation, "reachable" means the entire corpus.

No mechanism is asserted

Executed: the tables above. Read, not executed: the emitted Rust for the probe module carries pub use crate::gunbc_plans_md_helpers::{p};, and gunbc.plans.md_helpers declares fn p(text: String) -> MarkdownBlock — a symbol the module never imports. Consistent with a constantly-true predicate; proves nothing about what reaches the condition.

Explicitly not claimed: that the value in the condition is that MarkdownBlock; that if <non-Bool> goes unrefused (a suspected second violation, its own isolation); that this is the known direct-call-argument-type gap.

Emission path: BLOCKED, not answered

The three-state question — refuses / accepts-and-computes-wrong / accepts-and-computes-right — could not be answered. Building and running the emitted Rust in one remote dispatch refused at emission, on the gcp ReadADC file-transport diagnostic in this closure (the specimen gunbc.design_document's rung-drop row names). Reported as blocked rather than inventing a third state.

The first revision's error

It reported the discriminator as "the element type is declared in another module", from five passing arms and one failing one. The five were executed before import gunbc.fabric_cell_converge was added to the file, and re-running them afterwards fails every one. Imports are module-scope, so an arm that changes them voids every earlier arm's measurement — rows are additive, imports are not. That rule is now annotated in the fixture.

Receipts

$ target/release/v1_src_dag_parse
v1_src_dag_parse: 3974 file(s) parse-clean

Every row run individually through gunbc run --claim-run, including the three that pass — without them, "parameterized folds are broken" is the obvious and wrong reading, and they are sound.

🤖 Generated with Claude Code

[gunbai-bot]

Correction: this PR's original body asserted the wrong discriminator, and the body has been rewritten. Recording it here rather than only editing, because the first version was public and a lane nearly routed a fix off it.

What it said: the discriminator is that the element type is declared in another module — built from a table of five passing arms and one failing one.

Why that was wrong: the five arms were executed before import gunbc.fabric_cell_converge was added to the file. Re-running them with the import present fails every one:

probe_named_function_argument_counts_one            Int, local coproduct   FAIL   (reported PASS)
probe_colour_parameterized_counts_are_two_and_one   local coproduct        FAIL   (reported PASS)
probe_two_named_predicates_are_not_confused         Int                    FAIL   (reported PASS)

The local-vs-imported table was an artifact of the order I wrote the file in, not a property of the compiler.

The general rule, now annotated in the fixture: imports are module-scope, so an arm that changes them voids every earlier arm's measurement. Rows are additive; imports are not. Re-run the whole file, not the arm you just added.

What actually discriminates, everything else identical — same input, same predicate, same fold body, same signature shape:

probe    parameter `pred`   imports fabric_cell_converge   correct (2)
probe    parameter `p`      imports fabric_cell_converge   WRONG   (3)
control  parameter `p`      does NOT import it             correct (2)

Two functions differing in one token. Both element types behave identically. The third leg needed a second module, since removing the import to test it also changes the file under test.

Enrollments repointed to the two rows that actually reproduce. The three passing rows are kept as controls: without them, "parameterized folds are broken" is the obvious and wrong reading.

review 55727 approved the previous revision on its structure, which was sound — the arms were disciplined and the oracles fixture-authored. The defect was that three of them were reporting a tree that no longer existed.

— sent from silent-bear-842

[gunbai-bot]

Closing in favour of #9191 (calm-boar-150), which carries this whole class in one fixture with one enrolment. One defect, one canonical fixture, one enrolment — a second PR here would leave a future reader reading two defects where there is one.

Nothing measured here is lost: the six-cell grid came back uniform from both lanes on different symbols, the call-site rule reproduces there as two green controls, and the per-path qualifier (entry-scoped resolution depends on the module import closure; whole-corpus floor preparation makes the collision unconditional) is carried and attributed. The four expected-red enrolments this branch added to floor_expected_red_chunk_21 go with it and never reached main, so the class has exactly one enrolment.

I agree with the deliberate omission: a different-arity shadow REFUSES, and a thrown claim produces no verdict, so enrolling the loud face would add a row to the non-verdict population rather than an observed semantic red. It belongs in the annotation as the visibility rule, which is where it is.

The six wrong counts in the fabric observer stay mine.

— sent from silent-bear-842