From 18c95168ee435e9fb9a8fa0b86667489a60f6e8e Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Sun, 20 May 2018 06:25:39 -0400
Subject: [PATCH 1/6] merge to shared trait

---
 chalk-engine/src/context.rs               | 66 +++++++++++++----------
 chalk-engine/src/context/prelude.rs       |  1 +
 chalk-engine/src/derived.rs               | 18 +++----
 chalk-engine/src/lib.rs                   | 20 +++----
 chalk-engine/src/logic.rs                 | 18 ++++---
 chalk-engine/src/simplify.rs              |  2 +-
 chalk-engine/src/strand.rs                |  2 +-
 chalk-engine/src/table.rs                 |  6 +--
 src/solve/slg/implementation.rs           | 44 +++++++++------
 src/solve/slg/implementation/resolvent.rs | 12 ++---
 10 files changed, 107 insertions(+), 82 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index a9107d9faca..fdabe8fb65b 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -1,15 +1,34 @@
 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;
 
+pub trait ExClauseContext: 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;
+
+    /// Represents a region constraint that will be propagated back
+    /// (but not verified).
+    type RegionConstraint: Debug;
+
+    /// Represents a goal along with an environment.
+    type GoalInEnvironment: Debug + Clone + Eq + Hash;
+}
+
 /// The "context" in which the SLG solver operates.
 // FIXME(leodasvacas): Clone and Debug bounds are just for easy derive,
 //                     they are not actually necessary.
-pub trait Context: Clone + Debug {
+pub trait Context: Clone + Debug + ExClauseContext {
     type CanonicalExClause: Debug;
 
     /// A map between universes. These are produced when
@@ -17,12 +36,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;
@@ -45,23 +58,10 @@ pub trait Context: Clone + Debug {
     type Solution;
 }
 
-pub trait ExClauseContext<C: Context>: Sized + Debug {
-    /// Represents a substitution from the "canonical variables" found
-    /// in a canonical goal to specific values.
-    type Substitution: Debug;
-
-    /// Represents a region constraint that will be propagated back
-    /// (but not verified).
-    type RegionConstraint: 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> {
+pub trait InferenceContext<C: Context>: ExClauseContext {
     /// Represents a set of hypotheses that are assumed to be true.
     type Environment: Debug + Clone;
 
@@ -118,7 +118,7 @@ pub trait InferenceContext<C: Context>: ExClauseContext<C> {
 
     /// 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>);
+    fn into_ex_clause(result: Self::UnificationResult, ex_clause: &mut ExClause<Self>);
 
     // Used by: simplify
     fn add_clauses(
@@ -222,7 +222,7 @@ pub trait WithInstantiatedExClause<C: Context> {
     fn with<I: InferenceContext<C>>(
         self,
         infer: &mut dyn InferenceTable<C, I>,
-        ex_clause: ExClause<C, I>,
+        ex_clause: ExClause<I>,
     ) -> Self::Output;
 }
 
@@ -259,13 +259,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 +280,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>;
 
@@ -330,11 +340,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..a084b09424e 100644
--- a/chalk-engine/src/context/prelude.rs
+++ b/chalk-engine/src/context/prelude.rs
@@ -1,5 +1,6 @@
 #![allow(unused_imports)] // rustc bug
 
+crate use super::ExClauseContext;
 crate use super::Context;
 crate use super::ContextOps;
 crate use super::AggregateOps;
diff --git a/chalk-engine/src/derived.rs b/chalk-engine/src/derived.rs
index 9855ab5ee74..42e3f72cb00 100644
--- a/chalk-engine/src/derived.rs
+++ b/chalk-engine/src/derived.rs
@@ -7,7 +7,7 @@ use std::hash::{Hash, Hasher};
 use std::mem;
 use super::*;
 
-impl<C: Context> PartialEq for DelayedLiteralSet<C> {
+impl<E: ExClauseContext> PartialEq for DelayedLiteralSet<E> {
     fn eq(&self, other: &Self) -> bool {
         let DelayedLiteralSet { delayed_literals: a1 } = self;
         let DelayedLiteralSet { delayed_literals: a2 } = other;
@@ -15,12 +15,12 @@ impl<C: Context> PartialEq for DelayedLiteralSet<C> {
     }
 }
 
-impl<C: Context> Eq for DelayedLiteralSet<C> {
+impl<E: ExClauseContext> Eq for DelayedLiteralSet<E> {
 }
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<C: Context> PartialEq for DelayedLiteral<C> {
+impl<E: ExClauseContext> PartialEq for DelayedLiteral<E> {
     fn eq(&self, other: &Self) -> bool {
         if mem::discriminant(self) != mem::discriminant(other) {
             return false;
@@ -41,10 +41,10 @@ impl<C: Context> PartialEq for DelayedLiteral<C> {
     }
 }
 
-impl<C: Context> Eq for DelayedLiteral<C> {
+impl<E: ExClauseContext> Eq for DelayedLiteral<E> {
 }
 
-impl<C: Context> Hash for DelayedLiteral<C> {
+impl<E: ExClauseContext> Hash for DelayedLiteral<E> {
     fn hash<H: Hasher>(&self, hasher: &mut H) {
         mem::discriminant(self).hash(hasher);
 
@@ -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<I: ExClauseContext> PartialEq for Literal<I> {
+    fn eq(&self, other: &Literal<I>) -> 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<I: ExClauseContext> Eq for Literal<I> {
 }
 
-impl<C: Context, I: ExClauseContext<C>> Hash for Literal<C, I> {
+impl<I: ExClauseContext> Hash for Literal<I> {
     fn hash<H: Hasher>(&self, state: &mut H) {
         mem::discriminant(self).hash(state);
         match self {
diff --git a/chalk-engine/src/lib.rs b/chalk-engine/src/lib.rs
index a8650b81e43..bc88f4458ec 100644
--- a/chalk-engine/src/lib.rs
+++ b/chalk-engine/src/lib.rs
@@ -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<E: ExClauseContext> {
     /// The substitution which, applied to the goal of our table,
     /// would yield A.
     pub subst: E::Substitution,
 
     /// Delayed literals: things that we depend on negatively,
     /// but which have not yet been fully evaluated.
-    pub delayed_literals: Vec<DelayedLiteral<C>>,
+    pub delayed_literals: Vec<DelayedLiteral<E>>,
 
     /// Region constraints we have accumulated.
     pub constraints: Vec<E::RegionConstraint>,
 
     /// Subgoals: literals that must be proven
-    pub subgoals: Vec<Literal<C, E>>,
+    pub subgoals: Vec<Literal<E>>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -170,12 +170,12 @@ enum InnerDelayedLiteralSets<C: Context> {
 /// delayed literal, which in turn forces its subgoal to be delayed,
 /// and so forth. Therefore, we store canonicalized goals.)
 #[derive(Clone, Debug, Default)]
-struct DelayedLiteralSet<C: Context> {
-    delayed_literals: FxHashSet<DelayedLiteral<C>>,
+struct DelayedLiteralSet<E: ExClauseContext> {
+    delayed_literals: FxHashSet<DelayedLiteral<E>>,
 }
 
 #[derive(Clone, Debug)]
-pub enum DelayedLiteral<C: Context> {
+pub enum DelayedLiteral<E: ExClauseContext> {
     /// Something which can never be proven nor disproven. Inserted
     /// when truncation triggers; doesn't arise normally.
     CannotProve(()),
@@ -189,12 +189,12 @@ pub enum DelayedLiteral<C: Context> {
     /// **conditional** answer (the `CanonicalConstrainedSubst`) within the
     /// given table, but we have to come back later and see whether
     /// that answer turns out to be true.
-    Positive(TableIndex, C::CanonicalConstrainedSubst),
+    Positive(TableIndex, E::CanonicalConstrainedSubst),
 }
 
 /// 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
+pub enum Literal<E: ExClauseContext> { // FIXME: pub b/c fold
     Positive(E::GoalInEnvironment),
     Negative(E::GoalInEnvironment),
 }
@@ -272,12 +272,12 @@ impl<C: Context> DelayedLiteralSets<C> {
     }
 }
 
-impl<C: Context> DelayedLiteralSet<C> {
+impl<E: ExClauseContext> DelayedLiteralSet<E> {
     fn is_empty(&self) -> bool {
         self.delayed_literals.is_empty()
     }
 
-    fn is_subset(&self, other: &DelayedLiteralSet<C>) -> bool {
+    fn is_subset(&self, other: &DelayedLiteralSet<E>) -> bool {
         self.delayed_literals
             .iter()
             .all(|elem| other.delayed_literals.contains(elem))
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
index d58ae1c1fec..5842e2f2b87 100644
--- a/chalk-engine/src/logic.rs
+++ b/chalk-engine/src/logic.rs
@@ -296,7 +296,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
             fn with<I: InferenceContext<C>>(
                 self,
                 infer: &mut dyn InferenceTable<C, I>,
-                ex_clause: ExClause<C, I>,
+                ex_clause: ExClause<I>,
             ) -> OP::Output {
                 self.op.with(Strand {
                     infer,
@@ -318,7 +318,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
 
     fn canonicalize_strand_from<I: InferenceContext<C>>(
         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);
@@ -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);
@@ -663,7 +665,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     fn get_or_create_table_for_subgoal<I: InferenceContext<C>>(
         &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);
 
@@ -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),
                         ));
                     }
                 }
@@ -1097,9 +1099,9 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// the resolvent (or factor) if it has grown too large.
     fn truncate_returned<I: InferenceContext<C>>(
         &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
@@ -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() {
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
index 098031a29a2..76d6c3f26ec 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -13,7 +13,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         subst: I::Substitution,
         initial_environment: &I::Environment,
         initial_hh_goal: HhGoal<C, I>,
-    ) -> Fallible<ExClause<C, I>> {
+    ) -> Fallible<ExClause<I>> {
         let mut ex_clause = ExClause {
             subst,
             delayed_literals: vec![],
diff --git a/chalk-engine/src/strand.rs b/chalk-engine/src/strand.rs
index b5a9331c8df..2353908c63f 100644
--- a/chalk-engine/src/strand.rs
+++ b/chalk-engine/src/strand.rs
@@ -14,7 +14,7 @@ crate struct CanonicalStrand<C: Context> {
 crate struct Strand<'table, C: Context + 'table, I: InferenceContext<C> + '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>>,
diff --git a/chalk-engine/src/table.rs b/chalk-engine/src/table.rs
index ca83bc9dfef..209864ec8f6 100644
--- a/chalk-engine/src/table.rs
+++ b/chalk-engine/src/table.rs
@@ -42,9 +42,9 @@ index_struct! {
 /// goal for a particular table (modulo delayed literals). It contains
 /// a substitution
 #[derive(Clone, Debug)]
-pub struct Answer<C: Context> {
-    crate subst: C::CanonicalConstrainedSubst,
-    crate delayed_literals: DelayedLiteralSet<C>,
+pub struct Answer<E: ExClauseContext> {
+    crate subst: E::CanonicalConstrainedSubst,
+    crate delayed_literals: DelayedLiteralSet<E>,
 }
 
 impl<C: Context> Table<C> {
diff --git a/src/solve/slg/implementation.rs b/src/solve/slg/implementation.rs
index 3d81a24169c..1ec625b757b 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -49,12 +49,18 @@ impl SlgContext {
     }
 }
 
+impl context::ExClauseContext for SlgContext {
+    type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
+    type GoalInEnvironment = InEnvironment<Goal>;
+    type Substitution = Substitution;
+    type RegionConstraint = InEnvironment<Constraint>;
+}
+
 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;
 }
@@ -78,7 +84,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 +94,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
     }
@@ -163,12 +169,6 @@ 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;
@@ -205,7 +205,7 @@ impl context::InferenceContext<SlgContext> for SlgContext {
 
     fn into_ex_clause(
         result: Self::UnificationResult,
-        ex_clause: &mut ExClause<SlgContext, SlgContext>,
+        ex_clause: &mut ExClause<SlgContext>,
     ) {
         ex_clause
             .subgoals
@@ -253,7 +253,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 +264,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 +305,18 @@ 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
+    }
 }
 
 impl Substitution {
@@ -453,7 +465,7 @@ impl MayInvalidate {
     }
 }
 
-type ExClauseSlgContext = ExClause<SlgContext, SlgContext>;
+type ExClauseSlgContext = ExClause<SlgContext>;
 struct_fold!(ExClauseSlgContext {
     subst,
     delayed_literals,
@@ -461,7 +473,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..2191af9ce18 100644
--- a/src/solve/slg/implementation/resolvent.rs
+++ b/src/solve/slg/implementation/resolvent.rs
@@ -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.
@@ -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,

From ab299640501144a7043789049bd0bf84b58f01a0 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 21 May 2018 04:46:28 -0400
Subject: [PATCH 2/6] pull all the types into `Context`

---
 chalk-engine/src/context.rs         | 50 ++++++++++++++---------------
 chalk-engine/src/context/prelude.rs |  1 -
 chalk-engine/src/derived.rs         | 18 +++++------
 chalk-engine/src/hh.rs              | 18 +++++------
 chalk-engine/src/lib.rs             | 30 ++++++++---------
 chalk-engine/src/simplify.rs        |  2 +-
 chalk-engine/src/table.rs           |  6 ++--
 src/solve/slg/implementation.rs     | 28 +++++++---------
 8 files changed, 73 insertions(+), 80 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index fdabe8fb65b..460b3b19aaf 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -6,29 +6,10 @@ use std::hash::Hash;
 
 crate mod prelude;
 
-pub trait ExClauseContext: 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;
-
-    /// Represents a region constraint that will be propagated back
-    /// (but not verified).
-    type RegionConstraint: Debug;
-
-    /// Represents a goal along with an environment.
-    type GoalInEnvironment: Debug + Clone + Eq + Hash;
-}
-
 /// The "context" in which the SLG solver operates.
 // FIXME(leodasvacas): Clone and Debug bounds are just for easy derive,
 //                     they are not actually necessary.
-pub trait Context: Clone + Debug + ExClauseContext {
+pub trait Context: Clone + Debug {
     type CanonicalExClause: Debug;
 
     /// A map between universes. These are produced when
@@ -56,12 +37,24 @@ pub trait Context: Clone + Debug + ExClauseContext {
     /// completely opaque to the SLG solver; it is produced by
     /// `make_solution`.
     type Solution;
-}
 
-/// 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 {
+    /// 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;
+
+    /// Represents a region constraint that will be propagated back
+    /// (but not verified).
+    type RegionConstraint: Debug;
+
+    /// Represents a goal along with an environment.
+    type GoalInEnvironment: Debug + Clone + Eq + Hash;
+
     /// Represents a set of hypotheses that are assumed to be true.
     type Environment: Debug + Clone;
 
@@ -94,7 +87,12 @@ pub trait InferenceContext<C: Context>: ExClauseContext {
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
     type UnificationResult;
+}
 
+/// 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>: Context {
     fn goal_in_environment(
         environment: &Self::Environment,
         goal: Self::Goal,
@@ -114,7 +112,7 @@ pub trait InferenceContext<C: Context>: ExClauseContext {
     /// 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>;
+    fn into_hh_goal(goal: Self::Goal) -> HhGoal<Self>;
 
     /// Add the residual subgoals as new subgoals of the ex-clause.
     /// Also add region constraints.
diff --git a/chalk-engine/src/context/prelude.rs b/chalk-engine/src/context/prelude.rs
index a084b09424e..39cf99b0904 100644
--- a/chalk-engine/src/context/prelude.rs
+++ b/chalk-engine/src/context/prelude.rs
@@ -1,6 +1,5 @@
 #![allow(unused_imports)] // rustc bug
 
-crate use super::ExClauseContext;
 crate use super::Context;
 crate use super::ContextOps;
 crate use super::AggregateOps;
diff --git a/chalk-engine/src/derived.rs b/chalk-engine/src/derived.rs
index 42e3f72cb00..37b95ad1909 100644
--- a/chalk-engine/src/derived.rs
+++ b/chalk-engine/src/derived.rs
@@ -7,7 +7,7 @@ use std::hash::{Hash, Hasher};
 use std::mem;
 use super::*;
 
-impl<E: ExClauseContext> PartialEq for DelayedLiteralSet<E> {
+impl<C: Context> PartialEq for DelayedLiteralSet<C> {
     fn eq(&self, other: &Self) -> bool {
         let DelayedLiteralSet { delayed_literals: a1 } = self;
         let DelayedLiteralSet { delayed_literals: a2 } = other;
@@ -15,12 +15,12 @@ impl<E: ExClauseContext> PartialEq for DelayedLiteralSet<E> {
     }
 }
 
-impl<E: ExClauseContext> Eq for DelayedLiteralSet<E> {
+impl<C: Context> Eq for DelayedLiteralSet<C> {
 }
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<E: ExClauseContext> PartialEq for DelayedLiteral<E> {
+impl<C: Context> PartialEq for DelayedLiteral<C> {
     fn eq(&self, other: &Self) -> bool {
         if mem::discriminant(self) != mem::discriminant(other) {
             return false;
@@ -41,10 +41,10 @@ impl<E: ExClauseContext> PartialEq for DelayedLiteral<E> {
     }
 }
 
-impl<E: ExClauseContext> Eq for DelayedLiteral<E> {
+impl<C: Context> Eq for DelayedLiteral<C> {
 }
 
-impl<E: ExClauseContext> Hash for DelayedLiteral<E> {
+impl<C: Context> Hash for DelayedLiteral<C> {
     fn hash<H: Hasher>(&self, hasher: &mut H) {
         mem::discriminant(self).hash(hasher);
 
@@ -65,8 +65,8 @@ impl<E: ExClauseContext> Hash for DelayedLiteral<E> {
 
 ///////////////////////////////////////////////////////////////////////////
 
-impl<I: ExClauseContext> PartialEq for Literal<I> {
-    fn eq(&self, other: &Literal<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<I: ExClauseContext> PartialEq for Literal<I> {
     }
 }
 
-impl<I: ExClauseContext> Eq for Literal<I> {
+impl<C: Context> Eq for Literal<C> {
 }
 
-impl<I: ExClauseContext> Hash for Literal<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..fa4b0f7f2db 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(Vec<C::ProgramClause>, 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 bc88f4458ec..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<E: ExClauseContext> {
+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<E>>,
+    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<E>>,
+    pub subgoals: Vec<Literal<C>>,
 }
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
@@ -170,12 +170,12 @@ enum InnerDelayedLiteralSets<C: Context> {
 /// delayed literal, which in turn forces its subgoal to be delayed,
 /// and so forth. Therefore, we store canonicalized goals.)
 #[derive(Clone, Debug, Default)]
-struct DelayedLiteralSet<E: ExClauseContext> {
-    delayed_literals: FxHashSet<DelayedLiteral<E>>,
+struct DelayedLiteralSet<C: Context> {
+    delayed_literals: FxHashSet<DelayedLiteral<C>>,
 }
 
 #[derive(Clone, Debug)]
-pub enum DelayedLiteral<E: ExClauseContext> {
+pub enum DelayedLiteral<C: Context> {
     /// Something which can never be proven nor disproven. Inserted
     /// when truncation triggers; doesn't arise normally.
     CannotProve(()),
@@ -189,14 +189,14 @@ pub enum DelayedLiteral<E: ExClauseContext> {
     /// **conditional** answer (the `CanonicalConstrainedSubst`) within the
     /// given table, but we have to come back later and see whether
     /// that answer turns out to be true.
-    Positive(TableIndex, E::CanonicalConstrainedSubst),
+    Positive(TableIndex, C::CanonicalConstrainedSubst),
 }
 
 /// Either `A` or `~A`, where `A` is a `Env |- Goal`.
 #[derive(Clone, Debug)]
-pub enum Literal<E: ExClauseContext> { // 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
@@ -272,12 +272,12 @@ impl<C: Context> DelayedLiteralSets<C> {
     }
 }
 
-impl<E: ExClauseContext> DelayedLiteralSet<E> {
+impl<C: Context> DelayedLiteralSet<C> {
     fn is_empty(&self) -> bool {
         self.delayed_literals.is_empty()
     }
 
-    fn is_subset(&self, other: &DelayedLiteralSet<E>) -> bool {
+    fn is_subset(&self, other: &DelayedLiteralSet<C>) -> bool {
         self.delayed_literals
             .iter()
             .all(|elem| other.delayed_literals.contains(elem))
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
index 76d6c3f26ec..9120f4b574b 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -12,7 +12,7 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         infer: &mut dyn InferenceTable<C, I>,
         subst: I::Substitution,
         initial_environment: &I::Environment,
-        initial_hh_goal: HhGoal<C, I>,
+        initial_hh_goal: HhGoal<I>,
     ) -> Fallible<ExClause<I>> {
         let mut ex_clause = ExClause {
             subst,
diff --git a/chalk-engine/src/table.rs b/chalk-engine/src/table.rs
index 209864ec8f6..ca83bc9dfef 100644
--- a/chalk-engine/src/table.rs
+++ b/chalk-engine/src/table.rs
@@ -42,9 +42,9 @@ index_struct! {
 /// goal for a particular table (modulo delayed literals). It contains
 /// a substitution
 #[derive(Clone, Debug)]
-pub struct Answer<E: ExClauseContext> {
-    crate subst: E::CanonicalConstrainedSubst,
-    crate delayed_literals: DelayedLiteralSet<E>,
+pub struct Answer<C: Context> {
+    crate subst: C::CanonicalConstrainedSubst,
+    crate delayed_literals: DelayedLiteralSet<C>,
 }
 
 impl<C: Context> Table<C> {
diff --git a/src/solve/slg/implementation.rs b/src/solve/slg/implementation.rs
index 1ec625b757b..f72d39b052f 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -49,13 +49,6 @@ impl SlgContext {
     }
 }
 
-impl context::ExClauseContext for SlgContext {
-    type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
-    type GoalInEnvironment = InEnvironment<Goal>;
-    type Substitution = Substitution;
-    type RegionConstraint = InEnvironment<Constraint>;
-}
-
 impl context::Context for SlgContext {
     type CanonicalGoalInEnvironment = Canonical<InEnvironment<Goal>>;
     type CanonicalExClause = Canonical<ExClause<Self>>;
@@ -63,6 +56,17 @@ impl context::Context for SlgContext {
     type UniverseMap = UniverseMap;
     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 UnificationResult = UnificationResult;
+    type CanonicalConstrainedSubst = Canonical<ConstrainedSubst>;
+    type GoalInEnvironment = InEnvironment<Goal>;
+    type Substitution = Substitution;
+    type RegionConstraint = InEnvironment<Constraint>;
 }
 
 impl context::ContextOps<SlgContext> for SlgContext {
@@ -170,14 +174,6 @@ impl context::TruncateOps<SlgContext, SlgContext> for TruncatingInferenceTable {
 impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTable {}
 
 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)
     }
@@ -190,7 +186,7 @@ impl context::InferenceContext<SlgContext> for SlgContext {
         Goal::CannotProve(())
     }
 
-    fn into_hh_goal(goal: Self::Goal) -> HhGoal<SlgContext, Self> {
+    fn into_hh_goal(goal: Self::Goal) -> HhGoal<Self> {
         match goal {
             Goal::Quantified(QuantifierKind::ForAll, binders_goal) => HhGoal::ForAll(binders_goal),
             Goal::Quantified(QuantifierKind::Exists, binders_goal) => HhGoal::Exists(binders_goal),

From b402078310ee9db9b6011a6796ca50c115bb7b8f Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 21 May 2018 04:54:28 -0400
Subject: [PATCH 3/6] remove InferenceContext and merge into Context

---
 chalk-engine/src/context.rs               | 48 ++++++-----
 chalk-engine/src/context/prelude.rs       |  1 -
 chalk-engine/src/logic.rs                 | 38 ++++-----
 chalk-engine/src/simplify.rs              |  6 +-
 chalk-engine/src/strand.rs                |  6 +-
 src/lib.rs                                |  1 +
 src/solve/slg/implementation.rs           | 97 ++++++++++++-----------
 src/solve/slg/implementation/resolvent.rs |  8 +-
 8 files changed, 112 insertions(+), 93 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index 460b3b19aaf..7e5a31243ae 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -6,9 +6,25 @@ 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 strange, 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;
 
@@ -87,12 +103,8 @@ pub trait Context: Clone + Debug {
     /// The successful result from unification: contains new subgoals
     /// and things that can be attached to an ex-clause.
     type UnificationResult;
-}
 
-/// 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>: Context {
+    /// Given an environment and a goal, glue them together to create a `GoalInEnvironment`.
     fn goal_in_environment(
         environment: &Self::Environment,
         goal: Self::Goal,
@@ -114,10 +126,6 @@ pub trait InferenceContext<C: Context>: Context {
     /// goals.
     fn into_hh_goal(goal: Self::Goal) -> HhGoal<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<Self>);
-
     // Used by: simplify
     fn add_clauses(
         env: &Self::Environment,
@@ -199,7 +207,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,
@@ -217,7 +225,7 @@ 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<I>,
@@ -235,13 +243,13 @@ 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>
 {
 }
 
 /// 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(
@@ -298,6 +306,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)
@@ -312,7 +324,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>;
@@ -322,7 +334,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).
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/logic.rs b/chalk-engine/src/logic.rs
index 5842e2f2b87..93548ced28d 100644
--- a/chalk-engine/src/logic.rs
+++ b/chalk-engine/src/logic.rs
@@ -293,7 +293,7 @@ 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<I>,
@@ -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,7 +316,7 @@ 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<I>,
         selected_subgoal: Option<SelectedSubgoal<C>>,
@@ -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 {
@@ -662,7 +662,7 @@ 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<I>,
@@ -741,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,
@@ -754,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>,
@@ -814,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,
@@ -858,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,
@@ -973,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;
@@ -1097,7 +1097,7 @@ 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<I>,
         infer: &mut dyn InferenceTable<C, I>,
@@ -1164,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))
     }
@@ -1175,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;
@@ -1191,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;
@@ -1311,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> {
@@ -1322,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)
     }
 }
@@ -1334,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 9120f4b574b..9c038e16f5a 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -8,7 +8,7 @@ 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,
@@ -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 2353908c63f..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,7 +11,7 @@ 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<I>,
@@ -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 f72d39b052f..9fe7d1991b2 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -67,6 +67,39 @@ impl context::Context for SlgContext {
     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(())
+    }
+
+    fn into_hh_goal(goal: Self::Goal) -> HhGoal<Self> {
+        match goal {
+            Goal::Quantified(QuantifierKind::ForAll, binders_goal) => HhGoal::ForAll(binders_goal),
+            Goal::Quantified(QuantifierKind::Exists, binders_goal) => HhGoal::Exists(binders_goal),
+            Goal::Implies(dg, subgoal) => HhGoal::Implies(dg, *subgoal),
+            Goal::And(g1, g2) => HhGoal::And(*g1, *g2),
+            Goal::Not(g1) => HhGoal::Not(*g1),
+            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify(a, b),
+            Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => HhGoal::DomainGoal(domain_goal),
+            Goal::CannotProve(()) => HhGoal::CannotProve,
+        }
+    }
+
+    // Used by: simplify
+    fn add_clauses(
+        env: &Self::Environment,
+        clauses: impl IntoIterator<Item = Self::ProgramClause>,
+    ) -> Self::Environment {
+        Environment::add_clauses(env, clauses)
+    }
 }
 
 impl context::ContextOps<SlgContext> for SlgContext {
@@ -173,51 +206,6 @@ impl context::TruncateOps<SlgContext, SlgContext> for TruncatingInferenceTable {
 
 impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTable {}
 
-impl context::InferenceContext<SlgContext> for SlgContext {
-    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<Self> {
-        match goal {
-            Goal::Quantified(QuantifierKind::ForAll, binders_goal) => HhGoal::ForAll(binders_goal),
-            Goal::Quantified(QuantifierKind::Exists, binders_goal) => HhGoal::Exists(binders_goal),
-            Goal::Implies(dg, subgoal) => HhGoal::Implies(dg, *subgoal),
-            Goal::And(g1, g2) => HhGoal::And(*g1, *g2),
-            Goal::Not(g1) => HhGoal::Not(*g1),
-            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify(a, b),
-            Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => HhGoal::DomainGoal(domain_goal),
-            Goal::CannotProve(()) => HhGoal::CannotProve,
-        }
-    }
-
-    fn into_ex_clause(
-        result: Self::UnificationResult,
-        ex_clause: &mut ExClause<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 {
-        Environment::add_clauses(env, clauses)
-    }
-}
-
 impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTable {
     fn program_clauses(
         &self,
@@ -313,6 +301,25 @@ impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTabl
     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 {
diff --git a/src/solve/slg/implementation/resolvent.rs b/src/solve/slg/implementation/resolvent.rs
index 2191af9ce18..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;
 
@@ -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
@@ -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,

From 125e0a8b3744c0521eba98a0acb5d8b7051066a8 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 21 May 2018 05:51:30 -0400
Subject: [PATCH 4/6] move some more methods to InferenceTable

I predict that these may need access to the interners etc in rustc
---
 chalk-engine/src/context.rs     | 35 ++++++++++++-------------
 chalk-engine/src/logic.rs       |  2 +-
 chalk-engine/src/simplify.rs    | 12 ++++-----
 src/solve/slg/implementation.rs | 45 +++++++++++++++++----------------
 4 files changed, 48 insertions(+), 46 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index 7e5a31243ae..41ad5c36c94 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -104,7 +104,8 @@ pub trait Context: Clone + Debug {
     /// 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`.
+    /// Given an environment and a goal, glue them together to create
+    /// a `GoalInEnvironment`.
     fn goal_in_environment(
         environment: &Self::Environment,
         goal: Self::Goal,
@@ -115,22 +116,6 @@ pub trait Context: Clone + Debug {
 
     /// 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<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> {
@@ -246,6 +231,22 @@ pub trait AggregateOps<C: Context> {
 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: Vec<I::ProgramClause>,
+    ) -> I::Environment;
 }
 
 /// Methods for unifying and manipulating terms and binders.
diff --git a/chalk-engine/src/logic.rs b/chalk-engine/src/logic.rs
index 93548ced28d..ee2d27b6999 100644
--- a/chalk-engine/src/logic.rs
+++ b/chalk-engine/src/logic.rs
@@ -763,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 {
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
index 9c038e16f5a..b98efa7569e 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -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
diff --git a/src/solve/slg/implementation.rs b/src/solve/slg/implementation.rs
index 9fe7d1991b2..edbd3b3f692 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -79,27 +79,6 @@ impl context::Context for SlgContext {
     fn cannot_prove() -> Self::Goal {
         Goal::CannotProve(())
     }
-
-    fn into_hh_goal(goal: Self::Goal) -> HhGoal<Self> {
-        match goal {
-            Goal::Quantified(QuantifierKind::ForAll, binders_goal) => HhGoal::ForAll(binders_goal),
-            Goal::Quantified(QuantifierKind::Exists, binders_goal) => HhGoal::Exists(binders_goal),
-            Goal::Implies(dg, subgoal) => HhGoal::Implies(dg, *subgoal),
-            Goal::And(g1, g2) => HhGoal::And(*g1, *g2),
-            Goal::Not(g1) => HhGoal::Not(*g1),
-            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify(a, b),
-            Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => HhGoal::DomainGoal(domain_goal),
-            Goal::CannotProve(()) => HhGoal::CannotProve,
-        }
-    }
-
-    // Used by: simplify
-    fn add_clauses(
-        env: &Self::Environment,
-        clauses: impl IntoIterator<Item = Self::ProgramClause>,
-    ) -> Self::Environment {
-        Environment::add_clauses(env, clauses)
-    }
 }
 
 impl context::ContextOps<SlgContext> for SlgContext {
@@ -204,7 +183,29 @@ impl context::TruncateOps<SlgContext, SlgContext> for TruncatingInferenceTable {
     }
 }
 
-impl context::InferenceTable<SlgContext, SlgContext> for TruncatingInferenceTable {}
+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),
+            Goal::Implies(dg, subgoal) => HhGoal::Implies(dg, *subgoal),
+            Goal::And(g1, g2) => HhGoal::And(*g1, *g2),
+            Goal::Not(g1) => HhGoal::Not(*g1),
+            Goal::Leaf(LeafGoal::EqGoal(EqGoal { a, b })) => HhGoal::Unify(a, b),
+            Goal::Leaf(LeafGoal::DomainGoal(domain_goal)) => HhGoal::DomainGoal(domain_goal),
+            Goal::CannotProve(()) => HhGoal::CannotProve,
+        }
+    }
+
+    // Used by: simplify
+    fn add_clauses(
+        &mut self,
+        env: &Arc<Environment>,
+        clauses: Vec<ProgramClause>,
+    ) -> Arc<Environment> {
+        Environment::add_clauses(env, clauses)
+    }
+}
 
 impl context::UnificationOps<SlgContext, SlgContext> for TruncatingInferenceTable {
     fn program_clauses(

From 1f179eb4490bd6a5e347922074b300438741955e Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 21 May 2018 05:53:49 -0400
Subject: [PATCH 5/6] don't hard-code the use of `Vec`

---
 chalk-engine/src/context.rs     | 5 ++++-
 chalk-engine/src/hh.rs          | 2 +-
 src/solve/slg/implementation.rs | 1 +
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index 41ad5c36c94..0b5cf70bfc7 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -100,6 +100,9 @@ pub trait Context: Clone + Debug {
     /// 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;
@@ -245,7 +248,7 @@ pub trait InferenceTable<C: Context, I: Context>:
     fn add_clauses(
         &mut self,
         env: &I::Environment,
-        clauses: Vec<I::ProgramClause>,
+        clauses: I::ProgramClauses,
     ) -> I::Environment;
 }
 
diff --git a/chalk-engine/src/hh.rs b/chalk-engine/src/hh.rs
index fa4b0f7f2db..39af0ec6caf 100644
--- a/chalk-engine/src/hh.rs
+++ b/chalk-engine/src/hh.rs
@@ -7,7 +7,7 @@ pub enum HhGoal<C: Context> {
     /// (deBruijn index).
     ForAll(C::BindersGoal),
     Exists(C::BindersGoal),
-    Implies(Vec<C::ProgramClause>, C::Goal),
+    Implies(C::ProgramClauses, C::Goal),
     And(C::Goal, C::Goal),
     Not(C::Goal),
     Unify(C::Parameter, C::Parameter),
diff --git a/src/solve/slg/implementation.rs b/src/solve/slg/implementation.rs
index edbd3b3f692..9bedec2f9b8 100644
--- a/src/solve/slg/implementation.rs
+++ b/src/solve/slg/implementation.rs
@@ -62,6 +62,7 @@ impl context::Context for SlgContext {
     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>;

From b657ec1c4cfb1517a7f204b521b16c3e227956cc Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Mon, 21 May 2018 10:48:36 -0400
Subject: [PATCH 6/6] fix typo

---
 chalk-engine/src/context.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index 0b5cf70bfc7..19cb0d0a00b 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -12,7 +12,7 @@ crate mod prelude;
 ///
 /// 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 strange, we will
+/// 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.
 ///