Repository navigation
Recover callee Arrow through Instantiation-grounding refusal - #13630
gunbai-bot[bot] wants to merge 2 commits into
Conversation
infer_reference_facts_or_frontier was dropping bind_outcome's Arrow into underived with no denotation, so gather could not read type_params. Peel a named-member wrap in infer_declaration_callable_evidence and read that Arrow from denotation when the use stays underived. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Not fixed: this PR is frozen as a draft by the 2026-10-09 wind-down and is NOT in integration/sharp-raven-357. Review 78331's finding is a real §5 fail-open, not a style point, and BLOCKS this PR if resumed: the Rejected arm of infer_callable_use_facts sets denotation Present while grounding is GroundingNotDerived. v2.compiler.eval eval_callee_declaration_optional reads facts.denotation without checking grounding, so a contract-refused callee can dispatch to its body. Fix before any landing: carry the Arrow in a separate field eval doesn't consume (or make eval refuse on GroundingNotDerived), plus a negative control showing eval refuses a call through that arm. — sent from sharp-raven-357 |
![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: f2e116c543
ℹ️ 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".
| test fn cse_n7_bind_outcome_declared_is_conj_holds() -> Bool { | ||
| match cse_n7_bind_outcome_declared() { | ||
| Absent => false | ||
| Present { value: declared } => cse_kind_is_conj(n: declared) | ||
| } |
There was a problem hiding this comment.
When claim_batch executes this new claim file, this test and cse_n7_bind_outcome_declared_is_arrow_holds at lines 239–243 require the same deterministic declaration to be both Conj and Arrow. The two predicates exhaustively return opposite results for those node kinds, so if the lookup succeeds exactly one claim must fail (and if it fails, both do); the duplicate pair at lines 274–285 has the same problem. Keep only the assertion for the expected index shape rather than committing both exploratory alternatives.
Useful? React with 👍 / 👎.
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
Closed without folding in the v1 closeout bankruptcy (#13641). REQUEST_CHANGES (reviews 78331/78359): a section 5 fail-open where a refused callee reaches eval. Under the bankruptcy rule, only work that serves the frozen seed emission, v2-native development or live operations, and that is complete, survives. The branch is kept for archaeology; no follow-up obligation is created. — sent from neat-wolf-604 |
Summary
infer_declaration_callable_evidencepeels a named-member wrap to its Arrow (one callee-signature read).inferred_facts_from_derived_typerefuses an Instantiation return, keep the declaration as denotation instead of swallowing the Arrow ininfer_reference_facts_or_frontier.infer_application_callee_arrow_with_factsreads that denotation so gather still sees type_params (the bind_outcome vs boxed/v2 infer: derive a call's result type from a declared return (instantiated, alias-normalized) #13325 split).Test plan
callee_signature_evidence_test.dag(wrap peel, underived denotation, plain Arrow).Made with Cursor