From b828b093b6312f91b9a7e758f879033c203e28f6 Mon Sep 17 00:00:00 2001
From: Wonwoo Choi <chwo9843@gmail.com>
Date: Thu, 2 Apr 2020 16:36:07 +0900
Subject: [PATCH 1/5] Intern ProgramClause<I>

---
 chalk-integration/src/lowering.rs         |  2 +-
 chalk-integration/src/program.rs          |  9 ++++
 chalk-ir/src/cast.rs                      | 14 +++---
 chalk-ir/src/could_match.rs               | 12 +++--
 chalk-ir/src/debug.rs                     | 13 +++--
 chalk-ir/src/fold/boring_impls.rs         | 25 ++++++++--
 chalk-ir/src/interner.rs                  | 59 +++++++++++++++++++++++
 chalk-ir/src/lib.rs                       | 41 +++++++++++++---
 chalk-ir/src/tls.rs                       |  8 ++-
 chalk-ir/src/zip.rs                       | 12 ++++-
 chalk-solve/src/clauses/builder.rs        | 11 +++--
 chalk-solve/src/clauses/env_elaborator.rs |  8 +--
 chalk-solve/src/solve/slg/resolvent.rs    |  6 +--
 13 files changed, 181 insertions(+), 39 deletions(-)

diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
index f7ff420971c..ae823685817 100644
--- a/chalk-integration/src/lowering.rs
+++ b/chalk-integration/src/lowering.rs
@@ -1198,7 +1198,7 @@ impl LowerClause for Clause {
             .into_iter()
             .map(
                 |implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
-                    chalk_ir::ProgramClause::ForAll(implication)
+                    chalk_ir::ProgramClauseData::ForAll(implication).intern(interner)
                 },
             )
             .collect();
diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs
index 77791ef4427..4cec4bbf5ee 100644
--- a/chalk-integration/src/program.rs
+++ b/chalk-integration/src/program.rs
@@ -173,6 +173,15 @@ impl tls::DebugContext for Program {
         write!(fmt, "{:?}", pci.debug(interner))
     }
 
+    fn debug_program_clause(
+        &self,
+        clause: &ProgramClause<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", clause.data(interner))
+    }
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,
diff --git a/chalk-ir/src/cast.rs b/chalk-ir/src/cast.rs
index d066b1bce6e..f9ca2f1e9fc 100644
--- a/chalk-ir/src/cast.rs
+++ b/chalk-ir/src/cast.rs
@@ -183,10 +183,11 @@ where
     I: Interner,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClause::Implies(ProgramClauseImplication {
+        ProgramClauseData::Implies(ProgramClauseImplication {
             consequence: self.cast(interner),
             conditions: Goals::new(interner),
         })
+        .intern(interner)
     }
 }
 
@@ -196,22 +197,23 @@ where
     I: Interner,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
-        ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
+        ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
             consequence: bound.cast(interner),
             conditions: Goals::new(interner),
         }))
+        .intern(interner)
     }
 }
 
 impl<I: Interner> CastTo<ProgramClause<I>> for ProgramClauseImplication<I> {
-    fn cast_to(self, _interner: &I) -> ProgramClause<I> {
-        ProgramClause::Implies(self)
+    fn cast_to(self, interner: &I) -> ProgramClause<I> {
+        ProgramClauseData::Implies(self).intern(interner)
     }
 }
 
 impl<I: Interner> CastTo<ProgramClause<I>> for Binders<ProgramClauseImplication<I>> {
-    fn cast_to(self, _interner: &I) -> ProgramClause<I> {
-        ProgramClause::ForAll(self)
+    fn cast_to(self, interner: &I) -> ProgramClause<I> {
+        ProgramClauseData::ForAll(self).intern(interner)
     }
 }
 
diff --git a/chalk-ir/src/could_match.rs b/chalk-ir/src/could_match.rs
index 6e830a083ec..a4bb37bc133 100644
--- a/chalk-ir/src/could_match.rs
+++ b/chalk-ir/src/could_match.rs
@@ -62,14 +62,20 @@ where
     }
 }
 
-impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
+impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClauseData<I> {
     fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
         match self {
-            ProgramClause::Implies(implication) => {
+            ProgramClauseData::Implies(implication) => {
                 implication.consequence.could_match(interner, other)
             }
 
-            ProgramClause::ForAll(clause) => clause.value.consequence.could_match(interner, other),
+            ProgramClauseData::ForAll(clause) => clause.value.consequence.could_match(interner, other),
         }
     }
 }
+
+impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
+    fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
+        self.data(interner).could_match(interner, other)
+    }
+}
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 6f0d82d65be..5208428569f 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -58,6 +58,13 @@ impl<I: Interner> Debug for ProgramClauseImplication<I> {
     }
 }
 
+impl<I: Interner> Debug for ProgramClause<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_program_clause(self, fmt)
+            .unwrap_or_else(|| write!(fmt, "{:?}", self.clause))
+    }
+}
+
 impl<I: Interner> Debug for ApplicationTy<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))
@@ -520,11 +527,11 @@ impl<T: Debug> Debug for Binders<T> {
     }
 }
 
-impl<I: Interner> Debug for ProgramClause<I> {
+impl<I: Interner> Debug for ProgramClauseData<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
-            ProgramClause::Implies(pc) => write!(fmt, "{:?}", pc),
-            ProgramClause::ForAll(pc) => write!(fmt, "{:?}", pc),
+            ProgramClauseData::Implies(pc) => write!(fmt, "{:?}", pc),
+            ProgramClauseData::ForAll(pc) => write!(fmt, "{:?}", pc),
         }
     }
 }
diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs
index 88a27d13219..ad16cd2a45d 100644
--- a/chalk-ir/src/fold/boring_impls.rs
+++ b/chalk-ir/src/fold/boring_impls.rs
@@ -228,7 +228,7 @@ id_fold!(StructId);
 id_fold!(TraitId);
 id_fold!(AssocTypeId);
 
-impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
+impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<I> {
     fn super_fold_with<'i>(
         &self,
         folder: &mut dyn Folder<'i, I, TI>,
@@ -239,16 +239,31 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
         TI: 'i,
     {
         match self {
-            ProgramClause::Implies(pci) => {
-                Ok(ProgramClause::Implies(pci.fold_with(folder, outer_binder)?))
+            ProgramClauseData::Implies(pci) => {
+                Ok(ProgramClauseData::Implies(pci.fold_with(folder, outer_binder)?))
             }
-            ProgramClause::ForAll(pci) => {
-                Ok(ProgramClause::ForAll(pci.fold_with(folder, outer_binder)?))
+            ProgramClauseData::ForAll(pci) => {
+                Ok(ProgramClauseData::ForAll(pci.fold_with(folder, outer_binder)?))
             }
         }
     }
 }
 
+impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
+    fn super_fold_with<'i>(
+        &self,
+        folder: &mut dyn Folder<'i, I, TI>,
+        outer_binder: DebruijnIndex,
+    ) -> ::chalk_engine::fallible::Fallible<Self::Result>
+    where
+        I: 'i,
+        TI: 'i,
+    {
+        let clause = self.data(folder.interner());
+        Ok(clause.super_fold_with(folder, outer_binder)?.intern(folder.target_interner()))
+    }
+}
+
 impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
     type Result = PhantomData<TI>;
 
diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs
index 7e74c337944..5655b1f6105 100644
--- a/chalk-ir/src/interner.rs
+++ b/chalk-ir/src/interner.rs
@@ -8,6 +8,8 @@ use crate::Lifetime;
 use crate::LifetimeData;
 use crate::Parameter;
 use crate::ParameterData;
+use crate::ProgramClause;
+use crate::ProgramClauseData;
 use crate::ProgramClauseImplication;
 use crate::SeparatorTraitRef;
 use crate::StructId;
@@ -94,6 +96,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// converted back to its underlying data via `substitution_data`.
     type InternedSubstitution: Debug + Clone + Eq + Hash;
 
+    /// "Interned" representation of a "program clause".  In normal user code,
+    /// `Self::InternedProgramClause` is not referenced. Instead, we refer to
+    /// `ProgramClause<Self>`, which wraps this type.
+    ///
+    /// An `InternedProgramClause` is created by `intern_program_clause` and can be
+    /// converted back to its underlying data via `program_clause_data`.
+    type InternedProgramClause: Debug + Clone + Eq + Hash;
+
     /// The core "id" type used for struct-ids and the like.
     type DefId: Debug + Copy + Eq + Ord + Hash;
 
@@ -234,6 +244,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of a ProgramClause. To get good
+    /// results, this requires inspecting TLS, and is difficult to
+    /// code without reference to a specific interner (and hence
+    /// fully known types).
+    ///
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    #[allow(unused_variables)]
+    fn debug_program_clause(
+        clause: &ProgramClause<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an ApplicationTy. To get good
     /// results, this requires inspecting TLS, and is difficult to
     /// code without reference to a specific interner (and hence
@@ -337,6 +362,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         &self,
         substitution: &'a Self::InternedSubstitution,
     ) -> &'a [Parameter<Self>];
+
+    /// Create an "interned" program clause from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `ProgramClauseData::intern` (which will ultimately call this
+    /// method).
+    fn intern_program_clause(&self, data: ProgramClauseData<Self>) -> Self::InternedProgramClause;
+
+    /// Lookup the `ProgramClauseData` that was interned to create a `ProgramClause`.
+    fn program_clause_data<'a>(
+        &self,
+        clause: &'a Self::InternedProgramClause,
+    ) -> &'a ProgramClauseData<Self>;
 }
 
 pub trait TargetInterner<I: Interner>: Interner {
@@ -391,6 +428,7 @@ mod default {
         type InternedGoal = Arc<GoalData<ChalkIr>>;
         type InternedGoals = Vec<Goal<ChalkIr>>;
         type InternedSubstitution = Vec<Parameter<ChalkIr>>;
+        type InternedProgramClause = ProgramClauseData<ChalkIr>;
         type DefId = RawId;
         type Identifier = Identifier;
 
@@ -459,6 +497,13 @@ mod default {
             tls::with_current_program(|prog| Some(prog?.debug_program_clause_implication(pci, fmt)))
         }
 
+        fn debug_program_clause(
+            clause: &ProgramClause<ChalkIr>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| Some(prog?.debug_program_clause(clause, fmt)))
+        }
+
         fn debug_application_ty(
             application_ty: &ApplicationTy<ChalkIr>,
             fmt: &mut fmt::Formatter<'_>,
@@ -544,6 +589,20 @@ mod default {
         ) -> &'a [Parameter<ChalkIr>] {
             substitution
         }
+
+        fn intern_program_clause(
+            &self,
+            data: ProgramClauseData<Self>,
+        ) -> ProgramClauseData<Self> {
+            data
+        }
+
+        fn program_clause_data<'a>(
+            &self,
+            clause: &'a ProgramClauseData<Self>,
+        ) -> &'a ProgramClauseData<Self> {
+            clause
+        }
     }
 
     impl HasInterner for ChalkIr {
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index ad4c9058114..fa75cea0d5c 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -1208,8 +1208,8 @@ pub struct ProgramClauseImplication<I: Interner> {
     pub conditions: Goals<I>,
 }
 
-#[derive(Clone, PartialEq, Eq, Hash, HasInterner)]
-pub enum ProgramClause<I: Interner> {
+#[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)]
+pub enum ProgramClauseData<I: Interner> {
     Implies(ProgramClauseImplication<I>),
     ForAll(Binders<ProgramClauseImplication<I>>),
 }
@@ -1227,17 +1227,42 @@ impl<I: Interner> ProgramClauseImplication<I> {
     }
 }
 
-impl<I: Interner> ProgramClause<I> {
-    pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
+impl<I: Interner> ProgramClauseData<I> {
+    pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseData<I> {
         match self {
-            ProgramClause::Implies(implication) => {
-                ProgramClause::Implies(implication.into_from_env_clause(interner))
+            ProgramClauseData::Implies(implication) => {
+                ProgramClauseData::Implies(implication.into_from_env_clause(interner))
             }
-            ProgramClause::ForAll(binders_implication) => {
-                ProgramClause::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
+            ProgramClauseData::ForAll(binders_implication) => {
+                ProgramClauseData::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
             }
         }
     }
+
+    pub fn intern(self, interner: &I) -> ProgramClause<I> {
+        ProgramClause {
+            clause: interner.intern_program_clause(self),
+        }
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
+pub struct ProgramClause<I: Interner> {
+    clause: I::InternedProgramClause,
+}
+
+impl<I: Interner> ProgramClause<I> {
+    pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
+        let program_clause_data = self.data(interner);
+        let new_clause = program_clause_data.clone().into_from_env_clause(interner);
+        ProgramClause {
+            clause: interner.intern_program_clause(new_clause),
+        }
+    }
+
+    pub fn data(&self, interner: &I) -> &ProgramClauseData<I> {
+        interner.program_clause_data(&self.clause)
+    }
 }
 
 /// Wraps a "canonicalized item". Items are canonicalized as follows:
diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs
index fe929b763e0..4f8bb048176 100644
--- a/chalk-ir/src/tls.rs
+++ b/chalk-ir/src/tls.rs
@@ -1,7 +1,7 @@
 use crate::interner::ChalkIr;
 use crate::{
     debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
-    Parameter, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
+    Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
 };
 use std::cell::RefCell;
 use std::fmt;
@@ -68,6 +68,12 @@ pub trait DebugContext {
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
 
+    fn debug_program_clause(
+        &self,
+        clause: &ProgramClause<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,
diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs
index d0dfc3f52c3..63ba17e89b7 100644
--- a/chalk-ir/src/zip.rs
+++ b/chalk-ir/src/zip.rs
@@ -309,7 +309,7 @@ enum_zip!(impl<I> for DomainGoal<I> {
     Compatible,
     DownstreamType
 });
-enum_zip!(impl<I> for ProgramClause<I> { Implies, ForAll });
+enum_zip!(impl<I> for ProgramClauseData<I> { Implies, ForAll });
 
 impl<I: Interner> Zip<I> for Substitution<I> {
     fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
@@ -396,3 +396,13 @@ impl<I: Interner> Zip<I> for Parameter<I> {
         Zip::zip_with(zipper, a.data(interner), b.data(interner))
     }
 }
+
+impl<I: Interner> Zip<I> for ProgramClause<I> {
+    fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
+    where
+        I: 'i,
+    {
+        let interner = zipper.interner();
+        Zip::zip_with(zipper, a.data(interner), b.data(interner))
+    }
+}
diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs
index 871f8d45bc5..767abda8ed1 100644
--- a/chalk-solve/src/clauses/builder.rs
+++ b/chalk-solve/src/clauses/builder.rs
@@ -44,18 +44,19 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
         consequence: impl CastTo<DomainGoal<I>>,
         conditions: impl IntoIterator<Item = impl CastTo<Goal<I>>>,
     ) {
+        let interner = self.db.interner();
         let clause = ProgramClauseImplication {
-            consequence: consequence.cast(self.db.interner()),
-            conditions: Goals::from(self.db.interner(), conditions),
+            consequence: consequence.cast(interner),
+            conditions: Goals::from(interner, conditions),
         };
 
         if self.binders.len() == 0 {
-            self.clauses.push(ProgramClause::Implies(clause));
+            self.clauses.push(ProgramClauseData::Implies(clause).intern(interner));
         } else {
-            self.clauses.push(ProgramClause::ForAll(Binders {
+            self.clauses.push(ProgramClauseData::ForAll(Binders {
                 binders: self.binders.clone(),
                 value: clause,
-            }));
+            }).intern(interner));
         }
 
         debug!("pushed clause {:?}", self.clauses.last());
diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs
index b99658e7133..cab626f9de9 100644
--- a/chalk-solve/src/clauses/env_elaborator.rs
+++ b/chalk-solve/src/clauses/env_elaborator.rs
@@ -4,6 +4,7 @@ use crate::clauses::match_type_name;
 use crate::DomainGoal;
 use crate::FromEnv;
 use crate::ProgramClause;
+use crate::ProgramClauseData;
 use crate::RustIrDatabase;
 use crate::Ty;
 use crate::TyData;
@@ -105,9 +106,10 @@ impl<'me, I: Interner> EnvElaborator<'me, I> {
 
     fn visit_program_clause(&mut self, clause: &ProgramClause<I>) {
         debug!("visit_program_clause(clause={:?})", clause);
-        match clause {
-            ProgramClause::Implies(clause) => self.visit_domain_goal(&clause.consequence),
-            ProgramClause::ForAll(clause) => self.visit_domain_goal(&clause.value.consequence),
+        let interner = self.db.interner();
+        match clause.data(interner) {
+            ProgramClauseData::Implies(clause) => self.visit_domain_goal(&clause.consequence),
+            ProgramClauseData::ForAll(clause) => self.visit_domain_goal(&clause.value.consequence),
         }
     }
 }
diff --git a/chalk-solve/src/solve/slg/resolvent.rs b/chalk-solve/src/solve/slg/resolvent.rs
index b4967ba762a..48ec269b7c7 100644
--- a/chalk-solve/src/solve/slg/resolvent.rs
+++ b/chalk-solve/src/solve/slg/resolvent.rs
@@ -83,9 +83,9 @@ impl<I: Interner> context::ResolventOps<SlgContext<I>> for TruncatingInferenceTa
         let ProgramClauseImplication {
             consequence,
             conditions,
-        } = match clause {
-            ProgramClause::Implies(implication) => implication.clone(),
-            ProgramClause::ForAll(implication) => self
+        } = match clause.data(interner) {
+            ProgramClauseData::Implies(implication) => implication.clone(),
+            ProgramClauseData::ForAll(implication) => self
                 .infer
                 .instantiate_binders_existentially(interner, implication),
         };

From 0dc925efa00882297bfcf7ca21f2700a5bcfbc59 Mon Sep 17 00:00:00 2001
From: Wonwoo Choi <chwo9843@gmail.com>
Date: Sat, 4 Apr 2020 04:01:07 +0900
Subject: [PATCH 2/5] Intern Vec<ProgramClause<I>>

---
 chalk-engine/src/context.rs               | 10 ++-
 chalk-engine/src/simplify.rs              |  2 +-
 chalk-integration/src/lowering.rs         |  6 +-
 chalk-integration/src/program.rs          | 13 +++-
 chalk-ir/src/debug.rs                     |  6 ++
 chalk-ir/src/fold/boring_impls.rs         | 20 ++++++
 chalk-ir/src/interner.rs                  | 61 ++++++++++++++++++
 chalk-ir/src/lib.rs                       | 75 +++++++++++++++++++----
 chalk-ir/src/tls.rs                       |  9 ++-
 chalk-ir/src/zip.rs                       | 16 ++++-
 chalk-solve/src/clauses.rs                |  4 +-
 chalk-solve/src/clauses/env_elaborator.rs |  2 +-
 chalk-solve/src/ext.rs                    |  6 +-
 chalk-solve/src/goal_builder.rs           |  2 +-
 chalk-solve/src/solve/slg.rs              | 19 +++---
 15 files changed, 214 insertions(+), 37 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index b539ff648d7..ecf4b11c85e 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -154,9 +154,6 @@ pub trait Context: Clone + Debug {
 
     fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;
 
-    // Used by: simplify
-    fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;
-
     /// Selects the next appropriate subgoal index for evaluation.
     /// Used by: logic
     fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize;
@@ -180,6 +177,13 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
         infer: &mut C::InferenceTable,
     ) -> Result<Vec<C::ProgramClause>, Floundered>;
 
+    // Used by: simplify
+    fn add_clauses(
+        &self,
+        env: &C::Environment,
+        clauses: C::ProgramClauses,
+    ) -> C::Environment;
+
     /// Create an inference table for processing a new goal and instantiate that goal
     /// in that context, returning "all the pieces".
     ///
diff --git a/chalk-engine/src/simplify.rs b/chalk-engine/src/simplify.rs
index 9fcc0bdeb07..0f46b1705b4 100644
--- a/chalk-engine/src/simplify.rs
+++ b/chalk-engine/src/simplify.rs
@@ -41,7 +41,7 @@ impl<C: Context> Forest<C> {
                     pending_goals.push((environment, context.into_hh_goal(subgoal)))
                 }
                 HhGoal::Implies(wc, subgoal) => {
-                    let new_environment = C::add_clauses(&environment, wc);
+                    let new_environment = context.add_clauses(&environment, wc);
                     pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
                 }
                 HhGoal::All(subgoals) => {
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
index ae823685817..5063f094dde 100644
--- a/chalk-integration/src/lowering.rs
+++ b/chalk-integration/src/lowering.rs
@@ -1303,11 +1303,11 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 // `T: Trait<Assoc = U>` to `FromEnv(T: Trait)` and `FromEnv(T: Trait<Assoc = U>)`
                 // in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to
                 // `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`.
-                let where_clauses: LowerResult<Vec<_>> = hyp
+                let where_clauses = hyp
                     .into_iter()
                     .flat_map(|h| h.lower_clause(env).apply_result())
-                    .map(|result| result.map(|h| h.into_from_env_clause(interner)))
-                    .collect();
+                    .map(|result| result.map(|h| h.into_from_env_clause(interner)));
+                let where_clauses = chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
                 Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
             }
             Goal::And(g1, g2s) => {
diff --git a/chalk-integration/src/program.rs b/chalk-integration/src/program.rs
index 4cec4bbf5ee..e1ef452c637 100644
--- a/chalk-integration/src/program.rs
+++ b/chalk-integration/src/program.rs
@@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr;
 use chalk_ir::tls;
 use chalk_ir::{
     debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
-    Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
-    TyData, TypeName,
+    Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
+    TraitId, Ty, TyData, TypeName,
 };
 use chalk_rust_ir::{
     AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -182,6 +182,15 @@ impl tls::DebugContext for Program {
         write!(fmt, "{:?}", clause.data(interner))
     }
 
+    fn debug_program_clauses(
+        &self,
+        clauses: &ProgramClauses<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", clauses.as_slice(interner))
+    }
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 5208428569f..74a09c1d0b0 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -65,6 +65,12 @@ impl<I: Interner> Debug for ProgramClause<I> {
     }
 }
 
+impl<I: Interner> Debug for ProgramClauses<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.clauses))
+    }
+}
+
 impl<I: Interner> Debug for ApplicationTy<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))
diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs
index ad16cd2a45d..b027c30ec05 100644
--- a/chalk-ir/src/fold/boring_impls.rs
+++ b/chalk-ir/src/fold/boring_impls.rs
@@ -172,6 +172,26 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
     }
 }
 
+impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClauses<I> {
+    type Result = ProgramClauses<TI>;
+    fn fold_with<'i>(
+        &self,
+        folder: &mut dyn Folder<'i, I, TI>,
+        outer_binder: DebruijnIndex,
+    ) -> Fallible<Self::Result>
+    where
+        I: 'i,
+        TI: 'i,
+    {
+        let interner = folder.interner();
+        let target_interner = folder.target_interner();
+        let folded = self
+            .iter(interner)
+            .map(|p| p.fold_with(folder, outer_binder));
+        Ok(ProgramClauses::from_fallible(target_interner, folded)?)
+    }
+}
+
 #[macro_export]
 macro_rules! copy_fold {
     ($t:ty) => {
diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs
index 5655b1f6105..122205c788f 100644
--- a/chalk-ir/src/interner.rs
+++ b/chalk-ir/src/interner.rs
@@ -11,6 +11,7 @@ use crate::ParameterData;
 use crate::ProgramClause;
 use crate::ProgramClauseData;
 use crate::ProgramClauseImplication;
+use crate::ProgramClauses;
 use crate::SeparatorTraitRef;
 use crate::StructId;
 use crate::Substitution;
@@ -96,6 +97,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// converted back to its underlying data via `substitution_data`.
     type InternedSubstitution: Debug + Clone + Eq + Hash;
 
+    /// "Interned" representation of a list of program clauses.  In normal user code,
+    /// `Self::InternedProgramClauses` is not referenced. Instead, we refer to
+    /// `ProgramClauses<Self>`, which wraps this type.
+    ///
+    /// An `InternedProgramClauses` is created by `intern_program_clauses` and can be
+    /// converted back to its underlying data via `program_clauses_data`.
+    type InternedProgramClauses: Debug + Clone + Eq + Hash;
+
     /// "Interned" representation of a "program clause".  In normal user code,
     /// `Self::InternedProgramClause` is not referenced. Instead, we refer to
     /// `ProgramClause<Self>`, which wraps this type.
@@ -259,6 +268,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of a ProgramClauses. To get good
+    /// results, this requires inspecting TLS, and is difficult to
+    /// code without reference to a specific interner (and hence
+    /// fully known types).
+    ///
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    #[allow(unused_variables)]
+    fn debug_program_clauses(
+        clauses: &ProgramClauses<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an ApplicationTy. To get good
     /// results, this requires inspecting TLS, and is difficult to
     /// code without reference to a specific interner (and hence
@@ -374,6 +398,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         &self,
         clause: &'a Self::InternedProgramClause,
     ) -> &'a ProgramClauseData<Self>;
+
+    /// Create an "interned" program clauses from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `ProgramClauses::from` (which will ultimately call this
+    /// method).
+    fn intern_program_clauses(
+        &self,
+        data: impl IntoIterator<Item = ProgramClause<Self>>,
+    ) -> Self::InternedProgramClauses;
+
+    /// Lookup the `ProgramClauseData` that was interned to create a `ProgramClause`.
+    fn program_clauses_data<'a>(
+        &self,
+        clauses: &'a Self::InternedProgramClauses,
+    ) -> &'a [ProgramClause<Self>];
 }
 
 pub trait TargetInterner<I: Interner>: Interner {
@@ -429,6 +468,7 @@ mod default {
         type InternedGoals = Vec<Goal<ChalkIr>>;
         type InternedSubstitution = Vec<Parameter<ChalkIr>>;
         type InternedProgramClause = ProgramClauseData<ChalkIr>;
+        type InternedProgramClauses = Vec<ProgramClause<ChalkIr>>;
         type DefId = RawId;
         type Identifier = Identifier;
 
@@ -504,6 +544,13 @@ mod default {
             tls::with_current_program(|prog| Some(prog?.debug_program_clause(clause, fmt)))
         }
 
+        fn debug_program_clauses(
+            clause: &ProgramClauses<ChalkIr>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| Some(prog?.debug_program_clauses(clause, fmt)))
+        }
+
         fn debug_application_ty(
             application_ty: &ApplicationTy<ChalkIr>,
             fmt: &mut fmt::Formatter<'_>,
@@ -603,6 +650,20 @@ mod default {
         ) -> &'a ProgramClauseData<Self> {
             clause
         }
+
+        fn intern_program_clauses(
+            &self,
+            data: impl IntoIterator<Item = ProgramClause<Self>>,
+        ) -> Vec<ProgramClause<Self>> {
+            data.into_iter().collect()
+        }
+
+        fn program_clauses_data<'a>(
+            &self,
+            clauses: &'a Vec<ProgramClause<Self>>,
+        ) -> &'a [ProgramClause<Self>] {
+            clauses
+        }
     }
 
     impl HasInterner for ChalkIr {
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index fa75cea0d5c..88e593bf406 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -48,20 +48,20 @@ pub mod tls;
 /// The set of assumptions we've made so far, and the current number of
 /// universal (forall) quantifiers we're within.
 pub struct Environment<I: Interner> {
-    pub clauses: Vec<ProgramClause<I>>,
+    pub clauses: ProgramClauses<I>,
 }
 
 impl<I: Interner> Environment<I> {
-    pub fn new() -> Self {
-        Environment { clauses: vec![] }
+    pub fn new(interner: &I) -> Self {
+        Environment { clauses: ProgramClauses::new(interner) }
     }
 
-    pub fn add_clauses<II>(&self, clauses: II) -> Self
+    pub fn add_clauses<II>(&self, interner: &I, clauses: II) -> Self
     where
         II: IntoIterator<Item = ProgramClause<I>>,
     {
         let mut env = self.clone();
-        env.clauses = env.clauses.into_iter().chain(clauses).collect();
+        env.clauses = ProgramClauses::from(interner, env.clauses.iter(interner).cloned().chain(clauses));
         env
     }
 }
@@ -1265,6 +1265,56 @@ impl<I: Interner> ProgramClause<I> {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
+pub struct ProgramClauses<I: Interner> {
+    clauses: I::InternedProgramClauses,
+}
+
+impl<I: Interner> ProgramClauses<I> {
+    pub fn new(interner: &I) -> Self {
+        Self::from(interner, None::<ProgramClause<I>>)
+    }
+
+    pub fn interned(&self) -> &I::InternedProgramClauses {
+        &self.clauses
+    }
+
+    pub fn from(interner: &I, clauses: impl IntoIterator<Item = impl CastTo<ProgramClause<I>>>) -> Self {
+        use crate::cast::Caster;
+        ProgramClauses {
+            clauses: I::intern_program_clauses(interner, clauses.into_iter().casted(interner)),
+        }
+    }
+
+    pub fn from_fallible<E>(
+        interner: &I,
+        clauses: impl IntoIterator<Item = Result<impl CastTo<ProgramClause<I>>, E>>,
+    ) -> Result<Self, E> {
+        use crate::cast::Caster;
+        let clauses = clauses
+            .into_iter()
+            .casted(interner)
+            .collect::<Result<Vec<ProgramClause<I>>, _>>()?;
+        Ok(Self::from(interner, clauses))
+    }
+
+    pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, ProgramClause<I>> {
+        self.as_slice(interner).iter()
+    }
+
+    pub fn is_empty(&self, interner: &I) -> bool {
+        self.as_slice(interner).is_empty()
+    }
+
+    pub fn len(&self, interner: &I) -> usize {
+        self.as_slice(interner).len()
+    }
+
+    pub fn as_slice(&self, interner: &I) -> &[ProgramClause<I>] {
+        interner.program_clauses_data(&self.clauses)
+    }
+}
+
 /// Wraps a "canonicalized item". Items are canonicalized as follows:
 ///
 /// All unresolved existential variables are "renumbered" according to their
@@ -1410,10 +1460,13 @@ impl<I: Interner> Goal<I> {
             QuantifierKind::ForAll,
             Binders::with_fresh_type_var(interner, |ty| {
                 GoalData::Implies(
-                    vec![
-                        DomainGoal::Compatible(()).cast(interner),
-                        DomainGoal::DownstreamType(ty).cast(interner),
-                    ],
+                    ProgramClauses::from(
+                        interner,
+                        vec![
+                            DomainGoal::Compatible(()),
+                            DomainGoal::DownstreamType(ty),
+                        ],
+                    ),
                     self.shifted_in(interner),
                 )
                 .intern(interner)
@@ -1422,7 +1475,7 @@ impl<I: Interner> Goal<I> {
         .intern(interner)
     }
 
-    pub fn implied_by(self, interner: &I, predicates: Vec<ProgramClause<I>>) -> Goal<I> {
+    pub fn implied_by(self, interner: &I, predicates: ProgramClauses<I>) -> Goal<I> {
         GoalData::Implies(predicates, self).intern(interner)
     }
 
@@ -1470,7 +1523,7 @@ pub enum GoalData<I: Interner> {
     /// Introduces a binding at depth 0, shifting other bindings up
     /// (deBruijn index).
     Quantified(QuantifierKind, Binders<Goal<I>>),
-    Implies(Vec<ProgramClause<I>>, Goal<I>),
+    Implies(ProgramClauses<I>, Goal<I>),
     All(Goals<I>),
     Not(Goal<I>),
 
diff --git a/chalk-ir/src/tls.rs b/chalk-ir/src/tls.rs
index 4f8bb048176..69be655a9f0 100644
--- a/chalk-ir/src/tls.rs
+++ b/chalk-ir/src/tls.rs
@@ -1,7 +1,8 @@
 use crate::interner::ChalkIr;
 use crate::{
     debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
-    Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
+    Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
+    TraitId, Ty,
 };
 use std::cell::RefCell;
 use std::fmt;
@@ -74,6 +75,12 @@ pub trait DebugContext {
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
 
+    fn debug_program_clauses(
+        &self,
+        clauses: &ProgramClauses<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
     fn debug_application_ty(
         &self,
         application_ty: &ApplicationTy<ChalkIr>,
diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs
index 63ba17e89b7..4a419677b24 100644
--- a/chalk-ir/src/zip.rs
+++ b/chalk-ir/src/zip.rs
@@ -250,8 +250,9 @@ impl<I: Interner> Zip<I> for Environment<I> {
     where
         I: 'i,
     {
-        assert_eq!(a.clauses.len(), b.clauses.len()); // or different numbers of clauses
-        Zip::zip_with(zipper, &a.clauses, &b.clauses)?;
+        let interner = zipper.interner();
+        assert_eq!(a.clauses.len(interner), b.clauses.len(interner)); // or different numbers of clauses
+        Zip::zip_with(zipper, a.clauses.as_slice(interner), b.clauses.as_slice(interner))?;
         Ok(())
     }
 }
@@ -267,6 +268,17 @@ impl<I: Interner> Zip<I> for Goals<I> {
     }
 }
 
+impl<I: Interner> Zip<I> for ProgramClauses<I> {
+    fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
+    where
+        I: 'i,
+    {
+        let interner = zipper.interner();
+        Zip::zip_with(zipper, a.as_slice(interner), b.as_slice(interner))?;
+        Ok(())
+    }
+}
+
 /// Generates a Zip impl that requires the two enums be the same
 /// variant, then zips each field of the variant in turn. Only works
 /// if all variants have a single parenthesized value right now.
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index 0c3a3707dba..4c534d4686c 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -397,12 +397,12 @@ fn program_clauses_for_env<'db, I: Interner>(
     clauses: &mut Vec<ProgramClause<I>>,
 ) {
     let mut last_round = FxHashSet::default();
-    elaborate_env_clauses(db, &environment.clauses, &mut last_round);
+    elaborate_env_clauses(db, environment.clauses.as_slice(db.interner()), &mut last_round);
 
     let mut closure = last_round.clone();
     let mut next_round = FxHashSet::default();
     while !last_round.is_empty() {
-        elaborate_env_clauses(db, &last_round.drain().collect(), &mut next_round);
+        elaborate_env_clauses(db, &last_round.drain().collect::<Vec<_>>(), &mut next_round);
         last_round.extend(
             next_round
                 .drain()
diff --git a/chalk-solve/src/clauses/env_elaborator.rs b/chalk-solve/src/clauses/env_elaborator.rs
index cab626f9de9..2919e7d63c3 100644
--- a/chalk-solve/src/clauses/env_elaborator.rs
+++ b/chalk-solve/src/clauses/env_elaborator.rs
@@ -20,7 +20,7 @@ use rustc_hash::FxHashSet;
 /// the rule `FromEnv(T: Copy) :- FromEnv(T: Clone)
 pub(super) fn elaborate_env_clauses<I: Interner>(
     db: &dyn RustIrDatabase<I>,
-    in_clauses: &Vec<ProgramClause<I>>,
+    in_clauses: &[ProgramClause<I>],
     out: &mut FxHashSet<ProgramClause<I>>,
 ) {
     let mut this_round = vec![];
diff --git a/chalk-solve/src/ext.rs b/chalk-solve/src/ext.rs
index eb3332db4cb..6911c620a8d 100644
--- a/chalk-solve/src/ext.rs
+++ b/chalk-solve/src/ext.rs
@@ -65,7 +65,7 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
     fn into_peeled_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
         let mut infer = InferenceTable::new();
         let peeled_goal = {
-            let mut env_goal = InEnvironment::new(&Environment::new(), self);
+            let mut env_goal = InEnvironment::new(&Environment::new(interner), self);
             loop {
                 let InEnvironment { environment, goal } = env_goal;
                 match goal.data(interner) {
@@ -80,7 +80,7 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
                     }
 
                     GoalData::Implies(wc, subgoal) => {
-                        let new_environment = environment.add_clauses(wc.iter().cloned());
+                        let new_environment = environment.add_clauses(interner, wc.iter(interner).cloned());
                         env_goal = InEnvironment::new(&new_environment, Goal::clone(subgoal));
                     }
 
@@ -103,7 +103,7 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
     /// Will panic if this goal does in fact contain free variables.
     fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
         let mut infer = InferenceTable::new();
-        let env_goal = InEnvironment::new(&Environment::new(), self);
+        let env_goal = InEnvironment::new(&Environment::new(interner), self);
         let canonical_goal = infer.canonicalize(interner, &env_goal).quantified;
         infer.u_canonicalize(interner, &canonical_goal).quantified
     }
diff --git a/chalk-solve/src/goal_builder.rs b/chalk-solve/src/goal_builder.rs
index 2bda8fe06e4..f4d17af73de 100644
--- a/chalk-solve/src/goal_builder.rs
+++ b/chalk-solve/src/goal_builder.rs
@@ -46,7 +46,7 @@ impl<'i, I: Interner> GoalBuilder<'i, I> {
         G: CastTo<Goal<I>>,
     {
         GoalData::Implies(
-            clauses.into_iter().casted(self.interner()).collect(),
+            ProgramClauses::from(self.interner(), clauses),
             goal(self).cast(self.interner()),
         )
         .intern(self.interner())
diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs
index 09417d5c359..226ec64ebb7 100644
--- a/chalk-solve/src/solve/slg.rs
+++ b/chalk-solve/src/solve/slg.rs
@@ -81,7 +81,7 @@ impl<I: Interner> context::Context for SlgContext<I> {
     type BindersGoal = Binders<Goal<I>>;
     type Parameter = Parameter<I>;
     type ProgramClause = ProgramClause<I>;
-    type ProgramClauses = Vec<ProgramClause<I>>;
+    type ProgramClauses = ProgramClauses<I>;
     type CanonicalConstrainedSubst = Canonical<ConstrainedSubst<I>>;
     type CanonicalAnswerSubst = Canonical<AnswerSubst<I>>;
     type GoalInEnvironment = InEnvironment<Goal<I>>;
@@ -138,11 +138,6 @@ impl<I: Interner> context::Context for SlgContext<I> {
         &goal.goal
     }
 
-    // Used by: simplify
-    fn add_clauses(env: &Environment<I>, clauses: Vec<ProgramClause<I>>) -> Environment<I> {
-        Environment::add_clauses(env, clauses)
-    }
-
     // Used by: logic
     fn next_subgoal_index(ex_clause: &ExClause<SlgContext<I>>) -> usize {
         // For now, we always pick the last subgoal in the
@@ -216,7 +211,7 @@ impl<'me, I: Interner> context::ContextOps<SlgContext<I>> for SlgContextOps<'me,
         clauses.extend(
             environment
                 .clauses
-                .iter()
+                .iter(interner)
                 .filter(|&env_clause| env_clause.could_match(interner, goal))
                 .cloned(),
         );
@@ -224,6 +219,16 @@ impl<'me, I: Interner> context::ContextOps<SlgContext<I>> for SlgContextOps<'me,
         Ok(clauses)
     }
 
+    // Used by: simplify
+    fn add_clauses(
+        &self,
+        env: &Environment<I>,
+        clauses: ProgramClauses<I>,
+    ) -> Environment<I> {
+        let interner = self.interner();
+        env.add_clauses(interner, clauses.iter(interner).cloned())
+    }
+
     fn instantiate_ucanonical_goal(
         &self,
         arg: &UCanonical<InEnvironment<Goal<I>>>,

From 9bd8b3d6345e20edfd671a79442a6f9c6117ccc0 Mon Sep 17 00:00:00 2001
From: Wonwoo Choi <chwo9843@gmail.com>
Date: Sat, 4 Apr 2020 04:14:15 +0900
Subject: [PATCH 3/5] cargo fmt

---
 chalk-engine/src/context.rs        |  6 +-----
 chalk-integration/src/lowering.rs  |  3 ++-
 chalk-ir/src/could_match.rs        |  4 +++-
 chalk-ir/src/debug.rs              |  3 +--
 chalk-ir/src/fold/boring_impls.rs  | 16 +++++++++-------
 chalk-ir/src/interner.rs           |  5 +----
 chalk-ir/src/lib.rs                | 23 +++++++++++++----------
 chalk-ir/src/zip.rs                |  6 +++++-
 chalk-solve/src/clauses.rs         |  6 +++++-
 chalk-solve/src/clauses/builder.rs | 14 +++++++++-----
 chalk-solve/src/ext.rs             |  3 ++-
 chalk-solve/src/solve/slg.rs       |  6 +-----
 12 files changed, 52 insertions(+), 43 deletions(-)

diff --git a/chalk-engine/src/context.rs b/chalk-engine/src/context.rs
index ecf4b11c85e..bfb9ce3ce6e 100644
--- a/chalk-engine/src/context.rs
+++ b/chalk-engine/src/context.rs
@@ -178,11 +178,7 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
     ) -> Result<Vec<C::ProgramClause>, Floundered>;
 
     // Used by: simplify
-    fn add_clauses(
-        &self,
-        env: &C::Environment,
-        clauses: C::ProgramClauses,
-    ) -> C::Environment;
+    fn add_clauses(&self, env: &C::Environment, clauses: C::ProgramClauses) -> C::Environment;
 
     /// Create an inference table for processing a new goal and instantiate that goal
     /// in that context, returning "all the pieces".
diff --git a/chalk-integration/src/lowering.rs b/chalk-integration/src/lowering.rs
index 5063f094dde..c2f156a6eaa 100644
--- a/chalk-integration/src/lowering.rs
+++ b/chalk-integration/src/lowering.rs
@@ -1307,7 +1307,8 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                     .into_iter()
                     .flat_map(|h| h.lower_clause(env).apply_result())
                     .map(|result| result.map(|h| h.into_from_env_clause(interner)));
-                let where_clauses = chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
+                let where_clauses =
+                    chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
                 Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
             }
             Goal::And(g1, g2s) => {
diff --git a/chalk-ir/src/could_match.rs b/chalk-ir/src/could_match.rs
index a4bb37bc133..32ca416f970 100644
--- a/chalk-ir/src/could_match.rs
+++ b/chalk-ir/src/could_match.rs
@@ -69,7 +69,9 @@ impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClauseData<I> {
                 implication.consequence.could_match(interner, other)
             }
 
-            ProgramClauseData::ForAll(clause) => clause.value.consequence.could_match(interner, other),
+            ProgramClauseData::ForAll(clause) => {
+                clause.value.consequence.could_match(interner, other)
+            }
         }
     }
 }
diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 74a09c1d0b0..5386781687a 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -60,8 +60,7 @@ impl<I: Interner> Debug for ProgramClauseImplication<I> {
 
 impl<I: Interner> Debug for ProgramClause<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        I::debug_program_clause(self, fmt)
-            .unwrap_or_else(|| write!(fmt, "{:?}", self.clause))
+        I::debug_program_clause(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.clause))
     }
 }
 
diff --git a/chalk-ir/src/fold/boring_impls.rs b/chalk-ir/src/fold/boring_impls.rs
index b027c30ec05..40485b7ca08 100644
--- a/chalk-ir/src/fold/boring_impls.rs
+++ b/chalk-ir/src/fold/boring_impls.rs
@@ -259,12 +259,12 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<
         TI: 'i,
     {
         match self {
-            ProgramClauseData::Implies(pci) => {
-                Ok(ProgramClauseData::Implies(pci.fold_with(folder, outer_binder)?))
-            }
-            ProgramClauseData::ForAll(pci) => {
-                Ok(ProgramClauseData::ForAll(pci.fold_with(folder, outer_binder)?))
-            }
+            ProgramClauseData::Implies(pci) => Ok(ProgramClauseData::Implies(
+                pci.fold_with(folder, outer_binder)?,
+            )),
+            ProgramClauseData::ForAll(pci) => Ok(ProgramClauseData::ForAll(
+                pci.fold_with(folder, outer_binder)?,
+            )),
         }
     }
 }
@@ -280,7 +280,9 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
         TI: 'i,
     {
         let clause = self.data(folder.interner());
-        Ok(clause.super_fold_with(folder, outer_binder)?.intern(folder.target_interner()))
+        Ok(clause
+            .super_fold_with(folder, outer_binder)?
+            .intern(folder.target_interner()))
     }
 }
 
diff --git a/chalk-ir/src/interner.rs b/chalk-ir/src/interner.rs
index 122205c788f..bacccd2105b 100644
--- a/chalk-ir/src/interner.rs
+++ b/chalk-ir/src/interner.rs
@@ -637,10 +637,7 @@ mod default {
             substitution
         }
 
-        fn intern_program_clause(
-            &self,
-            data: ProgramClauseData<Self>,
-        ) -> ProgramClauseData<Self> {
+        fn intern_program_clause(&self, data: ProgramClauseData<Self>) -> ProgramClauseData<Self> {
             data
         }
 
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index 88e593bf406..0e197e20758 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -53,7 +53,9 @@ pub struct Environment<I: Interner> {
 
 impl<I: Interner> Environment<I> {
     pub fn new(interner: &I) -> Self {
-        Environment { clauses: ProgramClauses::new(interner) }
+        Environment {
+            clauses: ProgramClauses::new(interner),
+        }
     }
 
     pub fn add_clauses<II>(&self, interner: &I, clauses: II) -> Self
@@ -61,7 +63,8 @@ impl<I: Interner> Environment<I> {
         II: IntoIterator<Item = ProgramClause<I>>,
     {
         let mut env = self.clone();
-        env.clauses = ProgramClauses::from(interner, env.clauses.iter(interner).cloned().chain(clauses));
+        env.clauses =
+            ProgramClauses::from(interner, env.clauses.iter(interner).cloned().chain(clauses));
         env
     }
 }
@@ -1233,9 +1236,9 @@ impl<I: Interner> ProgramClauseData<I> {
             ProgramClauseData::Implies(implication) => {
                 ProgramClauseData::Implies(implication.into_from_env_clause(interner))
             }
-            ProgramClauseData::ForAll(binders_implication) => {
-                ProgramClauseData::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
-            }
+            ProgramClauseData::ForAll(binders_implication) => ProgramClauseData::ForAll(
+                binders_implication.map(|i| i.into_from_env_clause(interner)),
+            ),
         }
     }
 
@@ -1279,7 +1282,10 @@ impl<I: Interner> ProgramClauses<I> {
         &self.clauses
     }
 
-    pub fn from(interner: &I, clauses: impl IntoIterator<Item = impl CastTo<ProgramClause<I>>>) -> Self {
+    pub fn from(
+        interner: &I,
+        clauses: impl IntoIterator<Item = impl CastTo<ProgramClause<I>>>,
+    ) -> Self {
         use crate::cast::Caster;
         ProgramClauses {
             clauses: I::intern_program_clauses(interner, clauses.into_iter().casted(interner)),
@@ -1462,10 +1468,7 @@ impl<I: Interner> Goal<I> {
                 GoalData::Implies(
                     ProgramClauses::from(
                         interner,
-                        vec![
-                            DomainGoal::Compatible(()),
-                            DomainGoal::DownstreamType(ty),
-                        ],
+                        vec![DomainGoal::Compatible(()), DomainGoal::DownstreamType(ty)],
                     ),
                     self.shifted_in(interner),
                 )
diff --git a/chalk-ir/src/zip.rs b/chalk-ir/src/zip.rs
index 4a419677b24..5aef08a92c1 100644
--- a/chalk-ir/src/zip.rs
+++ b/chalk-ir/src/zip.rs
@@ -252,7 +252,11 @@ impl<I: Interner> Zip<I> for Environment<I> {
     {
         let interner = zipper.interner();
         assert_eq!(a.clauses.len(interner), b.clauses.len(interner)); // or different numbers of clauses
-        Zip::zip_with(zipper, a.clauses.as_slice(interner), b.clauses.as_slice(interner))?;
+        Zip::zip_with(
+            zipper,
+            a.clauses.as_slice(interner),
+            b.clauses.as_slice(interner),
+        )?;
         Ok(())
     }
 }
diff --git a/chalk-solve/src/clauses.rs b/chalk-solve/src/clauses.rs
index 4c534d4686c..dac36b6debd 100644
--- a/chalk-solve/src/clauses.rs
+++ b/chalk-solve/src/clauses.rs
@@ -397,7 +397,11 @@ fn program_clauses_for_env<'db, I: Interner>(
     clauses: &mut Vec<ProgramClause<I>>,
 ) {
     let mut last_round = FxHashSet::default();
-    elaborate_env_clauses(db, environment.clauses.as_slice(db.interner()), &mut last_round);
+    elaborate_env_clauses(
+        db,
+        environment.clauses.as_slice(db.interner()),
+        &mut last_round,
+    );
 
     let mut closure = last_round.clone();
     let mut next_round = FxHashSet::default();
diff --git a/chalk-solve/src/clauses/builder.rs b/chalk-solve/src/clauses/builder.rs
index 767abda8ed1..4a40dde4397 100644
--- a/chalk-solve/src/clauses/builder.rs
+++ b/chalk-solve/src/clauses/builder.rs
@@ -51,12 +51,16 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
         };
 
         if self.binders.len() == 0 {
-            self.clauses.push(ProgramClauseData::Implies(clause).intern(interner));
+            self.clauses
+                .push(ProgramClauseData::Implies(clause).intern(interner));
         } else {
-            self.clauses.push(ProgramClauseData::ForAll(Binders {
-                binders: self.binders.clone(),
-                value: clause,
-            }).intern(interner));
+            self.clauses.push(
+                ProgramClauseData::ForAll(Binders {
+                    binders: self.binders.clone(),
+                    value: clause,
+                })
+                .intern(interner),
+            );
         }
 
         debug!("pushed clause {:?}", self.clauses.last());
diff --git a/chalk-solve/src/ext.rs b/chalk-solve/src/ext.rs
index 6911c620a8d..9d15d8c6c9b 100644
--- a/chalk-solve/src/ext.rs
+++ b/chalk-solve/src/ext.rs
@@ -80,7 +80,8 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
                     }
 
                     GoalData::Implies(wc, subgoal) => {
-                        let new_environment = environment.add_clauses(interner, wc.iter(interner).cloned());
+                        let new_environment =
+                            environment.add_clauses(interner, wc.iter(interner).cloned());
                         env_goal = InEnvironment::new(&new_environment, Goal::clone(subgoal));
                     }
 
diff --git a/chalk-solve/src/solve/slg.rs b/chalk-solve/src/solve/slg.rs
index 226ec64ebb7..29cb27ad6cc 100644
--- a/chalk-solve/src/solve/slg.rs
+++ b/chalk-solve/src/solve/slg.rs
@@ -220,11 +220,7 @@ impl<'me, I: Interner> context::ContextOps<SlgContext<I>> for SlgContextOps<'me,
     }
 
     // Used by: simplify
-    fn add_clauses(
-        &self,
-        env: &Environment<I>,
-        clauses: ProgramClauses<I>,
-    ) -> Environment<I> {
+    fn add_clauses(&self, env: &Environment<I>, clauses: ProgramClauses<I>) -> Environment<I> {
         let interner = self.interner();
         env.add_clauses(interner, clauses.iter(interner).cloned())
     }

From 3318461f3375bf625c71ffcfd0d4aa7055660cc3 Mon Sep 17 00:00:00 2001
From: Wonwoo Choi <chwo9843@gmail.com>
Date: Sat, 4 Apr 2020 16:35:03 +0900
Subject: [PATCH 4/5] Address reviews

---
 chalk-ir/src/debug.rs |  4 ++--
 chalk-ir/src/lib.rs   | 27 +++++++++++++++++----------
 2 files changed, 19 insertions(+), 12 deletions(-)

diff --git a/chalk-ir/src/debug.rs b/chalk-ir/src/debug.rs
index 5386781687a..31f328bd5e7 100644
--- a/chalk-ir/src/debug.rs
+++ b/chalk-ir/src/debug.rs
@@ -60,13 +60,13 @@ impl<I: Interner> Debug for ProgramClauseImplication<I> {
 
 impl<I: Interner> Debug for ProgramClause<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        I::debug_program_clause(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.clause))
+        I::debug_program_clause(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
     }
 }
 
 impl<I: Interner> Debug for ProgramClauses<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.clauses))
+        I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
     }
 }
 
diff --git a/chalk-ir/src/lib.rs b/chalk-ir/src/lib.rs
index 0e197e20758..acff418fead 100644
--- a/chalk-ir/src/lib.rs
+++ b/chalk-ir/src/lib.rs
@@ -1244,33 +1244,40 @@ impl<I: Interner> ProgramClauseData<I> {
 
     pub fn intern(self, interner: &I) -> ProgramClause<I> {
         ProgramClause {
-            clause: interner.intern_program_clause(self),
+            interned: interner.intern_program_clause(self),
         }
     }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub struct ProgramClause<I: Interner> {
-    clause: I::InternedProgramClause,
+    interned: I::InternedProgramClause,
 }
 
 impl<I: Interner> ProgramClause<I> {
+    pub fn new(interner: &I, clause: ProgramClauseData<I>) -> Self {
+        let interned = interner.intern_program_clause(clause);
+        Self { interned }
+    }
+
     pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
         let program_clause_data = self.data(interner);
         let new_clause = program_clause_data.clone().into_from_env_clause(interner);
-        ProgramClause {
-            clause: interner.intern_program_clause(new_clause),
-        }
+        Self::new(interner, new_clause)
+    }
+
+    pub fn interned(&self) -> &I::InternedProgramClause {
+        &self.interned
     }
 
     pub fn data(&self, interner: &I) -> &ProgramClauseData<I> {
-        interner.program_clause_data(&self.clause)
+        interner.program_clause_data(&self.interned)
     }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
 pub struct ProgramClauses<I: Interner> {
-    clauses: I::InternedProgramClauses,
+    interned: I::InternedProgramClauses,
 }
 
 impl<I: Interner> ProgramClauses<I> {
@@ -1279,7 +1286,7 @@ impl<I: Interner> ProgramClauses<I> {
     }
 
     pub fn interned(&self) -> &I::InternedProgramClauses {
-        &self.clauses
+        &self.interned
     }
 
     pub fn from(
@@ -1288,7 +1295,7 @@ impl<I: Interner> ProgramClauses<I> {
     ) -> Self {
         use crate::cast::Caster;
         ProgramClauses {
-            clauses: I::intern_program_clauses(interner, clauses.into_iter().casted(interner)),
+            interned: I::intern_program_clauses(interner, clauses.into_iter().casted(interner)),
         }
     }
 
@@ -1317,7 +1324,7 @@ impl<I: Interner> ProgramClauses<I> {
     }
 
     pub fn as_slice(&self, interner: &I) -> &[ProgramClause<I>] {
-        interner.program_clauses_data(&self.clauses)
+        interner.program_clauses_data(&self.interned)
     }
 }
 

From 6ad46a2db28c45717836906142072be8f08f4d0d Mon Sep 17 00:00:00 2001
From: Wonwoo Choi <chwo9843@gmail.com>
Date: Sat, 4 Apr 2020 16:37:11 +0900
Subject: [PATCH 5/5] Fix tests

---
 chalk-solve/src/infer/test.rs     | 24 ++++++++++++------------
 chalk-solve/src/solve/truncate.rs |  4 ++--
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/chalk-solve/src/infer/test.rs b/chalk-solve/src/infer/test.rs
index 4db887456ac..9d448ac82cf 100644
--- a/chalk-solve/src/infer/test.rs
+++ b/chalk-solve/src/infer/test.rs
@@ -8,7 +8,7 @@ use chalk_ir::interner::ChalkIr;
 fn infer() {
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U0).to_ty(interner);
     table
@@ -32,7 +32,7 @@ fn universe_error() {
     // exists(A -> forall(X -> A = X)) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     table
         .unify(interner, &environment0, &a, &ty!(placeholder 1))
@@ -44,7 +44,7 @@ fn cycle_error() {
     // exists(A -> A = foo A) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     table
         .unify(interner, &environment0, &a, &ty!(apply (item 0) (expr a)))
@@ -61,7 +61,7 @@ fn cycle_indirect() {
     // exists(A -> A = foo B, A = B) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U0).to_ty(interner);
     table
@@ -75,7 +75,7 @@ fn universe_error_indirect_1() {
     // exists(A -> forall(X -> exists(B -> B = X, A = B))) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U1).to_ty(interner);
     table
@@ -89,7 +89,7 @@ fn universe_error_indirect_2() {
     // exists(A -> forall(X -> exists(B -> B = A, B = X))) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U1).to_ty(interner);
     table.unify(interner, &environment0, &a, &b).unwrap();
@@ -103,7 +103,7 @@ fn universe_promote() {
     // exists(A -> forall(X -> exists(B -> A = foo(B), A = foo(i32)))) ---> OK
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U1).to_ty(interner);
     table
@@ -124,7 +124,7 @@ fn universe_promote_bad() {
     // exists(A -> forall(X -> exists(B -> A = foo(B), B = X))) ---> error
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
     let b = table.new_variable(U1).to_ty(interner);
     table
@@ -142,7 +142,7 @@ fn projection_eq() {
     //                       we say no, but it's an interesting question.
     let interner = &ChalkIr;
     let mut table: InferenceTable<ChalkIr> = InferenceTable::new();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     let a = table.new_variable(U0).to_ty(interner);
 
     // expect an error ("cycle during unification")
@@ -194,7 +194,7 @@ fn quantify_simple() {
 fn quantify_bound() {
     let interner = &ChalkIr;
     let mut table = make_table();
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
 
     let v0 = table.new_variable(U0).to_ty(interner);
     let v1 = table.new_variable(U1).to_ty(interner);
@@ -237,7 +237,7 @@ fn quantify_ty_under_binder() {
     let _r2 = table.new_variable(U0);
 
     // Unify v0 and v1.
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
     table
         .unify(
             interner,
@@ -274,7 +274,7 @@ fn lifetime_constraint_indirect() {
     let _t_0 = table.new_variable(U0);
     let _l_1 = table.new_variable(U1);
 
-    let environment0 = Environment::new();
+    let environment0 = Environment::new(interner);
 
     // Here, we unify '?1 (the lifetime variable in universe 1) with
     // '!1.
diff --git a/chalk-solve/src/solve/truncate.rs b/chalk-solve/src/solve/truncate.rs
index 966c1923bee..827e0c42dc1 100644
--- a/chalk-solve/src/solve/truncate.rs
+++ b/chalk-solve/src/solve/truncate.rs
@@ -139,7 +139,7 @@ fn truncate_types() {
     use chalk_ir::interner::ChalkIr;
     let interner = &ChalkIr;
     let mut table = InferenceTable::<chalk_ir::interner::ChalkIr>::new();
-    let environment0 = &Environment::new();
+    let environment0 = &Environment::new(interner);
     let _u1 = table.new_universe();
 
     // Vec<Vec<Vec<Vec<T>>>>
@@ -233,7 +233,7 @@ fn truncate_normalizes() {
     let interner = &ChalkIr;
     let mut table = InferenceTable::<chalk_ir::interner::ChalkIr>::new();
 
-    let environment0 = &Environment::new();
+    let environment0 = &Environment::new(interner);
     let u1 = table.new_universe();
 
     // ty0 = Vec<Vec<X>>