Auto merge of #752 - Dirbaio:fix-recursive-hang, r=jackh726

recursive: fix hang on fulfill by slightly smarter check for progress.

This fixes a hang using the recursive solver when trying to prove `exists<'a, T> { if(T: 'a) { WellFormed(&'a T) } }`.

<details>
<summary>Snippet of the log when looping</summary>

            617ms DEBUG start of round, 2 obligations
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
            618ms DEBUG fulfill::apply_solution: adding constraints []
            618ms DEBUG unify(?2, ?1140) succeeded
            618ms DEBUG unify: goals=[]
            618ms DEBUG unify('?3, '?1141) succeeded
            618ms DEBUG unify: goals=[]
            618ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 })
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown))
            618ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) })
            618ms DEBUG end of round, 2 obligations left

            618ms DEBUG start of round, 2 obligations
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown))
            619ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) })
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
            619ms DEBUG fulfill::apply_solution: adding constraints []
            619ms DEBUG unify(?2, ?1142) succeeded
            619ms DEBUG unify: goals=[]
            619ms DEBUG unify('?3, '?1143) succeeded
            619ms DEBUG unify: goals=[]
            619ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 })
            619ms DEBUG end of round, 2 obligations left

            619ms DEBUG start of round, 2 obligations
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: ^0.0: '^0.1 }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Definite(Canonical { value: [?0 := ^0.0, ?1 := '^0.1], binders: [U0 with kind type, U0 with kind lifetime] })))
            620ms DEBUG fulfill::apply_solution: adding constraints []
            620ms DEBUG unify(?2, ?1144) succeeded
            620ms DEBUG unify: goals=[]
            620ms DEBUG unify('?3, '?1145) succeeded
            620ms DEBUG unify: goals=[]
            620ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 })
            prove wc=InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) }
              solve_goal goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }
                0ms DEBUG Cache hit, goal=UCanonical { canonical: Canonical { value: InEnvironment { environment: Env([for<> ^1.0: '^1.1]), goal: WellFormed(^0.0) }, binders: [U0 with kind type, U0 with kind lifetime] }, universes: 1 }, result=Ok(Ambig(Unknown))
                0ms DEBUG solve_reduced_goal: cache hit, value=Ok(Ambig(Unknown))
            620ms DEBUG ambiguous result: Prove(InEnvironment { environment: Env([for<> ?0: '?1]), goal: WellFormed(?2) })
            620ms DEBUG end of round, 2 obligations left
</details>

The issue is:

- it tries to prove `InEnvironment { environment: Env([for<> ?0: '?1]), goal: ?2: '?3 }`
- it gets "useless" substs `[?0 := ^0.0, ?1 := '^0.1]`
- it applies them, they cause nothing to change but it thinks they did
- so in next round it processes again the exact same obligation...

There was already an `if` treating empty substs as "useless", this extends it to treating trivial subs as "useless". (empty substs are also trivial).

Author: bors

chalk-recursive/src/fulfill.rs

@@ -6,10 +6,10 @@ use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::visit::Visit;
 use chalk_ir::zip::Zip;
 use chalk_ir::{
-    Binders, Canonical, ConstrainedSubst, Constraint, Constraints, DomainGoal, Environment, EqGoal,
-    Fallible, GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClauseImplication,
-    QuantifierKind, Substitution, SubtypeGoal, TyKind, TyVariableKind, UCanonical,
-    UnificationDatabase, UniverseMap, Variance,
+    Binders, BoundVar, Canonical, ConstrainedSubst, Constraint, Constraints, DomainGoal,
+    Environment, EqGoal, Fallible, GenericArg, GenericArgData, Goal, GoalData, InEnvironment,
+    NoSolution, ProgramClauseImplication, QuantifierKind, Substitution, SubtypeGoal, TyKind,
+    TyVariableKind, UCanonical, UnificationDatabase, UniverseMap, Variance,
 };
 use chalk_solve::debug_span;
 use chalk_solve::infer::{InferenceTable, ParameterEnaVariableExt};
@@ -466,17 +466,19 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>> Fulfill<'s, I, Solver> {
                         } = self.prove(wc.clone(), 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!
+                            // If the substitution is trivial, 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())
-                            {
+                            let nontrivial_subst = !is_trivial_canonical_subst(
+                                self.interner(),
+                                &constrained_subst.value.subst,
+                            );
+
+                            let has_constraints = !constrained_subst
+                                .value
+                                .constraints
+                                .is_empty(self.interner());
+
+                            if nontrivial_subst || has_constraints {
                                 self.apply_solution(free_vars, universes, constrained_subst);
                                 progress = true;
                             }
@@ -608,3 +610,28 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>> Fulfill<'s, I, Solver> {
         self.solver.interner()
     }
 }
+
+fn is_trivial_canonical_subst<I: Interner>(interner: I, subst: &Substitution<I>) -> bool {
+    // A subst is trivial if..
+    subst.iter(interner).enumerate().all(|(index, parameter)| {
+        let is_trivial = |b: Option<BoundVar>| match b {
+            None => false,
+            Some(bound_var) => {
+                if let Some(index1) = bound_var.index_if_innermost() {
+                    index == index1
+                } else {
+                    false
+                }
+            }
+        };
+
+        match parameter.data(interner) {
+            // All types and consts are mapped to distinct variables. Since this
+            // has been canonicalized, those will also be the first N
+            // variables.
+            GenericArgData::Ty(t) => is_trivial(t.bound_var(interner)),
+            GenericArgData::Const(t) => is_trivial(t.bound_var(interner)),
+            GenericArgData::Lifetime(t) => is_trivial(t.bound_var(interner)),
+        }
+    })
+}

tests/test/misc.rs

@@ -826,3 +826,22 @@ fn env_bound_vars() {
         }
     }
 }
+
+#[test]
+fn recursive_hang() {
+    test! {
+        program {}
+
+        goal {
+            exists<'a, T> {
+                if(T: 'a) {
+                    WellFormed(&'a T)
+                }
+            }
+        } yields[SolverChoice::slg_default()] {
+            expect![["Ambiguous; definite substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
+        } yields[SolverChoice::recursive_default()] {
+            expect![["Ambiguous; suggested substitution for<?U0,?U0> { [?0 := ^0.0, ?1 := '^0.1] }"]]
+        }
+    }
+}