Migrate Vec<ParameterKinds<()>> and Vec<ParameterKinds<UniverseIndex>> to interned

chalk-engine/src/forest.rs

@@ -113,6 +113,23 @@ pub enum SubstitutionResult<S> {
     Floundered,
 }
 
+impl<S> SubstitutionResult<S> {
+    pub fn as_ref(&self) -> SubstitutionResult<&S> {
+        match self {
+            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst),
+            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst),
+            SubstitutionResult::Floundered => SubstitutionResult::Floundered,
+        }
+    }
+    pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> {
+        match self {
+            SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)),
+            SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)),
+            SubstitutionResult::Floundered => SubstitutionResult::Floundered,
+        }
+    }
+}
+
 impl<S: Display> Display for SubstitutionResult<S> {
     fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self {

chalk-integration/src/lib.rs

@@ -11,6 +11,7 @@ pub mod program;
 pub mod program_environment;
 pub mod query;
 
+use chalk_ir::interner::{ChalkIr, HasInterner};
 pub use chalk_ir::interner::{Identifier, RawId};
 use chalk_ir::Binders;
 
@@ -21,9 +22,16 @@ pub enum TypeSort {
     Opaque,
 }
 
+#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Unit;
+
+impl HasInterner for Unit {
+    type Interner = ChalkIr;
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct TypeKind {
     pub sort: TypeSort,
     pub name: Identifier,
-    pub binders: Binders<()>,
+    pub binders: Binders<Unit>,
 }

chalk-integration/src/lowering.rs

@@ -1,7 +1,7 @@
 use chalk_ir::cast::{Cast, Caster};
-use chalk_ir::interner::ChalkIr;
+use chalk_ir::interner::{ChalkIr, HasInterner};
 use chalk_ir::{
-    self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId,
+    self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
     QuantifiedWhereClauses, StructId, Substitution, TraitId,
 };
 use chalk_parse::ast::*;
@@ -174,11 +174,16 @@ impl<'k> Env<'k> {
     where
         I: IntoIterator<Item = chalk_ir::ParameterKind<Ident>>,
         I::IntoIter: ExactSizeIterator,
+        T: HasInterner<Interner = ChalkIr>,
         OP: FnOnce(&Self) -> LowerResult<T>,
     {
+        let interner = &ChalkIr;
         let binders: Vec<_> = binders.into_iter().collect();
         let env = self.introduce(binders.iter().cloned())?;
-        Ok(chalk_ir::Binders::new(binders.anonymize(), op(&env)?))
+        Ok(chalk_ir::Binders::new(
+            ParameterKinds::from(interner, binders.anonymize()),
+            op(&env)?,
+        ))
     }
 }
 
@@ -594,10 +599,14 @@ trait LowerWhereClauses {
 
 impl LowerTypeKind for StructDefn {
     fn lower_type_kind(&self) -> LowerResult<TypeKind> {
+        let interner = &ChalkIr;
         Ok(TypeKind {
             sort: TypeSort::Struct,
             name: self.name.str,
-            binders: chalk_ir::Binders::new(self.all_parameters().anonymize(), ()),
+            binders: chalk_ir::Binders::new(
+                ParameterKinds::from(interner, self.all_parameters().anonymize()),
+                crate::Unit,
+            ),
         })
     }
 }
@@ -610,26 +619,31 @@ impl LowerWhereClauses for StructDefn {
 
 impl LowerTypeKind for TraitDefn {
     fn lower_type_kind(&self) -> LowerResult<TypeKind> {
+        let interner = &ChalkIr;
         let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
         Ok(TypeKind {
             sort: TypeSort::Trait,
             name: self.name.str,
             binders: chalk_ir::Binders::new(
                 // for the purposes of the *type*, ignore `Self`:
-                binders.anonymize(),
-                (),
+                ParameterKinds::from(interner, binders.anonymize()),
+                crate::Unit,
             ),
         })
     }
 }
 
 impl LowerTypeKind for OpaqueTyDefn {
     fn lower_type_kind(&self) -> LowerResult<TypeKind> {
+        let interner = &ChalkIr;
         let binders: Vec<_> = self.parameter_kinds.iter().map(|p| p.lower()).collect();
         Ok(TypeKind {
             sort: TypeSort::Opaque,
             name: self.identifier.str,
-            binders: chalk_ir::Binders::new(binders.anonymize(), ()),
+            binders: chalk_ir::Binders::new(
+                ParameterKinds::from(interner, binders.anonymize()),
+                crate::Unit,
+            ),
         })
     }
 }
@@ -835,6 +849,7 @@ trait LowerTraitBound {
 
 impl LowerTraitBound for TraitBound {
     fn lower(&self, env: &Env) -> LowerResult<rust_ir::TraitBound<ChalkIr>> {
+        let interner = &ChalkIr;
         let trait_id = env.lookup_trait(self.trait_name)?;
 
         let k = env.trait_kind(trait_id);
@@ -848,15 +863,15 @@ impl LowerTraitBound for TraitBound {
             .map(|a| Ok(a.lower(env)?))
             .collect::<LowerResult<Vec<_>>>()?;
 
-        if parameters.len() != k.binders.len() {
+        if parameters.len() != k.binders.len(interner) {
             Err(RustIrError::IncorrectNumberOfTypeParameters {
                 identifier: self.trait_name,
-                expected: k.binders.len(),
+                expected: k.binders.len(interner),
                 actual: parameters.len(),
             })?;
         }
 
-        for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
+        for (binder, param) in k.binders.binders.iter(interner).zip(parameters.iter()) {
             if binder.kind() != param.kind() {
                 Err(RustIrError::IncorrectTraitParameterKind {
                     identifier: self.trait_name,
@@ -1062,10 +1077,10 @@ impl LowerTy for Ty {
             Ty::Id { name } => match env.lookup_type(name)? {
                 TypeLookup::Struct(id) => {
                     let k = env.struct_kind(id);
-                    if k.binders.len() > 0 {
+                    if k.binders.len(interner) > 0 {
                         Err(RustIrError::IncorrectNumberOfTypeParameters {
                             identifier: name,
-                            expected: k.binders.len(),
+                            expected: k.binders.len(interner),
                             actual: 0,
                         })
                     } else {
@@ -1118,10 +1133,10 @@ impl LowerTy for Ty {
                 };
 
                 let k = env.struct_kind(id);
-                if k.binders.len() != args.len() {
+                if k.binders.len(interner) != args.len() {
                     Err(RustIrError::IncorrectNumberOfTypeParameters {
                         identifier: name,
-                        expected: k.binders.len(),
+                        expected: k.binders.len(interner),
                         actual: args.len(),
                     })?;
                 }
@@ -1131,7 +1146,7 @@ impl LowerTy for Ty {
                     args.iter().map(|t| Ok(t.lower(env)?)),
                 )?;
 
-                for (param, arg) in k.binders.binders.iter().zip(args.iter()) {
+                for (param, arg) in k.binders.binders.iter(interner).zip(args.iter()) {
                     if param.kind() != arg.kind() {
                         Err(RustIrError::IncorrectParameterKind {
                             identifier: name,
@@ -1362,14 +1377,16 @@ pub trait LowerGoal<A> {
 
 impl LowerGoal<LoweredProgram> for Goal {
     fn lower(&self, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
+        let interner = &ChalkIr;
         let associated_ty_lookups: BTreeMap<_, _> = program
             .associated_ty_data
             .iter()
             .map(|(&associated_ty_id, datum)| {
                 let trait_datum = &program.trait_data[&datum.trait_id];
-                let num_trait_params = trait_datum.binders.len();
-                let num_addl_params = datum.binders.len() - num_trait_params;
-                let addl_parameter_kinds = datum.binders.binders[..num_addl_params].to_owned();
+                let num_trait_params = trait_datum.binders.len(interner);
+                let num_addl_params = datum.binders.len(interner) - num_trait_params;
+                let addl_parameter_kinds =
+                    datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
                 let lookup = AssociatedTyLookup {
                     id: associated_ty_id,
                     addl_parameter_kinds,

chalk-integration/src/program.rs

@@ -188,6 +188,33 @@ impl tls::DebugContext for Program {
         write!(fmt, "{:?}", parameter.data(interner).inner_debug())
     }
 
+    fn debug_parameter_kinds(
+        &self,
+        parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
+    }
+
+    fn debug_parameter_kinds_with_angles(
+        &self,
+        parameter_kinds: &chalk_ir::ParameterKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", parameter_kinds.inner_debug(interner))
+    }
+
+    fn debug_canonical_var_kinds(
+        &self,
+        parameter_kinds: &chalk_ir::CanonicalVarKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", parameter_kinds.as_slice(interner))
+    }
+
     fn debug_goal(
         &self,
         goal: &Goal<ChalkIr>,

chalk-ir/src/cast.rs

@@ -82,6 +82,8 @@ reflexive_impl!(for(I: Interner) Goal<I>);
 reflexive_impl!(for(I: Interner) WhereClause<I>);
 reflexive_impl!(for(I: Interner) ProgramClause<I>);
 reflexive_impl!(for(I: Interner) QuantifiedWhereClause<I>);
+reflexive_impl!(for(I: Interner) ParameterKinds<I>);
+reflexive_impl!(for(I: Interner) CanonicalVarKinds<I>);
 
 impl<I: Interner> CastTo<WhereClause<I>> for TraitRef<I> {
     fn cast_to(self, _interner: &I) -> WhereClause<I> {
@@ -138,7 +140,7 @@ impl<I: Interner> CastTo<Goal<I>> for EqGoal<I> {
     }
 }
 
-impl<T: CastTo<Goal<I>>, I: Interner> CastTo<Goal<I>> for Binders<T> {
+impl<I: Interner, T: HasInterner<Interner = I> + CastTo<Goal<I>>> CastTo<Goal<I>> for Binders<T> {
     fn cast_to(self, interner: &I) -> Goal<I> {
         GoalData::Quantified(
             QuantifierKind::ForAll,
@@ -193,10 +195,10 @@ where
     }
 }
 
-impl<T, I> CastTo<ProgramClause<I>> for Binders<T>
+impl<I, T> CastTo<ProgramClause<I>> for Binders<T>
 where
-    T: CastTo<DomainGoal<I>>,
     I: Interner,
+    T: HasInterner<Interner = I> + CastTo<DomainGoal<I>>,
 {
     fn cast_to(self, interner: &I) -> ProgramClause<I> {
         ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
@@ -268,16 +270,16 @@ where
 impl<T, U> CastTo<Canonical<U>> for Canonical<T>
 where
     T: CastTo<U> + HasInterner,
-    U: HasInterner,
+    U: HasInterner<Interner = T::Interner>,
 {
-    fn cast_to(self, interner: &U::Interner) -> Canonical<U> {
+    fn cast_to(self, interner: &T::Interner) -> Canonical<U> {
         // Subtle point: It should be ok to re-use the binders here,
         // because `cast()` never introduces new inference variables,
         // nor changes the "substance" of the type we are working
         // with. It just introduces new wrapper types.
         Canonical {
             value: self.value.cast(interner),
-            binders: self.binders,
+            binders: self.binders.cast(interner),
         }
     }
 }

chalk-ir/src/could_match.rs

@@ -50,7 +50,7 @@ where
 
             fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
             where
-                T: Zip<I>,
+                T: HasInterner + Zip<I>,
             {
                 Zip::zip_with(self, &a.value, &b.value)
             }

chalk-ir/src/debug.rs

@@ -210,22 +210,63 @@ impl<I: Interner> Debug for LifetimeData<I> {
     }
 }
 
+impl<I: Interner> ParameterKinds<I> {
+    fn debug(&self) -> ParameterKindsDebug<'_, I> {
+        ParameterKindsDebug(self)
+    }
+
+    pub fn inner_debug<'a>(&'a self, interner: &'a I) -> ParameterKindsInnerDebug<'a, I> {
+        ParameterKindsInnerDebug {
+            parameter_kinds: self,
+            interner,
+        }
+    }
+}
+
+struct ParameterKindsDebug<'a, I: Interner>(&'a ParameterKinds<I>);
+
+impl<'a, I: Interner> Debug for ParameterKindsDebug<'a, I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_parameter_kinds_with_angles(self.0, fmt)
+            .unwrap_or_else(|| write!(fmt, "{:?}", self.0.interned))
+    }
+}
+
+pub struct ParameterKindsInnerDebug<'a, I: Interner> {
+    parameter_kinds: &'a ParameterKinds<I>,
+    interner: &'a I,
+}
+
+impl<'a, I: Interner> Debug for ParameterKindsInnerDebug<'a, I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        // NB: We print parameter kinds as a list delimited by `<>`,
+        // like `<K1, K2, ..>`. This is because parameter kind lists
+        // are always associated with binders like `forall<type> {
+        // ... }`.
+        write!(fmt, "<")?;
+        for (index, binder) in self.parameter_kinds.iter(self.interner).enumerate() {
+            if index > 0 {
+                write!(fmt, ", ")?;
+            }
+            match *binder {
+                ParameterKind::Ty(()) => write!(fmt, "type")?,
+                ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
+            }
+        }
+        write!(fmt, ">")
+    }
+}
+
 impl<I: Interner> Debug for GoalData<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         match self {
-            GoalData::Quantified(qkind, ref subgoal) => {
-                write!(fmt, "{:?}<", qkind)?;
-                for (index, binder) in subgoal.binders.iter().enumerate() {
-                    if index > 0 {
-                        write!(fmt, ", ")?;
-                    }
-                    match *binder {
-                        ParameterKind::Ty(()) => write!(fmt, "type")?,
-                        ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
-                    }
-                }
-                write!(fmt, "> {{ {:?} }}", subgoal.value)
-            }
+            GoalData::Quantified(qkind, ref subgoal) => write!(
+                fmt,
+                "{:?}{:?} {{ {:?} }}",
+                qkind,
+                subgoal.binders.debug(),
+                subgoal.value
+            ),
             GoalData::Implies(ref wc, ref g) => write!(fmt, "if ({:?}) {{ {:?} }}", wc, g),
             GoalData::All(ref goals) => write!(fmt, "all{:?}", goals),
             GoalData::Not(ref g) => write!(fmt, "not {{ {:?} }}", g),
@@ -593,30 +634,13 @@ impl<I: Interner> Debug for EqGoal<I> {
     }
 }
 
-impl<T: Debug> Debug for Binders<T> {
+impl<T: HasInterner + Debug> Debug for Binders<T> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         let Binders {
             ref binders,
             ref value,
         } = *self;
-
-        // NB: We always print the `for<>`, even if it is empty,
-        // because it may affect the debruijn indices of things
-        // contained within. For example, `for<> { ^1.0 }` is very
-        // different from `^1.0` in terms of what variable is being
-        // referenced.
-
-        write!(fmt, "for<")?;
-        for (index, binder) in binders.iter().enumerate() {
-            if index > 0 {
-                write!(fmt, ", ")?;
-            }
-            match *binder {
-                ParameterKind::Ty(()) => write!(fmt, "type")?,
-                ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
-            }
-        }
-        write!(fmt, "> ")?;
+        write!(fmt, "for{:?} ", binders.debug())?;
         Debug::fmt(value, fmt)
     }
 }
@@ -636,10 +660,32 @@ impl<I: Interner> Debug for Environment<I> {
     }
 }
 
-impl<T: Display> Display for Canonical<T> {
-    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
-        let Canonical { binders, value } = self;
+impl<I: Interner> Debug for CanonicalVarKinds<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_canonical_var_kinds(self, fmt)
+            .unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
+    }
+}
 
+impl<T: HasInterner + Display> Canonical<T> {
+    pub fn display<'a>(&'a self, interner: &'a T::Interner) -> CanonicalDisplay<'a, T> {
+        CanonicalDisplay {
+            canonical: self,
+            interner,
+        }
+    }
+}
+
+pub struct CanonicalDisplay<'a, T: HasInterner> {
+    canonical: &'a Canonical<T>,
+    interner: &'a T::Interner,
+}
+
+impl<'a, T: HasInterner + Display> Display for CanonicalDisplay<'a, T> {
+    fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
+        let Canonical { binders, value } = self.canonical;
+        let interner = self.interner;
+        let binders = binders.as_slice(interner);
         if binders.is_empty() {
             // Ordinarily, we try to print all binder levels, if they
             // are empty, but we can skip in this *particular* case

chalk-ir/src/fold/binder_impls.rs

@@ -30,7 +30,8 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Fn<I> {
 
 impl<T, I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Binders<T>
 where
-    T: Fold<I, TI>,
+    T: HasInterner<Interner = I> + Fold<I, TI>,
+    <T as Fold<I, TI>>::Result: HasInterner<Interner = TI>,
     I: Interner,
 {
     type Result = Binders<T::Result>;
@@ -48,17 +49,18 @@ where
             value: self_value,
         } = self;
         let value = self_value.fold_with(folder, outer_binder.shifted_in())?;
-        Ok(Binders {
-            binders: self_binders.clone(),
-            value: value,
-        })
+        let binders = ParameterKinds {
+            interned: TI::transfer_parameter_kinds(self_binders.interned().clone()),
+        };
+        Ok(Binders::new(binders, value))
     }
 }
 
-impl<T, I, TI> Fold<I, TI> for Canonical<T>
+impl<I, T, TI> Fold<I, TI> for Canonical<T>
 where
-    T: Fold<I, TI>,
     I: Interner,
+    T: HasInterner<Interner = I> + Fold<I, TI>,
+    <T as Fold<I, TI>>::Result: HasInterner<Interner = TI>,
     TI: TargetInterner<I>,
 {
     type Result = Canonical<T::Result>;
@@ -76,8 +78,11 @@ where
             value: self_value,
         } = self;
         let value = self_value.fold_with(folder, outer_binder.shifted_in())?;
+        let binders = CanonicalVarKinds {
+            interned: TI::transfer_canonical_var_kinds(self_binders.interned().clone()),
+        };
         Ok(Canonical {
-            binders: self_binders.clone(),
+            binders: binders,
             value: value,
         })
     }

chalk-ir/src/interner.rs

@@ -1,6 +1,7 @@
 use crate::AliasTy;
 use crate::ApplicationTy;
 use crate::AssocTypeId;
+use crate::CanonicalVarKinds;
 use crate::Goal;
 use crate::GoalData;
 use crate::Goals;
@@ -10,6 +11,8 @@ use crate::OpaqueTy;
 use crate::OpaqueTyId;
 use crate::Parameter;
 use crate::ParameterData;
+use crate::ParameterKind;
+use crate::ParameterKinds;
 use crate::ProgramClause;
 use crate::ProgramClauseData;
 use crate::ProgramClauseImplication;
@@ -23,6 +26,7 @@ use crate::Substitution;
 use crate::TraitId;
 use crate::Ty;
 use crate::TyData;
+use crate::UniverseIndex;
 use chalk_engine::context::Context;
 use chalk_engine::ExClause;
 use std::fmt::{self, Debug};
@@ -126,6 +130,23 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// and can be converted back to its underlying data via `quantified_where_clauses_data`.
     type InternedQuantifiedWhereClauses: Debug + Clone + Eq + Hash;
 
+    /// "Interned" representation of a list of parameter kind.  
+    /// In normal user code, `Self::InternedParameterKinds` is not referenced.
+    /// Instead, we refer to `ParameterKinds<Self>`, which wraps this type.
+    ///
+    /// An `InternedParameterKinds` is created by `intern_parameter_kinds`
+    /// and can be converted back to its underlying data via `parameter_kinds_data`.
+    type InternedParameterKinds: Debug + Clone + Eq + Hash;
+
+    /// "Interned" representation of a list of parameter kind with universe index.  
+    /// In normal user code, `Self::InternedCanonicalVarKinds` is not referenced.
+    /// Instead, we refer to `CanonicalVarKinds<Self>`, which wraps this type.
+    ///
+    /// An `InternedCanonicalVarKinds` is created by
+    /// `intern_canonical_var_kinds` and can be converted back
+    /// to its underlying data via `canonical_var_kinds_data`.
+    type InternedCanonicalVarKinds: Debug + Clone + Eq + Hash;
+
     /// The core "id" type used for struct-ids and the like.
     type DefId: Debug + Copy + Eq + Ord + Hash;
 
@@ -263,6 +284,51 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of a parameter kinds list. 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_parameter_kinds(
+        parameter_kinds: &ParameterKinds<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
+    /// Prints the debug representation of a parameter kinds list, with angle brackets.
+    /// 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_parameter_kinds_with_angles(
+        parameter_kinds: &ParameterKinds<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
+    /// Prints the debug representation of an parameter kinds list with universe index.
+    /// 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_canonical_var_kinds(
+        canonical_var_kinds: &CanonicalVarKinds<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an goal. To get good
     /// results, this requires inspecting TLS, and is difficult to
     /// code without reference to a specific interner (and hence
@@ -493,16 +559,68 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         &self,
         clauses: &'a Self::InternedQuantifiedWhereClauses,
     ) -> &'a [QuantifiedWhereClause<Self>];
+
+    /// Create an "interned" parameter kinds from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `ParameterKinds::from` (which will ultimately call this
+    /// method).
+    fn intern_parameter_kinds(
+        &self,
+        data: impl IntoIterator<Item = ParameterKind<()>>,
+    ) -> Self::InternedParameterKinds;
+
+    /// Lookup the slice of `ParameterKind` that was interned to
+    /// create a `ParameterKinds`.
+    fn parameter_kinds_data<'a>(
+        &self,
+        parameter_kinds: &'a Self::InternedParameterKinds,
+    ) -> &'a [ParameterKind<()>];
+
+    /// Create an "interned" parameter kinds with universe index from `data`. This is not
+    /// normally invoked directly; instead, you invoke
+    /// `CanonicalVarKinds::from` (which will ultimately call this
+    /// method).
+    fn intern_canonical_var_kinds(
+        &self,
+        data: impl IntoIterator<Item = ParameterKind<UniverseIndex>>,
+    ) -> Self::InternedCanonicalVarKinds;
+
+    /// Lookup the slice of `ParameterKind` that was interned to
+    /// create a `ParameterKinds`.
+    fn canonical_var_kinds_data<'a>(
+        &self,
+        canonical_var_kinds: &'a Self::InternedCanonicalVarKinds,
+    ) -> &'a [ParameterKind<UniverseIndex>];
 }
 
 pub trait TargetInterner<I: Interner>: Interner {
     fn transfer_def_id(def_id: I::DefId) -> Self::DefId;
+
+    fn transfer_parameter_kinds(
+        parameter_kinds: I::InternedParameterKinds,
+    ) -> Self::InternedParameterKinds;
+
+    fn transfer_canonical_var_kinds(
+        parameter_kinds: I::InternedCanonicalVarKinds,
+    ) -> Self::InternedCanonicalVarKinds;
 }
 
 impl<I: Interner> TargetInterner<I> for I {
     fn transfer_def_id(def_id: I::DefId) -> Self::DefId {
         def_id
     }
+
+    fn transfer_parameter_kinds(
+        parameter_kinds: I::InternedParameterKinds,
+    ) -> Self::InternedParameterKinds {
+        parameter_kinds
+    }
+
+    fn transfer_canonical_var_kinds(
+        parameter_kinds: I::InternedCanonicalVarKinds,
+    ) -> Self::InternedCanonicalVarKinds {
+        parameter_kinds
+    }
 }
 
 /// Implemented by types that have an associated interner (which
@@ -550,6 +668,8 @@ mod default {
         type InternedProgramClause = ProgramClauseData<ChalkIr>;
         type InternedProgramClauses = Vec<ProgramClause<ChalkIr>>;
         type InternedQuantifiedWhereClauses = Vec<QuantifiedWhereClause<ChalkIr>>;
+        type InternedParameterKinds = Vec<ParameterKind<()>>;
+        type InternedCanonicalVarKinds = Vec<ParameterKind<UniverseIndex>>;
         type DefId = RawId;
         type Identifier = Identifier;
 
@@ -621,6 +741,33 @@ mod default {
             tls::with_current_program(|prog| Some(prog?.debug_parameter(parameter, fmt)))
         }
 
+        fn debug_parameter_kinds(
+            parameter_kinds: &ParameterKinds<Self>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| {
+                Some(prog?.debug_parameter_kinds(parameter_kinds, fmt))
+            })
+        }
+
+        fn debug_parameter_kinds_with_angles(
+            parameter_kinds: &ParameterKinds<Self>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| {
+                Some(prog?.debug_parameter_kinds_with_angles(parameter_kinds, fmt))
+            })
+        }
+
+        fn debug_canonical_var_kinds(
+            canonical_var_kinds: &CanonicalVarKinds<Self>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| {
+                Some(prog?.debug_canonical_var_kinds(canonical_var_kinds, fmt))
+            })
+        }
+
         fn debug_goal(goal: &Goal<ChalkIr>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result> {
             tls::with_current_program(|prog| Some(prog?.debug_goal(goal, fmt)))
         }
@@ -786,6 +933,30 @@ mod default {
         ) -> &'a [QuantifiedWhereClause<Self>] {
             clauses
         }
+        fn intern_parameter_kinds(
+            &self,
+            data: impl IntoIterator<Item = ParameterKind<()>>,
+        ) -> Self::InternedParameterKinds {
+            data.into_iter().collect()
+        }
+        fn parameter_kinds_data<'a>(
+            &self,
+            parameter_kinds: &'a Self::InternedParameterKinds,
+        ) -> &'a [ParameterKind<()>] {
+            parameter_kinds
+        }
+        fn intern_canonical_var_kinds(
+            &self,
+            data: impl IntoIterator<Item = ParameterKind<UniverseIndex>>,
+        ) -> Self::InternedCanonicalVarKinds {
+            data.into_iter().collect()
+        }
+        fn canonical_var_kinds_data<'a>(
+            &self,
+            canonical_var_kinds: &'a Self::InternedCanonicalVarKinds,
+        ) -> &'a [ParameterKind<UniverseIndex>] {
+            canonical_var_kinds
+        }
     }
 
     impl HasInterner for ChalkIr {
@@ -826,6 +997,10 @@ where
     type Interner = I;
 }
 
+impl<'a, T: HasInterner> HasInterner for std::slice::Iter<'a, T> {
+    type Interner = T::Interner;
+}
+
 impl<C: HasInterner + Context> HasInterner for ExClause<C> {
     type Interner = <C as HasInterner>::Interner;
 }

chalk-ir/src/lib.rs

@@ -1193,18 +1193,18 @@ impl<I: Interner> HasInterner for AliasEq<I> {
 ///
 /// (IOW, we use deBruijn indices, where binders are introduced in reverse order
 /// of `self.binders`.)
-#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub struct Binders<T> {
-    pub binders: Vec<ParameterKind<()>>,
+#[derive(Clone, PartialEq, Eq, Hash)]
+pub struct Binders<T: HasInterner> {
+    pub binders: ParameterKinds<T::Interner>,
     value: T,
 }
 
 impl<T: HasInterner> HasInterner for Binders<T> {
     type Interner = T::Interner;
 }
 
-impl<T> Binders<T> {
-    pub fn new(binders: Vec<ParameterKind<()>>, value: T) -> Self {
+impl<T: HasInterner> Binders<T> {
+    pub fn new(binders: ParameterKinds<T::Interner>, value: T) -> Self {
         Self { binders, value }
     }
 
@@ -1236,6 +1236,7 @@ impl<T> Binders<T> {
     pub fn map<U, OP>(self, op: OP) -> Binders<U>
     where
         OP: FnOnce(T) -> U,
+        U: HasInterner<Interner = T::Interner>,
     {
         let value = op(self.value);
         Binders {
@@ -1247,6 +1248,7 @@ impl<T> Binders<T> {
     pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders<U>
     where
         OP: FnOnce(&'a T) -> U,
+        U: HasInterner<Interner = T::Interner>,
     {
         self.as_ref().map(op)
     }
@@ -1257,26 +1259,23 @@ impl<T> Binders<T> {
     /// from the closure to account for the binder that will be added.
     ///
     /// XXX FIXME -- this is potentially a pretty footgun-y function.
-    pub fn with_fresh_type_var<I>(interner: &I, op: impl FnOnce(Ty<I>) -> T) -> Binders<T>
-    where
-        I: Interner,
-    {
+    pub fn with_fresh_type_var(
+        interner: &T::Interner,
+        op: impl FnOnce(Ty<T::Interner>) -> T,
+    ) -> Binders<T> {
         // The new variable is at the front and everything afterwards is shifted up by 1
-        let new_var =
-            TyData::<I>::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
+        let new_var = TyData::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
         let value = op(new_var);
-        Binders {
-            binders: iter::once(ParameterKind::Ty(())).collect(),
-            value,
-        }
+        let binders = ParameterKinds::from(interner, iter::once(ParameterKind::Ty(())));
+        Binders { binders, value }
     }
 
-    pub fn len(&self) -> usize {
-        self.binders.len()
+    pub fn len(&self, interner: &T::Interner) -> usize {
+        self.binders.len(interner)
     }
 }
 
-impl<T> From<Binders<T>> for (Vec<ParameterKind<()>>, T) {
+impl<T: HasInterner> From<Binders<T>> for (ParameterKinds<T::Interner>, T) {
     fn from(binders: Binders<T>) -> Self {
         (binders.binders, binders.value)
     }
@@ -1297,7 +1296,7 @@ where
         parameters: &(impl AsParameters<I> + ?Sized),
     ) -> T::Result {
         let parameters = parameters.as_parameters(interner);
-        assert_eq!(self.binders.len(), parameters.len());
+        assert_eq!(self.binders.len(interner), parameters.len());
         Subst::apply(interner, parameters, &self.value)
     }
 }
@@ -1308,6 +1307,7 @@ impl<'a, V> IntoIterator for &'a Binders<V>
 where
     V: HasInterner,
     &'a V: IntoIterator,
+    <&'a V as IntoIterator>::Item: HasInterner<Interner = V::Interner>,
 {
     type Item = Binders<<&'a V as IntoIterator>::Item>;
     type IntoIter = BindersIntoIterator<&'a V>;
@@ -1319,8 +1319,12 @@ where
 
 /// Allows iterating over a Binders<Vec<T>>, for instance.
 /// Each element will include the same set of parameter bounds.
-impl<V: IntoIterator> IntoIterator for Binders<V> {
-    type Item = Binders<<V as IntoIterator>::Item>;
+impl<V, U> IntoIterator for Binders<V>
+where
+    V: HasInterner + IntoIterator<Item = U>,
+    U: HasInterner<Interner = V::Interner>,
+{
+    type Item = Binders<U>;
     type IntoIter = BindersIntoIterator<V>;
 
     fn into_iter(self) -> Self::IntoIter {
@@ -1331,18 +1335,21 @@ impl<V: IntoIterator> IntoIterator for Binders<V> {
     }
 }
 
-pub struct BindersIntoIterator<V: IntoIterator> {
+pub struct BindersIntoIterator<V: HasInterner + IntoIterator> {
     iter: <V as IntoIterator>::IntoIter,
-    binders: Vec<ParameterKind<()>>,
+    binders: ParameterKinds<V::Interner>,
 }
 
-impl<V: IntoIterator> Iterator for BindersIntoIterator<V> {
+impl<V> Iterator for BindersIntoIterator<V>
+where
+    V: HasInterner + IntoIterator,
+    <V as IntoIterator>::Item: HasInterner<Interner = V::Interner>,
+{
     type Item = Binders<<V as IntoIterator>::Item>;
     fn next(&mut self) -> Option<Self::Item> {
-        self.iter.next().map(|v| Binders {
-            binders: self.binders.clone(),
-            value: v,
-        })
+        self.iter
+            .next()
+            .map(|v| Binders::new(self.binders.clone(), v))
     }
 }
 
@@ -1490,21 +1497,118 @@ impl<I: Interner> ProgramClauses<I> {
     }
 }
 
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
+pub struct ParameterKinds<I: Interner> {
+    interned: I::InternedParameterKinds,
+}
+
+impl<I: Interner> ParameterKinds<I> {
+    pub fn new(interner: &I) -> Self {
+        Self::from(interner, None::<ParameterKind<()>>)
+    }
+
+    pub fn interned(&self) -> &I::InternedParameterKinds {
+        &self.interned
+    }
+
+    pub fn from(
+        interner: &I,
+        parameter_kinds: impl IntoIterator<Item = ParameterKind<()>>,
+    ) -> Self {
+        ParameterKinds {
+            interned: I::intern_parameter_kinds(interner, parameter_kinds.into_iter()),
+        }
+    }
+
+    pub fn from_fallible<E>(
+        interner: &I,
+        parameter_kinds: impl IntoIterator<Item = Result<ParameterKind<()>, E>>,
+    ) -> Result<Self, E> {
+        let parameter_kinds = parameter_kinds
+            .into_iter()
+            .collect::<Result<Vec<ParameterKind<()>>, _>>()?;
+        Ok(Self::from(interner, parameter_kinds))
+    }
+
+    pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, ParameterKind<()>> {
+        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) -> &[ParameterKind<()>] {
+        interner.parameter_kinds_data(&self.interned)
+    }
+}
+
+#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
+pub struct CanonicalVarKinds<I: Interner> {
+    interned: I::InternedCanonicalVarKinds,
+}
+
+impl<I: Interner> CanonicalVarKinds<I> {
+    pub fn new(interner: &I) -> Self {
+        Self::from(interner, None::<ParameterKind<UniverseIndex>>)
+    }
+
+    pub fn interned(&self) -> &I::InternedCanonicalVarKinds {
+        &self.interned
+    }
+
+    pub fn from(
+        interner: &I,
+        parameter_kinds: impl IntoIterator<Item = ParameterKind<UniverseIndex>>,
+    ) -> Self {
+        CanonicalVarKinds {
+            interned: I::intern_canonical_var_kinds(interner, parameter_kinds.into_iter()),
+        }
+    }
+
+    pub fn from_fallible<E>(
+        interner: &I,
+        parameter_kinds: impl IntoIterator<Item = Result<ParameterKind<UniverseIndex>, E>>,
+    ) -> Result<Self, E> {
+        let parameter_kinds = parameter_kinds
+            .into_iter()
+            .collect::<Result<Vec<ParameterKind<UniverseIndex>>, _>>()?;
+        Ok(Self::from(interner, parameter_kinds))
+    }
+
+    pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, ParameterKind<UniverseIndex>> {
+        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) -> &[ParameterKind<UniverseIndex>] {
+        interner.canonical_var_kinds_data(&self.interned)
+    }
+}
+
 /// Wraps a "canonicalized item". Items are canonicalized as follows:
 ///
 /// All unresolved existential variables are "renumbered" according to their
 /// first appearance; the kind/universe of the variable is recorded in the
 /// `binders` field.
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct Canonical<T> {
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct Canonical<T: HasInterner> {
     pub value: T,
-    pub binders: Vec<ParameterKind<UniverseIndex>>,
+    pub binders: CanonicalVarKinds<T::Interner>,
 }
 
-impl<T> HasInterner for Canonical<T>
-where
-    T: HasInterner,
-{
+impl<T: HasInterner> HasInterner for Canonical<T> {
     type Interner = T::Interner;
 }
 
@@ -1514,32 +1618,32 @@ where
 /// distinctions.
 ///
 /// To produce one of these values, use the `u_canonicalize` method.
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct UCanonical<T> {
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct UCanonical<T: HasInterner> {
     pub canonical: Canonical<T>,
     pub universes: usize,
 }
 
-impl<T> UCanonical<T> {
-    pub fn is_trivial_substitution<I: Interner>(
+impl<T: HasInterner> UCanonical<T> {
+    pub fn is_trivial_substitution(
         &self,
-        interner: &I,
-        canonical_subst: &Canonical<AnswerSubst<I>>,
+        interner: &T::Interner,
+        canonical_subst: &Canonical<AnswerSubst<T::Interner>>,
     ) -> bool {
         let subst = &canonical_subst.value.subst;
         assert_eq!(
-            self.canonical.binders.len(),
+            self.canonical.binders.len(interner),
             subst.parameters(interner).len()
         );
         subst.is_identity_subst(interner)
     }
 
-    pub fn trivial_substitution<I: Interner>(&self, interner: &I) -> Substitution<I> {
+    pub fn trivial_substitution(&self, interner: &T::Interner) -> Substitution<T::Interner> {
         let binders = &self.canonical.binders;
         Substitution::from(
             interner,
             binders
-                .iter()
+                .iter(interner)
                 .enumerate()
                 .map(|(index, pk)| {
                     let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index);
@@ -1634,16 +1738,9 @@ impl<I: Interner> Goal<I> {
         self,
         interner: &I,
         kind: QuantifierKind,
-        binders: Vec<ParameterKind<()>>,
+        binders: ParameterKinds<I>,
     ) -> Goal<I> {
-        GoalData::Quantified(
-            kind,
-            Binders {
-                value: self,
-                binders,
-            },
-        )
-        .intern(interner)
+        GoalData::Quantified(kind, Binders::new(binders, self)).intern(interner)
     }
 
     /// Takes a goal `G` and turns it into `not { G }`

chalk-ir/src/tls.rs

@@ -1,8 +1,9 @@
 use crate::interner::ChalkIr;
 use crate::{
-    debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime, OpaqueTy,
-    OpaqueTyId, Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy,
-    QuantifiedWhereClauses, StructId, Substitution, TraitId, Ty,
+    debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, CanonicalVarKinds, Goal, Goals,
+    Lifetime, OpaqueTy, OpaqueTyId, Parameter, ParameterKinds, ProgramClause,
+    ProgramClauseImplication, ProgramClauses, ProjectionTy, QuantifiedWhereClauses, StructId,
+    Substitution, TraitId, Ty,
 };
 use std::cell::RefCell;
 use std::fmt;
@@ -69,6 +70,24 @@ pub trait DebugContext {
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
 
+    fn debug_parameter_kinds(
+        &self,
+        parameter_kinds: &ParameterKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
+    fn debug_parameter_kinds_with_angles(
+        &self,
+        parameter_kinds: &ParameterKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
+    fn debug_canonical_var_kinds(
+        &self,
+        parameter_kinds: &CanonicalVarKinds<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
     fn debug_goal(
         &self,
         goal: &Goal<ChalkIr>,

chalk-ir/src/visit/binder_impls.rs

@@ -3,6 +3,7 @@
 //!
 //! The more interesting impls of `Visit` remain in the `visit` module.
 
+use crate::interner::HasInterner;
 use crate::{Binders, Canonical, DebruijnIndex, Fn, Interner, Visit, VisitResult, Visitor};
 
 impl<I: Interner> Visit<I> for Fn<I> {
@@ -23,7 +24,7 @@ impl<I: Interner> Visit<I> for Fn<I> {
 
 impl<T, I: Interner> Visit<I> for Binders<T>
 where
-    T: Visit<I>,
+    T: HasInterner + Visit<I>,
 {
     fn visit_with<'i, R: VisitResult>(
         &self,
@@ -37,10 +38,10 @@ where
     }
 }
 
-impl<T, I> Visit<I> for Canonical<T>
+impl<I, T> Visit<I> for Canonical<T>
 where
-    T: Visit<I>,
     I: Interner,
+    T: HasInterner<Interner = I> + Visit<I>,
 {
     fn visit_with<'i, R: VisitResult>(
         &self,

chalk-ir/src/zip.rs

@@ -31,7 +31,7 @@ pub trait Zipper<'i, I: Interner> {
     /// Zips two values appearing beneath binders.
     fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
     where
-        T: Zip<I> + Fold<I, I, Result = T>;
+        T: HasInterner<Interner = I> + Zip<I> + Fold<I, I, Result = T>;
 
     /// Retreives the interner from the underlying zipper object
     fn interner(&self) -> &'i I;
@@ -52,7 +52,7 @@ where
 
     fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
     where
-        T: Zip<I> + Fold<I, I, Result = T>,
+        T: HasInterner<Interner = I> + Zip<I> + Fold<I, I, Result = T>,
     {
         (**self).zip_binders(a, b)
     }
@@ -166,7 +166,9 @@ impl<I: Interner> Zip<I> for Lifetime<I> {
     }
 }
 
-impl<I: Interner, T: Zip<I> + Fold<I, I, Result = T>> Zip<I> for Binders<T> {
+impl<I: Interner, T: HasInterner<Interner = I> + Zip<I> + Fold<I, I, Result = T>> Zip<I>
+    for Binders<T>
+{
     fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
     where
         I: 'i,

chalk-rust-ir/src/lib.rs

@@ -72,7 +72,7 @@ pub struct DefaultImplDatum<I: Interner> {
     pub binders: Binders<DefaultImplDatumBound<I>>,
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)]
 pub struct DefaultImplDatumBound<I: Interner> {
     pub trait_ref: TraitRef<I>,
     pub accessible_tys: Vec<Ty<I>>,
@@ -169,7 +169,7 @@ impl<I: Interner> TraitDatum<I> {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)]
 pub struct TraitDatumBound<I: Interner> {
     /// Where clauses defined on the trait:
     ///
@@ -429,7 +429,10 @@ impl<I: Interner> AssociatedTyDatum<I> {
         // scope for this associated type:
         let substitution = Substitution::from(
             interner,
-            binders.iter().zip(0..).map(|p| p.to_parameter(interner)),
+            binders
+                .iter(interner)
+                .zip(0..)
+                .map(|p| p.to_parameter(interner)),
         );
 
         // The self type will be `<P0 as Foo<P1..Pn>>::Item<Pn..Pm>` etc

chalk-solve/src/clauses.rs

@@ -58,12 +58,16 @@ pub fn push_auto_trait_impls<I: Interner>(
     );
 
     let struct_datum = &builder.db.struct_datum(struct_id);
+    let interner = builder.interner();
 
     // Must be an auto trait.
     assert!(builder.db.trait_datum(auto_trait_id).is_auto_trait());
 
     // Auto traits never have generic parameters of their own (apart from `Self`).
-    assert_eq!(builder.db.trait_datum(auto_trait_id).binders.len(), 1);
+    assert_eq!(
+        builder.db.trait_datum(auto_trait_id).binders.len(interner),
+        1
+    );
 
     // If there is a `impl AutoTrait for Foo<..>` or `impl !AutoTrait
     // for Foo<..>`, where `Foo` is the struct we're looking at, then
@@ -74,7 +78,6 @@ pub fn push_auto_trait_impls<I: Interner>(
     }
 
     let binders = struct_datum.binders.map_ref(|b| &b.fields);
-    let interner = builder.interner();
     builder.push_binders(&binders, |builder, fields| {
         let self_ty: Ty<_> = ApplicationTy {
             name: struct_id.cast(interner),

chalk-solve/src/clauses/builder.rs

@@ -81,8 +81,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
                 .push(ProgramClauseData::Implies(clause).intern(interner));
         } else {
             self.clauses.push(
-                ProgramClauseData::ForAll(Binders::new(self.binders.clone(), clause))
-                    .intern(interner),
+                ProgramClauseData::ForAll(Binders::new(
+                    ParameterKinds::from(interner, self.binders.clone()),
+                    clause,
+                ))
+                .intern(interner),
             );
         }
 
@@ -119,11 +122,11 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
 
         let old_len = self.binders.len();
         let interner = self.interner();
-        self.binders.extend(binders.binders.clone());
+        self.binders.extend(binders.binders.iter(interner).cloned());
         self.parameters.extend(
             binders
                 .binders
-                .iter()
+                .iter(interner)
                 .zip(old_len..)
                 .map(|p| p.to_parameter(interner)),
         );
@@ -144,7 +147,10 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
     #[allow(dead_code)]
     pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) {
         let interner = self.interner();
-        let binders = Binders::new(vec![ParameterKind::Ty(())], PhantomData::<I>);
+        let binders = Binders::new(
+            ParameterKinds::from(interner, vec![ParameterKind::Ty(())]),
+            PhantomData::<I>,
+        );
         self.push_binders(&binders, |this, PhantomData| {
             let ty = this
                 .placeholders_in_scope()

chalk-solve/src/clauses/generalize.rs

@@ -9,8 +9,9 @@
 use chalk_engine::fallible::Fallible;
 use chalk_ir::{
     fold::{Fold, Folder},
-    interner::Interner,
-    Binders, BoundVar, DebruijnIndex, Lifetime, LifetimeData, ParameterKind, Ty, TyData,
+    interner::{HasInterner, Interner},
+    Binders, BoundVar, DebruijnIndex, Lifetime, LifetimeData, ParameterKind, ParameterKinds, Ty,
+    TyData,
 };
 use std::collections::HashMap;
 
@@ -21,7 +22,11 @@ pub struct Generalize<'i, I: Interner> {
 }
 
 impl<I: Interner> Generalize<'_, I> {
-    pub fn apply<T: Fold<I, I>>(interner: &I, value: &T) -> Binders<T::Result> {
+    pub fn apply<T>(interner: &I, value: &T) -> Binders<T::Result>
+    where
+        T: HasInterner<Interner = I> + Fold<I, I>,
+        T::Result: HasInterner<Interner = I>,
+    {
         let mut generalize = Generalize {
             binders: Vec::new(),
             mapping: HashMap::new(),
@@ -30,7 +35,7 @@ impl<I: Interner> Generalize<'_, I> {
         let value = value
             .fold_with(&mut generalize, DebruijnIndex::INNERMOST)
             .unwrap();
-        Binders::new(generalize.binders, value)
+        Binders::new(ParameterKinds::from(interner, generalize.binders), value)
     }
 }
 

chalk-solve/src/goal_builder.rs

@@ -137,7 +137,7 @@ impl<'i, I: Interner> GoalBuilder<'i, I> {
             interner,
             binders
                 .binders
-                .iter()
+                .iter(interner)
                 .zip(0..)
                 .map(|p| p.to_parameter(interner)),
         );

chalk-solve/src/infer.rs

@@ -1,4 +1,4 @@
-use chalk_ir::interner::Interner;
+use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::*;
 use chalk_ir::{cast::Cast, fold::Fold};
 
@@ -52,7 +52,7 @@ impl<I: Interner> InferenceTable<I> {
         canonical: &Canonical<T>,
     ) -> (Self, Substitution<I>, T)
     where
-        T: Fold<I, Result = T> + Clone,
+        T: HasInterner<Interner = I> + Fold<I, Result = T> + Clone,
     {
         let mut table = InferenceTable::new();
 
@@ -61,7 +61,7 @@ impl<I: Interner> InferenceTable<I> {
             table.new_universe();
         }
 
-        let subst = table.fresh_subst(interner, &canonical.binders);
+        let subst = table.fresh_subst(interner, canonical.binders.as_slice(interner));
         let value = subst.apply(&canonical.value, interner);
         // let value = canonical.value.fold_with(&mut &subst, 0).unwrap();
 

chalk-solve/src/infer/canonicalize.rs

@@ -74,14 +74,19 @@ struct Canonicalizer<'q, I: Interner> {
 }
 
 impl<'q, I: Interner> Canonicalizer<'q, I> {
-    fn into_binders(self) -> Vec<ParameterKind<UniverseIndex>> {
+    fn into_binders(self) -> CanonicalVarKinds<I> {
         let Canonicalizer {
-            table, free_vars, ..
+            table,
+            free_vars,
+            interner,
+            ..
         } = self;
-        free_vars
-            .into_iter()
-            .map(|p_v| p_v.map(|v| table.universe_of_unbound_var(v)))
-            .collect()
+        CanonicalVarKinds::from(
+            interner,
+            free_vars
+                .into_iter()
+                .map(|p_v| p_v.map(|v| table.universe_of_unbound_var(v))),
+        )
     }
 
     fn add(&mut self, free_var: ParameterEnaVariable<I>) -> usize {

chalk-solve/src/infer/instantiate.rs

@@ -1,4 +1,5 @@
 use chalk_ir::fold::*;
+use chalk_ir::interner::HasInterner;
 use std::fmt::Debug;
 
 use super::*;
@@ -30,9 +31,9 @@ impl<I: Interner> InferenceTable<I> {
         bound: &Canonical<T>,
     ) -> T::Result
     where
-        T: Fold<I> + Debug,
+        T: HasInterner<Interner = I> + Fold<I> + Debug,
     {
-        let subst = self.fresh_subst(interner, &bound.binders);
+        let subst = self.fresh_subst(interner, &bound.binders.as_slice(interner));
         subst.apply(&bound.value, interner)
     }
 
@@ -61,28 +62,28 @@ impl<I: Interner> InferenceTable<I> {
     }
 
     /// Variant on `instantiate_in` that takes a `Binders<T>`.
-    pub(crate) fn instantiate_binders_existentially<T>(
+    pub(crate) fn instantiate_binders_existentially<'a, T>(
         &mut self,
-        interner: &I,
-        arg: impl IntoBindersAndValue<Value = T>,
+        interner: &'a I,
+        arg: impl IntoBindersAndValue<'a, I, Value = T>,
     ) -> T::Result
     where
         T: Fold<I>,
     {
-        let (binders, value) = arg.into_binders_and_value();
+        let (binders, value) = arg.into_binders_and_value(interner);
         let max_universe = self.max_universe;
         self.instantiate_in(interner, max_universe, binders, &value)
     }
 
-    pub(crate) fn instantiate_binders_universally<T>(
+    pub(crate) fn instantiate_binders_universally<'a, T>(
         &mut self,
-        interner: &I,
-        arg: impl IntoBindersAndValue<Value = T>,
+        interner: &'a I,
+        arg: impl IntoBindersAndValue<'a, I, Value = T>,
     ) -> T::Result
     where
         T: Fold<I>,
     {
-        let (binders, value) = arg.into_binders_and_value();
+        let (binders, value) = arg.into_binders_and_value(interner);
         let ui = self.new_universe();
         let parameters: Vec<_> = binders
             .into_iter()
@@ -102,30 +103,34 @@ impl<I: Interner> InferenceTable<I> {
     }
 }
 
-pub(crate) trait IntoBindersAndValue {
+pub(crate) trait IntoBindersAndValue<'a, I: Interner> {
     type Binders: IntoIterator<Item = ParameterKind<()>>;
     type Value;
 
-    fn into_binders_and_value(self) -> (Self::Binders, Self::Value);
+    fn into_binders_and_value(self, interner: &'a I) -> (Self::Binders, Self::Value);
 }
 
-impl<'a, T> IntoBindersAndValue for &'a Binders<T> {
+impl<'a, I, T> IntoBindersAndValue<'a, I> for &'a Binders<T>
+where
+    I: Interner,
+    T: HasInterner<Interner = I>,
+{
     type Binders = std::iter::Cloned<std::slice::Iter<'a, ParameterKind<()>>>;
     type Value = &'a T;
 
-    fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
-        (self.binders.iter().cloned(), self.skip_binders())
+    fn into_binders_and_value(self, interner: &'a I) -> (Self::Binders, Self::Value) {
+        (self.binders.iter(interner).cloned(), self.skip_binders())
     }
 }
 
-impl<'a, I> IntoBindersAndValue for &'a Fn<I>
+impl<'a, I> IntoBindersAndValue<'a, I> for &'a Fn<I>
 where
     I: Interner,
 {
     type Binders = std::iter::Map<std::ops::Range<usize>, fn(usize) -> chalk_ir::ParameterKind<()>>;
     type Value = &'a Substitution<I>;
 
-    fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
+    fn into_binders_and_value(self, _interner: &'a I) -> (Self::Binders, Self::Value) {
         fn make_lifetime(_: usize) -> ParameterKind<()> {
             ParameterKind::Lifetime(())
         }
@@ -135,11 +140,11 @@ where
     }
 }
 
-impl<'a, T> IntoBindersAndValue for (&'a Vec<ParameterKind<()>>, &'a T) {
+impl<'a, T, I: Interner> IntoBindersAndValue<'a, I> for (&'a Vec<ParameterKind<()>>, &'a T) {
     type Binders = std::iter::Cloned<std::slice::Iter<'a, ParameterKind<()>>>;
     type Value = &'a T;
 
-    fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
+    fn into_binders_and_value(self, _interner: &'a I) -> (Self::Binders, Self::Value) {
         (self.0.iter().cloned(), &self.1)
     }
 }

chalk-solve/src/infer/invert.rs

@@ -88,7 +88,7 @@ impl<I: Interner> InferenceTable<I> {
         }
 
         // If this contains free universal variables, replace them with existentials.
-        assert!(quantified.binders.is_empty());
+        assert!(quantified.binders.is_empty(interner));
         let inverted = quantified
             .value
             .fold_with(&mut Inverter::new(interner, self), DebruijnIndex::INNERMOST)

chalk-solve/src/infer/test.rs

@@ -181,11 +181,14 @@ fn quantify_simple() {
             .quantified,
         Canonical {
             value: ty!(apply (item 0) (bound 0) (bound 1) (bound 2)),
-            binders: vec![
-                ParameterKind::Ty(U2),
-                ParameterKind::Ty(U1),
-                ParameterKind::Ty(U0),
-            ],
+            binders: CanonicalVarKinds::from(
+                interner,
+                vec![
+                    ParameterKind::Ty(U2),
+                    ParameterKind::Ty(U1),
+                    ParameterKind::Ty(U0),
+                ]
+            ),
         }
     );
 }
@@ -219,11 +222,14 @@ fn quantify_bound() {
             .quantified,
         Canonical {
             value: ty!(apply (item 0) (apply (item 1) (bound 0) (bound 1)) (bound 2) (bound 0) (bound 1)),
-            binders: vec![
-                ParameterKind::Ty(U1),
-                ParameterKind::Ty(U0),
-                ParameterKind::Ty(U2),
-            ],
+            binders: CanonicalVarKinds::from(
+                interner,
+                vec![
+                    ParameterKind::Ty(U1),
+                    ParameterKind::Ty(U0),
+                    ParameterKind::Ty(U2),
+                ]
+            ),
         }
     );
 }
@@ -260,7 +266,10 @@ fn quantify_ty_under_binder() {
             .quantified,
         Canonical {
             value: ty!(function 3 (apply (item 0) (bound 1) (bound 1 0) (bound 1 0) (lifetime (bound 1 1)))),
-            binders: vec![ParameterKind::Ty(U0), ParameterKind::Lifetime(U0)],
+            binders: CanonicalVarKinds::from(
+                interner,
+                vec![ParameterKind::Ty(U0), ParameterKind::Lifetime(U0)]
+            ),
         }
     );
 }

chalk-solve/src/infer/ucanonicalize.rs

@@ -1,17 +1,21 @@
 use chalk_engine::fallible::*;
 use chalk_ir::fold::{Fold, Folder};
-use chalk_ir::interner::Interner;
+use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::visit::{Visit, Visitor};
 use chalk_ir::*;
 
 use super::InferenceTable;
 
 impl<I: Interner> InferenceTable<I> {
-    pub(crate) fn u_canonicalize<T: Fold<I> + Visit<I>>(
+    pub(crate) fn u_canonicalize<T>(
         &mut self,
         interner: &I,
         value0: &Canonical<T>,
-    ) -> UCanonicalized<T::Result> {
+    ) -> UCanonicalized<T::Result>
+    where
+        T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
+        T::Result: HasInterner<Interner = I>,
+    {
         debug!("u_canonicalize({:#?})", value0);
 
         // First, find all the universes that appear in `value`.
@@ -37,11 +41,13 @@ impl<I: Interner> InferenceTable<I> {
                 DebruijnIndex::INNERMOST,
             )
             .unwrap();
-        let binders = value0
-            .binders
-            .iter()
-            .map(|pk| pk.map(|ui| universes.map_universe_to_canonical(ui)))
-            .collect();
+        let binders = CanonicalVarKinds::from(
+            interner,
+            value0
+                .binders
+                .iter(interner)
+                .map(|pk| pk.map(|ui| universes.map_universe_to_canonical(ui))),
+        );
 
         UCanonicalized {
             quantified: UCanonical {
@@ -57,7 +63,7 @@ impl<I: Interner> InferenceTable<I> {
 }
 
 #[derive(Debug)]
-pub(crate) struct UCanonicalized<T> {
+pub(crate) struct UCanonicalized<T: HasInterner> {
     /// The canonicalized result.
     pub(crate) quantified: UCanonical<T>,
 

chalk-solve/src/infer/unify.rs

@@ -4,7 +4,7 @@ use crate::infer::instantiate::IntoBindersAndValue;
 use chalk_engine::fallible::*;
 use chalk_ir::cast::Cast;
 use chalk_ir::fold::{Fold, Folder};
-use chalk_ir::interner::Interner;
+use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::zip::{Zip, Zipper};
 use std::fmt::Debug;
 
@@ -185,14 +185,15 @@ impl<'t, I: Interner> Unifier<'t, I> {
         }
     }
 
-    fn unify_binders<T, R>(
+    fn unify_binders<'a, T, R>(
         &mut self,
-        a: impl IntoBindersAndValue<Value = T> + Copy + Debug,
-        b: impl IntoBindersAndValue<Value = T> + Copy + Debug,
+        a: impl IntoBindersAndValue<'a, I, Value = T> + Copy + Debug,
+        b: impl IntoBindersAndValue<'a, I, Value = T> + Copy + Debug,
     ) -> Fallible<()>
     where
         T: Fold<I, Result = R>,
         R: Zip<I> + Fold<I, Result = R>,
+        't: 'a,
     {
         // for<'a...> T == for<'b...> U
         //
@@ -352,7 +353,7 @@ impl<'i, I: Interner> Zipper<'i, I> for Unifier<'i, I> {
 
     fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
     where
-        T: Zip<I> + Fold<I, Result = T>,
+        T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
     {
         // The binders that appear in types (apart from quantified types, which are
         // handled in `unify_ty`) appear as part of `dyn Trait` and `impl Trait` types.

chalk-solve/src/recursive.rs

@@ -366,7 +366,10 @@ impl<'me, I: Interner> Solver<'me, I> {
                 ProgramClauseData::Implies(implication) => {
                     let res = self.solve_via_implication(
                         canonical_goal,
-                        &Binders::new(vec![], implication.clone()),
+                        &Binders::new(
+                            ParameterKinds::from(self.program.interner(), vec![]),
+                            implication.clone(),
+                        ),
                         minimums,
                     );
                     if let (Ok(solution), priority) = res {
@@ -521,10 +524,10 @@ fn combine_with_priorities<I: Interner>(
                 );
                 (higher, ClausePriority::High)
             } else {
-                (higher.combine(lower), ClausePriority::High)
+                (higher.combine(lower, interner), ClausePriority::High)
             }
         }
-        (_, _, a, b) => (a.combine(b), prio_a),
+        (_, _, a, b) => (a.combine(b, interner), prio_a),
     }
 }
 

chalk-solve/src/recursive/fulfill.rs

@@ -108,7 +108,7 @@ impl<'s, 'db, I: Interner> Fulfill<'s, 'db, I> {
     /// Wraps `InferenceTable::instantiate_in`
     pub(crate) fn instantiate_binders_existentially<T>(
         &mut self,
-        arg: impl IntoBindersAndValue<Value = T>,
+        arg: impl IntoBindersAndValue<'s, I, Value = T>,
     ) -> T::Result
     where
         T: Fold<I, I>,

chalk-solve/src/solve.rs

@@ -69,14 +69,18 @@ impl<I: Interner> Solution<I> {
     //    Clone`.
     //
     // But you get the idea.
-    pub(crate) fn combine(self, other: Solution<I>) -> Solution<I> {
+    pub(crate) fn combine(self, other: Solution<I>, interner: &I) -> Solution<I> {
         use self::Guidance::*;
 
         if self == other {
             return self;
         }
 
-        debug!("combine {} with {}", self, other);
+        debug!(
+            "combine {} with {}",
+            self.display(interner),
+            other.display(interner)
+        );
 
         // Otherwise, always downgrade to Ambig:
 
@@ -138,18 +142,35 @@ impl<I: Interner> Solution<I> {
             _ => false,
         }
     }
+
+    pub fn display<'a>(&'a self, interner: &'a I) -> SolutionDisplay<'a, I> {
+        SolutionDisplay {
+            solution: self,
+            interner,
+        }
+    }
+}
+
+pub struct SolutionDisplay<'a, I: Interner> {
+    solution: &'a Solution<I>,
+    interner: &'a I,
 }
 
-impl<I: Interner> fmt::Display for Solution<I> {
+impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> {
-        match self {
-            Solution::Unique(constrained) => write!(f, "Unique; {}", constrained,),
-            Solution::Ambig(Guidance::Definite(subst)) => {
-                write!(f, "Ambiguous; definite substitution {}", subst)
-            }
-            Solution::Ambig(Guidance::Suggested(subst)) => {
-                write!(f, "Ambiguous; suggested substitution {}", subst)
-            }
+        let SolutionDisplay { solution, interner } = self;
+        match solution {
+            Solution::Unique(constrained) => write!(f, "Unique; {}", constrained.display(interner)),
+            Solution::Ambig(Guidance::Definite(subst)) => write!(
+                f,
+                "Ambiguous; definite substitution {}",
+                subst.display(interner)
+            ),
+            Solution::Ambig(Guidance::Suggested(subst)) => write!(
+                f,
+                "Ambiguous; suggested substitution {}",
+                subst.display(interner)
+            ),
             Solution::Ambig(Guidance::Unknown) => write!(f, "Ambiguous; no inference guidance"),
         }
     }

chalk-solve/src/solve/slg/aggregate.rs

@@ -146,7 +146,7 @@ fn merge_into_guidance<I: Interner>(
             // We have two values for some variable X that
             // appears in the root goal. Find out the universe
             // of X.
-            let universe = root_goal.binders[index].into_inner();
+            let universe = root_goal.binders.as_slice(interner)[index].into_inner();
 
             let ty = match value.data(interner) {
                 ParameterKind::Ty(ty) => ty,

chalk-solve/src/solve/slg/resolvent.rs

@@ -3,7 +3,7 @@ use crate::solve::slg::{self, SlgContext, TruncatingInferenceTable};
 use chalk_engine::fallible::Fallible;
 use chalk_ir::fold::shift::Shift;
 use chalk_ir::fold::Fold;
-use chalk_ir::interner::Interner;
+use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::zip::{Zip, Zipper};
 use chalk_ir::*;
 
@@ -483,7 +483,7 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
 
     fn zip_binders<T>(&mut self, answer: &Binders<T>, pending: &Binders<T>) -> Fallible<()>
     where
-        T: Zip<I> + Fold<I, Result = T>,
+        T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
     {
         self.outer_binder.shift_in();
         Zip::zip_with(self, answer.skip_binders(), pending.skip_binders())?;

chalk-solve/src/split.rs

@@ -29,7 +29,7 @@ pub trait Split<I: Interner>: RustIrDatabase<I> {
         let parameters = substitution.parameters(interner);
         let associated_ty_data = &self.associated_ty_data(associated_ty_id);
         let trait_datum = &self.trait_datum(associated_ty_data.trait_id);
-        let trait_num_params = trait_datum.binders.len();
+        let trait_num_params = trait_datum.binders.len(interner);
         let split_point = parameters.len() - trait_num_params;
         let (other_params, trait_params) = parameters.split_at(split_point);
         (associated_ty_data.clone(), trait_params, other_params)
@@ -86,8 +86,9 @@ pub trait Split<I: Interner>: RustIrDatabase<I> {
         parameters: &'p [P],
         associated_ty_value: &AssociatedTyValue<I>,
     ) -> (&'p [P], &'p [P]) {
+        let interner = self.interner();
         let impl_datum = self.impl_datum(associated_ty_value.impl_id);
-        let impl_params_len = impl_datum.binders.len();
+        let impl_params_len = impl_datum.binders.len(interner);
         assert!(parameters.len() >= impl_params_len);
 
         // the impl parameters are a suffix

src/main.rs

@@ -8,6 +8,7 @@ use std::process::exit;
 use chalk_integration::db::ChalkDatabase;
 use chalk_integration::lowering::*;
 use chalk_integration::query::LoweringDatabase;
+use chalk_ir::interner::ChalkIr;
 use chalk_solve::ext::*;
 use chalk_solve::{RustIrDatabase, SolverChoice};
 use docopt::Docopt;
@@ -67,7 +68,7 @@ impl LoadedProgram {
         let peeled_goal = goal.into_peeled_goal(self.db.interner());
         if multiple_answers {
             if self.db.solve_multiple(&peeled_goal, |v, has_next| {
-                println!("{}\n", v);
+                println!("{}\n", v.as_ref().map(|v| v.display(&ChalkIr)));
                 if has_next {
                     if let Some(ref mut rl) = rl {
                         loop {
@@ -94,7 +95,7 @@ impl LoadedProgram {
             }
         } else {
             match self.db.solve(&peeled_goal) {
-                Some(v) => println!("{}\n", v),
+                Some(v) => println!("{}\n", v.display(&ChalkIr)),
                 None => println!("No possible solution.\n"),
             }
         }

tests/test/mod.rs

@@ -26,7 +26,7 @@ fn assert_result(mut result: Option<Solution<ChalkIr>>, expected: &str) {
         _ => {}
     }
     let result = match result {
-        Some(v) => format!("{}", v),
+        Some(v) => format!("{}", v.display(&ChalkIr)),
         None => format!("No possible solution"),
     };
 
@@ -262,7 +262,13 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) {
                         db.solve_multiple(&peeled_goal, |result, next_result| {
                             match expected.next() {
                                 Some(expected) => {
-                                    assert_same(&format!("{}", &result), expected);
+                                    assert_same(
+                                        &format!(
+                                            "{}",
+                                            result.as_ref().map(|v| v.display(&ChalkIr))
+                                        ),
+                                        expected,
+                                    );
                                 }
                                 None => {
                                     assert!(!next_result, "Unexpected next solution");
@@ -280,7 +286,10 @@ fn solve_goal(program_text: &str, goals: Vec<(&str, SolverChoice, TestGoal)>) {
                     let mut expected = expected.into_iter();
                     db.solve_multiple(&peeled_goal, |result, next_result| match expected.next() {
                         Some(solution) => {
-                            assert_same(&format!("{}", &result), solution);
+                            assert_same(
+                                &format!("{}", result.as_ref().map(|v| v.display(&ChalkIr))),
+                                solution,
+                            );
                             if !next_result {
                                 assert!(expected.next().is_none(), "Not enough solutions found");
                             }