rust-lang · bors · Nov 1, 2020 · Nov 1, 2020
diff --git a/chalk-integration/src/lib.rs b/chalk-integration/src/lib.rs
@@ -55,6 +55,7 @@ pub enum SolverChoice {
     Recursive {
         overflow_depth: usize,
         caching_enabled: bool,
+        max_size: usize,
     },
 }
 
@@ -73,10 +74,20 @@ impl SolverChoice {
     }
 
     /// Returns the default recursive solver setup.
-    pub fn recursive() -> Self {
+    pub fn recursive_default() -> Self {
         SolverChoice::Recursive {
             overflow_depth: 100,
             caching_enabled: true,
+            max_size: 30,
+        }
+    }
+
+    /// Returns a recursive solver with specific parameters.
+    pub fn recursive(max_size: usize, overflow_depth: usize) -> Self {
+        SolverChoice::Recursive {
+            overflow_depth,
+            caching_enabled: true,
+            max_size,
         }
     }
 
@@ -89,7 +100,12 @@ impl SolverChoice {
             SolverChoice::Recursive {
                 overflow_depth,
                 caching_enabled,
-            } => Box::new(RecursiveSolver::new(overflow_depth, caching_enabled)),
+                max_size,
+            } => Box::new(RecursiveSolver::new(
+                overflow_depth,
+                max_size,
+                caching_enabled,
+            )),
         }
     }
 }

diff --git a/chalk-recursive/src/fulfill.rs b/chalk-recursive/src/fulfill.rs
@@ -234,7 +234,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
             Obligation::Prove(goal) => {
                 if self
                     .infer
-                    .needs_truncation(self.solver.interner(), 30, goal)
+                    .needs_truncation(self.solver.interner(), self.solver.max_size(), goal)
                 {
                     // the goal is too big. Record that we should return Ambiguous
                     self.cannot_prove = true;
@@ -244,7 +244,7 @@ impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I
             Obligation::Refute(goal) => {
                 if self
                     .infer
-                    .needs_truncation(self.solver.interner(), 30, goal)
+                    .needs_truncation(self.solver.interner(), self.solver.max_size(), goal)
                 {
                     // the goal is too big. Record that we should return Ambiguous
                     self.cannot_prove = true;

diff --git a/chalk-recursive/src/recursive.rs b/chalk-recursive/src/recursive.rs
@@ -24,6 +24,9 @@ struct RecursiveContext<I: Interner> {
     /// result.
     cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
 
+    /// The maximum size for goals.
+    max_size: usize,
+
     caching_enabled: bool,
 }
 
@@ -42,9 +45,13 @@ pub struct RecursiveSolver<I: Interner> {
 }
 
 impl<I: Interner> RecursiveSolver<I> {
-    pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {
+    pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
         Self {
-            ctx: Box::new(RecursiveContext::new(overflow_depth, caching_enabled)),
+            ctx: Box::new(RecursiveContext::new(
+                overflow_depth,
+                max_size,
+                caching_enabled,
+            )),
         }
     }
 }
@@ -76,11 +83,12 @@ impl<T> MergeWith<T> for Fallible<T> {
 }
 
 impl<I: Interner> RecursiveContext<I> {
-    pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {
+    pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
         RecursiveContext {
             stack: Stack::new(overflow_depth),
             search_graph: SearchGraph::new(),
             cache: FxHashMap::default(),
+            max_size,
             caching_enabled,
         }
     }
@@ -291,6 +299,10 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
     fn db(&self) -> &dyn RustIrDatabase<I> {
         self.program
     }
+
+    fn max_size(&self) -> usize {
+        self.context.max_size
+    }
 }
 
 impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {

diff --git a/chalk-recursive/src/solve.rs b/chalk-recursive/src/solve.rs
@@ -24,6 +24,8 @@ pub(super) trait SolveDatabase<I: Interner>: Sized {
         minimums: &mut Minimums,
     ) -> Fallible<Solution<I>>;
 
+    fn max_size(&self) -> usize;
+
     fn interner(&self) -> &I;
 
     fn db(&self) -> &dyn RustIrDatabase<I>;

diff --git a/tests/test/coinduction.rs b/tests/test/coinduction.rs
@@ -219,7 +219,7 @@ fn coinductive_unsound1() {
 
         goal {
             forall<X> { X: C1orC2 }
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
             "Unique; substitution [], lifetime constraints []"
         }
@@ -455,7 +455,7 @@ fn coinductive_multicycle4() {
 
         goal {
             forall<X> { X: Any }
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             // FIXME(chalk#399) recursive solver doesn't handle coinduction correctly
             "Unique; substitution [], lifetime constraints []"
         }

diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs
@@ -165,7 +165,7 @@ fn overflow() {
             S<Z>: Q
         } yields[SolverChoice::slg(10, None)] {
             "Ambiguous; no inference guidance"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous; no inference guidance"
         }
     }

diff --git a/tests/test/existential_types.rs b/tests/test/existential_types.rs
@@ -413,7 +413,7 @@ fn dyn_associated_type_binding() {
                     <dyn FnOnce<(), Output = i32> + 's as FnOnce<()>>::Output = T
                 }
             }
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Int(I32)], lifetime constraints []"
         } yields[SolverChoice::slg_default()] {
             // #234

diff --git a/tests/test/misc.rs b/tests/test/misc.rs
@@ -130,7 +130,7 @@ fn only_draw_so_many() {
             exists<T> { T: Sized }
         } yields[SolverChoice::slg(10, Some(2))] {
             "Ambiguous; no inference guidance"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous; no inference guidance"
         }
     }
@@ -158,7 +158,7 @@ fn only_draw_so_many_blow_up() {
             exists<T> { T: Foo }
         } yields[SolverChoice::slg(10, Some(2))] {
             "Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
         }
     }
@@ -696,7 +696,7 @@ fn not_really_ambig() {
             exists<T> { Vec<T>: A }
         } yields[SolverChoice::slg_default()] {
             "Unique; substitution [?0 := Uint(U32)], lifetime constraints []"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous; no inference guidance"
         }
     }
@@ -754,7 +754,7 @@ fn empty_definite_guidance() {
             // recursive solver infinite loop.
         } yields[SolverChoice::slg_default()] {
             "Unique"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous"
         }
     }

diff --git a/tests/test/mod.rs b/tests/test/mod.rs
@@ -77,7 +77,7 @@ macro_rules! parse_test_data {
               @parsed_goals[
                   $($parsed_goals)*
                       (stringify!($goal), SolverChoice::slg_default(), TestGoal::Aggregated($expected))
-                      (stringify!($goal), SolverChoice::recursive(), TestGoal::Aggregated($expected))
+                      (stringify!($goal), SolverChoice::recursive_default(), TestGoal::Aggregated($expected))
               ]
               @unparsed_goals[$($unparsed_goals)*])
     };

diff --git a/tests/test/opaque_types.rs b/tests/test/opaque_types.rs
@@ -166,7 +166,7 @@ fn opaque_generics() {
             }
         } yields[SolverChoice::slg_default()] {
             "Ambiguous" // #234
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Bar], lifetime constraints []"
         }
     }

diff --git a/tests/test/projection.rs b/tests/test/projection.rs
@@ -142,7 +142,7 @@ fn projection_equality() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Uint(U32)]"
         }
 
@@ -153,7 +153,7 @@ fn projection_equality() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Uint(U32)]"
         }
     }
@@ -183,7 +183,7 @@ fn projection_equality_priority1() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             // This is.. interesting, but not necessarily wrong.
             // It's certainly true that based on the impls we see
             // the only possible value for `U` is `u32`.
@@ -271,7 +271,7 @@ fn projection_equality_priority2() {
             // use the impl, but the SLG solver can't decide between
             // the placeholder and the normalized form.
             "Ambiguous; definite substitution for<?U1> { [?0 := S1, ?1 := ^0.0] }"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             // Constraining Out1 = S1 gives us only one choice, use the impl,
             // and the recursive solver prefers the normalized form.
             "Unique; substitution [?0 := S1, ?1 := Uint(U32)], lifetime constraints []"
@@ -298,7 +298,7 @@ fn projection_equality_from_env() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Uint(U32)]"
         }
     }
@@ -326,7 +326,7 @@ fn projection_equality_nested() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        }  yields[SolverChoice::recursive()] {
+        }  yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Uint(U32)]"
         }
     }
@@ -368,7 +368,7 @@ fn iterator_flatten() {
         } yields[SolverChoice::slg_default()] {
             // this is wrong, chalk#234
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Uint(U32)]"
         }
     }
@@ -720,7 +720,7 @@ fn normalize_under_binder() {
         } yields[SolverChoice::slg_default()] {
             // chalk#234, I think
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := I32], lifetime constraints []"
         }
 
@@ -743,7 +743,7 @@ fn normalize_under_binder() {
         } yields[SolverChoice::slg_default()] {
             // chalk#234, I think
             "Ambiguous"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []"
         }
 
@@ -1038,7 +1038,7 @@ fn guidance_for_projection_on_flounder() {
                     <Range<T> as Iterator>::Item = U
                 }
             }
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             "Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }"
         }
     }

diff --git a/tests/test/unify.rs b/tests/test/unify.rs
@@ -166,7 +166,7 @@ fn unify_quantified_lifetimes() {
              InEnvironment { environment: Env([]), goal: '^0.0: '!1_0 }\
              ] \
              }"
-        } yields[SolverChoice::recursive()] {
+        } yields[SolverChoice::recursive_default()] {
             // only difference is in the value of ?1, which is equivalent
             "Unique; for<?U0> { \
              substitution [?0 := '^0.0, ?1 := '^0.0], \