Pack lifetimes from the same binder into the same universe

This changes the output of some tests, should not alter any semantics

Author: leoyvens

chalk-solve/src/infer/instantiate.rs

@@ -100,19 +100,24 @@ impl InferenceTable {
         T: Fold,
     {
         let (binders, value) = arg.split();
+        let lifetime_ui = self.new_universe();
+        let mut idx = 0;
         let parameters: Vec<_> = binders
             .iter()
             .map(|pk| {
-                let new_universe = self.new_universe();
                 match *pk {
                     ParameterKind::Lifetime(()) => {
-                        let lt = Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 });
+                        let lt = Lifetime::ForAll(UniversalIndex { ui: lifetime_ui, idx });
+                        idx += 1;
                         ParameterKind::Lifetime(lt)
                     }
-                    ParameterKind::Ty(()) => ParameterKind::Ty(Ty::Apply(ApplicationTy {
-                        name: TypeName::ForAll(new_universe),
-                        parameters: vec![],
-                    })),
+                    ParameterKind::Ty(()) => {
+                        let new_universe = self.new_universe();
+                        ParameterKind::Ty(Ty::Apply(ApplicationTy {
+                            name: TypeName::ForAll(new_universe),
+                            parameters: vec![],
+                        }))
+                    }
                 }
             })
             .collect();

chalk-solve/src/infer/unify.rs

@@ -166,19 +166,22 @@ impl<'t> Unifier<'t> {
     }
 
     fn unify_forall_tys(&mut self, ty1: &QuantifiedTy, ty2: &QuantifiedTy) -> Fallible<()> {
-        // for<'a...> T == for<'b...> U where 'a != 'b
+        // for<'a...> T == for<'b...> U
         //
         // if:
         //
         // for<'a...> exists<'b...> T == U &&
         // for<'b...> exists<'a...> T == U
+        //
+        // Here we only check for<'a...> exists<'b...> T == U,
+        // can someone smart comment why this is sufficient?
 
         debug!("unify_forall_tys({:?}, {:?})", ty1, ty2);
 
+        let ui = self.table.new_universe();
         let lifetimes1: Vec<_> = (0..ty1.num_binders)
-            .map(|_| {
-                let new_universe = self.table.new_universe();
-                Lifetime::ForAll(UniversalIndex { ui: new_universe, idx: 0 }).cast()
+            .map(|idx| {
+                Lifetime::ForAll(UniversalIndex { ui, idx }).cast()
             })
             .collect();
 

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

@@ -550,7 +550,7 @@ fn basic_region_constraint_from_positive_impl() {
                             constraints: [
                                 InEnvironment {
                                     environment: Env([]),
-                                    goal: '!2'0 == '!1'0
+                                    goal: '!1'1 == '!1'0
                                 }
                             ]
                         },

chalk-solve/src/solve/test.rs

@@ -922,7 +922,7 @@ fn region_equality() {
         } yields {
             "Unique; substitution [],
                      lifetime constraints \
-                     [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]
+                     [InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 }]
                      "
         }
 
@@ -966,12 +966,12 @@ fn forall_equality() {
             // this is because the region constraints are unsolvable.
             //
             // Note that `?0` (in universe 2) must be equal to both
-            // `!1` and `!2`, which of course it cannot be.
+            // `!1'0` and `!1'1`, which of course it cannot be.
             for<'a, 'b> Ref<'a, Ref<'b, Ref<'a, Unit>>>: Eq<
                 for<'c, 'd> Ref<'c, Ref<'d, Ref<'d, Unit>>>>
         } yields {
             "Unique; substitution [], lifetime constraints [
-                 InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }
+                 InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 }
              ]"
         }
     }