Guard against infinite loop in recursive solver

chalk-recursive/src/fulfill.rs

@@ -447,9 +447,17 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
                             solution,
                         } = self.prove(wc, minimums)?;
 
-                        if solution.has_definite() {
-                            if let Some(constrained_subst) =
-                                solution.constrained_subst(self.interner())
+                        if let Some(constrained_subst) = solution.definite_subst(self.interner()) {
+                            // If the substitution is empty, we won't actually make any progress by applying it!
+                            // So we need to check this to prevent endless loops.
+                            // (An ambiguous solution with empty substitution
+                            // can probably not happen in valid code, but it can
+                            // happen e.g. when there are overlapping impls.)
+                            if !constrained_subst.value.subst.is_empty(self.interner())
+                                || !constrained_subst
+                                    .value
+                                    .constraints
+                                    .is_empty(self.interner())
                             {
                                 self.apply_solution(free_vars, universes, constrained_subst);
                                 progress = true;

chalk-recursive/src/lib.rs

@@ -148,12 +148,21 @@ impl<I: Interner> Solution<I> {
     }
 
     /// Determine whether this solution contains type information that *must*
-    /// hold.
-    pub(crate) fn has_definite(&self) -> bool {
-        match *self {
-            Solution::Unique(_) => true,
-            Solution::Ambig(Guidance::Definite(_)) => true,
-            _ => false,
+    /// hold, and returns the subst in that case.
+    pub(crate) fn definite_subst(&self, interner: &I) -> Option<Canonical<ConstrainedSubst<I>>> {
+        match self {
+            Solution::Unique(constrained) => Some(constrained.clone()),
+            Solution::Ambig(Guidance::Definite(canonical)) => {
+                let value = ConstrainedSubst {
+                    subst: canonical.value.clone(),
+                    constraints: Constraints::empty(interner),
+                };
+                Some(Canonical {
+                    value,
+                    binders: canonical.binders.clone(),
+                })
+            }
+            _ => None,
         }
     }
 

tests/test/misc.rs

@@ -727,3 +727,35 @@ fn canonicalization_regression() {
         }
     }
 }
+
+#[test]
+fn empty_definite_guidance() {
+    test! {
+        disable_coherence;
+        program {
+            trait Trait<T> {}
+
+            struct S<'a> {}
+            struct A {}
+
+            impl<'a> Trait<S<'a>> for A {}
+            impl<'a> Trait<S<'a>> for A where A: 'a {}
+
+            trait OtherTrait<'a> {}
+            impl<'a> OtherTrait<'a> for A where A: Trait<S<'a>> {}
+        }
+
+        goal {
+            forall<'static> {
+                A: OtherTrait<'static>
+            }
+            // the program fails coherence, so which answer we get here exactly
+            // isn't that important -- this is mainly a regression test for a
+            // recursive solver infinite loop.
+        } yields[SolverChoice::slg_default()] {
+            "Unique"
+        } yields[SolverChoice::recursive()] {
+            "Ambiguous"
+        }
+    }
+}

tests/test/mod.rs

@@ -49,7 +49,11 @@ pub enum TestGoal {
 macro_rules! test {
     (program $program:tt $($goals:tt)*) => {{
         let (program, goals) = parse_test_data!(program $program $($goals)*);
-        solve_goal(program, goals)
+        solve_goal(program, goals, true)
+    }};
+    (disable_coherence; program $program:tt $($goals:tt)*) => {{
+        let (program, goals) = parse_test_data!(program $program $($goals)*);
+        solve_goal(program, goals, false)
     }};
 }
 
@@ -215,7 +219,7 @@ macro_rules! parse_test_data {
     };
 }
 
-fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) {
+fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>, coherence: bool) {
     with_tracing_logs(|| {
         println!("program {}", program_text);
         assert!(program_text.starts_with("{"));
@@ -226,7 +230,11 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) {
             SolverChoice::default(),
         );
 
-        let program = db.checked_program().unwrap();
+        let program = if coherence {
+            db.checked_program().unwrap()
+        } else {
+            db.program_ir().unwrap()
+        };
 
         for (goal_text, solver_choice, expected) in goals {
             match (&solver_choice, &expected) {