Enforce supertrait outlives obligations hold when confirming impl by compiler-errors · Pull Request #124336 · rust-lang/rust (original) (raw)

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:

use std::fmt::Display;

trait Static: 'static {} impl Static for &'static T {} fn foo<S: Display>(x: S) -> Box 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:

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.