From b2778196f11d32489e26e1d63d9b8fa5b6f25dcf Mon Sep 17 00:00:00 2001
From: Florian Diebold <flodiebold@gmail.com>
Date: Sat, 11 Jul 2020 16:10:58 +0200
Subject: [PATCH 1/2] 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 |  9 ++++++---
 chalk-recursive/src/lib.rs     | 21 +++++++++++++++------
 tests/test/misc.rs             | 31 +++++++++++++++++++++++++++++++
 3 files changed, 52 insertions(+), 9 deletions(-)

diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs
index 63d597923f5..a30c8237e2f 100644
--- a/chalk-recursive/src/fulfill.rs
+++ b/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;
diff --git a/chalk-recursive/src/lib.rs b/chalk-recursive/src/lib.rs
index ff4caabbedf..77e01cdd606 100644
--- a/chalk-recursive/src/lib.rs
+++ b/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,
         }
     }
 
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
index 8ad6c638d83..28ab66f6685 100644
--- a/tests/test/misc.rs
+++ b/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"
+        }
+    }
+}

From 3b138082ffd6913895fbbd6f865cf9a8ccfa7026 Mon Sep 17 00:00:00 2001
From: Florian Diebold <flodiebold@gmail.com>
Date: Mon, 3 Aug 2020 14:52:36 +0200
Subject: [PATCH 2/2] Make it possible to disable coherence checks in tests and
 use that

... to make the infinite loop regression test work.
---
 chalk-recursive/src/fulfill.rs |  5 +++++
 tests/test/misc.rs             |  7 ++++---
 tests/test/mod.rs              | 14 +++++++++++---
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs
index a30c8237e2f..b2cf64cf1cd 100644
--- a/chalk-recursive/src/fulfill.rs
+++ b/chalk-recursive/src/fulfill.rs
@@ -448,6 +448,11 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
                         } = self.prove(wc, minimums)?;
 
                         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
diff --git a/tests/test/misc.rs b/tests/test/misc.rs
index 28ab66f6685..23ddd2591ad 100644
--- a/tests/test/misc.rs
+++ b/tests/test/misc.rs
@@ -729,11 +729,9 @@ 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! {
+        disable_coherence;
         program {
             trait Trait<T> {}
 
@@ -751,6 +749,9 @@ fn empty_definite_guidance() {
             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()] {
diff --git a/tests/test/mod.rs b/tests/test/mod.rs
index 5bdb2789da4..b10e4a45ad2 100644
--- a/tests/test/mod.rs
+++ b/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) {