Skip to content

fix(safe): consume the full shared group prefix - #1704

Open
sebastian-griego wants to merge 1 commit into
bendlang:mainfrom
sebastian-griego:fix/safe-group-shared-arity
Open

sebastian-griego wants to merge 1 commit into
bendlang:mainfrom
sebastian-griego:fix/safe-group-shared-arity

Conversation

@sebastian-griego

Copy link
Copy Markdown
Contributor

A recursion group can share an argument bound by a returned lambda beyond a member's declared parameters. For g(n: Nat) -> Nat -> Nat, the group can consume both n and x before its selector. group_emit previously consumed only the declared n. The generated g mode still returned Nat -> Nat, so --verdict rejected the book when the call expected Nat.

Consume max(declared parameters, shared parameters) when constructing each member's remaining type and body. Require the same lower bound at group calls. This prevents a call from receiving the selector in a missing shared argument slot. Calls that reach group_call without the full prefix remain out of scope.

The five tests cover a returned helper lambda, a structural decrease in that lambda's argument, a helper with no declared parameters, a returned lambda in the leading member, and a dependent result. They use a forward law in an erased lambda. All five source programs check and run on main, but their BendTT books fail. This change makes all five pass the unchanged kernel and --verdict.

Validation:

  • Five regressions pass source checking, --checkup, interpretation, JavaScript, C, and the unchanged kernel. Source checking, interpretation, export, kernel checking, and --verdict were also rerun on the final branch.
  • A local gates/safe_node.ts sweep preserves every result across 1,733 existing test, demo, and benchmark files. There are no timeouts or infrastructure errors. Existing rejections remain rejections.
  • The repository gate passes 54 / 54. safe.ts adds six tokens and uses 23,992 / 24,000 ttok tokens.
  • TypeScript diagnostics are unchanged from main. The cluster gates have not been run locally.

The patch changes two lines in safe.ts. It does not change the source checker or the kernel.

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