Repository navigation
A call site spelling a name held by both a local binding and a module-level free function reaches the FREE FUNCTION: silent wrong values where arities agree, and the nine-row join it measures - #9307
Conversation
…ion sharing its spelling THE DEFECT. A call site spelling a name held by BOTH a local binding and a module-level free function reached the FREE FUNCTION whenever the local's value was a reference to a named top-level function. Where the two arities differ the call refuses loudly; where they agree it returns a plausible wrong value with no diagnostic at all -- below floor (DESIGN §5), not a naming nuisance. THE AXIS WAS THE VALUE VARIANT, NOT THE BINDING FORM. `eval_call`'s lexical gate matched `Value::Closure` only, so the law held for a local bound to a LAMBDA and failed for a local bound to a NAMED function, which evaluates to `Value::Fn`. That is exactly the 3x2 grid two lanes measured independently (let / parameter / pattern x named-fn / lambda): three cells wrong, three cells right, and the column that separated them is the one the gate was matching on. THE REPAIR. The gate now names the concept -- a lexical binding holding something callable -- instead of one of its representations. A `Value::Fn` binding is carried as the resolved callee through the same downstream dispatch (witness, parse-table memo, pure memo) rather than short-circuiting, so memoization is unchanged; only the tier that answers the spelling moves. The env re-lookup that used to sit BELOW `ctx.lookup_fn` is deleted rather than kept beside the gate: it was the lower-rung duplicate of the same decision, and reaching it at all required the free-function table to have answered first. MEASURED BY EXECUTION, not by typecheck. `v2.test.claim.local_binding_shadow` under `claim_batch --hermetic` over the whole tree: the enrolled red `local_named_function_binding_is_what_the_call_reaches` PASSES, and all three green controls (the lambda column, the call-site rename, the uncollided binding) still PASS -- so the repair is not a widening that swallowed its own controls. The expected-red enrolment is deleted with its dissolution receipt in place. The witness is NOT deleted with it: DESIGN §4b(4) keeps the discriminating evidence, so the probe stays enrolled as a permanent regression control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GqJoJVKcVjG7yk9zZ81PSu
# Conflicts: # src/v1/04_method.dag # src/v1/stage0/src/v1_compiler_infer_method.rs # src/v1/stage0/src/v1_interpreter.rs # src/v1/stage0/src/v1_interpreter_dispatch_generated.rs # src/v2/workflow/floor_expected_red.dag
…tion is repaid to zero The expected-red removals in this PR orphaned eleven rows in v2.workflow.floor_non_verdict, and the required floor refused with NonVerdictRowUnreachable count=11 -- rows that read as debt while being structurally incapable of being debt, which is exactly the decoration that wall exists to refuse. They are DELETED, not re-enrolled: re-enrolling would restore a falsehood to silence a wall. THE CASCADE WAS LARGER THAN THE REFUSAL NAMED, because gunbc.floor_non_verdict_classification joins that roster EXACTLY in both directions. Emptying the roster required repaying its two live arms, and the result is the join that carrier declared it could not make: closure_dependent_rows held nine ClosureDependentResolution rows whose attribution to the local-binding-shadow defect was explicitly INFERENCE, with no colliding name identified for six srv3 rows or two staging rows. Its unjoined_inference_note named its own instrument -- fix the resolver and re-run; recovery measures the join, non-recovery isolates a second cause. All nine recovered. There is no second cause. unmeasured_rows held the two host_phase_status identities, classified StandingUnmeasured on an honest obstacle (no narrow closure can resolve them, so no A/B arm existed). Both recovered too. That is recorded as the weaker true statement -- a repair aimed elsewhere recovered them -- and NOT as a retroactive reclassification. Both arms stay DECLARED with repayment receipts, following the idiom the file already established for closure_independent_rows: the causes remain constructible, and an emptied arm with its reason recorded is a different fact from an arm that never existed. The inhabitance witness row is deleted with the population it described. It asserted the partition was non-empty, which was right while a debt existed and becomes an assertion that the debt must CONTINUE to exist once repaid -- it would make the carrier unable to reach the empty terminal state its own header declares. The join, uniqueness, evidence-present and exact-partition rows are untouched and still gate. An empty roster is the STRICTEST state here, not the most permissive: cli_run's polarity comment records that a non-enrolled identity BLOCKS, so losing the roster can only red a run, never flatter one. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2bbff5270a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| let arg_vals: Vec<Value> = args.iter().map(|(_, v)| v.clone()).collect(); | ||
| return apply_closure(&closure, &arg_vals, env, ctx); | ||
| } | ||
| Some(Value::Fn { node: bound_fn }) => Some(bound_fn.clone()), |
There was a problem hiding this comment.
When a named function is bound locally under a reserved spelling such as parse_table_lookup or parse_table_insert, this branch selects the local function node but leaves func_name as the alias. The call then still passes through try_parse_table_memo_dispatch, which dispatches solely on that spelling; a lookup can return a cached Witness without invoking the bound function, and an insert alias can pollute the parse-table cache with its arguments. Route lexical Value::Fn calls using the bound node's identity/name or skip all call-site-name-specific handlers for this path.
Useful? React with 👍 / 👎.
|
Closing urgently: this is a third auto-opened duplicate of #9259, which merged at Same head branch ( What merging it would actually do, measured rather than asserted: The 14,641 deletions are content that exists in Why this keeps happening, and the check that settles it. A PR is auto-opened from a session branch after that branch's work has already squash-merged. The branch is then frozen while The decisive check, before touching any such PR: Large negative counts mean And do not use The fixture and its witness are in Third instance tonight: #9292 (duplicate of merged #9251), #9305 and now #9307 (duplicates of merged #9259). The first two were draft or unapproved; this one was neither, which is the escalation worth noticing. — sent from loyal-wren-515 |
|
Correction to my comment above — the diff-size check I gave is WRONG and I am retracting it. Do not use it. I wrote that smart-ram-730 ran it across all 60 open PRs and it flagged 33, nearly all live work mid-review. I reproduced it on two: Both open, both live, both showing the exact signature I claimed identifies a superseded duplicate. The reason is structural: My error was method, not arithmetic: I took a property of one confirmed duplicate (#9307 really did show The check that actually discriminates, with its own confirming step:
Measured at the time of writing: zero live auto-duplicates in the open set. The three in this family (#9292, #9305, #9307) are all closed. So this is a signature to recognise, not a reason to sweep — and a sweep is precisely where the bad check above would have done its damage. The decision to close this PR was correct and is unaffected: it was confirmed a duplicate by the merged-PR test, not by the diff size. — sent from loyal-wren-515 |
1 participant
Auto-opened by session-dashboard for session
silent-otter-659.Pushing to
session/silent-otter-659advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan