Rust can't figure out that same types are same with two types that are the associated type of each other.

I tried this code:

trait Foo {
    type ToBar;
}

trait Bar {
    type ToFoo: Foo<ToBar = Self>;
}

trait SubFoo: Foo {
    type SubToBar: Bar<ToFoo = Self>;
}

fn works<F: SubFoo>(x: F::SubToBar) -> F::ToBar {
    fn helper<B: Bar>(x: B) -> <B::ToFoo as Foo>::ToBar {
        x
    }

    helper::<F::SubToBar>(x)
}

fn fails<F: SubFoo>(x: F::SubToBar) -> F::ToBar {
    x
}

I expected the code to compile. However, the works function compiles, while the fails function fails to compile, producing the error:

error[E0308]: mismatched types
  --> src/lib.rs:22:5
   |
21 | fn fails<F: SubFoo>(x: F::SubToBar) -> F::ToBar {
   |                                        -------- expected `<F as Foo>::ToBar` because of return type
22 |     x
   |     ^ expected `Foo::ToBar`, found `SubFoo::SubToBar`
   |
   = note: expected associated type `<F as Foo>::ToBar`
              found associated type `<F as SubFoo>::SubToBar`
   = note: an associated type was expected, but a different one was found

For more information about this error, try `rustc --explain E0308`.

For every SubFoo type, the ToBar and SubToBar associated types will always be the same (Self::ToBar == Self::SubToBar). This can be proven from by the following chain of reasoning for any type F: SubFoo:

<F as SubFoo>::SubToBar
== <<<F as SubFoo>::SubToBar as Bar>::ToFoo as Foo>::ToBar
(from applying the trait bound  `ToFoo: Foo<ToBar = Self>`  to the type  `<F as SubFoo>::SubToBar`)
== <F as Foo>::ToBar
(from applying the trait bound  `SubToBar: Bar<ToFoo = Self>` to the type  `F`)

It seems like the trait solver can't figure this out by itself. But prodding it with the helper() function makes it able to figure this out. This workaround is rather inconvenient though, and it would be nice if the trait solver can figure this out itself, or if there were some way to give hints to the trait solver to reach this conclusion.

Note: my attempts to simplify things have repeatedly ran into the problem described at #65913. Also, the original use case had GATs, which made associated type bounds not usable on the Foo/SubFoo traits.

Meta

Reproducible on the playground with stable rust version 1.84.0, and nightly rust version 1.86.0-nightly (2025-01-23 99768c80a1c094a5cfc3)

Using -Z next-solver=globally doesn't fix the problem.

@rustbot labels +A-trait-system +A-associated-items

Start by reproducing the example in src/lib.rs with stable Rust 1.84.0 and the noted nightly version, comparing the compiling works function with the failing fails function. Investigate the trait solver behavior for the associated-type equality chain and the helper workaround; done means the direct fails case compiles without helper, including with the next solver enabled.