One universe many types

Author: leoyvens

src/fold.rs

@@ -134,7 +134,7 @@ 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(
@@ -150,8 +150,8 @@ 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(

src/ir.rs

@@ -138,21 +138,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 {
-    crate 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:
@@ -457,6 +448,13 @@ impl UniversalIndex {
     crate fn to_lifetime(self) -> Lifetime {
         Lifetime::ForAll(self)
     }
+
+    crate fn to_ty(self) -> Ty {
+        Ty::Apply(ApplicationTy {
+            name: TypeName::ForAll(self),
+            parameters: vec![],
+        })
+    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]

src/ir/debug.rs

@@ -37,7 +37,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),
         }
     }

src/ir/macros.rs

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

src/solve/infer/canonicalize.rs

@@ -94,9 +94,9 @@ 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(

src/solve/infer/instantiate.rs

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

src/solve/infer/invert.rs

@@ -97,7 +97,7 @@ impl InferenceTable {
 
 struct Inverter<'q> {
     table: &'q mut InferenceTable,
-    inverted_ty: HashMap<UniverseIndex, InferenceVariable>,
+    inverted_ty: HashMap<UniversalIndex, InferenceVariable>,
     inverted_lifetime: HashMap<UniversalIndex, InferenceVariable>,
 }
 
@@ -114,12 +114,12 @@ 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()
                 .up_shift(binders),
         )

src/solve/infer/ucanonicalize.rs

@@ -220,9 +220,9 @@ 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(
@@ -246,11 +246,11 @@ 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(
@@ -274,11 +274,11 @@ 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(

src/solve/infer/unify.rs

@@ -377,11 +377,11 @@ impl<'u, 't> OccursCheck<'u, 't> {
 impl<'u, 't> DefaultTypeFolder for OccursCheck<'u, 't> {}
 
 impl<'u, 't> UniversalFolder for OccursCheck<'u, 't> {
-    fn fold_free_universal_ty(&mut self, universe: UniverseIndex, _binders: usize) -> Fallible<Ty> {
-        if self.universe_index < universe {
+    fn fold_free_universal_ty(&mut self, universe: UniversalIndex, _binders: usize) -> Fallible<Ty> {
+        if self.universe_index < universe.ui {
             Err(NoSolution)
         } else {
-            Ok(TypeName::ForAll(universe).to_ty()) // no need to shift, not relative to depth
+            Ok(universe.to_ty()) // no need to shift, not relative to depth
         }
     }
 

src/solve/slg/test.rs

@@ -483,7 +483,7 @@ fn subgoal_cycle_uninhabited() {
                 Answer {
                     subst: Canonical {
                         value: ConstrainedSubst {
-                            subst: [?0 := !1],
+                            subst: [?0 := !1_0],
                             constraints: []
                         },
                         binders: []

src/solve/test.rs

@@ -476,7 +476,7 @@ fn normalize_basic() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := !1], lifetime constraints []"
+            "Unique; substitution [?0 := !1_0], lifetime constraints []"
         }
 
         goal {
@@ -506,7 +506,7 @@ fn normalize_basic() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := (Iterator::Item)<!1>]"
+            "Unique; substitution [?0 := (Iterator::Item)<!1_0>]"
         }
 
         goal {
@@ -518,7 +518,7 @@ fn normalize_basic() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := (Iterator::Item)<!1>]"
+            "Unique; substitution [?0 := (Iterator::Item)<!1_0>]"
         }
 
         goal {
@@ -581,7 +581,7 @@ fn normalize_gat1() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Iter<'!2_0, !1>], lifetime constraints []"
+            "Unique; substitution [?0 := Iter<'!2_0, !1_0>], 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, !1_1>], lifetime constraints []"
         }
 
         goal {
@@ -664,7 +664,7 @@ fn normalize_gat_with_where_clause() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Value<!1>]"
+            "Unique; substitution [?0 := Value<!1_0>]"
         }
     }
 }
@@ -703,7 +703,7 @@ fn normalize_gat_with_where_clause2() {
                 }
             }
         } yields {
-            "Unique; substitution [?0 := !2]"
+            "Unique; substitution [?0 := !1_1]"
         }
     }
 }