Universal indexing: change 1'0 to 1_0, leverage it in unify_forall_apply

Author: leoyvens

chalk-ir/src/debug.rs

@@ -60,7 +60,7 @@ impl Debug for Lifetime {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match self {
             Lifetime::Var(depth) => write!(fmt, "'?{}", depth),
-            Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}'{}", ui.counter, idx),
+            Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}_{}", ui.counter, idx),
         }
     }
 }

chalk-solve/src/infer/test.rs

@@ -294,6 +294,6 @@ fn lifetime_constraint_indirect() {
     assert_eq!(constraints.len(), 1);
     assert_eq!(
         format!("{:?}", constraints[0]),
-        "InEnvironment { environment: Env([]), goal: \'?2 == \'!1'0 }",
+        "InEnvironment { environment: Env([]), goal: \'?2 == \'!1_0 }",
     );
 }

chalk-solve/src/infer/unify.rs

@@ -242,10 +242,10 @@ impl<'t> Unifier<'t> {
     }
 
     fn unify_forall_apply(&mut self, ty1: &QuantifiedTy, ty2: &Ty) -> Fallible<()> {
+        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: '!1'1 == '!1'0
+                                    goal: '!1_1 == '!1_0
                                 }
                             ]
                         },

chalk-solve/src/solve/test.rs

@@ -581,7 +581,7 @@ fn normalize_gat1() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Iter<'!2'0, !1>], lifetime constraints []"
+            "Unique; substitution [?0 := Iter<'!2_0, !1>], lifetime constraints []"
         }
     }
 }
@@ -606,7 +606,7 @@ fn normalize_gat2() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Span<'!1'0, !2>], lifetime constraints []"
+            "Unique; substitution [?0 := Span<'!1_0, !2>], lifetime constraints []"
         }
 
         goal {
@@ -922,7 +922,7 @@ fn region_equality() {
         } yields {
             "Unique; substitution [],
                      lifetime constraints \
-                     [InEnvironment { environment: Env([]), goal: '!1'1 == '!1'0 }]
+                     [InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }]
                      "
         }
 
@@ -933,7 +933,7 @@ fn region_equality() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := '!1'0], lifetime constraints []"
+            "Unique; substitution [?0 := '!1_0], lifetime constraints []"
         }
     }
 }
@@ -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'0` and `!1'1`, 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: '!1'1 == '!1'0 }
+                 InEnvironment { environment: Env([]), goal: '!1_1 == '!1_0 }
              ]"
         }
     }
@@ -1185,7 +1185,7 @@ fn normalize_under_binder() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Ref<'!1'0, I32>], lifetime constraints []"
+            "Unique; substitution [?0 := Ref<'!1_0, I32>], lifetime constraints []"
         }
 
         goal {
@@ -1197,7 +1197,7 @@ fn normalize_under_binder() {
         } yields {
             "Unique; for<?U0> { \
              substitution [?0 := Ref<'?0, I32>], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \
              }"
         }
     }
@@ -1221,7 +1221,7 @@ fn unify_quantified_lifetimes() {
         } yields {
             "Unique; for<?U0> { \
              substitution [?0 := '?0], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \
              }"
         }
 
@@ -1237,8 +1237,8 @@ fn unify_quantified_lifetimes() {
             }
         } yields {
             "Unique; for<?U0> { \
-             substitution [?0 := '?0, ?1 := '!1'0], \
-             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1'0 }] \
+             substitution [?0 := '?0, ?1 := '!1_0], \
+             lifetime constraints [InEnvironment { environment: Env([]), goal: '?0 == '!1_0 }] \
              }"
         }
     }
@@ -1263,7 +1263,7 @@ fn equality_binder() {
         } yields {
             "Unique; for<?U1> { \
                  substitution [?0 := '?0], \
-                 lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '?0 }] \
+                 lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '?0 }] \
              }"
         }
     }
@@ -2394,7 +2394,7 @@ fn quantified_types() {
         } yields {
             // Lifetime constraints are unsatisfiable
             "Unique; substitution [], \
-            lifetime constraints [InEnvironment { environment: Env([]), goal: '!2'0 == '!1'0 }]"
+            lifetime constraints [InEnvironment { environment: Env([]), goal: '!2_0 == '!1_0 }]"
         }
     }
 }