Make object bound candidates sound in the new trait solver #108333
Merged
Conversation
This file contains 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
rustbot
added
S-waiting-on-review
|
Some changes occurred to the core trait solver cc @rust-lang/initiative-trait-system-refactor |
compiler-errors
force-pushed
the
new-solver-object-sound
branch
from
becd8bb
to
abda8ee
Compare
lcnr
reviewed
Feb 22, 2023
compiler/rustc_trait_selection/src/solve/trait_goals/structural_traits.rs
Outdated
Show resolved
Hide resolved
| .predicates, | ||
| ); | ||
| for item in infcx.tcx.associated_items(trait_ref.def_id).in_definition_order() { | ||
| if item.kind == ty::AssocKind::Type { |
There was a problem hiding this comment.
Suggested change
| if item.kind == ty::AssocKind::Type { | |
| // FIXME(associated_const_equality): Also add associated consts to | |
| // the requirements here. | |
| if item.kind == ty::AssocKind::Type { |
I think that will be necessary
There was a problem hiding this comment.
Can assoc consts have WC?
compiler/rustc_trait_selection/src/solve/trait_goals/structural_traits.rs
Show resolved
Hide resolved
| /// impl Bar for dyn Foo<Item = Ty> {} | ||
| /// ``` | ||
| /// | ||
| /// However, in order to make such impls well-formed, we need to do an |
There was a problem hiding this comment.
That's the main concerning step here 🤔 because I don't have a strong understanding of why the impl with unnormalized projections is not well-formed.
It doesn't compile with either the new solver or the old one, but that doesn't feel like a good enough explanation :< can look into this a bit myself (and should have a rustc-dev-guide section about this)
There was a problem hiding this comment.
trait Trait {
type Assoc: Bound;
}
trait Bound {}
struct Ty;
/*
impl Trait for dyn Trait<Assoc = Ty> {
type Assoc = Ty;
}
*/
struct DynTrait;
impl Trait for DynTrait
where
<DynTrait as Trait>::Assoc: Bound,
{
type Assoc = Ty;
}
fn needs_trait(_: impl Trait) {}
fn main() {
needs_trait(DynTrait);
}So this actually isn't (technically) failing during wfcheck. On both the "classic" solver and "next" solver, this overflows in normalize_param_env_or_error in the param_env query for the impl. 🤔
There was a problem hiding this comment.
lcnr/solver-woes#10 to track this
|
☔ The latest upstream changes (presumably #108339) made this pull request unmergeable. Please resolve the merge conflicts. |
compiler-errors
force-pushed
the
new-solver-object-sound
branch
from
abda8ee
to
ed30eff
Compare
|
Addressed the comments (except for the main "is this enough for soundness" issue). @bors r=lcnr |
bors
added
S-waiting-on-bors
|
@bors rollup only new solver |
bors
added a commit
to rust-lang-ci/rust
that referenced
this pull request
Feb 25, 2023
…mpiler-errors Rollup of 7 pull requests Successful merges: - rust-lang#105736 (Test that the compiler/library builds with validate-mir) - rust-lang#107291 ([breaking change] Remove a rustdoc back compat warning) - rust-lang#107675 (Implement -Zlink-directives=yes/no) - rust-lang#107848 (Split `x setup` sub-actions to CLI arguments) - rust-lang#107911 (Add check for invalid #[macro_export] arguments) - rust-lang#108229 ([107049] Recognise top level keys in config.toml.example) - rust-lang#108333 (Make object bound candidates sound in the new trait solver) Failed merges: - rust-lang#108337 (hir-analysis: make a helpful note) r? `@ghost` `@rustbot` modify labels: rollup
matthiaskrgr
added a commit
to matthiaskrgr/rust
that referenced
this pull request
May 10, 2023
…lcnr Make alias bounds sound in the new solver (take 2) Make alias bounds sound in the new solver (in a way that does not require coinduction) by only considering them for projection types whose corresponding trait refs come from a param-env candidate. That is, given `<T as Trait>::Assoc: Bound`, we only *really* need to consider the alias bound if `T: Trait` is satisfied via a param-env candidate. If it's instead satisfied, e.g., via an user provided impl candidate or a , then that impl should have a concrete type to which we could otherwise normalize `<T as Trait>::Assoc`, and that concrete type is then responsible to prove the `Bound` on it. Similar consideration is given to opaque types, since we only need to consider alias bounds if we're *not* in reveal-all mode, since similarly we'd be able to reveal the opaque types and prove any bounds that way. This does not remove that hacky "eager projection replacement" logic from object bounds, which are somewhat like alias bounds. But removing this eager normalization behavior (added in rust-lang#108333) would require full coinduction to be enabled. Compare to rust-lang#110628, which does remove this object-bound custom logic but requires coinduction to be sound. r? `@lcnr`
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
r? @lcnr