rust-lang / trait-system-refactor-initiative

The Rustc Trait System Refactor Initiative
21 stars 0 forks source link

eagerly proving nested goals + incompleteness -> breakage #97

Open lcnr opened 8 months ago

lcnr commented 8 months ago
trait ConstrainArgEnv<U> {}
impl<T, U> ConstrainArgEnv<U> for T {}

trait ConstrainArgImpl<U> {}
impl<T> ConstrainArgImpl<()> for T {}

trait Shallow<U> {}
impl<T: ConstrainArgEnv<U>, U> Shallow<U> for T {}

// Make sure to first prove `T: Shallow<?0>`, then `T: ConstrainArgImpl<?0>`.
fn add_bounds<T: Shallow<U> + ConstrainArgImpl<U> + Shallow<U>, U>() {}

fn foo<T: ConstrainArgEnv<T>>() {
    add_bounds::<T, _>();
}

fn main() {
    foo::<()>();
}

compiles with the old solver, errors with new:

error[E0277]: the trait bound `T: ConstrainArgImpl<T>` is not satisfied
  --> src/main.rs:13:18
   |
13 |     add_bounds::<T, _>();
   |                  ^ the trait `ConstrainArgImpl<T>` is not implemented for `T`
   |
note: required by a bound in `add_bounds`
  --> src/main.rs:10:31
   |
10 | fn add_bounds<T: Shallow<U> + ConstrainArgImpl<U>, U>() {}
   |                               ^^^^^^^^^^^^^^^^^^^ required by this bound in `add_bounds`
help: consider further restricting this bound
   |
12 | fn foo<T: ConstrainArgEnv<T> + ConstrainArgImpl<T>>() {
   |                              +++++++++++++++++++++

In the old solver T: Shallow<?0> succeeds, returning a nested T: ConstrainArgEnv<?0> goal. Proving that would incompletely constrain ?0 to T. However, the old solver first proves the other goal T: ConstrainArgImpl<?0> which constrains ?0 to (). At this point ConstrainArgEnv also uses the impl candidates