Many lifetimes one universe

chalk-ir/src/debug.rs

@@ -30,7 +30,7 @@ impl Debug for TypeName {
     fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
         match self {
             TypeName::ItemId(id) => write!(fmt, "{:?}", id),
-            TypeName::ForAll(universe) => write!(fmt, "!{}", universe.counter),
+            TypeName::ForAll(universe) => write!(fmt, "!{}_{}", universe.ui.counter, universe.idx),
             TypeName::AssociatedType(assoc_ty) => write!(fmt, "{:?}", assoc_ty),
         }
     }
@@ -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(universe) => write!(fmt, "'!{}", universe.counter),
+            Lifetime::ForAll(UniversalIndex { ui, idx }) => write!(fmt, "'!{}_{}", ui.counter, idx),
         }
     }
 }

chalk-ir/src/fold.rs

@@ -135,12 +135,12 @@ pub trait UniversalFolder {
     ///
     /// - `universe` is the universe of the `TypeName::ForAll` that was found
     /// - `binders` is the number of binders in scope
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible<Ty>;
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible<Ty>;
 
     /// As with `fold_free_universal_ty`, but for lifetimes.
     fn fold_free_universal_lifetime(
         &mut self,
-        universe: UniverseIndex,
+        universe: UniversalIndex,
         binders: usize,
     ) -> Fallible<Lifetime>;
 }
@@ -151,13 +151,13 @@ pub trait UniversalFolder {
 pub trait IdentityUniversalFolder {}
 
 impl<T: IdentityUniversalFolder> UniversalFolder for T {
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
-        Ok(TypeName::ForAll(universe).to_ty())
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
+        Ok(universe.to_ty())
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe: UniverseIndex,
+        universe: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Lifetime> {
         Ok(universe.to_lifetime())

chalk-ir/src/lib.rs

@@ -96,21 +96,12 @@ pub enum TypeName {
     ItemId(ItemId),
 
     /// skolemized form of a type parameter like `T`
-    ForAll(UniverseIndex),
+    ForAll(UniversalIndex),
 
     /// an associated type like `Iterator::Item`; see `AssociatedType` for details
     AssociatedType(ItemId),
 }
 
-impl TypeName {
-    pub fn to_ty(self) -> Ty {
-        Ty::Apply(ApplicationTy {
-            name: self,
-            parameters: vec![],
-        })
-    }
-}
-
 /// An universe index is how a universally quantified parameter is
 /// represented when it's binder is moved into the environment.
 /// An example chain of transformations would be:
@@ -134,10 +125,6 @@ impl UniverseIndex {
         self.counter >= ui.counter
     }
 
-    pub fn to_lifetime(self) -> Lifetime {
-        Lifetime::ForAll(self)
-    }
-
     pub fn next(self) -> UniverseIndex {
         UniverseIndex {
             counter: self.counter + 1,
@@ -206,7 +193,31 @@ pub struct QuantifiedTy {
 pub enum Lifetime {
     /// See Ty::Var(_).
     Var(usize),
-    ForAll(UniverseIndex),
+    ForAll(UniversalIndex),
+}
+
+/// Index of an universally quantified parameter in the environment.
+/// Two indexes are required, the one of the universe itself
+/// and the relative index inside the universe.
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct UniversalIndex {
+    /// Index *of* the universe.
+    pub ui: UniverseIndex,
+    /// Index *in* the universe.
+    pub idx: usize,
+}
+
+impl UniversalIndex {
+    pub fn to_lifetime(self) -> Lifetime {
+        Lifetime::ForAll(self)
+    }
+
+    pub fn to_ty(self) -> Ty {
+        Ty::Apply(ApplicationTy {
+            name: TypeName::ForAll(self),
+            parameters: vec![],
+        })
+    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]

chalk-ir/src/macros.rs

@@ -54,7 +54,7 @@ macro_rules! lifetime {
     };
 
     (skol $b:expr) => {
-        $crate::Lifetime::ForAll(UniverseIndex { counter: $b })
+        $crate::Lifetime::ForAll(UniversalIndex { ui: UniverseIndex { counter: $b }, idx: 0})
     };
 
     (expr $b:expr) => {
@@ -69,5 +69,10 @@ macro_rules! lifetime {
 #[macro_export]
 macro_rules! ty_name {
     ((item $n:expr)) => { $crate::TypeName::ItemId(ItemId { index: $n }) };
-    ((skol $n:expr)) => { $crate::TypeName::ForAll(UniverseIndex { counter: $n }) }
+    ((skol $n:expr)) => { $crate::TypeName::ForAll(
+                            UniversalIndex {
+                                ui: UniverseIndex { counter: $n },
+                                idx: 0,
+                            })
+                        }
 }

chalk-solve/src/infer/canonicalize.rs

@@ -94,17 +94,17 @@ impl<'q> Canonicalizer<'q> {
 impl<'q> DefaultTypeFolder for Canonicalizer<'q> {}
 
 impl<'q> UniversalFolder for Canonicalizer<'q> {
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
-        self.max_universe = max(self.max_universe, universe);
-        Ok(TypeName::ForAll(universe).to_ty())
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
+        self.max_universe = max(self.max_universe, universe.ui);
+        Ok(universe.to_ty())
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe: UniverseIndex,
+        universe: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Lifetime> {
-        self.max_universe = max(self.max_universe, universe);
+        self.max_universe = max(self.max_universe, universe.ui);
         Ok(universe.to_lifetime())
     }
 }

chalk-solve/src/infer/instantiate.rs

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

chalk-solve/src/infer/invert.rs

@@ -97,8 +97,8 @@ impl InferenceTable {
 
 struct Inverter<'q> {
     table: &'q mut InferenceTable,
-    inverted_ty: HashMap<UniverseIndex, InferenceVariable>,
-    inverted_lifetime: HashMap<UniverseIndex, InferenceVariable>,
+    inverted_ty: HashMap<UniversalIndex, InferenceVariable>,
+    inverted_lifetime: HashMap<UniversalIndex, InferenceVariable>,
 }
 
 impl<'q> Inverter<'q> {
@@ -114,27 +114,27 @@ impl<'q> Inverter<'q> {
 impl<'q> DefaultTypeFolder for Inverter<'q> {}
 
 impl<'q> UniversalFolder for Inverter<'q> {
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, binders: usize) -> Fallible<Ty> {
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, binders: usize) -> Fallible<Ty> {
         let table = &mut self.table;
         Ok(
             self.inverted_ty
                 .entry(universe)
-                .or_insert_with(|| table.new_variable(universe))
+                .or_insert_with(|| table.new_variable(universe.ui))
                 .to_ty()
                 .shifted_in(binders),
         )
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe: UniverseIndex,
+        universe: UniversalIndex,
         binders: usize,
     ) -> Fallible<Lifetime> {
         let table = &mut self.table;
         Ok(
             self.inverted_lifetime
                 .entry(universe)
-                .or_insert_with(|| table.new_variable(universe))
+                .or_insert_with(|| table.new_variable(universe.ui))
                 .to_lifetime()
                 .shifted_in(binders),
         )

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 }",
+        "InEnvironment { environment: Env([]), goal: \'?2 == \'!1_0 }",
     );
 }

chalk-solve/src/infer/ucanonicalize.rs

@@ -220,17 +220,17 @@ struct UCollector<'q> {
 impl<'q> DefaultTypeFolder for UCollector<'q> {}
 
 impl<'q> UniversalFolder for UCollector<'q> {
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
-        self.universes.add(universe);
-        Ok(TypeName::ForAll(universe).to_ty())
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
+        self.universes.add(universe.ui);
+        Ok(universe.to_ty())
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe: UniverseIndex,
+        universe: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Lifetime> {
-        self.universes.add(universe);
+        self.universes.add(universe.ui);
         Ok(universe.to_lifetime())
     }
 }
@@ -246,20 +246,20 @@ impl<'q> DefaultTypeFolder for UMapToCanonical<'q> {}
 impl<'q> UniversalFolder for UMapToCanonical<'q> {
     fn fold_free_universal_ty(
         &mut self,
-        universe0: UniverseIndex,
+        universe0: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Ty> {
-        let universe = self.universes.map_universe_to_canonical(universe0);
-        Ok(TypeName::ForAll(universe).to_ty())
+        let ui = self.universes.map_universe_to_canonical(universe0.ui);
+        Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty())
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe0: UniverseIndex,
+        universe0: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Lifetime> {
-        let universe = self.universes.map_universe_to_canonical(universe0);
-        Ok(universe.to_lifetime())
+        let universe = self.universes.map_universe_to_canonical(universe0.ui);
+        Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime())
     }
 }
 
@@ -274,20 +274,20 @@ impl<'q> DefaultTypeFolder for UMapFromCanonical<'q> {}
 impl<'q> UniversalFolder for UMapFromCanonical<'q> {
     fn fold_free_universal_ty(
         &mut self,
-        universe0: UniverseIndex,
+        universe0: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Ty> {
-        let universe = self.universes.map_universe_from_canonical(universe0);
-        Ok(TypeName::ForAll(universe).to_ty())
+        let ui = self.universes.map_universe_from_canonical(universe0.ui);
+        Ok(UniversalIndex { ui, idx: universe0.idx }.to_ty())
     }
 
     fn fold_free_universal_lifetime(
         &mut self,
-        universe0: UniverseIndex,
+        universe0: UniversalIndex,
         _binders: usize,
     ) -> Fallible<Lifetime> {
-        let universe = self.universes.map_universe_from_canonical(universe0);
-        Ok(universe.to_lifetime())
+        let universe = self.universes.map_universe_from_canonical(universe0.ui);
+        Ok(UniversalIndex { ui: universe, idx: universe0.idx }.to_lifetime())
     }
 }