Auto merge of #647 - flodiebold:recursive-max-size, r=jackh726

bors · bors · commit faafc66ffffe · 2020-11-01T22:18:27.000Z
Make max goal size for recursive solver configurable
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], \

Original file line number	Diff line number	Diff line change
`@@ -55,6 +55,7 @@ pub enum SolverChoice {`
`55`	`55`	`Recursive {`
`56`	`56`	`overflow_depth: usize,`
`57`	`57`	`caching_enabled: bool,`
	`58`	`+ max_size: usize,`
`58`	`59`	`},`
`59`	`60`	`}`
`60`	`61`
`@@ -73,10 +74,20 @@ impl SolverChoice {`
`73`	`74`	`}`
`74`	`75`
`75`	`76`	`/// Returns the default recursive solver setup.`
`76`		`- pub fn recursive() -> Self {`
	`77`	`+ pub fn recursive_default() -> Self {`
`77`	`78`	`SolverChoice::Recursive {`
`78`	`79`	`overflow_depth: 100,`
`79`	`80`	`caching_enabled: true,`
	`81`	`+ max_size: 30,`
	`82`	`+ }`
	`83`	`+ }`
	`84`	`+`
	`85`	`+ /// Returns a recursive solver with specific parameters.`
	`86`	`+ pub fn recursive(max_size: usize, overflow_depth: usize) -> Self {`
	`87`	`+ SolverChoice::Recursive {`
	`88`	`+ overflow_depth,`
	`89`	`+ caching_enabled: true,`
	`90`	`+ max_size,`
`80`	`91`	`}`
`81`	`92`	`}`
`82`	`93`
`@@ -89,7 +100,12 @@ impl SolverChoice {`
`89`	`100`	`SolverChoice::Recursive {`
`90`	`101`	`overflow_depth,`
`91`	`102`	`caching_enabled,`
`92`		`- } => Box::new(RecursiveSolver::new(overflow_depth, caching_enabled)),`
	`103`	`+ max_size,`
	`104`	`+ } => Box::new(RecursiveSolver::new(`
	`105`	`+ overflow_depth,`
	`106`	`+ max_size,`
	`107`	`+ caching_enabled,`
	`108`	`+ )),`
`93`	`109`	`}`
`94`	`110`	`}`
`95`	`111`	`}`
Original file line number	Diff line number	Diff line change
`@@ -24,6 +24,9 @@ struct RecursiveContext<I: Interner> {`
`24`	`24`	`/// result.`
`25`	`25`	`cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,`
`26`	`26`
	`27`	`+ /// The maximum size for goals.`
	`28`	`+ max_size: usize,`
	`29`	`+`
`27`	`30`	`caching_enabled: bool,`
`28`	`31`	`}`
`29`	`32`
`@@ -42,9 +45,13 @@ pub struct RecursiveSolver<I: Interner> {`
`42`	`45`	`}`
`43`	`46`
`44`	`47`	`impl<I: Interner> RecursiveSolver<I> {`
`45`		`- pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {`
	`48`	`+ pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {`
`46`	`49`	`Self {`
`47`		`- ctx: Box::new(RecursiveContext::new(overflow_depth, caching_enabled)),`
	`50`	`+ ctx: Box::new(RecursiveContext::new(`
	`51`	`+ overflow_depth,`
	`52`	`+ max_size,`
	`53`	`+ caching_enabled,`
	`54`	`+ )),`
`48`	`55`	`}`
`49`	`56`	`}`
`50`	`57`	`}`
`@@ -76,11 +83,12 @@ impl<T> MergeWith<T> for Fallible<T> {`
`76`	`83`	`}`
`77`	`84`
`78`	`85`	`impl<I: Interner> RecursiveContext<I> {`
`79`		`- pub fn new(overflow_depth: usize, caching_enabled: bool) -> Self {`
	`86`	`+ pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {`
`80`	`87`	`RecursiveContext {`
`81`	`88`	`stack: Stack::new(overflow_depth),`
`82`	`89`	`search_graph: SearchGraph::new(),`
`83`	`90`	`cache: FxHashMap::default(),`
	`91`	`+ max_size,`
`84`	`92`	`caching_enabled,`
`85`	`93`	`}`
`86`	`94`	`}`
`@@ -291,6 +299,10 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {`
`291`	`299`	`fn db(&self) -> &dyn RustIrDatabase<I> {`
`292`	`300`	`self.program`
`293`	`301`	`}`
	`302`	`+`
	`303`	`+ fn max_size(&self) -> usize {`
	`304`	`+ self.context.max_size`
	`305`	`+ }`
`294`	`306`	`}`
`295`	`307`
`296`	`308`	`impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {`
Original file line number	Diff line number	Diff line change
`@@ -165,7 +165,7 @@ fn overflow() {`
`165`	`165`	`S<Z>: Q`
`166`	`166`	`} yields[SolverChoice::slg(10, None)] {`
`167`	`167`	`"Ambiguous; no inference guidance"`
`168`		`- } yields[SolverChoice::recursive()] {`
	`168`	`+ } yields[SolverChoice::recursive_default()] {`
`169`	`169`	`"Ambiguous; no inference guidance"`
`170`	`170`	`}`
`171`	`171`	`}`
Original file line number	Diff line number	Diff line change
`@@ -413,7 +413,7 @@ fn dyn_associated_type_binding() {`
`413`	`413`	`<dyn FnOnce<(), Output = i32> + 's as FnOnce<()>>::Output = T`
`414`	`414`	`}`
`415`	`415`	`}`
`416`		`- } yields[SolverChoice::recursive()] {`
	`416`	`+ } yields[SolverChoice::recursive_default()] {`
`417`	`417`	`"Unique; substitution [?0 := Int(I32)], lifetime constraints []"`
`418`	`418`	`} yields[SolverChoice::slg_default()] {`
`419`	`419`	`// #234`
Original file line number	Diff line number	Diff line change
`@@ -130,7 +130,7 @@ fn only_draw_so_many() {`
`130`	`130`	`exists<T> { T: Sized }`
`131`	`131`	`} yields[SolverChoice::slg(10, Some(2))] {`
`132`	`132`	`"Ambiguous; no inference guidance"`
`133`		`- } yields[SolverChoice::recursive()] {`
	`133`	`+ } yields[SolverChoice::recursive_default()] {`
`134`	`134`	`"Ambiguous; no inference guidance"`
`135`	`135`	`}`
`136`	`136`	`}`
`@@ -158,7 +158,7 @@ fn only_draw_so_many_blow_up() {`
`158`	`158`	`exists<T> { T: Foo }`
`159`	`159`	`} yields[SolverChoice::slg(10, Some(2))] {`
`160`	`160`	`"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"`
`161`		`- } yields[SolverChoice::recursive()] {`
	`161`	`+ } yields[SolverChoice::recursive_default()] {`
`162`	`162`	`"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"`
`163`	`163`	`}`
`164`	`164`	`}`
`@@ -696,7 +696,7 @@ fn not_really_ambig() {`
`696`	`696`	`exists<T> { Vec<T>: A }`
`697`	`697`	`} yields[SolverChoice::slg_default()] {`
`698`	`698`	`"Unique; substitution [?0 := Uint(U32)], lifetime constraints []"`
`699`		`- } yields[SolverChoice::recursive()] {`
	`699`	`+ } yields[SolverChoice::recursive_default()] {`
`700`	`700`	`"Ambiguous; no inference guidance"`
`701`	`701`	`}`
`702`	`702`	`}`
`@@ -754,7 +754,7 @@ fn empty_definite_guidance() {`
`754`	`754`	`// recursive solver infinite loop.`
`755`	`755`	`} yields[SolverChoice::slg_default()] {`
`756`	`756`	`"Unique"`
`757`		`- } yields[SolverChoice::recursive()] {`
	`757`	`+ } yields[SolverChoice::recursive_default()] {`
`758`	`758`	`"Ambiguous"`
`759`	`759`	`}`
`760`	`760`	`}`
Original file line number	Diff line number	Diff line change
`@@ -77,7 +77,7 @@ macro_rules! parse_test_data {`
`77`	`77`	`@parsed_goals[`
`78`	`78`	`$($parsed_goals)*`
`79`	`79`	`(stringify!($goal), SolverChoice::slg_default(), TestGoal::Aggregated($expected))`
`80`		`- (stringify!($goal), SolverChoice::recursive(), TestGoal::Aggregated($expected))`
	`80`	`+ (stringify!($goal), SolverChoice::recursive_default(), TestGoal::Aggregated($expected))`
`81`	`81`	`]`
`82`	`82`	`@unparsed_goals[$($unparsed_goals)*])`
`83`	`83`	`};`
Original file line number	Diff line number	Diff line change
`@@ -166,7 +166,7 @@ fn opaque_generics() {`
`166`	`166`	`}`
`167`	`167`	`} yields[SolverChoice::slg_default()] {`
`168`	`168`	`"Ambiguous" // #234`
`169`		`- } yields[SolverChoice::recursive()] {`
	`169`	`+ } yields[SolverChoice::recursive_default()] {`
`170`	`170`	`"Unique; substitution [?0 := Bar], lifetime constraints []"`
`171`	`171`	`}`
`172`	`172`	`}`