diff --git a/chalk-solve/src/recursive.rs b/chalk-solve/src/recursive.rs
index 8955067ff6d..b78d89b70e4 100644
--- a/chalk-solve/src/recursive.rs
+++ b/chalk-solve/src/recursive.rs
@@ -1,29 +1,19 @@
+mod combine;
 mod fulfill;
 pub mod lib;
 mod search_graph;
+mod solve;
 mod stack;
 
-use self::fulfill::{Fulfill, RecursiveInferenceTable, RecursiveSolver};
-use self::lib::{Guidance, Minimums, Solution, UCanonicalGoal};
+use self::lib::{Minimums, Solution, UCanonicalGoal};
 use self::search_graph::{DepthFirstNumber, SearchGraph};
+use self::solve::{SolveDatabase, SolveIteration};
 use self::stack::{Stack, StackDepth};
-use crate::clauses::program_clauses_for_goal;
-use crate::infer::{InferenceTable, ParameterEnaVariableExt};
-use crate::solve::truncate;
 use crate::{coinductive_goal::IsCoinductive, RustIrDatabase};
-use chalk_ir::fold::Fold;
-use chalk_ir::interner::{HasInterner, Interner};
-use chalk_ir::visit::Visit;
-use chalk_ir::zip::Zip;
+use chalk_ir::interner::Interner;
 use chalk_ir::{debug, debug_heading, info, info_heading};
-use chalk_ir::{
-    Binders, Canonical, ClausePriority, ConstrainedSubst, Constraint, DomainGoal, Environment,
-    Fallible, Floundered, GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause,
-    ProgramClauseData, ProgramClauseImplication, Substitution, UCanonical, UniverseMap,
-    VariableKinds,
-};
+use chalk_ir::{Canonical, ConstrainedSubst, Fallible};
 use rustc_hash::FxHashMap;
-use std::fmt::Debug;
 
 pub(crate) struct RecursiveContext<I: Interner> {
     stack: Stack,
@@ -40,104 +30,6 @@ pub(crate) struct RecursiveContext<I: Interner> {
     caching_enabled: bool,
 }
 
-pub(crate) struct RecursiveInferenceTableImpl<I: Interner> {
-    pub(crate) infer: InferenceTable<I>,
-}
-
-impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I> {
-    fn instantiate_binders_universally<'a, T>(
-        &mut self,
-        interner: &'a I,
-        arg: &'a Binders<T>,
-    ) -> T::Result
-    where
-        T: Fold<I> + HasInterner<Interner = I>,
-    {
-        self.infer.instantiate_binders_universally(interner, arg)
-    }
-
-    fn instantiate_binders_existentially<'a, T>(
-        &mut self,
-        interner: &'a I,
-        arg: &'a Binders<T>,
-    ) -> T::Result
-    where
-        T: Fold<I> + HasInterner<Interner = I>,
-    {
-        self.infer.instantiate_binders_existentially(interner, arg)
-    }
-
-    fn canonicalize<T>(
-        &mut self,
-        interner: &I,
-        value: &T,
-    ) -> (Canonical<T::Result>, Vec<GenericArg<I>>)
-    where
-        T: Fold<I>,
-        T::Result: HasInterner<Interner = I>,
-    {
-        let res = self.infer.canonicalize(interner, value);
-        let free_vars = res
-            .free_vars
-            .into_iter()
-            .map(|free_var| free_var.to_generic_arg(interner))
-            .collect();
-        (res.quantified, free_vars)
-    }
-
-    fn u_canonicalize<T>(
-        &mut self,
-        interner: &I,
-        value0: &Canonical<T>,
-    ) -> (UCanonical<T::Result>, UniverseMap)
-    where
-        T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
-        T::Result: HasInterner<Interner = I>,
-    {
-        let res = self.infer.u_canonicalize(interner, value0);
-        (res.quantified, res.universes)
-    }
-
-    fn unify<T>(
-        &mut self,
-        interner: &I,
-        environment: &Environment<I>,
-        a: &T,
-        b: &T,
-    ) -> Fallible<(
-        Vec<InEnvironment<DomainGoal<I>>>,
-        Vec<InEnvironment<Constraint<I>>>,
-    )>
-    where
-        T: ?Sized + Zip<I>,
-    {
-        let res = self.infer.unify(interner, environment, a, b)?;
-        Ok((res.goals, res.constraints))
-    }
-
-    fn instantiate_canonical<T>(&mut self, interner: &I, bound: &Canonical<T>) -> T::Result
-    where
-        T: HasInterner<Interner = I> + Fold<I> + Debug,
-    {
-        self.infer.instantiate_canonical(interner, bound)
-    }
-
-    fn invert_then_canonicalize<T>(
-        &mut self,
-        interner: &I,
-        value: &T,
-    ) -> Option<Canonical<T::Result>>
-    where
-        T: Fold<I, Result = T> + HasInterner<Interner = I>,
-    {
-        self.infer.invert_then_canonicalize(interner, value)
-    }
-
-    fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool {
-        truncate::needs_truncation(interner, &mut self.infer, max_size, value)
-    }
-}
-
 /// A Solver is the basic context in which you can propose goals for a given
 /// program. **All questions posed to the solver are in canonical, closed form,
 /// so that each question is answered with effectively a "clean slate"**. This
@@ -190,25 +82,6 @@ impl<I: Interner> RecursiveContext<I> {
 }
 
 impl<'me, I: Interner> Solver<'me, I> {
-    pub(crate) fn new_inference_table<
-        T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone,
-    >(
-        &self,
-        ucanonical_goal: &UCanonical<InEnvironment<T>>,
-    ) -> (
-        RecursiveInferenceTableImpl<I>,
-        Substitution<I>,
-        InEnvironment<T::Result>,
-    ) {
-        let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
-            self.program.interner(),
-            ucanonical_goal.universes,
-            &ucanonical_goal.canonical,
-        );
-        let infer = crate::recursive::RecursiveInferenceTableImpl { infer };
-        (infer, subst, canonical_goal)
-    }
-
     /// Solves a canonical goal. The substitution returned in the
     /// solution will be for the fully decomposed goal. For example, given the
     /// program
@@ -256,68 +129,9 @@ impl<'me, I: Interner> Solver<'me, I> {
         // - None < Some(CannotProve)
         // the function which maps the loop iteration to `answer` is a nondecreasing function
         // so this function will eventually be constant and the loop terminates.
-        let minimums = &mut Minimums::new();
         loop {
-            let UCanonical {
-                universes,
-                canonical:
-                    Canonical {
-                        binders,
-                        value: InEnvironment { environment, goal },
-                    },
-            } = canonical_goal.clone();
-
-            let (current_answer, current_prio) = match goal.data(self.program.interner()) {
-                GoalData::DomainGoal(domain_goal) => {
-                    let canonical_goal = UCanonical {
-                        universes,
-                        canonical: Canonical {
-                            binders,
-                            value: InEnvironment {
-                                environment,
-                                goal: domain_goal.clone(),
-                            },
-                        },
-                    };
-
-                    // "Domain" goals (i.e., leaf goals that are Rust-specific) are
-                    // always solved via some form of implication. We can either
-                    // apply assumptions from our environment (i.e. where clauses),
-                    // or from the lowered program, which includes fallback
-                    // clauses. We try each approach in turn:
-
-                    let InEnvironment { environment, goal } = &canonical_goal.canonical.value;
-
-                    let (prog_solution, prog_prio) = {
-                        debug_heading!("prog_clauses");
-
-                        let prog_clauses = self.program_clauses_for_goal(environment, &goal);
-                        match prog_clauses {
-                            Ok(clauses) => {
-                                self.solve_from_clauses(&canonical_goal, clauses, minimums)
-                            }
-                            Err(Floundered) => {
-                                (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High)
-                            }
-                        }
-                    };
-                    debug!("prog_solution={:?}", prog_solution);
-
-                    (prog_solution, prog_prio)
-                }
-
-                _ => {
-                    let canonical_goal = UCanonical {
-                        universes,
-                        canonical: Canonical {
-                            binders,
-                            value: InEnvironment { environment, goal },
-                        },
-                    };
-
-                    self.solve_via_simplification(&canonical_goal, minimums)
-                }
-            };
+            let minimums = &mut Minimums::new();
+            let (current_answer, current_prio) = self.solve_iteration(&canonical_goal, minimums);
 
             debug!(
                 "solve_new_subgoal: loop iteration result = {:?} with minimums {:?}",
@@ -335,7 +149,7 @@ impl<'me, I: Interner> Solver<'me, I> {
             let old_answer = &self.context.search_graph[dfn].solution;
             let old_prio = self.context.search_graph[dfn].solution_priority;
 
-            let (current_answer, current_prio) = combine_with_priorities_for_goal(
+            let (current_answer, current_prio) = combine::with_priorities_for_goal(
                 self.program.interner(),
                 &canonical_goal.canonical.value.goal,
                 old_answer.clone(),
@@ -370,106 +184,9 @@ impl<'me, I: Interner> Solver<'me, I> {
             self.context.search_graph.rollback_to(dfn + 1);
         }
     }
-
-    fn solve_via_simplification(
-        &mut self,
-        canonical_goal: &UCanonicalGoal<I>,
-        minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
-        debug_heading!("solve_via_simplification({:?})", canonical_goal);
-        let (infer, subst, goal) = self.new_inference_table(canonical_goal);
-        match Fulfill::new_with_simplification(self, infer, subst, goal) {
-            Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High),
-            Err(e) => (Err(e), ClausePriority::High),
-        }
-    }
-
-    /// See whether we can solve a goal by implication on any of the given
-    /// clauses. If multiple such solutions are possible, we attempt to combine
-    /// them.
-    fn solve_from_clauses<C>(
-        &mut self,
-        canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
-        clauses: C,
-        minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority)
-    where
-        C: IntoIterator<Item = ProgramClause<I>>,
-    {
-        let mut cur_solution = None;
-        for program_clause in clauses {
-            debug_heading!("clause={:?}", program_clause);
-
-            // If we have a completely ambiguous answer, it's not going to get better, so stop
-            if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
-                return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
-            }
-
-            let res = match program_clause.data(self.program.interner()) {
-                ProgramClauseData::Implies(implication) => self.solve_via_implication(
-                    canonical_goal,
-                    &Binders::new(
-                        VariableKinds::from(self.program.interner(), vec![]),
-                        implication.clone(),
-                    ),
-                    minimums,
-                ),
-                ProgramClauseData::ForAll(implication) => {
-                    self.solve_via_implication(canonical_goal, implication, minimums)
-                }
-            };
-            if let (Ok(solution), priority) = res {
-                debug!("ok: solution={:?} prio={:?}", solution, priority);
-                cur_solution = Some(match cur_solution {
-                    None => (solution, priority),
-                    Some((cur, cur_priority)) => combine_with_priorities(
-                        self.program.interner(),
-                        &canonical_goal.canonical.value.goal,
-                        cur,
-                        cur_priority,
-                        solution,
-                        priority,
-                    ),
-                });
-            } else {
-                debug!("error");
-            }
-        }
-        cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p))
-    }
-
-    /// Modus ponens! That is: try to apply an implication by proving its premises.
-    fn solve_via_implication(
-        &mut self,
-        canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
-        clause: &Binders<ProgramClauseImplication<I>>,
-        minimums: &mut Minimums,
-    ) -> (Fallible<Solution<I>>, ClausePriority) {
-        info_heading!(
-            "solve_via_implication(\
-             \n    canonical_goal={:?},\
-             \n    clause={:?})",
-            canonical_goal,
-            clause
-        );
-
-        let (infer, subst, goal) = self.new_inference_table(canonical_goal);
-        match Fulfill::new_with_clause(self, infer, subst, goal, clause) {
-            Ok(fulfill) => (fulfill.solve(minimums), clause.skip_binders().priority),
-            Err(e) => (Err(e), ClausePriority::High),
-        }
-    }
-
-    fn program_clauses_for_goal(
-        &self,
-        environment: &Environment<I>,
-        goal: &DomainGoal<I>,
-    ) -> Result<Vec<ProgramClause<I>>, Floundered> {
-        program_clauses_for_goal(self.program, environment, goal)
-    }
 }
 
-impl<'me, I: Interner> RecursiveSolver<I> for Solver<'me, I> {
+impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
     /// Attempt to solve a goal that has been fully broken down into leaf form
     /// and canonicalized. This is where the action really happens, and is the
     /// place where we would perform caching in rustc (and may eventually do in Chalk).
@@ -562,77 +279,8 @@ impl<'me, I: Interner> RecursiveSolver<I> for Solver<'me, I> {
     fn interner(&self) -> &I {
         &self.program.interner()
     }
-}
-
-fn calculate_inputs<I: Interner>(
-    interner: &I,
-    domain_goal: &DomainGoal<I>,
-    solution: &Solution<I>,
-) -> Vec<GenericArg<I>> {
-    if let Some(subst) = solution.constrained_subst() {
-        let subst_goal = subst.value.subst.apply(&domain_goal, interner);
-        subst_goal.inputs(interner)
-    } else {
-        domain_goal.inputs(interner)
-    }
-}
 
-fn combine_with_priorities_for_goal<I: Interner>(
-    interner: &I,
-    goal: &Goal<I>,
-    a: Fallible<Solution<I>>,
-    prio_a: ClausePriority,
-    b: Fallible<Solution<I>>,
-    prio_b: ClausePriority,
-) -> (Fallible<Solution<I>>, ClausePriority) {
-    let domain_goal = match goal.data(interner) {
-        GoalData::DomainGoal(domain_goal) => domain_goal,
-        _ => {
-            // non-domain goals currently have no priorities, so we always take the new solution here
-            return (b, prio_b);
-        }
-    };
-    match (a, b) {
-        (Ok(a), Ok(b)) => {
-            let (solution, prio) =
-                combine_with_priorities(interner, domain_goal, a, prio_a, b, prio_b);
-            (Ok(solution), prio)
-        }
-        (Ok(solution), Err(_)) => (Ok(solution), prio_a),
-        (Err(_), Ok(solution)) => (Ok(solution), prio_b),
-        (Err(_), Err(e)) => (Err(e), prio_b),
-    }
-}
-
-fn combine_with_priorities<I: Interner>(
-    interner: &I,
-    domain_goal: &DomainGoal<I>,
-    a: Solution<I>,
-    prio_a: ClausePriority,
-    b: Solution<I>,
-    prio_b: ClausePriority,
-) -> (Solution<I>, ClausePriority) {
-    match (prio_a, prio_b, a, b) {
-        (ClausePriority::High, ClausePriority::Low, higher, lower)
-        | (ClausePriority::Low, ClausePriority::High, lower, higher) => {
-            // if we have a high-priority solution and a low-priority solution,
-            // the high-priority solution overrides *if* they are both for the
-            // same inputs -- we don't want a more specific high-priority
-            // solution overriding a general low-priority one. Currently inputs
-            // only matter for projections; in a goal like `AliasEq(<?0 as
-            // Trait>::Type = ?1)`, ?0 is the input.
-            let inputs_higher = calculate_inputs(interner, domain_goal, &higher);
-            let inputs_lower = calculate_inputs(interner, domain_goal, &lower);
-            if inputs_higher == inputs_lower {
-                debug!(
-                    "preferring solution: {:?} over {:?} because of higher prio",
-                    higher, lower
-                );
-                (higher, ClausePriority::High)
-            } else {
-                (higher.combine(lower, interner), ClausePriority::High)
-            }
-        }
-        (_, _, a, b) => (a.combine(b, interner), prio_a),
+    fn db(&self) -> &dyn RustIrDatabase<I> {
+        self.program
     }
 }
diff --git a/chalk-solve/src/recursive/combine.rs b/chalk-solve/src/recursive/combine.rs
new file mode 100644
index 00000000000..9118092ed27
--- /dev/null
+++ b/chalk-solve/src/recursive/combine.rs
@@ -0,0 +1,76 @@
+use super::lib::Solution;
+use chalk_ir::debug;
+use chalk_ir::interner::Interner;
+use chalk_ir::{ClausePriority, DomainGoal, Fallible, GenericArg, Goal, GoalData};
+
+pub(super) fn with_priorities_for_goal<I: Interner>(
+    interner: &I,
+    goal: &Goal<I>,
+    a: Fallible<Solution<I>>,
+    prio_a: ClausePriority,
+    b: Fallible<Solution<I>>,
+    prio_b: ClausePriority,
+) -> (Fallible<Solution<I>>, ClausePriority) {
+    let domain_goal = match goal.data(interner) {
+        GoalData::DomainGoal(domain_goal) => domain_goal,
+        _ => {
+            // non-domain goals currently have no priorities, so we always take the new solution here
+            return (b, prio_b);
+        }
+    };
+    match (a, b) {
+        (Ok(a), Ok(b)) => {
+            let (solution, prio) = with_priorities(interner, domain_goal, a, prio_a, b, prio_b);
+            (Ok(solution), prio)
+        }
+        (Ok(solution), Err(_)) => (Ok(solution), prio_a),
+        (Err(_), Ok(solution)) => (Ok(solution), prio_b),
+        (Err(_), Err(e)) => (Err(e), prio_b),
+    }
+}
+
+pub(super) fn with_priorities<I: Interner>(
+    interner: &I,
+    domain_goal: &DomainGoal<I>,
+    a: Solution<I>,
+    prio_a: ClausePriority,
+    b: Solution<I>,
+    prio_b: ClausePriority,
+) -> (Solution<I>, ClausePriority) {
+    match (prio_a, prio_b, a, b) {
+        (ClausePriority::High, ClausePriority::Low, higher, lower)
+        | (ClausePriority::Low, ClausePriority::High, lower, higher) => {
+            // if we have a high-priority solution and a low-priority solution,
+            // the high-priority solution overrides *if* they are both for the
+            // same inputs -- we don't want a more specific high-priority
+            // solution overriding a general low-priority one. Currently inputs
+            // only matter for projections; in a goal like `AliasEq(<?0 as
+            // Trait>::Type = ?1)`, ?0 is the input.
+            let inputs_higher = calculate_inputs(interner, domain_goal, &higher);
+            let inputs_lower = calculate_inputs(interner, domain_goal, &lower);
+            if inputs_higher == inputs_lower {
+                debug!(
+                    "preferring solution: {:?} over {:?} because of higher prio",
+                    higher, lower
+                );
+                (higher, ClausePriority::High)
+            } else {
+                (higher.combine(lower, interner), ClausePriority::High)
+            }
+        }
+        (_, _, a, b) => (a.combine(b, interner), prio_a),
+    }
+}
+
+fn calculate_inputs<I: Interner>(
+    interner: &I,
+    domain_goal: &DomainGoal<I>,
+    solution: &Solution<I>,
+) -> Vec<GenericArg<I>> {
+    if let Some(subst) = solution.constrained_subst() {
+        let subst_goal = subst.value.subst.apply(&domain_goal, interner);
+        subst_goal.inputs(interner)
+    } else {
+        domain_goal.inputs(interner)
+    }
+}
diff --git a/chalk-solve/src/recursive/fulfill.rs b/chalk-solve/src/recursive/fulfill.rs
index 493070676b9..299765632e5 100644
--- a/chalk-solve/src/recursive/fulfill.rs
+++ b/chalk-solve/src/recursive/fulfill.rs
@@ -1,4 +1,5 @@
 use super::lib::{Guidance, Minimums, Solution};
+use super::solve::SolveDatabase;
 use chalk_ir::cast::Cast;
 use chalk_ir::fold::Fold;
 use chalk_ir::interner::{HasInterner, Interner};
@@ -56,7 +57,7 @@ enum NegativeSolution {
     Ambiguous,
 }
 
-pub(crate) trait RecursiveInferenceTable<I: Interner> {
+pub(super) trait RecursiveInferenceTable<I: Interner> {
     fn instantiate_binders_universally<'a, T>(
         &mut self,
         interner: &'a I,
@@ -119,16 +120,6 @@ pub(crate) trait RecursiveInferenceTable<I: Interner> {
     fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool;
 }
 
-pub trait RecursiveSolver<I: Interner> {
-    fn solve_goal(
-        &mut self,
-        goal: UCanonical<InEnvironment<Goal<I>>>,
-        minimums: &mut Minimums,
-    ) -> Fallible<Solution<I>>;
-
-    fn interner(&self) -> &I;
-}
-
 /// A `Fulfill` is where we actually break down complex goals, instantiate
 /// variables, and perform inference. It's highly stateful. It's generally used
 /// in Chalk to try to solve a goal, and then package up what was learned in a
@@ -139,10 +130,10 @@ pub trait RecursiveSolver<I: Interner> {
 /// of type inference in general. But when solving trait constraints, *fresh*
 /// `Fulfill` instances will be created to solve canonicalized, free-standing
 /// goals, and transport what was learned back to the outer context.
-pub(crate) struct Fulfill<
+pub(super) struct Fulfill<
     's,
     I: Interner,
-    Solver: RecursiveSolver<I>,
+    Solver: SolveDatabase<I>,
     Infer: RecursiveInferenceTable<I>,
 > {
     solver: &'s mut Solver,
@@ -162,10 +153,10 @@ pub(crate) struct Fulfill<
     cannot_prove: bool,
 }
 
-impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable<I>>
+impl<'s, I: Interner, Solver: SolveDatabase<I>, Infer: RecursiveInferenceTable<I>>
     Fulfill<'s, I, Solver, Infer>
 {
-    pub(crate) fn new_with_clause(
+    pub(super) fn new_with_clause(
         solver: &'s mut Solver,
         infer: Infer,
         subst: Substitution<I>,
@@ -209,7 +200,7 @@ impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable
         Ok(fulfill)
     }
 
-    pub(crate) fn new_with_simplification(
+    pub(super) fn new_with_simplification(
         solver: &'s mut Solver,
         infer: Infer,
         subst: Substitution<I>,
@@ -263,7 +254,7 @@ impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable
     ///
     /// Wraps `InferenceTable::unify`; any resulting normalizations are added
     /// into our list of pending obligations with the given environment.
-    pub(crate) fn unify<T>(&mut self, environment: &Environment<I>, a: &T, b: &T) -> Fallible<()>
+    pub(super) fn unify<T>(&mut self, environment: &Environment<I>, a: &T, b: &T) -> Fallible<()>
     where
         T: ?Sized + Zip<I> + Debug,
     {
@@ -283,7 +274,7 @@ impl<'s, I: Interner, Solver: RecursiveSolver<I>, Infer: RecursiveInferenceTable
 
     /// Create obligations for the given goal in the given environment. This may
     /// ultimately create any number of obligations.
-    pub(crate) fn push_goal(
+    pub(super) fn push_goal(
         &mut self,
         environment: &Environment<I>,
         goal: Goal<I>,
diff --git a/chalk-solve/src/recursive/lib.rs b/chalk-solve/src/recursive/lib.rs
index 6e8e5f7aeb8..c9e793e55fd 100644
--- a/chalk-solve/src/recursive/lib.rs
+++ b/chalk-solve/src/recursive/lib.rs
@@ -9,8 +9,8 @@ pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
 /// The `minimums` struct is used while solving to track whether we encountered
 /// any cycles in the process.
 #[derive(Copy, Clone, Debug)]
-pub struct Minimums {
-    pub positive: DepthFirstNumber,
+pub(super) struct Minimums {
+    pub(super) positive: DepthFirstNumber,
 }
 
 impl Minimums {
diff --git a/chalk-solve/src/recursive/search_graph.rs b/chalk-solve/src/recursive/search_graph.rs
index 96f42c05250..c93bba6984d 100644
--- a/chalk-solve/src/recursive/search_graph.rs
+++ b/chalk-solve/src/recursive/search_graph.rs
@@ -17,7 +17,7 @@ pub(super) struct SearchGraph<I: Interner> {
 }
 
 #[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
-pub struct DepthFirstNumber {
+pub(super) struct DepthFirstNumber {
     index: usize,
 }
 
diff --git a/chalk-solve/src/recursive/solve.rs b/chalk-solve/src/recursive/solve.rs
new file mode 100644
index 00000000000..8248ee7b4ba
--- /dev/null
+++ b/chalk-solve/src/recursive/solve.rs
@@ -0,0 +1,331 @@
+use super::combine;
+use super::fulfill::{Fulfill, RecursiveInferenceTable};
+use super::lib::{Guidance, Minimums, Solution, UCanonicalGoal};
+use super::Solver;
+use crate::clauses::program_clauses_for_goal;
+use crate::infer::{InferenceTable, ParameterEnaVariableExt};
+use crate::{solve::truncate, RustIrDatabase};
+use chalk_ir::fold::Fold;
+use chalk_ir::interner::{HasInterner, Interner};
+use chalk_ir::visit::Visit;
+use chalk_ir::zip::Zip;
+use chalk_ir::{debug, debug_heading, info_heading};
+use chalk_ir::{
+    Binders, Canonical, ClausePriority, Constraint, DomainGoal, Environment, Fallible, Floundered,
+    GenericArg, Goal, GoalData, InEnvironment, NoSolution, ProgramClause, ProgramClauseData,
+    ProgramClauseImplication, Substitution, UCanonical, UniverseMap, VariableKinds,
+};
+use std::fmt::Debug;
+
+pub(super) trait SolveDatabase<I: Interner>: Sized {
+    fn solve_goal(
+        &mut self,
+        goal: UCanonical<InEnvironment<Goal<I>>>,
+        minimums: &mut Minimums,
+    ) -> Fallible<Solution<I>>;
+
+    fn interner(&self) -> &I;
+
+    fn db(&self) -> &dyn RustIrDatabase<I>;
+}
+
+/// The `solve_iteration` method -- implemented for any type that implements
+/// `SolveDb`.
+pub(super) trait SolveIteration<I: Interner>: SolveDatabase<I> {
+    /// Executes one iteration of the recursive solver, computing the current
+    /// solution to the given canonical goal. This is used as part of a loop in
+    /// the case of cyclic goals.
+    fn solve_iteration(
+        &mut self,
+        canonical_goal: &UCanonicalGoal<I>,
+        minimums: &mut Minimums,
+    ) -> (Fallible<Solution<I>>, ClausePriority) {
+        let UCanonical {
+            universes,
+            canonical:
+                Canonical {
+                    binders,
+                    value: InEnvironment { environment, goal },
+                },
+        } = canonical_goal.clone();
+
+        match goal.data(self.interner()) {
+            GoalData::DomainGoal(domain_goal) => {
+                let canonical_goal = UCanonical {
+                    universes,
+                    canonical: Canonical {
+                        binders,
+                        value: InEnvironment {
+                            environment,
+                            goal: domain_goal.clone(),
+                        },
+                    },
+                };
+
+                // "Domain" goals (i.e., leaf goals that are Rust-specific) are
+                // always solved via some form of implication. We can either
+                // apply assumptions from our environment (i.e. where clauses),
+                // or from the lowered program, which includes fallback
+                // clauses. We try each approach in turn:
+
+                let InEnvironment { environment, goal } = &canonical_goal.canonical.value;
+
+                let (prog_solution, prog_prio) = {
+                    debug_heading!("prog_clauses");
+
+                    let prog_clauses = self.program_clauses_for_goal(environment, &goal);
+                    match prog_clauses {
+                        Ok(clauses) => self.solve_from_clauses(&canonical_goal, clauses, minimums),
+                        Err(Floundered) => {
+                            (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High)
+                        }
+                    }
+                };
+                debug!("prog_solution={:?}", prog_solution);
+
+                (prog_solution, prog_prio)
+            }
+
+            _ => {
+                let canonical_goal = UCanonical {
+                    universes,
+                    canonical: Canonical {
+                        binders,
+                        value: InEnvironment { environment, goal },
+                    },
+                };
+
+                self.solve_via_simplification(&canonical_goal, minimums)
+            }
+        }
+    }
+}
+
+impl<S, I> SolveIteration<I> for S
+where
+    S: SolveDatabase<I>,
+    I: Interner,
+{
+}
+
+/// Helper methods for `solve_iteration`, private to this module.
+trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
+    fn solve_via_simplification(
+        &mut self,
+        canonical_goal: &UCanonicalGoal<I>,
+        minimums: &mut Minimums,
+    ) -> (Fallible<Solution<I>>, ClausePriority) {
+        debug_heading!("solve_via_simplification({:?})", canonical_goal);
+        let (infer, subst, goal) = self.new_inference_table(canonical_goal);
+        match Fulfill::new_with_simplification(self, infer, subst, goal) {
+            Ok(fulfill) => (fulfill.solve(minimums), ClausePriority::High),
+            Err(e) => (Err(e), ClausePriority::High),
+        }
+    }
+
+    /// See whether we can solve a goal by implication on any of the given
+    /// clauses. If multiple such solutions are possible, we attempt to combine
+    /// them.
+    fn solve_from_clauses<C>(
+        &mut self,
+        canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
+        clauses: C,
+        minimums: &mut Minimums,
+    ) -> (Fallible<Solution<I>>, ClausePriority)
+    where
+        C: IntoIterator<Item = ProgramClause<I>>,
+    {
+        let mut cur_solution = None;
+        for program_clause in clauses {
+            debug_heading!("clause={:?}", program_clause);
+
+            // If we have a completely ambiguous answer, it's not going to get better, so stop
+            if cur_solution == Some((Solution::Ambig(Guidance::Unknown), ClausePriority::High)) {
+                return (Ok(Solution::Ambig(Guidance::Unknown)), ClausePriority::High);
+            }
+
+            let res = match program_clause.data(self.interner()) {
+                ProgramClauseData::Implies(implication) => self.solve_via_implication(
+                    canonical_goal,
+                    &Binders::new(
+                        VariableKinds::from(self.interner(), vec![]),
+                        implication.clone(),
+                    ),
+                    minimums,
+                ),
+                ProgramClauseData::ForAll(implication) => {
+                    self.solve_via_implication(canonical_goal, implication, minimums)
+                }
+            };
+            if let (Ok(solution), priority) = res {
+                debug!("ok: solution={:?} prio={:?}", solution, priority);
+                cur_solution = Some(match cur_solution {
+                    None => (solution, priority),
+                    Some((cur, cur_priority)) => combine::with_priorities(
+                        self.interner(),
+                        &canonical_goal.canonical.value.goal,
+                        cur,
+                        cur_priority,
+                        solution,
+                        priority,
+                    ),
+                });
+            } else {
+                debug!("error");
+            }
+        }
+        cur_solution.map_or((Err(NoSolution), ClausePriority::High), |(s, p)| (Ok(s), p))
+    }
+
+    /// Modus ponens! That is: try to apply an implication by proving its premises.
+    fn solve_via_implication(
+        &mut self,
+        canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
+        clause: &Binders<ProgramClauseImplication<I>>,
+        minimums: &mut Minimums,
+    ) -> (Fallible<Solution<I>>, ClausePriority) {
+        info_heading!(
+            "solve_via_implication(\
+         \n    canonical_goal={:?},\
+         \n    clause={:?})",
+            canonical_goal,
+            clause
+        );
+
+        let (infer, subst, goal) = self.new_inference_table(canonical_goal);
+        match Fulfill::new_with_clause(self, infer, subst, goal, clause) {
+            Ok(fulfill) => (fulfill.solve(minimums), clause.skip_binders().priority),
+            Err(e) => (Err(e), ClausePriority::High),
+        }
+    }
+
+    fn new_inference_table<T: Fold<I, I, Result = T> + HasInterner<Interner = I> + Clone>(
+        &self,
+        ucanonical_goal: &UCanonical<InEnvironment<T>>,
+    ) -> (
+        RecursiveInferenceTableImpl<I>,
+        Substitution<I>,
+        InEnvironment<T::Result>,
+    ) {
+        let (infer, subst, canonical_goal) = InferenceTable::from_canonical(
+            self.interner(),
+            ucanonical_goal.universes,
+            &ucanonical_goal.canonical,
+        );
+        let infer = RecursiveInferenceTableImpl { infer };
+        (infer, subst, canonical_goal)
+    }
+
+    fn program_clauses_for_goal(
+        &self,
+        environment: &Environment<I>,
+        goal: &DomainGoal<I>,
+    ) -> Result<Vec<ProgramClause<I>>, Floundered> {
+        program_clauses_for_goal(self.db(), environment, goal)
+    }
+}
+
+impl<S, I> SolveIterationHelpers<I> for S
+where
+    S: SolveDatabase<I>,
+    I: Interner,
+{
+}
+
+struct RecursiveInferenceTableImpl<I: Interner> {
+    infer: InferenceTable<I>,
+}
+
+impl<I: Interner> RecursiveInferenceTable<I> for RecursiveInferenceTableImpl<I> {
+    fn instantiate_binders_universally<'a, T>(
+        &mut self,
+        interner: &'a I,
+        arg: &'a Binders<T>,
+    ) -> T::Result
+    where
+        T: Fold<I> + HasInterner<Interner = I>,
+    {
+        self.infer.instantiate_binders_universally(interner, arg)
+    }
+
+    fn instantiate_binders_existentially<'a, T>(
+        &mut self,
+        interner: &'a I,
+        arg: &'a Binders<T>,
+    ) -> T::Result
+    where
+        T: Fold<I> + HasInterner<Interner = I>,
+    {
+        self.infer.instantiate_binders_existentially(interner, arg)
+    }
+
+    fn canonicalize<T>(
+        &mut self,
+        interner: &I,
+        value: &T,
+    ) -> (Canonical<T::Result>, Vec<GenericArg<I>>)
+    where
+        T: Fold<I>,
+        T::Result: HasInterner<Interner = I>,
+    {
+        let res = self.infer.canonicalize(interner, value);
+        let free_vars = res
+            .free_vars
+            .into_iter()
+            .map(|free_var| free_var.to_generic_arg(interner))
+            .collect();
+        (res.quantified, free_vars)
+    }
+
+    fn u_canonicalize<T>(
+        &mut self,
+        interner: &I,
+        value0: &Canonical<T>,
+    ) -> (UCanonical<T::Result>, UniverseMap)
+    where
+        T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
+        T::Result: HasInterner<Interner = I>,
+    {
+        let res = self.infer.u_canonicalize(interner, value0);
+        (res.quantified, res.universes)
+    }
+
+    fn unify<T>(
+        &mut self,
+        interner: &I,
+        environment: &Environment<I>,
+        a: &T,
+        b: &T,
+    ) -> Fallible<(
+        Vec<InEnvironment<DomainGoal<I>>>,
+        Vec<InEnvironment<Constraint<I>>>,
+    )>
+    where
+        T: ?Sized + Zip<I>,
+    {
+        let res = self.infer.unify(interner, environment, a, b)?;
+        Ok((res.goals, res.constraints))
+    }
+
+    fn instantiate_canonical<T>(&mut self, interner: &I, bound: &Canonical<T>) -> T::Result
+    where
+        T: HasInterner<Interner = I> + Fold<I> + Debug,
+    {
+        self.infer.instantiate_canonical(interner, bound)
+    }
+
+    fn invert_then_canonicalize<T>(
+        &mut self,
+        interner: &I,
+        value: &T,
+    ) -> Option<Canonical<T::Result>>
+    where
+        T: Fold<I, Result = T> + HasInterner<Interner = I>,
+    {
+        self.infer.invert_then_canonicalize(interner, value)
+    }
+
+    fn needs_truncation(&mut self, interner: &I, max_size: usize, value: impl Visit<I>) -> bool {
+        truncate::needs_truncation(interner, &mut self.infer, max_size, value)
+    }
+}