Skip to content

eagerly proving nested goals + incompleteness -> breakage #97

Open
@lcnr

Description

@lcnr
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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions