Skip to content

v2 infer: Cardinality (T?) nodes wrongly refused for descent - #12807

Closed
briansrls wants to merge 3 commits into
mainfrom
session/cool-cat-831
Closed

v2 infer: Cardinality (T?) nodes wrongly refused for descent#12807
briansrls wants to merge 3 commits into
mainfrom
session/cool-cat-831

Conversation

@briansrls

@briansrls briansrls commented Sep 30, 2026

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session cool-cat-831.
Pushing to session/cool-cat-831 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

Brian Searls and others added 3 commits September 30, 2026 13:01
Brian Searls @claude
v2 infer: the Cardinality type connective owes no descent (T? no long…
9e01617 
…er refused for infer_descent_not_derived)

v2.std.cardinality connective_multiplicity mapped Cardinality to RequiresTerminationProof while
every other type connective is Bounded; termination_proof_witness_for_node folds that over every
node, so any tree carrying T? refused. A type node is never evaluated; repetition enters only
through Loop (loop_multiplicity), which is unchanged.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls @claude
Supplied-tree claims only: keep the discriminating T? red and a corre…
520fc4b 
…ctly-shaped Loop descent control

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Brian Searls
Merge origin/main
671246f
@briansrls
briansrls marked this pull request as ready for review September 30, 2026 16:39
@chatgpt-codex-connector

chatgpt-codex-connector Bot commented Sep 30, 2026 •
edited
Loading

Copy link
Copy Markdown

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review Status Commit Review trigger
📝 Code Review ✅ Completed 2026-09-30T16:57:42.296811Z 671246f Draft marked ready
ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

@gunbai-bot

gunbai-bot Bot commented Sep 30, 2026

Copy link
Copy Markdown
Contributor

Closing: this change is absorbed into #12806, which carries these commits together with the Int?-at-Int refusal. On its own, this PR turns fn f(x: Int?) -> Int { x } from refused into silently ACCEPTED, so by ruling it must never land alone (a dequeued #12806 would leave main admitting Int? into Int). Review 73302's findings are noted for #12806: the approval stands on the substance, and the design note (connective_multiplicity now returns Bounded for every connective, so the call site could return Bounded directly) is a valid simplification to consider there.

— sent from quiet-gull-780

@gunbai-bot gunbai-bot Bot closed this Sep 30, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@briansrls