Pass interner to IntoBindersAndValue trait associated fn.

Author: crlf0710

chalk-solve/src/ext.rs

@@ -70,14 +70,12 @@ impl<I: Interner> GoalExt<I> for Goal<I> {
                 let InEnvironment { environment, goal } = env_goal;
                 match goal.data(interner) {
                     GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
-                        let subgoal =
-                            infer.instantiate_binders_universally(interner, (subgoal, interner));
+                        let subgoal = infer.instantiate_binders_universally(interner, subgoal);
                         env_goal = InEnvironment::new(&environment, subgoal);
                     }
 
                     GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
-                        let subgoal =
-                            infer.instantiate_binders_existentially(interner, (subgoal, interner));
+                        let subgoal = infer.instantiate_binders_existentially(interner, subgoal);
                         env_goal = InEnvironment::new(&environment, subgoal);
                     }
 

chalk-solve/src/infer/instantiate.rs

@@ -62,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()
@@ -103,34 +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, I, T> IntoBindersAndValue for (&'a Binders<T>, &'a I)
+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.0.binders.iter(self.1).cloned(), self.0.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(())
         }
@@ -140,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/unify.rs

@@ -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
         //
@@ -354,7 +355,6 @@ impl<'i, I: Interner> Zipper<'i, I> for Unifier<'i, I> {
     where
         T: HasInterner<Interner = I> + Zip<I> + Fold<I, Result = T>,
     {
-        let interner = self.interner();
         // 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.
         //
@@ -366,7 +366,7 @@ impl<'i, I: Interner> Zipper<'i, I> for Unifier<'i, I> {
         //
         // In both cases we can use the same `unify_binders` routine.
 
-        self.unify_binders((a, interner), (b, interner))
+        self.unify_binders(a, b)
     }
 
     fn interner(&self) -> &'i I {

chalk-solve/src/solve/slg.rs

@@ -323,17 +323,15 @@ impl<I: Interner> context::InferenceTable<SlgContext<I>> for TruncatingInference
 
 impl<I: Interner> context::UnificationOps<SlgContext<I>> for TruncatingInferenceTable<I> {
     fn instantiate_binders_universally(&mut self, interner: &I, arg: &Binders<Goal<I>>) -> Goal<I> {
-        self.infer
-            .instantiate_binders_universally(interner, (arg, interner))
+        self.infer.instantiate_binders_universally(interner, arg)
     }
 
     fn instantiate_binders_existentially(
         &mut self,
         interner: &I,
         arg: &Binders<Goal<I>>,
     ) -> Goal<I> {
-        self.infer
-            .instantiate_binders_existentially(interner, (arg, interner))
+        self.infer.instantiate_binders_existentially(interner, arg)
     }
 
     fn debug_ex_clause<'v>(

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

@@ -88,7 +88,7 @@ impl<I: Interner> context::ResolventOps<SlgContext<I>> for TruncatingInferenceTa
             ProgramClauseData::Implies(implication) => implication.clone(),
             ProgramClauseData::ForAll(implication) => self
                 .infer
-                .instantiate_binders_existentially(interner, (implication, interner)),
+                .instantiate_binders_existentially(interner, implication),
         };
         debug!("consequence = {:?}", consequence);
         debug!("conditions = {:?}", conditions);