Skip to content

eagerly proving nested goals + incompleteness -> breakage #97

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lcnr opened this issue Feb 27, 2024 · 0 comments
Open

eagerly proving nested goals + incompleteness -> breakage #97

lcnr opened this issue Feb 27, 2024 · 0 comments

Comments

@lcnr
Copy link
Contributor

lcnr commented Feb 27, 2024

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

@lcnr lcnr moved this to potentially irrelevant in -Znext-solver=globally Jan 29, 2025
@lcnr lcnr moved this from potentially irrelevant to accepted breakage in -Znext-solver=globally Jan 29, 2025
@lcnr lcnr moved this from accepted breakage to potentially irrelevant in -Znext-solver=globally Jan 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Status: potentially irrelevant
Development

No branches or pull requests

1 participant