-
Notifications
You must be signed in to change notification settings - Fork 12.7k
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of #124336 - compiler-errors:super-outlives, r=lcnr
Enforce supertrait outlives obligations hold when confirming impl **TL;DR:** We elaborate super-predicates and apply any outlives obligations when proving an impl holds to fix a mismatch between implied bounds. Bugs in implied bounds (and implied well-formedness) occur whenever there is a mismatch between the assumptions that some code can assume to hold, and the obligations that a caller/user of that code must prove. If the former is stronger than the latter, then unsoundness occurs. Take a look at the example unsoundness: ```rust use std::fmt::Display; trait Static: 'static {} impl<T> Static for &'static T {} fn foo<S: Display>(x: S) -> Box<dyn Display> where &'static S: Static, { Box::new(x) } fn main() { let s = foo(&String::from("blah blah blah")); println!("{}", s); } ``` This specific example occurs because we elaborate obligations in `fn foo`: * `&'static S: Static` * `&'static S: 'static` <- super predicate * `S: 'static` <- elaborating outlives bounds However, when calling `foo`, we only need to prove the direct set of where clauses. So at the call site for some substitution `S = &'not_static str`, that means only proving `&'static &'not_static str: Static`. To prove this, we apply the impl, which itself holds trivially since it has no where clauses. This is the mismatch -- `foo` is allowed to assume that `S: 'static` via elaborating supertraits, but callers of `foo` never need to prove that `S: 'static`. There are several approaches to fixing this, all of which have problems due to current limitations in our type system: 1. proving the elaborated set of predicates always - This leads to issues since we don't have coinductive trait semantics, so we easily hit new cycles. * This would fix our issue, since callers of `foo` would have to both prove `&'static &'not_static str: Static` and its elaborated bounds, which would surface the problematic `'not_static: 'static` outlives obligation. * However, proving supertraits when proving impls leads to inductive cycles which can't be fixed until we get coinductive trait semantics. 2. Proving that an impl header is WF when applying that impl: * This would fix our issue, since when we try to prove `&'static &'not_static str: Static`, we'd need to prove `WF(&'static &'not_static str)`, which would surface the problematic `'not_static: 'static` outlives obligation. * However, this leads to issues since we don't have higher-ranked implied bounds. This breaks things when trying to apply impls to higher-ranked trait goals. To get around these limitations, we apply a subset of (1.), which is to elaborate the supertrait obligations of the impl but filter only the (region/type) outlives out of that set, since those can never participate in an inductive cycle. This is likely not sufficient to fix a pathological example of this issue, but it does clearly fill in a major gap that we're currently overlooking. This can also result in 'unintended' errors due to missing implied-bounds on binders. We did not encounter this in the crater run and don't expect people to rely on this code in practice: ```rust trait Outlives<'b>: 'b {} impl<'b, T> Outlives<'b> for &'b T {} fn foo<'b>() where // This bound will break due to this PR as we end up proving // `&'b &'!a (): 'b` without the implied `'!a: 'b` // bound. for<'a> &'b &'a (): Outlives<'b>, {} ``` Fixes #98117 --- Crater: #124336 (comment) Triaged: #124336 (comment) All of the fallout is due to generic const exprs, and can be ignored.
- Loading branch information
Showing
11 changed files
with
132 additions
and
15 deletions.
There are no files selected for viewing
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
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
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
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
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,6 +1,7 @@ | ||
pub trait Arbitrary: Sized + 'static {} | ||
|
||
impl<'a, A: Clone> Arbitrary for ::std::borrow::Cow<'a, A> {} //~ ERROR lifetime bound | ||
//~^ ERROR cannot infer an appropriate lifetime for lifetime parameter `'a` | ||
|
||
fn main() { | ||
} |
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
error[E0716]: temporary value dropped while borrowed | ||
--> $DIR/wf-in-where-clause-static.rs:18:18 | ||
| | ||
LL | let s = foo(&String::from("blah blah blah")); | ||
| -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- temporary value is freed at the end of this statement | ||
| | | | ||
| | creates a temporary value which is freed while still in use | ||
| argument requires that borrow lasts for `'static` | ||
|
||
error: aborting due to 1 previous error | ||
|
||
For more information about this error, try `rustc --explain E0716`. |
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
error[E0716]: temporary value dropped while borrowed | ||
--> $DIR/wf-in-where-clause-static.rs:18:18 | ||
| | ||
LL | let s = foo(&String::from("blah blah blah")); | ||
| -----^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^-- temporary value is freed at the end of this statement | ||
| | | | ||
| | creates a temporary value which is freed while still in use | ||
| argument requires that borrow lasts for `'static` | ||
|
||
error: aborting due to 1 previous error | ||
|
||
For more information about this error, try `rustc --explain E0716`. |
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