add test for coinduction in new solver

3 files changed, 80 insertions, 2 deletions

diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs
index e56588c58bd..38a86d55a2c 100644
--- a/compiler/rustc_trait_selection/src/solve/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/mod.rs
@@ -265,12 +265,18 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
         // call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
         // could constrain `U` to `u32` which would cause this check to result in a
         // solver cycle.
-        if cfg!(debug_assertions) && has_changed && !self.in_projection_eq_hack {
+        if cfg!(debug_assertions)
+            && has_changed
+            && !self.in_projection_eq_hack
+            && !self.search_graph.in_cycle()
+        {
             let mut orig_values = OriginalQueryValues::default();
             let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
             let canonical_response =
                 EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
-            assert!(canonical_response.value.var_values.is_identity());
+            if !canonical_response.value.var_values.is_identity() {
+                bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}");
+            }
             assert_eq!(certainty, canonical_response.value.certainty);
         }
 
diff --git a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
index a2ca4bc189c..e989c9145d1 100644
--- a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
+++ b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs
@@ -42,6 +42,24 @@ impl<'tcx> SearchGraph<'tcx> {
             && !self.overflow_data.did_overflow()
     }
 
+    /// Whether we're currently in a cycle. This should only be used
+    /// for debug assertions.
+    pub(super) fn in_cycle(&self) -> bool {
+        if let Some(stack_depth) = self.stack.last() {
+            // Either the current goal on the stack is the root of a cycle...
+            if self.stack[stack_depth].has_been_used {
+                return true;
+            }
+
+            // ...or it depends on a goal with a lower depth.
+            let current_goal = self.stack[stack_depth].goal;
+            let entry_index = self.provisional_cache.lookup_table[&current_goal];
+            self.provisional_cache.entries[entry_index].depth != stack_depth
+        } else {
+            false
+        }
+    }
+
     /// Tries putting the new goal on the stack, returning an error if it is already cached.
     ///
     /// This correctly updates the provisional cache if there is a cycle.
diff --git a/tests/ui/coinduction/canonicalization-rerun.rs b/tests/ui/coinduction/canonicalization-rerun.rs
new file mode 100644
index 00000000000..b10ba3a810f
--- /dev/null
+++ b/tests/ui/coinduction/canonicalization-rerun.rs
@@ -0,0 +1,54 @@
+// check-pass
+// revisions: old new
+//[new] compile-flags: -Ztrait-solver=next
+
+// If we use canonical goals during trait solving we have to reevaluate
+// the root goal of a cycle until we hit a fixpoint.
+//
+// Here `main` has a goal `(?0, ?1): Trait` which is canonicalized to
+// `exists<^0, ^1> (^0, ^1): Trait`.
+//
+// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
+//   -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
+//     - COINDUCTIVE CYCLE OK (no constraints)
+//   - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
+//     - OK (^0 = u32 -apply-> ?0 = u32)
+//   - OK (?0 = u32 -canonicalize-> ^0 = u32)
+//   - coinductive cycle with provisional result != final result, rerun
+//
+// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
+//   -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
+//     - COINDUCTIVE CYCLE OK (^0 = u32 -apply-> ?1 = u32)
+//   - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
+//     - OK (^0 = u32 -apply-> ?1 = u32)
+//   - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32)
+//   - coinductive cycle with provisional result != final result, rerun
+//
+// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait`
+//   -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait`
+//     - COINDUCTIVE CYCLE OK (^0 = u32, ^1 = u32 -apply-> ?1 = u32, ?0 = u32)
+//   - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>`
+//     - OK (^0 = u32 -apply-> ?1 = u32)
+//   - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32)
+//   - coinductive cycle with provisional result == final result, DONE
+#![feature(rustc_attrs)]
+#[rustc_coinductive]
+trait Trait {}
+
+impl<T, U> Trait for (T, U)
+where
+    (U, T): Trait,
+    (): ConstrainToU32<T>,
+{}
+
+trait ConstrainToU32<T> {}
+impl ConstrainToU32<u32> for () {}
+
+fn impls_trait<T, U>()
+where
+    (T, U): Trait,
+{}
+
+fn main() {
+    impls_trait::<_, _>();
+}