Rebase fixes; flounder instead of truncating, like SLG

Author: flodiebold

chalk-solve/src/clauses/generalize.rs

@@ -30,10 +30,7 @@ impl<I: Interner> Generalize<'_, I> {
         let value = value
             .fold_with(&mut generalize, DebruijnIndex::INNERMOST)
             .unwrap();
-        Binders {
-            binders: generalize.binders,
-            value,
-        }
+        Binders::new(generalize.binders, value)
     }
 }
 

chalk-solve/src/recursive.rs

@@ -369,10 +369,7 @@ impl<'me, I: Interner> Solver<'me, I> {
                 ProgramClauseData::Implies(implication) => {
                     let res = self.solve_via_implication(
                         canonical_goal,
-                        &Binders {
-                            binders: vec![],
-                            value: implication.clone(),
-                        },
+                        &Binders::new(vec![], implication.clone()),
                         minimums,
                     );
                     if let (Ok(solution), priority) = res {
@@ -452,7 +449,10 @@ impl<'me, I: Interner> Solver<'me, I> {
         }
 
         // and then try to solve
-        (fulfill.solve(subst, minimums), clause.value.priority)
+        (
+            fulfill.solve(subst, minimums),
+            clause.skip_binders().priority,
+        )
     }
 
     fn program_clauses_for_goal(

chalk-solve/src/recursive/fulfill.rs

@@ -119,16 +119,30 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
 
     fn push_obligation(&mut self, obligation: Obligation<I>) {
         // truncate to avoid overflows
-        let obligation = match obligation {
+        match &obligation {
             Obligation::Prove(goal) => {
-                let truncated =
-                    truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal);
-                Obligation::Prove(truncated.value)
+                if truncate::needs_truncation(
+                    self.solver.program.interner(),
+                    &mut self.infer,
+                    30,
+                    goal,
+                ) {
+                    // the goal is too big. Record that we should return Ambiguous
+                    self.cannot_prove = true;
+                    return;
+                }
             }
             Obligation::Refute(goal) => {
-                let truncated =
-                    truncate::truncate(self.solver.program.interner(), &mut self.infer, 30, &goal);
-                Obligation::Refute(truncated.value)
+                if truncate::needs_truncation(
+                    self.solver.program.interner(),
+                    &mut self.infer,
+                    30,
+                    goal,
+                ) {
+                    // the goal is too big. Record that we should return Ambiguous
+                    self.cannot_prove = true;
+                    return;
+                }
             }
         };
         self.obligations.push(obligation);

chalk-solve/src/solve/slg.rs

@@ -14,8 +14,7 @@ use chalk_engine::hh::HhGoal;
 use chalk_engine::{CompleteAnswer, ExClause, Literal};
 use chalk_ir::cast::Cast;
 use chalk_ir::cast::Caster;
-use chalk_ir::could_match::CouldMatch;
-use chalk_ir::interner::{HasInterner, Interner};
+use chalk_ir::interner::Interner;
 use chalk_ir::*;
 
 use std::fmt::Debug;

tests/test/cycle.rs

@@ -165,12 +165,8 @@ fn overflow() {
             S<Z>: Q
         } yields[SolverChoice::slg(10, None)] {
             "Ambiguous; no inference guidance"
-        }
-
-        goal {
-            S<Z>: Q
         } yields[SolverChoice::recursive()] {
-            "No possible solution"
+            "Ambiguous; no inference guidance"
         }
     }
 }