diff --git a/src/solve/solver.rs b/src/solve/solver.rs index 31a3b7ba036..545e2707287 100644 --- a/src/solve/solver.rs +++ b/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, }; diff --git a/src/solve/test.rs b/src/solve/test.rs index 0f36bae5843..5ba31a533cd 100644 --- a/src/solve/test.rs +++ b/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 { } + struct Int { } + + impl Sized for Int { } + impl WF for Int { } + + impl WF for Vec where T: Sized { } + impl Sized for Vec where T: WF, T: Sized { } + } + + // ?T: WF + // | + // | + // | + // Int: WF. <-----> (Vec: WF) :- (?T: Sized) + // | + // | + // | + // Int: Sized. <-------> (Vec: 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: WF + } + } yields { + "Ambig" + } + } +} + #[test] fn normalize_basic() { test! {