Endless loop in recursive solver

[flodiebold]

#[test]
fn endless_loop() {
    test! {
        disable_coherence;
        program {
            trait FnOnce {
                type Output;
            }

            struct MyClosure<F> {}
            impl<T> FnOnce for MyClosure<fn() -> T> {
                type Output = T;
            }
        }
        goal {
            exists<T> {
                <MyClosure<fn() -> T> as FnOnce>::Output = T
            }
        } yields[SolverChoice::recursive_default()] {
            "Unique; for<?U0> { substitution [?0 := ^0.0], lifetime constraints [] }"
        }
    }
}

This hangs forever in the recursive solver; in the SLG solver, it results in Ambiguous; no inference guidance, which seems wrong as well? Replacing fn() -> T by T makes the test succeed (in both solvers).

CC rust-lang/rust-analyzer#6945.

[jackh726]

I wouldn't be surprised if the ambiguity in SLG is because of #234. Not sure why recursive solver is having problems though.

[jackh726]

Ugh no. SLG is failing because when trying to solve AliasEq(<MyClosure<"rust" for<0> [?0 := ?0]> as FnOnce>::Output = ?0) we end up with

          floundered_subgoals: [
              FlounderedSubgoal {
                  floundered_literal: Positive(
                      InEnvironment {
                          environment: Env([]),
                          goal: Normalize(<MyClosure<"rust" for<0> [?0 := ?1]> as FnOnce>::Output -> ?0),
                      },
                  ),
                  floundered_time: TimeStamp {
                      clock: 0,
                  },
              },
              FlounderedSubgoal {
                  floundered_literal: Positive(
                      InEnvironment {
                          environment: Env([]),
                          goal: (?1 <: ?0),
                      },
                  ),
                  floundered_time: TimeStamp {
                      clock: 0,
                  },
              },
              FlounderedSubgoal {
                  floundered_literal: Positive(
                      InEnvironment {
                          environment: Env([]),
                          goal: (?0 <: ?1),
                      },
                  ),
                  floundered_time: TimeStamp {
                      clock: 0,
                  },
              },
          ],

Have to look more into the details here, but yeah seems to be a generalizer issue. For the recursive solver, I wonder if we're constantly retrying to solve the subtyping goals. Haven't looked at it yet.

[jackh726]

More specifically, we have a goal: AliasEq(<MyClosure<"rust" for<0> [?0 := ^1.0]> as FnOnce>::Output = ^0.0)
We get a program clause: for<type> AliasEq(<^0.0 as FnOnce>::Output = (FnOnce::Output)<^0.0>)
We try to relate with Invariant:

a=AliasEq(<MyClosure<"rust" for<0> [?0 := ?0]> as FnOnce>::Output = ?0)
b=AliasEq(<?1 as FnOnce>::Output = (FnOnce::Output)<?1>)

?1 generalized to MyClosure<"rust" for<0> [?0 := ?2]>

then relate

a=MyClosure<"rust" for<0> [?0 := ?2]>
b=MyClosure<"rust" for<0> [?0 := ?0]>

leading to

?2 <: ?0
?0 <: ?2

We get a similar situation for the other program clause that gets generated. But it doesn't matter, because ?2 <: ?0 and ?0 <: ?2 aren't solvable and we also can't make progress on the Normalize goal

[jackh726]

We get a similar situation for the other program clause that gets generated. But it doesn't matter, because ?2 <: ?0 and ?0 <: ?2 aren't solvable and we also can't make progress on the Normalize goal

Without going into all the same details, we try to relate

a=Normalize(<MyClosure<"rust" for<0> [?0 := ?0]> as FnOnce>::Output -> ?1)
b=Normalize(<MyClosure<"rust" for<0> [?0 := ?2]> as FnOnce>::Output -> ?2)

which obviously fails for the same reason: both ?0 and ?2` are under binders, so rather than being unified, they are related in both directions.