Repository navigation
Conversation
A call to a trait method with a default body was typed by the trait method's type, which is inferred from the default body, even when it resolved to an override annotated with its own spec. The override is checked only against that spec, so callers assumed a postcondition nobody proved. Use the resolved impl method's type when there is one; an unannotated override's type is the trait method's type anyway. Fixes #337 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01SHVtHJd3xtzyFQiUiyqD3m
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. |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #337
fn_def_tytyped a trait method call with the trait method's own type whenever it had one. For a trait method with a default body, that type comes from the default body. When the call resolved to an override annotated with its own spec (#[thrust::callable]), the override was checked only against that spec. Callers still assumed the default body's postcondition, soassert!(A.m() == 2)verified even though the override returns1.The call is now typed by the resolved impl method's type whenever that method has one. For an unannotated override that type is
trait_item_ty, i.e. the trait method's type, so nothing changes there. For an annotated override it is the spec the body is actually checked against.Added
tests/ui/{pass,fail}/trait_default_override_callable.rs. Thefailcase verified as safe before this change.cargo testpasses: 402 UI tests, run with the pinned Z3 and PCSat.🤖 Generated with Claude Code
https://claude.ai/code/session_01SHVtHJd3xtzyFQiUiyqD3m
Generated by Claude Code