Recursive solver hangs on cyclic traits

[detrumi]

Found in rust-analyzer#12897, the following test causes the recursive solver to loop:

#[test]
fn cyclic_traits() {
    test! {
        program {
            trait Clone { }
            trait A {
                type X: B;
            }
            trait B {
                type Y: A<X = Self>;
            }
        }

        goal {
            exists<T> {
                if (<T as B>::Y: A) {
                    if (<<T as B>::Y as A>::X: Clone) {
                        T: A
                    }
                }
            }
        } yields {
            expect![["Ambiguous; no inference guidance"]]
        }
    }
}

Output:

comparing solvers:
        expected: SLG { max_size: 10, expected_answers: None }
        actual: Recursive { overflow_depth: 100, caching_enabled: true, max_size: 30 }

expected:
Ambiguous; no inference guidance
actual:
Ambiguous; definite substitution for<?U0> { [?0 := (B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<(B::Y)<(A::X)<^0.0>>>>>>>>>>>>>>>>>>>>>>>>>>>>] }
thread 'test::cycle::cyclic_traits' panicked at 'assertion failed: `(left == right)`

[detrumi]

Slightly simpler repro, this one from rust-lang/rust-analyzer#12667. Hangs even with default depth.

#[test]
fn ra_12667() {
    test! {
        program {
            trait Clone { }
            trait A {
                type X: B;
            }
            trait B {
                type Y: A<X = Self>;
            }
        }

        goal {
            exists<T> {
                if (T: A) {
                    <T as A>::X: Clone
                }
            }
        } yields[SolverChoice::recursive_default()] {
            expect![["No possible solution"]]
        }
    }
}

[detrumi]

So it's expanding the goals like this:

AliasEq(<(B::Y)<^0.0> as A>::X = ^0.1)
AliasEq(<(A::X)<(B::Y)<^0.0>> as B>::Y = ^0.1),
AliasEq(<(B::Y)<(A::X)<(B::Y)<^0.0>>> as A>::X = ^0.1)

which replaces <(B::Y)<^0.0> with <(B::Y)<(A::X)<(B::Y)<^0.0>>>, and then the solver just repeatedly expands the left side. And because the goal keeps expanding, it's not triggering the cycle detection.

Do we need to start inspecting substitutions/goals for such repetitions, or is there a better solution?

[mgjm]

I ran into another variant of this problem. The following code also hangs with rust-analyzer analysis-stats . on the function outer:

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

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

type Inner<A> = <<A as Foo>::Bar as Bar>::Foo;

fn inner<A: Foo>(val: Inner<A>) -> A {
    val
}

fn outer<A: Foo>(val: Inner<A>) -> A {
    let ret = inner(val);
    ret
}

I think this is the same underlying problem, but I also wanted to share this variation to trigger the problem.