Skip to content

Collapse FuncItem into FnItem: one callable item kind - #11289

Merged
gunbai-bot[bot] merged 6 commits into
mainfrom
session/cool-ibex-701-b
Sep 13, 2026
Merged

gunbai-bot[bot] merged 6 commits into
mainfrom
session/cool-ibex-701-b

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 13, 2026 •

Copy link
Copy Markdown
Contributor

What

Follow-up to #10850. That PR deleted the func spelling; ItemKind::FuncItem was its shadow in the node model — "an item with a body and a non-empty uses row" — and every consumer treated it identically to FnItem (export kind, callable admission, decl-index, census label, interpreter dispatch, emit registry) except one. This collapses the variant: ItemKind = FnItem | TypeItem | DataItem | ServiceItem | OtherItem, and item_kind drops the uses-count arm so an effectful declaration is classified by the same body/params test as any other fn.

What the collapse exposed, and what this PR does about it

The FuncItem arm of build_item_info hardcoded is_self_recursive: false / has_non_tail_self_call: false, so the registry said every effectful item was non-recursive. (Parameter-bearing effectful functions already entered infer_item's descent analysis; the erased fact was the REGISTRY projection.) With one arm, the registry is truthful. Two consequences the side chat's HOLD (review 5191771473) named, both landed here:

  1. The zero-parameter branch of infer_item erased the same facts on the typed node: uses: [], no resource in scope, recursion hardcoded false. A zero-parameter fn … uses net that read net refused as unbound, and its emitted Rust signature carried no resource parameter while the registry called it effectful — two contradictory observations of one declaration. The branch is deleted; the parameter-bearing branch's guard widens to params > 0 || inferred != none, so one branch types every function with a body.

  2. Effectful self-recursion had no realization and no refusal. emit_func_def renders effectful declarations as async fn and never consults is_tco_eligible/is_self_recursive (the loop transform and stacker guard belong to the pure path), so a self-call reached rustc verbatim and failed E0733 after a green gunbc compile — §5's fabricated plausible output. EffectfulSelfRecursionUnrealized is a new typed, located, blocking diagnostic raised at the Rust emitter boundary (beside AmbiguousAnonymousRecordLiteral, same fold shape), read from the SAME registry row the pure path's TCO decision reads. It is the first consumer of is_self_recursive on an effectful item — before this collapse it could not have fired. Rust-specific by construction; Python and Go recurse without boxing.

Evidence

test.claim.effectful_item_kind_collapse_witness_test, enrolled in dag/test/claim, executed in both directions on a remote runner:

  • under the pre-fix seed (mirrors before regen): a_zero_parameter_effectful_declaration_binds_its_resource FAIL, …_emits_its_resource_parameter FAIL, an_effectful_tail_self_call_is_refused_at_the_rust_emitter FAIL, an_effectful_non_tail_self_call_is_refused_at_the_rust_emitter FAIL, an_effectful_declaration_calling_a_pure_recursive_helper_is_admitted PASS;
  • under the regenerated seed: all five PASS.

So the four subject arms discriminate and the control rules out a refusal that fires on every effectful declaration. The mutation bar (restore hardcoded-false in build_item_info; restore uses: [] on the zero-parameter node) is stated in the file with the tree it must be made in.

Files

  • .dag: v1.compiler.infer_items (variant + item_kind), v1.compiler.infer (export kind, build_item_info), infer_lookup / infer_service imports, v2.std.decl_index, v2.lens.interface_summary, gunbc.bare_name_fork_lens; two annotation/reason texts that named the pair.
  • .dag (this round): v1.std.core (EffectfulSelfRecursionUnrealized: variant, span, render, disposition), v1.compiler.infer (infer_item unification), v1.compiler.emit_rust (effectful_self_recursion_diagnostics, EmitRustContext.effectful_recursion_diags).
  • Hand Rust: cli_run/compile_clean.rs (diagnostic class name/subject/exemplar), cli_run.rs, cli_run/emit_host.rs, cli_run/complexity_gates.rs, bin/claim_batch.rs, coproduct_reflection.rs (sort key renumbered), v1_interpreter.rs — each an FnItem | FuncItem pattern narrowed to FnItem.
  • Generated mirrors: regenerated on a remote runner from the edited .dag and taken byte-for-byte (v1_compiler_infer.rs, v1_compiler_emit_rust.rs, v1_std_core.rs, _items, _lookup, _service); the regen lane adjudicates the fixed point.

Test plan

  • cargo clippy --all-targets -- -D warnings: exit 0 (remote).
  • Witness executed RED under the pre-fix seed and GREEN under the regenerated one (above).
  • git grep FuncItem over src/ and dag/ (excluding the failure-mode ledger): empty.
  • Required lanes + heal-generated-artifacts on CI.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XjkfJ59JXcYnbtgTCH2Utn

gunbc-ci-auto-heal and others added 2 commits September 13, 2026 17:00
The func item form was deleted in #10850; FuncItem was the node-model
shadow of that spelling, and its only distinguishing content was that
build_item_info hardcoded is_self_recursive/has_non_tail_self_call to
false for effectful declarations. With one kind, effectful functions
enter the same descent analysis as every other fn.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XjkfJ59JXcYnbtgTCH2Utn
The regen candidate imports ItemKind's variants by glob once no single
variant is named; the hand boot had dropped the line entirely.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XjkfJ59JXcYnbtgTCH2Utn

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD at exact head 944d13385e3d49b7c5ab4b0d9c76c3d99f0b10c7.

The mechanical collapse is correct and the exact-head required run is clean, but this head does not yet satisfy the previously stated B acceptance bar. Two load-bearing gaps remain.

1. Zero-parameter effectful functions now have contradictory authoritative facts

src/v1/04_infer.dag::infer_item, in the branch

item.body != none && item.params |> count == 0 && item.inferred != none

still:

  • infers the body without folding item.uses into scope;
  • publishes uses: [];
  • hardcodes is_self_recursive: false;
  • hardcodes has_non_tail_self_call: false.

After this PR, that same declaration is FnItem, so build_item_info takes the sole FnItem arm and computes both recursion facts from the body. The registry can therefore say “recursive effectful fn” while the typed item says “no effects, not recursive.” This is the exact split the earlier B ruling said must not land: a pure enum collapse making ItemInfo truthful while the typed function node still erases the declared row.

Repair that branch before deleting the structural distinction: extend its scope with item.uses, preserve uses: item.uses, compute the two recursion facts, and apply the same descent-evidence policy as the parameter-bearing fn branch. A zero-parameter source-level fn is still a function; absence of value parameters is not authority to reinterpret or erase its effect row.

2. The behavioral delta has no discriminating execution evidence

This PR changes no test file. The required floor proves the existing corpus stays green; it does not prove the new recursion facts are correct or safely consumed, especially if the live corpus contains no recursive effectful declaration.

Add constructed controls covering at least:

  1. a zero-parameter effectful fn that references its declared resource, proving the typed item preserves the row and the resource is in scope;
  2. a parameter-bearing tail-recursive effectful fn;
  3. a parameter-bearing non-tail-recursive effectful fn;
  4. agreement between the typed node and ItemInfo for uses, is_self_recursive, and has_non_tail_self_call;
  5. each selected effectful emitter either safely realizes the recursive case with resource/effect threading preserved or produces an explicit typed refusal.

Execute the mutation that restores the old hardcoded-false FuncItem behavior (and the zero-argument uses: [] behavior) and require the controls to RED. Green build/floor/regen alone is not a discriminator for this change.

Also correct the PR body: parameter-bearing effectful functions already entered infer_item's descent analysis before this PR—the branch is keyed on body/parameters and already folds item.uses into scope. The newly changed fact is the build_item_info/registry projection, not universal entry into descent analysis.

The enum and consumer narrowing otherwise look correct. Bring back the repaired exact head with terminal required contexts and the constructed receipts above.

@briansrls
briansrls dismissed their stale review September 13, 2026 20:05

Superseded by exact head 3a505ff. The zero-parameter erasure branch is deleted, effectful function typing is unified, the Rust emitter now has a typed blocking consumer of effectful self-recursion, and the five-row witness plus terminal exact-head required run close both findings.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LAND @ 3a505ffe7a53d08d542a96d11daa35cbdc2462b6.

The prior HOLD is satisfied and dismissed.

The zero-parameter erasure is removed at the source authority: one infer_item branch now handles every body-bearing function with an established return, folds item.uses into scope, preserves the row on the typed node, and computes recursion/descent facts. The deleted FuncItem arm no longer creates a second registry truth.

The newly truthful effectful-recursion fact now has an explicit consumer at the correct target boundary. Rust emission alone raises the typed, located, blocking EffectfulSelfRecursionUnrealized diagnostic before publishing files; Python and Go are not widened into that refusal. The control permits an effectful function that calls a pure recursive helper.

The five-row witness discriminates both repaired seams: zero-parameter resource binding and emitted parameter; tail and non-tail direct self-recursion refusal; and the non-self-recursive effectful control. Although the floor cannot import src/v1 to compare the typed node and ItemInfo as records, the source construction plus the independent consequences establish the needed agreement: typed uses is required by the first two rows, while registry is_self_recursive is required by the refusal rows. The unified source branches compute has_non_tail_self_call on both carriers; Rust safely refuses the broader self-recursive population rather than pretending to realize either tail shape.

The exact-head workflow is terminal SUCCESS across all four contexts, including clippy and regenerated-mirror fixed point; the required floor is clean and namespace-wave-admission admitted. GitHub reports the PR open, non-draft, mergeable, and CLEAN.

This authorizes enqueue only, with expectedHeadOid pinned to the full SHA above. Approval does not transfer to a new head and does not authorize manual merge or native-review bypass. If main advances before admission, the composed merge-group run remains the final integration proof; any required-context red holds landing.

@gunbai-bot
gunbai-bot Bot added this pull request to the merge queue Sep 13, 2026
Merged via the queue into main with commit 138955f Sep 13, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/cool-ibex-701-b branch September 13, 2026 20:53
@briansrls
briansrls restored the session/cool-ibex-701-b branch September 13, 2026 20:57
gunbai-bot Bot pushed a commit that referenced this pull request Sep 13, 2026
…tem form

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01534A1UAkjSmypHMjNWw11e
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant