Return early when treating ambiguous cycles

src/solve/solver.rs

@@ -183,12 +183,20 @@ impl Solver {
             match self.cycle_strategy {
                 CycleStrategy::Tabling if slot.cycle => {
                     let actual_answer = result.as_ref().ok().map(|s| s.clone());
-                    if actual_answer == answer {
-                        // Fixed point: break
-                        return result;
-                    } else {
-                        answer = actual_answer;
-                    }
+                    let fixed_point = answer == actual_answer;
+
+                    // If we reach a fixed point, we can break.
+                    // If the answer is `Ambig`, then we know that we already have multiple
+                    // solutions, and we *must* break because an `Ambig` solution may not perform
+                    // any unification and thus fail to correctly reach a fixed point. See test
+                    // `multiple_ambiguous_cycles`.
+                    match (fixed_point, &actual_answer) {
+                        (_, &Some(Solution::Ambig(_))) | (true, _) =>
+                            return result,
+                        _ => ()
+                    };
+
+                    answer = actual_answer;
                 }
                 _ => return result,
             };

src/solve/test.rs

@@ -291,6 +291,52 @@ fn cycle_unique_solution() {
     }
 }
 
+#[test]
+fn multiple_ambiguous_cycles() {
+    test! {
+        program {
+            trait WF { }
+            trait Sized { }
+
+            struct Vec<T> { }
+            struct Int { }
+
+            impl Sized for Int { }
+            impl WF for Int { }
+
+            impl<T> WF for Vec<T> where T: Sized { }
+            impl<T> Sized for Vec<T> where T: WF, T: Sized { }
+        }
+
+        //          ?T: WF
+        //             |
+        //             |
+        //             |
+        // Int: WF. <-----> (Vec<?T>: WF) :- (?T: Sized)
+        //                              |
+        //                              |
+        //                              |
+        //              Int: Sized. <-------> (Vec<?T>: Sized) :- (?T: Sized), (?T: WF)
+        //                                                            |            |
+        //                                                            |            |
+        //                                                            |            |
+        //                                                          cycle        cycle
+        //
+        // Depending on the evaluation order of the above tree (which cycle we come upon first),
+        // we may fail to reach a fixed point if we loop continuously because `Ambig` does not perform
+        // any unification. We must stop looping as soon as we encounter `Ambig`. In fact without
+        // this strategy, the above program will not even be loaded because of the overlap check which
+        // will loop forever.
+        goal {
+            exists<T> {
+                T: WF
+            }
+        } yields {
+            "Ambig"
+        }
+    }
+}
+
 #[test]
 fn normalize_basic() {
     test! {