Require coherence of supertrait associated item bounds for dyn-compability - #158915
Require coherence of supertrait associated item bounds for dyn-compability#158915theemathas wants to merge 2 commits into
Conversation
…ics. See rust-lang#154662 These tests will be fixed in a subsequent commit.
|
I'm unsure of what to do with the now-failing tests. I'm also rather unsure of my code in general. Please be careful with the review to make sure I didn't do anything stupid. Thank you. |
…ility Fixes rust-lang#154662 In a `dyn` type, if multiple bounds are specified via supertraits for the same associated item, then we previously accepted them if the relevant trait's generics are different, even if the bounds conflict. This was unsound, since those generics could end up being instantiated with identical concrete types, causing the `dyn` type to have two different "values" for the same bound. Thus, if a trait has multiple supertrait bounds for the same associated item, we check whether those bounds are coherent, similarly to how we check for overlap between impulse (i.e., we check if the generics could be instantiated to be the same while the "values" of the bounds are different). If the bounds are incoherent, then we consider the trait to be dyn-incompatible.
4d67fa1 to
256670e
Compare
|
r? types |
| // Note that we discard any obligations we get here. | ||
| // We don't care about proving them. | ||
| // | ||
| // If this call returns an Err, then the two sets of generic args | ||
| // can't possibly be instantiated with the same concrete types. | ||
| // So, we return true from the function |
There was a problem hiding this comment.
you could do the proper coherence thing and actually use an ObligationCtxt and try_evaluate
makes slightly more compile
There was a problem hiding this comment.
Sorry, but I don't understand what you mean. What is an ObligationCtxt, and how does using it cause more code to compile?
| .instantiate_identity(tcx) | ||
| .predicates | ||
| .into_iter() | ||
| .map(Unnormalized::skip_normalization); |
There was a problem hiding this comment.
| .map(Unnormalized::skip_normalization); | |
| .map(Unnormalized::skip_norm_wip); |
| ) -> bool { | ||
| // We syntactically compare the two terms. If they're equal, then | ||
| // they do not conflict with each other. | ||
| // FIXME: This is an overly strict definition of equality. Could this be done better? |
There was a problem hiding this comment.
if we check for equality in the param_env of the trait and prove nested obligations + regions, this should be correct?
as in, what we prove here is
for<trait_params, trait-where-clauses> assoc1 == assoc2
=> assoc1_term == assoc2_term
and we under-approximate by
for<trait_params, trait-where-clauses> assoc1 != assoc2
OR
for<trait_params, trait-where-clauses> assoc1term == assoc2term
which we impl as
!exists<trait_params, trait-where-clauses> assoc1 == assoc2
OR
for<trait_params, trait-where-clauses> assoc1term == assoc2term
so to make this check more permissive, you could check the where-clauses of the trait in the exists check :>
There was a problem hiding this comment.
What's a nested obligation? What's a nested region? What's "the param_env of the trait"? What does it mean to "check" the where clauses of a trait?
|
after that, we should do a crater run 😁 |
|
@rustbot author |
|
Reminder, once the PR becomes ready for a review, use |
This PR is an alternative to #157710. However, unlike that PR, this PR does not address #150936.
Fixes #154662
In a
dyntype, if multiple bounds are specified via supertraits for the same associated item, then we previously accepted them if the relevant trait's generics are different, even if the bounds conflict.This was unsound, since those generics could end up being instantiated with identical concrete types, causing the
dyntype to have two different "values" for the same bound.Thus, if a trait has multiple supertrait bounds for the same associated item, we check whether those bounds are coherent, similarly to how we check for overlap between impulse (i.e., we check if the generics could be instantiated to be the same while the "values" of the bounds are different). If the bounds are incoherent, then we consider the trait to be dyn-incompatible.
r? @fmease