Guard against infinite loop in recursive solver

This happened in some tests in rust-analyzer. I think it can only happen with
overlapping impls, so I don't know how to actually test it. (In rust-analyzer,
it happened because of built-in impls provided both by RA and now Chalk.)

chalk-recursive/src/fulfill.rs

@@ -447,9 +447,12 @@ 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 !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,34 @@ fn canonicalization_regression() {
         }
     }
 }
+
+#[test]
+#[ignore]
+// this is a regression test for an infinite loop, but it doesn't actually work
+// because the code fails coherence checking.
+fn empty_definite_guidance() {
+    test! {
+        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>
+            }
+        } yields[SolverChoice::slg_default()] {
+            "Unique"
+        } yields[SolverChoice::recursive()] {
+            "Ambiguous"
+        }
+    }
+}