Unexpected "impl has stricter requirements" with identical bounds

[afetisov]

I tried this code (playground):

trait Bar<T> {}

impl<T> Bar<T> for () {}

trait Foo<C> {
    type Out;
}

trait Quux {
    type A;

    fn quux<R>()
    where
        R: Foo<Self::A>,
        (): Bar<<R as Foo<Self::A>>::Out>,
    ;
}

impl Quux for () {
    type A = ();

    fn quux<R>()
    where
        R: Foo<Self::A>,
        (): Bar<<R as Foo<Self::A>>::Out>,
    {}
}

I expected to see this happen: the code compiles successfully.

Instead, this happened:

error[E0277]: the trait bound `R: Foo<()>` is not satisfied
  --> src/lib.rs:22:5
   |
22 | /     fn quux<R>()
23 | |     where
24 | |         R: Foo<Self::A>,
25 | |         (): Bar<<R as Foo<Self::A>>::Out>,
   | |__________________________________________^ the trait `Foo<()>` is not implemented for `R`

error[E0276]: impl has stricter requirements than trait
  --> src/lib.rs:24:12
   |
12 | /     fn quux<R>()
13 | |     where
14 | |         R: Foo<Self::A>,
15 | |         (): Bar<<R as Foo<Self::A>>::Out>,
16 | |     ;
   | |_____- definition of `quux` from trait
...
24 |           R: Foo<Self::A>,
   |              ^^^^^^^^^^^^ impl has extra requirement `R: Foo<()>`

error[E0277]: the trait bound `R: Foo<()>` is not satisfied
  --> src/lib.rs:22:8
   |
22 |     fn quux<R>()
   |        ^^^^ the trait `Foo<()>` is not implemented for `R`

error[E0277]: the trait bound `R: Foo<()>` is not satisfied
  --> src/lib.rs:25:13
   |
25 |         (): Bar<<R as Foo<Self::A>>::Out>,
   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ the trait `Foo<()>` is not implemented for `R`
   |
note: required by a bound in `Bar`
  --> src/lib.rs:1:11
   |
1  | trait Bar<T> {}
   |           ^ required by this bound in `Bar`

This error reproduces on stable-1.85, corresponding beta branch, and the nightly-2025-02-24 compiler.

[compiler-errors]

There's a few other bugs of this sort, perhaps take a look at the label fixed-by-next-solver. It has to do with certain kinds of conditions where the old trait solver gets confused about associated type bounds that can be "normalized" or simplified using themselves.