diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index a9107d9faca..19cb0d0a00b 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -1,14 +1,30 @@
 use crate::fallible::Fallible;
 use crate::hh::HhGoal;
-use crate::{ExClause, SimplifiedAnswer};
+use crate::{DelayedLiteral, ExClause, SimplifiedAnswer};
 use std::fmt::Debug;
 use std::hash::Hash;
 
 crate mod prelude;
 
-/// The "context" in which the SLG solver operates.
-// FIXME(leodasvacas): Clone and Debug bounds are just for easy derive,
-//                     they are not actually necessary.
+/// The "context" in which the SLG solver operates. It defines all the
+/// types that the SLG solver may need to refer to, as well as a few
+/// very simple interconversion methods.
+///
+/// At any given time, the SLG solver may have more than one context
+/// active. First, there is always the *global* context, but when we
+/// are in the midst of pursuing some particular strand, we will
+/// instantiate a second context just for that work, via the
+/// `instantiate_ucanonical_goal` and `instantiate_ex_clause` methods.
+///
+/// In the chalk implementation, these two contexts are mapped to the
+/// same type. But in the rustc implementation, this second context
+/// corresponds to a fresh arena, and data allocated in that second
+/// context will be freed once the work is done. (The "canonicalizing"
+/// steps offer a way to convert data from the inference context back
+/// into the global context.)
+///
+/// FIXME: Clone and Debug bounds are just for easy derive, they are
+/// not actually necessary. But dang are they convenient.
 pub trait Context: Clone + Debug {
     type CanonicalExClause: Debug;
 
@@ -17,12 +33,6 @@ pub trait Context: Clone + Debug {
     /// the universes from the original.
     type UniverseMap: Clone + Debug;
 
-    /// Part of an answer: represents a canonicalized substitution,
-    /// combined with region constraints. See [the rustc-guide] for more information.
-    ///
-    /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
-    type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;
-
     /// Extracted from a canonicalized substitution or canonicalized ex clause, this is the type of
     /// substitution that is fully normalized with respect to inference variables.
     type InferenceNormalizedSubst: Debug;
@@ -43,9 +53,13 @@ pub trait Context: Clone + Debug {
     /// completely opaque to the SLG solver; it is produced by
     /// `make_solution`.
     type Solution;
-}
 
-pub trait ExClauseContext<C: Context>: Sized + Debug {
+    /// Part of an answer: represents a canonicalized substitution,
+    /// combined with region constraints. See [the rustc-guide] for more information.
+    ///
+    /// [the rustc-guide]: https://rust-lang-nursery.github.io/rustc-guide/traits-canonicalization.html#canonicalizing-the-query-result
+    type CanonicalConstrainedSubst: Clone + Debug + Eq + Hash;
+
     /// Represents a substitution from the "canonical variables" found
     /// in a canonical goal to specific values.
     type Substitution: Debug;
@@ -56,12 +70,7 @@ pub trait ExClauseContext<C: Context>: Sized + Debug {
 
     /// Represents a goal along with an environment.
     type GoalInEnvironment: Debug + Clone + Eq + Hash;
-}
 
-/// The set of types belonging to an "inference context"; in rustc,
-/// these types are tied to the lifetime of the arena within which an
-/// inference context operates.
-pub trait InferenceContext<C: Context>: ExClauseContext<C> {
     /// Represents a set of hypotheses that are assumed to be true.
     type Environment: Debug + Clone;
 
@@ -91,10 +100,15 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
     /// goal we are trying to solve to produce an ex-clause.
     type ProgramClause: Debug;
 
+    /// A vector of program clauses.
+    type ProgramClauses: Debug;
+
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
     type UnificationResult;
 
+    /// Given an environment and a goal, glue them together to create
+    /// a `GoalInEnvironment`.
     fn goal_in_environment(
         environment: &Self::Environment,
         goal: Self::Goal,
@@ -105,26 +119,6 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
 
     /// Create a "cannot prove" goal (see `HhGoal::CannotProve`).
     fn cannot_prove() -> Self::Goal;
-
-    /// Convert the context's goal type into the `HhGoal` type that
-    /// the SLG solver understands. The expectation is that the
-    /// context's goal type has the same set of variants, but with
-    /// different names and a different setup. If you inspect
-    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
-    /// conversion -- that is, we convert the outermost goal into an
-    /// `HhGoal`, but the goals contained within are left as context
-    /// goals.
-    fn into_hh_goal(goal: Self::Goal) -> HhGoal<C, Self>;
-
-    /// Add the residual subgoals as new subgoals of the ex-clause.
-    /// Also add region constraints.
-    fn into_ex_clause(result: Self::UnificationResult, ex_clause: &mut ExClause<C, Self>);
-
-    // Used by: simplify
-    fn add_clauses(
-        env: &Self::Environment,
-        clauses: impl IntoIterator<Item = Self::ProgramClause>,
-    ) -> Self::Environment;
 }
 
 pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
@@ -201,7 +195,7 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
 pub trait WithInstantiatedUCanonicalGoal<C: Context> {
     type Output;
 
-    fn with<I: InferenceContext<C>>(
+    fn with<I: Context>(
         self,
         infer: &mut dyn InferenceTable<C, I>,
         subst: I::Substitution,
@@ -219,10 +213,10 @@ pub trait WithInstantiatedUCanonicalGoal<C: Context> {
 pub trait WithInstantiatedExClause<C: Context> {
     type Output;
 
-    fn with<I: InferenceContext<C>>(
+    fn with<I: Context>(
         self,
         infer: &mut dyn InferenceTable<C, I>,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
     ) -> Self::Output;
 }
 
@@ -237,13 +231,29 @@ pub trait AggregateOps<C: Context> {
 
 /// An "inference table" contains the state to support unification and
 /// other operations on terms.
-pub trait InferenceTable<C: Context, I: InferenceContext<C>>:
+pub trait InferenceTable<C: Context, I: Context>:
     ResolventOps<C, I> + TruncateOps<C, I> + UnificationOps<C, I>
 {
+    /// Convert the context's goal type into the `HhGoal` type that
+    /// the SLG solver understands. The expectation is that the
+    /// context's goal type has the same set of variants, but with
+    /// different names and a different setup. If you inspect
+    /// `HhGoal`, you will see that this is a "shallow" or "lazy"
+    /// conversion -- that is, we convert the outermost goal into an
+    /// `HhGoal`, but the goals contained within are left as context
+    /// goals.
+    fn into_hh_goal(&mut self, goal: I::Goal) -> HhGoal<I>;
+
+    // Used by: simplify
+    fn add_clauses(
+        &mut self,
+        env: &I::Environment,
+        clauses: I::ProgramClauses,
+    ) -> I::Environment;
 }
 
 /// Methods for unifying and manipulating terms and binders.
-pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
+pub trait UnificationOps<C: Context, I: Context> {
     /// Returns the set of program clauses that might apply to
     /// `goal`. (This set can be over-approximated, naturally.)
     fn program_clauses(
@@ -259,13 +269,13 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
     fn instantiate_binders_existentially(&mut self, arg: &I::BindersGoal) -> I::Goal;
 
     // Used by: logic (but for debugging only)
-    fn debug_ex_clause(&mut self, value: &'v ExClause<C, I>) -> Box<dyn Debug + 'v>;
+    fn debug_ex_clause(&mut self, value: &'v ExClause<I>) -> Box<dyn Debug + 'v>;
 
     // Used by: logic
     fn canonicalize_goal(&mut self, value: &I::GoalInEnvironment) -> C::CanonicalGoalInEnvironment;
 
     // Used by: logic
-    fn canonicalize_ex_clause(&mut self, value: &ExClause<C, I>) -> C::CanonicalExClause;
+    fn canonicalize_ex_clause(&mut self, value: &ExClause<I>) -> C::CanonicalExClause;
 
     // Used by: logic
     fn canonicalize_constrained_subst(
@@ -280,6 +290,16 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
         value: &C::CanonicalGoalInEnvironment,
     ) -> (C::UCanonicalGoalInEnvironment, C::UniverseMap);
 
+    fn sink_answer_subset(
+        &self,
+        value: &C::CanonicalConstrainedSubst,
+    ) -> I::CanonicalConstrainedSubst;
+
+    fn lift_delayed_literal(
+        &self,
+        value: DelayedLiteral<I>,
+    ) -> DelayedLiteral<C>;
+
     // Used by: logic
     fn invert_goal(&mut self, value: &I::GoalInEnvironment) -> Option<I::GoalInEnvironment>;
 
@@ -290,6 +310,10 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
         a: &I::Parameter,
         b: &I::Parameter,
     ) -> Fallible<I::UnificationResult>;
+
+    /// Add the residual subgoals as new subgoals of the ex-clause.
+    /// Also add region constraints.
+    fn into_ex_clause(&mut self, result: I::UnificationResult, ex_clause: &mut ExClause<I>);
 }
 
 /// "Truncation" (called "abstraction" in the papers referenced below)
@@ -304,7 +328,7 @@ pub trait UnificationOps<C: Context, I: InferenceContext<C>> {
 ///   - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
 /// - Radial Restraint
 ///   - Grosof and Swift; 2013
-pub trait TruncateOps<C: Context, I: InferenceContext<C>> {
+pub trait TruncateOps<C: Context, I: Context> {
     /// If `subgoal` is too large, return a truncated variant (else
     /// return `None`).
     fn truncate_goal(&mut self, subgoal: &I::GoalInEnvironment) -> Option<I::GoalInEnvironment>;
@@ -314,7 +338,7 @@ pub trait TruncateOps<C: Context, I: InferenceContext<C>> {
     fn truncate_answer(&mut self, subst: &I::Substitution) -> Option<I::Substitution>;
 }
 
-pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
+pub trait ResolventOps<C: Context, I: Context> {
     /// Combines the `goal` (instantiated within `infer`) with the
     /// given program clause to yield the start of a new strand (a
     /// canonical ex-clause).
@@ -330,11 +354,11 @@ pub trait ResolventOps<C: Context, I: InferenceContext<C>> {
 
     fn apply_answer_subst(
         &mut self,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
         selected_goal: &I::GoalInEnvironment,
         answer_table_goal: &C::CanonicalGoalInEnvironment,
         canonical_answer_subst: &C::CanonicalConstrainedSubst,
-    ) -> Fallible<ExClause<C, I>>;
+    ) -> Fallible<ExClause<I>>;
 }
 
 pub trait AnswerStream<C: Context> {
diff --git a/chalk-engine/src/context/prelude.rs b/chalk-engine/src/context/prelude.rs
index 39cf99b0904..978d14f5ae2 100644
--- a/chalk-engine/src/context/prelude.rs
+++ b/chalk-engine/src/context/prelude.rs
@@ -6,4 +6,3 @@ crate use super::AggregateOps;
 crate use super::ResolventOps;
 crate use super::TruncateOps;
 crate use super::InferenceTable;
-crate use super::InferenceContext;
diff --git a/chalk-engine/src/derived.rs b/chalk-engine/src/derived.rs
index 9855ab5ee74..37b95ad1909 100644
--- a/chalk-engine/src/derived.rs
+++ b/chalk-engine/src/derived.rs
@@ -65,8 +65,8 @@ impl<C: Context> Hash for DelayedLiteral<C> {
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<C: Context, I: ExClauseContext<C>> PartialEq for Literal<C, I> {
-    fn eq(&self, other: &Literal<C, I>) -> bool {
+impl<C: Context> PartialEq for Literal<C> {
+    fn eq(&self, other: &Literal<C>) -> bool {
         match (self, other) {
             (Literal::Positive(goal1), Literal::Positive(goal2))
             | (Literal::Negative(goal1), Literal::Negative(goal2)) => goal1 == goal2,
@@ -76,10 +76,10 @@ impl<C: Context, I: ExClauseContext<C>> PartialEq for Literal<C, I> {
     }
 }
 
-impl<C: Context, I: ExClauseContext<C>> Eq for Literal<C, I> {
+impl<C: Context> Eq for Literal<C> {
 }
 
-impl<C: Context, I: ExClauseContext<C>> Hash for Literal<C, I> {
+impl<C: Context> Hash for Literal<C> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         mem::discriminant(self).hash(state);
         match self {
diff --git a/chalk-engine/src/hh.rs b/chalk-engine/src/hh.rs
index 29494acc01c..39af0ec6caf 100644
--- a/chalk-engine/src/hh.rs
+++ b/chalk-engine/src/hh.rs
@@ -1,17 +1,17 @@
-use crate::context::{Context, InferenceContext};
+use crate::context::Context;
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
 /// A general goal; this is the full range of questions you can pose to Chalk.
-pub enum HhGoal<C: Context, I: InferenceContext<C>> {
+pub enum HhGoal<C: Context> {
     /// Introduces a binding at depth 0, shifting other bindings up
     /// (deBruijn index).
-    ForAll(I::BindersGoal),
-    Exists(I::BindersGoal),
-    Implies(Vec<I::ProgramClause>, I::Goal),
-    And(I::Goal, I::Goal),
-    Not(I::Goal),
-    Unify(I::Parameter, I::Parameter),
-    DomainGoal(I::DomainGoal),
+    ForAll(C::BindersGoal),
+    Exists(C::BindersGoal),
+    Implies(C::ProgramClauses, C::Goal),
+    And(C::Goal, C::Goal),
+    Not(C::Goal),
+    Unify(C::Parameter, C::Parameter),
+    DomainGoal(C::DomainGoal),
 
     /// Indicates something that cannot be proven to be true or false
     /// definitively. This can occur with overflow but also with
diff --git a/chalk-engine/src/lib.rs b/chalk-engine/src/lib.rs
index a8650b81e43..805bdacc2e7 100644
--- a/chalk-engine/src/lib.rs
+++ b/chalk-engine/src/lib.rs
@@ -66,7 +66,7 @@
 extern crate stacker;
 extern crate fxhash;
 
-use crate::context::{Context, ExClauseContext};
+use crate::context::Context;
 use fxhash::FxHashSet;
 use std::cmp::min;
 use std::usize;
@@ -111,20 +111,20 @@ struct DepthFirstNumber {
 
 /// The paper describes these as `A :- D | G`.
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
-pub struct ExClause<C: Context, E: ExClauseContext<C>> {
+pub struct ExClause<C: Context> {
     /// The substitution which, applied to the goal of our table,
     /// would yield A.
-    pub subst: E::Substitution,
+    pub subst: C::Substitution,
 
     /// Delayed literals: things that we depend on negatively,
     /// but which have not yet been fully evaluated.
     pub delayed_literals: Vec<DelayedLiteral<C>>,
 
     /// Region constraints we have accumulated.
-    pub constraints: Vec<E::RegionConstraint>,
+    pub constraints: Vec<C::RegionConstraint>,
 
     /// Subgoals: literals that must be proven
-    pub subgoals: Vec<Literal<C, E>>,
+    pub subgoals: Vec<Literal<C>>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -194,9 +194,9 @@ pub enum DelayedLiteral<C: Context> {
 
 /// Either `A` or `~A`, where `A` is a `Env |- Goal`.
 #[derive(Clone, Debug)]
-pub enum Literal<C: Context, E: ExClauseContext<C>> { // FIXME: pub b/c fold
-    Positive(E::GoalInEnvironment),
-    Negative(E::GoalInEnvironment),
+pub enum Literal<C: Context> { // FIXME: pub b/c fold
+    Positive(C::GoalInEnvironment),
+    Negative(C::GoalInEnvironment),
 }
 
 /// The `Minimums` structure is used to track the dependencies between
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
index d58ae1c1fec..ee2d27b6999 100644
--- a/chalk-engine/src/logic.rs
+++ b/chalk-engine/src/logic.rs
@@ -293,10 +293,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
             WithInstantiatedExClause<C> for With<C, CO, OP> {
             type Output = OP::Output;
 
-            fn with<I: InferenceContext<C>>(
+            fn with<I: Context>(
                 self,
                 infer: &mut dyn InferenceTable<C, I>,
-                ex_clause: ExClause<C, I>,
+                ex_clause: ExClause<I>,
             ) -> OP::Output {
                 self.op.with(Strand {
                     infer,
@@ -307,7 +307,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
     }
 
-    fn canonicalize_strand(strand: Strand<'_, C, impl InferenceContext<C>>) -> CanonicalStrand<C> {
+    fn canonicalize_strand(strand: Strand<'_, C, impl Context>) -> CanonicalStrand<C> {
         let Strand {
             infer,
             ex_clause,
@@ -316,9 +316,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         Self::canonicalize_strand_from(&mut *infer, &ex_clause, selected_subgoal)
     }
 
-    fn canonicalize_strand_from<I: InferenceContext<C>>(
+    fn canonicalize_strand_from<I: Context>(
         infer: &mut dyn InferenceTable<C, I>,
-        ex_clause: &ExClause<C, I>,
+        ex_clause: &ExClause<I>,
         selected_subgoal: Option<SelectedSubgoal<C>>,
     ) -> CanonicalStrand<C> {
         let canonical_ex_clause = infer.canonicalize_ex_clause(&ex_clause);
@@ -431,7 +431,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
 
     fn delay_strand_after_cycle(
         table: TableIndex,
-        mut strand: Strand<'_, C, impl InferenceContext<C>>,
+        mut strand: Strand<'_, C, impl Context>,
     ) -> (CanonicalStrand<C>, TableIndex) {
         let (subgoal_index, subgoal_table) = match &strand.selected_subgoal {
             Some(selected_subgoal) => (
@@ -467,7 +467,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn pursue_strand(
         &mut self,
         depth: StackIndex,
-        mut strand: Strand<'_, C, impl InferenceContext<C>>,
+        mut strand: Strand<'_, C, impl Context>,
     ) -> StrandResult<C, ()> {
         info_heading!(
             "pursue_strand(table={:?}, depth={:?}, ex_clause={:#?}, selected_subgoal={:?})",
@@ -541,7 +541,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn pursue_answer(
         &mut self,
         depth: StackIndex,
-        strand: Strand<'_, C, impl InferenceContext<C>>,
+        strand: Strand<'_, C, impl Context>,
     ) -> StrandResult<C, ()> {
         let table = self.stack[depth].table;
         let Strand {
@@ -561,7 +561,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         debug!("answer: table={:?}, answer_subst={:?}", table, answer_subst);
 
         let delayed_literals = {
-            let mut delayed_literals: FxHashSet<_> = delayed_literals.into_iter().collect();
+            let mut delayed_literals: FxHashSet<_> = delayed_literals.into_iter()
+                .map(|dl| infer.lift_delayed_literal(dl))
+                .collect();
             DelayedLiteralSet { delayed_literals }
         };
         debug!("answer: delayed_literals={:?}", delayed_literals);
@@ -660,10 +662,10 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// In terms of the NFTD paper, creating a new table corresponds
     /// to the *New Subgoal* step as well as the *Program Clause
     /// Resolution* steps.
-    fn get_or_create_table_for_subgoal<I: InferenceContext<C>>(
+    fn get_or_create_table_for_subgoal<I: Context>(
         &mut self,
         infer: &mut dyn InferenceTable<C, I>,
-        subgoal: &Literal<C, I>,
+        subgoal: &Literal<I>,
     ) -> Option<(TableIndex, C::UniverseMap)> {
         debug_heading!("get_or_create_table_for_subgoal(subgoal={:?})", subgoal);
 
@@ -739,7 +741,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                                                 for PushInitialStrandsInstantiated<'a, C, CO> {
             type Output = ();
 
-            fn with<I: InferenceContext<C>>(
+            fn with<I: Context>(
                 self,
                 infer: &mut dyn InferenceTable<C, I>,
                 subst: I::Substitution,
@@ -752,7 +754,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
     }
 
-    fn push_initial_strands_instantiated<I: InferenceContext<C>>(
+    fn push_initial_strands_instantiated<I: Context>(
         &mut self,
         table: TableIndex,
         infer: &mut dyn InferenceTable<C, I>,
@@ -761,7 +763,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         goal: I::Goal,
     ) {
         let table_ref = &mut self.tables[table];
-        match I::into_hh_goal(goal) {
+        match infer.into_hh_goal(goal) {
             HhGoal::DomainGoal(domain_goal) => {
                 let clauses = infer.program_clauses(&environment, &domain_goal);
                 for clause in clauses {
@@ -812,7 +814,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// truncate the goal to ensure termination.
     ///
     /// This technique is described in the SA paper.
-    fn abstract_positive_literal<I: InferenceContext<C>>(
+    fn abstract_positive_literal<I: Context>(
         &mut self,
         infer: &mut dyn InferenceTable<C, I>,
         subgoal: &I::GoalInEnvironment,
@@ -856,7 +858,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// fail to yield a useful result, for example if free existential
     /// variables appear in `subgoal` (in which case the execution is
     /// said to "flounder").
-    fn abstract_negative_literal<I: InferenceContext<C>>(
+    fn abstract_negative_literal<I: Context>(
         &mut self,
         infer: &mut dyn InferenceTable<C, I>,
         subgoal: &I::GoalInEnvironment,
@@ -971,7 +973,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn pursue_positive_subgoal(
         &mut self,
         depth: StackIndex,
-        mut strand: Strand<'_, C, impl InferenceContext<C>>,
+        mut strand: Strand<'_, C, impl Context>,
         selected_subgoal: &SelectedSubgoal<C>,
     ) -> StrandResult<C, ()> {
         let table = self.stack[depth].table;
@@ -1064,7 +1066,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                     if !answer.delayed_literals.is_empty() {
                         ex_clause.delayed_literals.push(DelayedLiteral::Positive(
                             subgoal_table,
-                            answer.subst.clone(),
+                            infer.sink_answer_subset(&answer.subst),
                         ));
                     }
                 }
@@ -1095,11 +1097,11 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// Used whenever we process an answer (whether new or cached) on
     /// a positive edge (the SLG POSITIVE RETURN operation). Truncates
     /// the resolvent (or factor) if it has grown too large.
-    fn truncate_returned<I: InferenceContext<C>>(
+    fn truncate_returned<I: Context>(
         &self,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
         infer: &mut dyn InferenceTable<C, I>,
-    ) -> ExClause<C, I> {
+    ) -> ExClause<I> {
         // DIVERGENCE
         //
         // In the original RR paper, truncation is only applied
@@ -1162,7 +1164,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn pursue_strand_recursively(
         &mut self,
         depth: StackIndex,
-        strand: Strand<'_, C, impl InferenceContext<C>>,
+        strand: Strand<'_, C, impl Context>,
     ) -> StrandResult<C, ()> {
         ::crate::maybe_grow_stack(|| self.pursue_strand(depth, strand))
     }
@@ -1173,7 +1175,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn push_strand_pursuing_next_answer(
         &mut self,
         depth: StackIndex,
-        strand: &mut Strand<'_, C, impl InferenceContext<C>>,
+        strand: &mut Strand<'_, C, impl Context>,
         selected_subgoal: &SelectedSubgoal<C>,
     ) {
         let table = self.stack[depth].table;
@@ -1189,7 +1191,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn pursue_negative_subgoal(
         &mut self,
         depth: StackIndex,
-        strand: Strand<'_, C, impl InferenceContext<C>>,
+        strand: Strand<'_, C, impl Context>,
         selected_subgoal: &SelectedSubgoal<C>,
     ) -> StrandResult<C, ()> {
         let table = self.stack[depth].table;
@@ -1208,7 +1210,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         // literal (in which case the negative literal *may* be true).
         // Before exiting the match, then, we set `delayed_literal` to
         // either `Some` or `None` depending.
-        let delayed_literal: Option<DelayedLiteral<C>>;
+        let delayed_literal: Option<DelayedLiteral<_>>;
         match self.ensure_answer_recursively(subgoal_table, answer_index) {
             Ok(EnsureSuccess::AnswerAvailable) => {
                 if self.answer(subgoal_table, answer_index).is_unconditional() {
@@ -1309,7 +1311,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
 trait WithInstantiatedStrand<C: Context, CO: AggregateOps<C>> {
     type Output;
 
-    fn with(self, strand: Strand<'_, C, impl InferenceContext<C>>) -> Self::Output;
+    fn with(self, strand: Strand<'_, C, impl Context>) -> Self::Output;
 }
 
 struct PursueStrand<'a, C: Context + 'a, CO: ContextOps<C> + 'a> {
@@ -1320,7 +1322,7 @@ struct PursueStrand<'a, C: Context + 'a, CO: ContextOps<C> + 'a> {
 impl<C: Context, CO: ContextOps<C>> WithInstantiatedStrand<C, CO> for PursueStrand<'a, C, CO> {
     type Output = StrandResult<C, ()>;
 
-    fn with(self, strand: Strand<'_, C, impl InferenceContext<C>>) -> Self::Output {
+    fn with(self, strand: Strand<'_, C, impl Context>) -> Self::Output {
         self.forest.pursue_strand(self.depth, strand)
     }
 }
@@ -1332,7 +1334,7 @@ struct DelayStrandAfterCycle {
 impl<C: Context, CO: ContextOps<C>> WithInstantiatedStrand<C, CO> for DelayStrandAfterCycle {
     type Output = (CanonicalStrand<C>, TableIndex);
 
-    fn with(self, strand: Strand<'_, C, impl InferenceContext<C>>) -> Self::Output {
+    fn with(self, strand: Strand<'_, C, impl Context>) -> Self::Output {
         <Forest<C, CO>>::delay_strand_after_cycle(self.table, strand)
     }
 }
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
index 098031a29a2..b98efa7569e 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -8,12 +8,12 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// Simplifies an HH goal into a series of positive domain goals
     /// and negative HH goals. This operation may fail if the HH goal
     /// includes unifications that cannot be completed.
-    pub(super) fn simplify_hh_goal<I: InferenceContext<C>>(
+    pub(super) fn simplify_hh_goal<I: Context>(
         infer: &mut dyn InferenceTable<C, I>,
         subst: I::Substitution,
         initial_environment: &I::Environment,
-        initial_hh_goal: HhGoal<C, I>,
-    ) -> Fallible<ExClause<C, I>> {
+        initial_hh_goal: HhGoal<I>,
+    ) -> Fallible<ExClause<I>> {
         let mut ex_clause = ExClause {
             subst,
             delayed_literals: vec![],
@@ -28,19 +28,19 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
             match hh_goal {
                 HhGoal::ForAll(subgoal) => {
                     let subgoal = infer.instantiate_binders_universally(&subgoal);
-                    pending_goals.push((environment, I::into_hh_goal(subgoal)));
+                    pending_goals.push((environment, infer.into_hh_goal(subgoal)));
                 }
                 HhGoal::Exists(subgoal) => {
                     let subgoal = infer.instantiate_binders_existentially(&subgoal);
-                    pending_goals.push((environment, I::into_hh_goal(subgoal)))
+                    pending_goals.push((environment, infer.into_hh_goal(subgoal)))
                 }
                 HhGoal::Implies(wc, subgoal) => {
-                    let new_environment = I::add_clauses(&environment, wc);
-                    pending_goals.push((new_environment, I::into_hh_goal(subgoal)));
+                    let new_environment = infer.add_clauses(&environment, wc);
+                    pending_goals.push((new_environment, infer.into_hh_goal(subgoal)));
                 }
                 HhGoal::And(subgoal1, subgoal2) => {
-                    pending_goals.push((environment.clone(), I::into_hh_goal(subgoal1)));
-                    pending_goals.push((environment, I::into_hh_goal(subgoal2)));
+                    pending_goals.push((environment.clone(), infer.into_hh_goal(subgoal1)));
+                    pending_goals.push((environment, infer.into_hh_goal(subgoal2)));
                 }
                 HhGoal::Not(subgoal) => {
                     ex_clause
@@ -48,8 +48,8 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
                         .push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
                 }
                 HhGoal::Unify(a, b) => {
-                    I::into_ex_clause(infer.unify_parameters(&environment, &a, &b)?,
-                                      &mut ex_clause)
+                    let result = infer.unify_parameters(&environment, &a, &b)?;
+                    infer.into_ex_clause(result, &mut ex_clause)
                 }
                 HhGoal::DomainGoal(domain_goal) => {
                     ex_clause
diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs
index b5a9331c8df..1e8ea35ca81 100644
--- a/chalk-engine/src/strand.rs
+++ b/chalk-engine/src/strand.rs
@@ -1,6 +1,6 @@
 use std::fmt::{Debug, Error, Formatter};
 use crate::{ExClause, TableIndex};
-use crate::context::{Context, InferenceContext, InferenceTable};
+use crate::context::{Context, InferenceTable};
 use crate::table::AnswerIndex;
 
 #[derive(Debug)]
@@ -11,10 +11,10 @@ crate struct CanonicalStrand<C: Context> {
     crate selected_subgoal: Option<SelectedSubgoal<C>>,
 }
 
-crate struct Strand<'table, C: Context + 'table, I: InferenceContext<C> + 'table> {
+crate struct Strand<'table, C: Context + 'table, I: Context + 'table> {
     crate infer: &'table mut dyn InferenceTable<C, I>,
 
-    pub(super) ex_clause: ExClause<C, I>,
+    pub(super) ex_clause: ExClause<I>,
 
     /// Index into `ex_clause.subgoals`.
     crate selected_subgoal: Option<SelectedSubgoal<C>>,
@@ -36,7 +36,7 @@ crate struct SelectedSubgoal<C: Context> {
     crate universe_map: C::UniverseMap,
 }
 
-impl<'table, C: Context, I: InferenceContext<C>> Debug for Strand<'table, C, I> {
+impl<'table, C: Context, I: Context> Debug for Strand<'table, C, I> {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         fmt.debug_struct("Strand")
             .field("ex_clause", &self.ex_clause)
diff --git a/src/lib.rs b/src/lib.rs
index 9a87e92b99c..b88e90a91be 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -9,6 +9,7 @@
 #![feature(specialization)]
 #![feature(step_trait)]
 #![feature(non_modrs_mods)]
+#![feature(underscore_imports)]
 
 extern crate chalk_parse;
 #[macro_use]
diff --git a/src/solve/slg/implementation.rs b/src/solve/slg/implementation.rs
index 3d81a24169c..9bedec2f9b8 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -51,12 +51,35 @@ impl SlgContext {
 
 impl context::Context for SlgContext {
     type CanonicalGoalInEnvironment = Canonical<InEnvironment<Goal>>;
-    type CanonicalExClause = Canonical<ExClause<Self, Self>>;
+    type CanonicalExClause = Canonical<ExClause<Self>>;
     type UCanonicalGoalInEnvironment = UCanonical<InEnvironment<Goal>>;
     type UniverseMap = UniverseMap;
-    type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
     type InferenceNormalizedSubst = Substitution;
     type Solution = Solution;
+    type Environment = Arc<Environment>;
+    type DomainGoal = DomainGoal;
+    type Goal = Goal;
+    type BindersGoal = Binders<Box<Goal>>;
+    type Parameter = Parameter;
+    type ProgramClause = ProgramClause;
+    type ProgramClauses = Vec<ProgramClause>;
+    type UnificationResult = UnificationResult;
+    type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
+    type GoalInEnvironment = InEnvironment<Goal>;
+    type Substitution = Substitution;
+    type RegionConstraint = InEnvironment<Constraint>;
+
+    fn goal_in_environment(environment: &Arc<Environment>, goal: Goal) -> InEnvironment<Goal> {
+        InEnvironment::new(environment, goal)
+    }
+
+    fn into_goal(domain_goal: Self::DomainGoal) -> Self::Goal {
+        domain_goal.cast()
+    }
+
+    fn cannot_prove() -> Self::Goal {
+        Goal::CannotProve(())
+    }
 }
 
 impl context::ContextOps<SlgContext> for SlgContext {
@@ -78,7 +101,7 @@ impl context::ContextOps<SlgContext> for SlgContext {
     fn instantiate_ex_clause<R>(
         &self,
         num_universes: usize,
-        canonical_ex_clause: &Canonical<ExClause<SlgContext, SlgContext>>,
+        canonical_ex_clause: &Canonical<ExClause<SlgContext>>,
         op: impl context::WithInstantiatedExClause<Self, Output = R>,
     ) -> R {
         let (infer, _subst, ex_cluse) =
@@ -88,7 +111,7 @@ impl context::ContextOps<SlgContext> for SlgContext {
     }
 
     fn inference_normalized_subst_from_ex_clause(
-        canon_ex_clause: &Canonical<ExClause<SlgContext, SlgContext>>,
+        canon_ex_clause: &Canonical<ExClause<SlgContext>>,
     ) -> &Substitution {
         &canon_ex_clause.value.subst
     }
@@ -161,36 +184,8 @@ impl context::TruncateOps<SlgContext, SlgContext> for TruncatingInferenceTable {
     }
 }
 
-impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTable {}
-
-impl context::ExClauseContext<SlgContext> for SlgContext {
-    type GoalInEnvironment = InEnvironment<Goal>;
-    type Substitution = Substitution;
-    type RegionConstraint = InEnvironment<Constraint>;
-}
-
-impl context::InferenceContext<SlgContext> for SlgContext {
-    type Environment = Arc<Environment>;
-    type DomainGoal = DomainGoal;
-    type Goal = Goal;
-    type BindersGoal = Binders<Box<Goal>>;
-    type Parameter = Parameter;
-    type ProgramClause = ProgramClause;
-    type UnificationResult = UnificationResult;
-
-    fn goal_in_environment(environment: &Arc<Environment>, goal: Goal) -> InEnvironment<Goal> {
-        InEnvironment::new(environment, goal)
-    }
-
-    fn into_goal(domain_goal: Self::DomainGoal) -> Self::Goal {
-        domain_goal.cast()
-    }
-
-    fn cannot_prove() -> Self::Goal {
-        Goal::CannotProve(())
-    }
-
-    fn into_hh_goal(goal: Self::Goal) -> HhGoal<SlgContext, Self> {
+impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTable {
+    fn into_hh_goal(&mut self, goal: Goal) -> HhGoal<SlgContext> {
         match goal {
             Goal::Quantified(QuantifierKind::ForAll, binders_goal) => HhGoal::ForAll(binders_goal),
             Goal::Quantified(QuantifierKind::Exists, binders_goal) => HhGoal::Exists(binders_goal),
@@ -203,21 +198,12 @@ impl context::InferenceContext<SlgContext> for SlgContext {
         }
     }
 
-    fn into_ex_clause(
-        result: Self::UnificationResult,
-        ex_clause: &mut ExClause<SlgContext, SlgContext>,
-    ) {
-        ex_clause
-            .subgoals
-            .extend(result.goals.into_iter().casted().map(Literal::Positive));
-        ex_clause.constraints.extend(result.constraints);
-    }
-
     // Used by: simplify
     fn add_clauses(
-        env: &Self::Environment,
-        clauses: impl IntoIterator<Item = Self::ProgramClause>,
-    ) -> Self::Environment {
+        &mut self,
+        env: &Arc<Environment>,
+        clauses: Vec<ProgramClause>,
+    ) -> Arc<Environment> {
         Environment::add_clauses(env, clauses)
     }
 }
@@ -253,7 +239,7 @@ impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTabl
 
     fn debug_ex_clause(
         &mut self,
-        value: &'v ExClause<SlgContext, SlgContext>,
+        value: &'v ExClause<SlgContext>,
     ) -> Box<dyn Debug + 'v> {
         Box::new(self.infer.normalize_deep(value))
     }
@@ -264,8 +250,8 @@ impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTabl
 
     fn canonicalize_ex_clause(
         &mut self,
-        value: &ExClause<SlgContext, SlgContext>,
-    ) -> Canonical<ExClause<SlgContext, SlgContext>> {
+        value: &ExClause<SlgContext>,
+    ) -> Canonical<ExClause<SlgContext>> {
         self.infer.canonicalize(value).quantified
     }
 
@@ -305,6 +291,37 @@ impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTabl
     ) -> Fallible<UnificationResult> {
         self.infer.unify(environment, a, b)
     }
+
+    /// Since we do not have distinct types for the inference context and the slg-context,
+    /// these conversion operations are just no-ops.q
+    fn sink_answer_subset(&self, c: &Canonical<ConstrainedSubst>) -> Canonical<ConstrainedSubst> {
+        c.clone()
+    }
+
+    /// Since we do not have distinct types for the inference context and the slg-context,
+    /// these conversion operations are just no-ops.q
+    fn lift_delayed_literal(&self, c: DelayedLiteral<SlgContext>) -> DelayedLiteral<SlgContext> {
+        c
+    }
+
+    fn into_ex_clause(
+        &mut self,
+        result: UnificationResult,
+        ex_clause: &mut ExClause<SlgContext>,
+    ) {
+        into_ex_clause(result, ex_clause)
+    }
+}
+
+/// Helper function
+fn into_ex_clause(
+    result: UnificationResult,
+    ex_clause: &mut ExClause<SlgContext>,
+) {
+    ex_clause
+        .subgoals
+        .extend(result.goals.into_iter().casted().map(Literal::Positive));
+    ex_clause.constraints.extend(result.constraints);
 }
 
 impl Substitution {
@@ -453,7 +470,7 @@ impl MayInvalidate {
     }
 }
 
-type ExClauseSlgContext = ExClause<SlgContext, SlgContext>;
+type ExClauseSlgContext = ExClause<SlgContext>;
 struct_fold!(ExClauseSlgContext {
     subst,
     delayed_literals,
@@ -461,7 +478,7 @@ struct_fold!(ExClauseSlgContext {
     subgoals,
 });
 
-type LiteralSlgContext = Literal<SlgContext, SlgContext>;
+type LiteralSlgContext = Literal<SlgContext>;
 enum_fold!(LiteralSlgContext {
     Literal :: {
         Positive(a), Negative(a)
diff --git a/src/solve/slg/implementation/resolvent.rs b/src/solve/slg/implementation/resolvent.rs
index 3d7023b2d8a..65cf83ee767 100644
--- a/src/solve/slg/implementation/resolvent.rs
+++ b/src/solve/slg/implementation/resolvent.rs
@@ -3,10 +3,10 @@ use crate::fold::shift::Shift;
 use crate::fold::Fold;
 use crate::ir::*;
 use crate::solve::infer::InferenceTable;
-use crate::solve::slg::implementation::{SlgContext, TruncatingInferenceTable};
+use crate::solve::slg::implementation::{self, SlgContext, TruncatingInferenceTable};
 use crate::zip::{Zip, Zipper};
 
-use chalk_engine::context::{self, InferenceContext};
+use chalk_engine::context;
 use chalk_engine::{ExClause, Literal};
 use std::sync::Arc;
 
@@ -61,7 +61,7 @@ impl context::ResolventOps<SlgContext, SlgContext> for TruncatingInferenceTable
         goal: &DomainGoal,
         subst: &Substitution,
         clause: &ProgramClause,
-    ) -> Fallible<Canonical<ExClause<SlgContext, SlgContext>>> {
+    ) -> Fallible<Canonical<ExClause<SlgContext>>> {
         // Relating the above description to our situation:
         //
         // - `goal` G, except with binders for any existential variables.
@@ -105,7 +105,7 @@ impl context::ResolventOps<SlgContext, SlgContext> for TruncatingInferenceTable
         };
 
         // Add the subgoals/region-constraints that unification gave us.
-        SlgContext::into_ex_clause(unification_result, &mut ex_clause);
+        implementation::into_ex_clause(unification_result, &mut ex_clause);
 
         // Add the `conditions` from the program clause into the result too.
         ex_clause
@@ -202,11 +202,11 @@ impl context::ResolventOps<SlgContext, SlgContext> for TruncatingInferenceTable
 
     fn apply_answer_subst(
         &mut self,
-        ex_clause: ExClause<SlgContext, SlgContext>,
+        ex_clause: ExClause<SlgContext>,
         selected_goal: &InEnvironment<Goal>,
         answer_table_goal: &Canonical<InEnvironment<Goal>>,
         canonical_answer_subst: &Canonical<ConstrainedSubst>,
-    ) -> Fallible<ExClause<SlgContext, SlgContext>> {
+    ) -> Fallible<ExClause<SlgContext>> {
         debug_heading!("apply_answer_subst()");
         debug!("ex_clause={:?}", ex_clause);
         debug!(
@@ -247,7 +247,7 @@ struct AnswerSubstitutor<'t> {
     answer_subst: &'t Substitution,
     answer_binders: usize,
     pending_binders: usize,
-    ex_clause: ExClause<SlgContext, SlgContext>,
+    ex_clause: ExClause<SlgContext>,
 }
 
 impl<'t> AnswerSubstitutor<'t> {
@@ -255,10 +255,10 @@ impl<'t> AnswerSubstitutor<'t> {
         table: &mut InferenceTable,
         environment: &Arc<Environment>,
         answer_subst: &Substitution,
-        ex_clause: ExClause<SlgContext, SlgContext>,
+        ex_clause: ExClause<SlgContext>,
         answer: &T,
         pending: &T,
-    ) -> Fallible<ExClause<SlgContext, SlgContext>> {
+    ) -> Fallible<ExClause<SlgContext>> {
         let mut this = AnswerSubstitutor {
             table,
             environment,
@@ -293,7 +293,7 @@ impl<'t> AnswerSubstitutor<'t> {
                 )
             });
 
-        SlgContext::into_ex_clause(
+        implementation::into_ex_clause(
             self.table
                 .unify(&self.environment, answer_param, pending_shifted)?,
             &mut self.ex_clause,