diff --git a/src/Cargo.lock b/src/Cargo.lock
index c4314b41e3966..a0db98f95b0c3 100644
--- a/src/Cargo.lock
+++ b/src/Cargo.lock
@@ -536,6 +536,14 @@ name = "either"
 version = "1.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 
+[[package]]
+name = "ena"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+dependencies = [
+ "log 0.3.8 (registry+https://github.com/rust-lang/crates.io-index)",
+]
+
 [[package]]
 name = "enum_primitive"
 version = "0.1.1"
@@ -1649,6 +1657,7 @@ dependencies = [
 name = "rustc_data_structures"
 version = "0.0.0"
 dependencies = [
+ "ena 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)",
  "log 0.3.8 (registry+https://github.com/rust-lang/crates.io-index)",
  "serialize 0.0.0",
 ]
@@ -2633,6 +2642,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 "checksum dtoa 0.4.2 (registry+https://github.com/rust-lang/crates.io-index)" = "09c3753c3db574d215cba4ea76018483895d7bff25a31b49ba45db21c48e50ab"
 "checksum duct 0.8.2 (registry+https://github.com/rust-lang/crates.io-index)" = "e45aa15fe0a8a8f511e6d834626afd55e49b62e5c8802e18328a87e8a8f6065c"
 "checksum either 1.3.0 (registry+https://github.com/rust-lang/crates.io-index)" = "e311a7479512fbdf858fb54d91ec59f3b9f85bc0113659f46bba12b199d273ce"
+"checksum ena 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)" = "58fb80e4764284ff0ec7054cb05c557f5ba01ccf65ff0c265e981c0b303d0ffc"
 "checksum enum_primitive 0.1.1 (registry+https://github.com/rust-lang/crates.io-index)" = "be4551092f4d519593039259a9ed8daedf0da12e5109c5280338073eaeb81180"
 "checksum env_logger 0.3.5 (registry+https://github.com/rust-lang/crates.io-index)" = "15abd780e45b3ea4f76b4e9a26ff4843258dd8a3eed2775a0e7368c2e7936c2f"
 "checksum env_logger 0.4.3 (registry+https://github.com/rust-lang/crates.io-index)" = "3ddf21e73e016298f5cb37d6ef8e8da8e39f91f9ec8b0df44b7deb16a9f8cd5b"
diff --git a/src/librustc/ich/impls_ty.rs b/src/librustc/ich/impls_ty.rs
index e7627b110fae4..c8000968e61e4 100644
--- a/src/librustc/ich/impls_ty.rs
+++ b/src/librustc/ich/impls_ty.rs
@@ -801,6 +801,7 @@ for ty::steal::Steal<T>
 
 impl_stable_hash_for!(struct ty::ParamEnv<'tcx> {
     caller_bounds,
+    universe,
     reveal
 });
 
@@ -970,3 +971,12 @@ for traits::VtableGeneratorData<'gcx, N> where N: HashStable<StableHashingContex
         nested.hash_stable(hcx, hasher);
     }
 }
+
+impl<'gcx> HashStable<StableHashingContext<'gcx>>
+for ty::UniverseIndex {
+    fn hash_stable<W: StableHasherResult>(&self,
+                                          hcx: &mut StableHashingContext<'gcx>,
+                                          hasher: &mut StableHasher<W>) {
+        self.depth().hash_stable(hcx, hasher);
+    }
+}
diff --git a/src/librustc/infer/combine.rs b/src/librustc/infer/combine.rs
index 40e933b26a257..c0ca157997bf4 100644
--- a/src/librustc/infer/combine.rs
+++ b/src/librustc/infer/combine.rs
@@ -34,10 +34,10 @@
 
 use super::equate::Equate;
 use super::glb::Glb;
+use super::{InferCtxt, MiscVariable, TypeTrace};
 use super::lub::Lub;
 use super::sub::Sub;
-use super::InferCtxt;
-use super::{MiscVariable, TypeTrace};
+use super::type_variable::TypeVariableValue;
 
 use hir::def_id::DefId;
 use ty::{IntType, UintType};
@@ -132,7 +132,7 @@ impl<'infcx, 'gcx, 'tcx> InferCtxt<'infcx, 'gcx, 'tcx> {
     {
         self.int_unification_table
             .borrow_mut()
-            .unify_var_value(vid, val)
+            .unify_var_value(vid, Some(val))
             .map_err(|e| int_unification_error(vid_is_expected, e))?;
         match val {
             IntType(v) => Ok(self.tcx.mk_mach_int(v)),
@@ -148,7 +148,7 @@ impl<'infcx, 'gcx, 'tcx> InferCtxt<'infcx, 'gcx, 'tcx> {
     {
         self.float_unification_table
             .borrow_mut()
-            .unify_var_value(vid, val)
+            .unify_var_value(vid, Some(ty::FloatVarValue(val)))
             .map_err(|e| float_unification_error(vid_is_expected, e))?;
         Ok(self.tcx.mk_mach_float(val))
     }
@@ -194,7 +194,7 @@ impl<'infcx, 'gcx, 'tcx> CombineFields<'infcx, 'gcx, 'tcx> {
         use self::RelationDir::*;
 
         // Get the actual variable that b_vid has been inferred to
-        debug_assert!(self.infcx.type_variables.borrow_mut().probe(b_vid).is_none());
+        debug_assert!(self.infcx.type_variables.borrow_mut().probe(b_vid).is_unknown());
 
         debug!("instantiate(a_ty={:?} dir={:?} b_vid={:?})", a_ty, dir, b_vid);
 
@@ -388,12 +388,12 @@ impl<'cx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx> for Generalizer<'cx, 'gcx, '
                     // `vid` are related via subtyping.
                     return Err(TypeError::CyclicTy);
                 } else {
-                    match variables.probe_root(vid) {
-                        Some(u) => {
+                    match variables.probe(vid) {
+                        TypeVariableValue::Known { value: u } => {
                             drop(variables);
                             self.relate(&u, &u)
                         }
-                        None => {
+                        TypeVariableValue::Unknown { universe } => {
                             match self.ambient_variance {
                                 // Invariant: no need to make a fresh type variable.
                                 ty::Invariant => return Ok(t),
@@ -409,8 +409,8 @@ impl<'cx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx> for Generalizer<'cx, 'gcx, '
                                 ty::Covariant | ty::Contravariant => (),
                             }
 
-                            let origin = variables.origin(vid);
-                            let new_var_id = variables.new_var(false, origin, None);
+                            let origin = *variables.var_origin(vid);
+                            let new_var_id = variables.new_var(universe, false, origin);
                             let u = self.tcx().mk_var(new_var_id);
                             debug!("generalize: replacing original vid={:?} with new={:?}",
                                    vid, u);
@@ -496,9 +496,9 @@ fn int_unification_error<'tcx>(a_is_expected: bool, v: (ty::IntVarValue, ty::Int
 }
 
 fn float_unification_error<'tcx>(a_is_expected: bool,
-                                 v: (ast::FloatTy, ast::FloatTy))
+                                 v: (ty::FloatVarValue, ty::FloatVarValue))
                                  -> TypeError<'tcx>
 {
-    let (a, b) = v;
+    let (ty::FloatVarValue(a), ty::FloatVarValue(b)) = v;
     TypeError::FloatMismatch(ty::relate::expected_found_bool(a_is_expected, &a, &b))
 }
diff --git a/src/librustc/infer/freshen.rs b/src/librustc/infer/freshen.rs
index 41e7dffe54dc1..468bfb514262a 100644
--- a/src/librustc/infer/freshen.rs
+++ b/src/librustc/infer/freshen.rs
@@ -212,7 +212,7 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for TypeFreshener<'a, 'gcx, 'tcx> {
 
         match t.sty {
             ty::TyInfer(ty::TyVar(v)) => {
-                let opt_ty = self.infcx.type_variables.borrow_mut().probe(v);
+                let opt_ty = self.infcx.type_variables.borrow_mut().probe(v).known();
                 self.freshen(
                     opt_ty,
                     ty::TyVar(v),
@@ -222,7 +222,7 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for TypeFreshener<'a, 'gcx, 'tcx> {
             ty::TyInfer(ty::IntVar(v)) => {
                 self.freshen(
                     self.infcx.int_unification_table.borrow_mut()
-                                                    .probe(v)
+                                                    .probe_value(v)
                                                     .map(|v| v.to_type(tcx)),
                     ty::IntVar(v),
                     ty::FreshIntTy)
@@ -231,7 +231,7 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for TypeFreshener<'a, 'gcx, 'tcx> {
             ty::TyInfer(ty::FloatVar(v)) => {
                 self.freshen(
                     self.infcx.float_unification_table.borrow_mut()
-                                                      .probe(v)
+                                                      .probe_value(v)
                                                       .map(|v| v.to_type(tcx)),
                     ty::FloatVar(v),
                     ty::FreshFloatTy)
diff --git a/src/librustc/infer/fudge.rs b/src/librustc/infer/fudge.rs
index 9cad6ce6f9fad..72f22856304fa 100644
--- a/src/librustc/infer/fudge.rs
+++ b/src/librustc/infer/fudge.rs
@@ -131,7 +131,9 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for RegionFudger<'a, 'gcx, 'tcx> {
                         // variables to their binding anyhow, we know
                         // that it is unbound, so we can just return
                         // it.
-                        debug_assert!(self.infcx.type_variables.borrow_mut().probe(vid).is_none());
+                        debug_assert!(self.infcx.type_variables.borrow_mut()
+                                      .probe(vid)
+                                      .is_unknown());
                         ty
                     }
 
@@ -139,7 +141,11 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for RegionFudger<'a, 'gcx, 'tcx> {
                         // This variable was created during the
                         // fudging. Recreate it with a fresh variable
                         // here.
-                        self.infcx.next_ty_var(origin)
+                        //
+                        // The ROOT universe is fine because we only
+                        // ever invoke this routine at the
+                        // "item-level" of inference.
+                        self.infcx.next_ty_var(ty::UniverseIndex::ROOT, origin)
                     }
                 }
             }
diff --git a/src/librustc/infer/higher_ranked/mod.rs b/src/librustc/infer/higher_ranked/mod.rs
index 6736751a5a2c2..ba6dde3ba6f50 100644
--- a/src/librustc/infer/higher_ranked/mod.rs
+++ b/src/librustc/infer/higher_ranked/mod.rs
@@ -242,7 +242,7 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
 
         fn generalize_region<'a, 'gcx, 'tcx>(infcx: &InferCtxt<'a, 'gcx, 'tcx>,
                                              span: Span,
-                                             snapshot: &CombinedSnapshot,
+                                             snapshot: &CombinedSnapshot<'a, 'tcx>,
                                              debruijn: ty::DebruijnIndex,
                                              new_vars: &[ty::RegionVid],
                                              a_map: &FxHashMap<ty::BoundRegion, ty::Region<'tcx>>,
@@ -338,7 +338,7 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
 
         fn generalize_region<'a, 'gcx, 'tcx>(infcx: &InferCtxt<'a, 'gcx, 'tcx>,
                                              span: Span,
-                                             snapshot: &CombinedSnapshot,
+                                             snapshot: &CombinedSnapshot<'a, 'tcx>,
                                              debruijn: ty::DebruijnIndex,
                                              new_vars: &[ty::RegionVid],
                                              a_map: &FxHashMap<ty::BoundRegion, ty::Region<'tcx>>,
@@ -477,7 +477,7 @@ fn fold_regions_in<'a, 'gcx, 'tcx, T, F>(tcx: TyCtxt<'a, 'gcx, 'tcx>,
 
 impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     fn tainted_regions(&self,
-                       snapshot: &CombinedSnapshot,
+                       snapshot: &CombinedSnapshot<'a, 'tcx>,
                        r: ty::Region<'tcx>,
                        directions: TaintDirections)
                        -> FxHashSet<ty::Region<'tcx>> {
@@ -485,7 +485,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     }
 
     fn region_vars_confined_to_snapshot(&self,
-                                        snapshot: &CombinedSnapshot)
+                                        snapshot: &CombinedSnapshot<'a, 'tcx>)
                                         -> Vec<ty::RegionVid>
     {
         /*!
@@ -576,7 +576,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     /// See `README.md` for more details.
     pub fn skolemize_late_bound_regions<T>(&self,
                                            binder: &ty::Binder<T>,
-                                           snapshot: &CombinedSnapshot)
+                                           snapshot: &CombinedSnapshot<'a, 'tcx>)
                                            -> (T, SkolemizationMap<'tcx>)
         where T : TypeFoldable<'tcx>
     {
@@ -601,7 +601,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
                       overly_polymorphic: bool,
                       _span: Span,
                       skol_map: &SkolemizationMap<'tcx>,
-                      snapshot: &CombinedSnapshot)
+                      snapshot: &CombinedSnapshot<'a, 'tcx>)
                       -> RelateResult<'tcx, ()>
     {
         debug!("leak_check: skol_map={:?}",
@@ -676,7 +676,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     /// predicate is `for<'a> &'a int : Clone`.
     pub fn plug_leaks<T>(&self,
                          skol_map: SkolemizationMap<'tcx>,
-                         snapshot: &CombinedSnapshot,
+                         snapshot: &CombinedSnapshot<'a, 'tcx>,
                          value: T) -> T
         where T : TypeFoldable<'tcx>
     {
@@ -762,8 +762,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     /// Note: popping also occurs implicitly as part of `leak_check`.
     pub fn pop_skolemized(&self,
                           skol_map: SkolemizationMap<'tcx>,
-                          snapshot: &CombinedSnapshot)
-    {
+                          snapshot: &CombinedSnapshot<'a, 'tcx>) {
         debug!("pop_skolemized({:?})", skol_map);
         let skol_regions: FxHashSet<_> = skol_map.values().cloned().collect();
         self.region_vars.pop_skolemized(&skol_regions, &snapshot.region_vars_snapshot);
diff --git a/src/librustc/infer/lattice.rs b/src/librustc/infer/lattice.rs
index d5c1163cfc1b1..c4722f9a7f96c 100644
--- a/src/librustc/infer/lattice.rs
+++ b/src/librustc/infer/lattice.rs
@@ -70,14 +70,6 @@ pub fn super_lattice_tys<'a, 'gcx, 'tcx, L>(this: &mut L,
     let a = infcx.type_variables.borrow_mut().replace_if_possible(a);
     let b = infcx.type_variables.borrow_mut().replace_if_possible(b);
     match (&a.sty, &b.sty) {
-        (&ty::TyInfer(TyVar(..)), &ty::TyInfer(TyVar(..)))
-            if infcx.type_var_diverges(a) && infcx.type_var_diverges(b) => {
-            let v = infcx.next_diverging_ty_var(
-                TypeVariableOrigin::LatticeVariable(this.cause().span));
-            this.relate_bound(v, a, b)?;
-            Ok(v)
-        }
-
         // If one side is known to be a variable and one is not,
         // create a variable (`v`) to represent the LUB. Make sure to
         // relate `v` to the non-type-variable first (by passing it
@@ -96,13 +88,17 @@ pub fn super_lattice_tys<'a, 'gcx, 'tcx, L>(this: &mut L,
         // is (e.g.) `Box<i32>`. A more obvious solution might be to
         // iterate on the subtype obligations that are returned, but I
         // think this suffices. -nmatsakis
-        (&ty::TyInfer(TyVar(..)), _) => {
-            let v = infcx.next_ty_var(TypeVariableOrigin::LatticeVariable(this.cause().span));
+        (&ty::TyInfer(TyVar(a_vid)), _) => {
+            let universe = infcx.type_variables.borrow_mut().probe(a_vid).universe().unwrap();
+            let v = infcx.next_ty_var(universe,
+                                      TypeVariableOrigin::LatticeVariable(this.cause().span));
             this.relate_bound(v, b, a)?;
             Ok(v)
         }
-        (_, &ty::TyInfer(TyVar(..))) => {
-            let v = infcx.next_ty_var(TypeVariableOrigin::LatticeVariable(this.cause().span));
+        (_, &ty::TyInfer(TyVar(b_vid))) => {
+            let universe = infcx.type_variables.borrow_mut().probe(b_vid).universe().unwrap();
+            let v = infcx.next_ty_var(universe,
+                                      TypeVariableOrigin::LatticeVariable(this.cause().span));
             this.relate_bound(v, a, b)?;
             Ok(v)
         }
diff --git a/src/librustc/infer/mod.rs b/src/librustc/infer/mod.rs
index 79eeebfb25031..f411ad5b29602 100644
--- a/src/librustc/infer/mod.rs
+++ b/src/librustc/infer/mod.rs
@@ -23,14 +23,14 @@ use middle::free_region::{FreeRegionMap, RegionRelations};
 use middle::region;
 use middle::lang_items;
 use mir::tcx::LvalueTy;
-use ty::subst::{Kind, Subst, Substs};
+use ty::subst::{Substs};
 use ty::{TyVid, IntVid, FloatVid};
 use ty::{self, Ty, TyCtxt};
 use ty::error::{ExpectedFound, TypeError, UnconstrainedNumeric};
 use ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
 use ty::relate::RelateResult;
 use traits::{self, ObligationCause, PredicateObligations, Reveal};
-use rustc_data_structures::unify::{self, UnificationTable};
+use rustc_data_structures::unify as ut;
 use std::cell::{Cell, RefCell, Ref};
 use std::fmt;
 use syntax::ast;
@@ -93,10 +93,10 @@ pub struct InferCtxt<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
     pub type_variables: RefCell<type_variable::TypeVariableTable<'tcx>>,
 
     // Map from integral variable to the kind of integer it represents
-    int_unification_table: RefCell<UnificationTable<ty::IntVid>>,
+    int_unification_table: RefCell<ut::UnificationTable<ut::InPlace<ty::IntVid>>>,
 
     // Map from floating variable to the kind of float it represents
-    float_unification_table: RefCell<UnificationTable<ty::FloatVid>>,
+    float_unification_table: RefCell<ut::UnificationTable<ut::InPlace<ty::FloatVid>>>,
 
     // For region variables.
     region_vars: RegionVarBindings<'a, 'gcx, 'tcx>,
@@ -377,8 +377,8 @@ impl<'a, 'gcx, 'tcx> InferCtxtBuilder<'a, 'gcx, 'tcx> {
             in_progress_tables,
             projection_cache: RefCell::new(traits::ProjectionCache::new()),
             type_variables: RefCell::new(type_variable::TypeVariableTable::new()),
-            int_unification_table: RefCell::new(UnificationTable::new()),
-            float_unification_table: RefCell::new(UnificationTable::new()),
+            int_unification_table: RefCell::new(ut::UnificationTable::new()),
+            float_unification_table: RefCell::new(ut::UnificationTable::new()),
             region_vars: RegionVarBindings::new(tcx),
             selection_cache: traits::SelectionCache::new(),
             evaluation_cache: traits::EvaluationCache::new(),
@@ -409,9 +409,9 @@ impl<'tcx, T> InferOk<'tcx, T> {
 #[must_use = "once you start a snapshot, you should always consume it"]
 pub struct CombinedSnapshot<'a, 'tcx:'a> {
     projection_cache_snapshot: traits::ProjectionCacheSnapshot,
-    type_snapshot: type_variable::Snapshot,
-    int_snapshot: unify::Snapshot<ty::IntVid>,
-    float_snapshot: unify::Snapshot<ty::FloatVid>,
+    type_snapshot: type_variable::Snapshot<'tcx>,
+    int_snapshot: ut::Snapshot<ut::InPlace<ty::IntVid>>,
+    float_snapshot: ut::Snapshot<ut::InPlace<ty::FloatVid>>,
     region_vars_snapshot: RegionSnapshot,
     was_in_snapshot: bool,
     _in_progress_tables: Option<Ref<'a, ty::TypeckTables<'tcx>>>,
@@ -611,14 +611,14 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         use ty::error::UnconstrainedNumeric::{UnconstrainedInt, UnconstrainedFloat};
         match ty.sty {
             ty::TyInfer(ty::IntVar(vid)) => {
-                if self.int_unification_table.borrow_mut().has_value(vid) {
+                if self.int_unification_table.borrow_mut().probe_value(vid).is_some() {
                     Neither
                 } else {
                     UnconstrainedInt
                 }
             },
             ty::TyInfer(ty::FloatVar(vid)) => {
-                if self.float_unification_table.borrow_mut().has_value(vid) {
+                if self.float_unification_table.borrow_mut().probe_value(vid).is_some() {
                     Neither
                 } else {
                     UnconstrainedFloat
@@ -628,46 +628,35 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         }
     }
 
-    /// Returns a type variable's default fallback if any exists. A default
-    /// must be attached to the variable when created, if it is created
-    /// without a default, this will return None.
-    ///
-    /// This code does not apply to integral or floating point variables,
-    /// only to use declared defaults.
-    ///
-    /// See `new_ty_var_with_default` to create a type variable with a default.
-    /// See `type_variable::Default` for details about what a default entails.
-    pub fn default(&self, ty: Ty<'tcx>) -> Option<type_variable::Default<'tcx>> {
-        match ty.sty {
-            ty::TyInfer(ty::TyVar(vid)) => self.type_variables.borrow().default(vid),
-            _ => None
-        }
-    }
-
     pub fn unsolved_variables(&self) -> Vec<Ty<'tcx>> {
         let mut variables = Vec::new();
 
-        let unbound_ty_vars = self.type_variables
-                                  .borrow_mut()
-                                  .unsolved_variables()
-                                  .into_iter()
-                                  .map(|t| self.tcx.mk_var(t));
-
-        let unbound_int_vars = self.int_unification_table
-                                   .borrow_mut()
-                                   .unsolved_variables()
-                                   .into_iter()
-                                   .map(|v| self.tcx.mk_int_var(v));
+        {
+            let mut type_variables = self.type_variables.borrow_mut();
+            variables.extend(
+                type_variables
+                    .unsolved_variables()
+                    .into_iter()
+                    .map(|t| self.tcx.mk_var(t)));
+        }
 
-        let unbound_float_vars = self.float_unification_table
-                                     .borrow_mut()
-                                     .unsolved_variables()
-                                     .into_iter()
-                                     .map(|v| self.tcx.mk_float_var(v));
+        {
+            let mut int_unification_table = self.int_unification_table.borrow_mut();
+            variables.extend(
+                (0..int_unification_table.len())
+                    .map(|i| ty::IntVid { index: i as u32 })
+                    .filter(|&vid| int_unification_table.probe_value(vid).is_none())
+                    .map(|v| self.tcx.mk_int_var(v)));
+        }
 
-        variables.extend(unbound_ty_vars);
-        variables.extend(unbound_int_vars);
-        variables.extend(unbound_float_vars);
+        {
+            let mut float_unification_table = self.float_unification_table.borrow_mut();
+            variables.extend(
+                (0..float_unification_table.len())
+                    .map(|i| ty::FloatVid { index: i as u32 })
+                    .filter(|&vid| float_unification_table.probe_value(vid).is_none())
+                    .map(|v| self.tcx.mk_float_var(v)));
+        }
 
         return variables;
     }
@@ -709,7 +698,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         result
     }
 
-    fn start_snapshot<'b>(&'b self) -> CombinedSnapshot<'b, 'tcx> {
+    fn start_snapshot(&self) -> CombinedSnapshot<'a, 'tcx> {
         debug!("start_snapshot()");
 
         let in_snapshot = self.in_snapshot.get();
@@ -730,7 +719,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         }
     }
 
-    fn rollback_to(&self, cause: &str, snapshot: CombinedSnapshot) {
+    fn rollback_to(&self, cause: &str, snapshot: CombinedSnapshot<'a, 'tcx>) {
         debug!("rollback_to(cause={})", cause);
         let CombinedSnapshot { projection_cache_snapshot,
                                type_snapshot,
@@ -758,7 +747,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
             .rollback_to(region_vars_snapshot);
     }
 
-    fn commit_from(&self, snapshot: CombinedSnapshot) {
+    fn commit_from(&self, snapshot: CombinedSnapshot<'a, 'tcx>) {
         debug!("commit_from()");
         let CombinedSnapshot { projection_cache_snapshot,
                                type_snapshot,
@@ -799,7 +788,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
 
     /// Execute `f` and commit the bindings if closure `f` returns `Ok(_)`
     pub fn commit_if_ok<T, E, F>(&self, f: F) -> Result<T, E> where
-        F: FnOnce(&CombinedSnapshot) -> Result<T, E>
+        F: FnOnce(&CombinedSnapshot<'a, 'tcx>) -> Result<T, E>
     {
         debug!("commit_if_ok()");
         let snapshot = self.start_snapshot();
@@ -814,7 +803,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
 
     // Execute `f` in a snapshot, and commit the bindings it creates
     pub fn in_snapshot<T, F>(&self, f: F) -> T where
-        F: FnOnce(&CombinedSnapshot) -> T
+        F: FnOnce(&CombinedSnapshot<'a, 'tcx>) -> T
     {
         debug!("in_snapshot()");
         let snapshot = self.start_snapshot();
@@ -825,7 +814,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
 
     /// Execute `f` then unroll any bindings it creates
     pub fn probe<R, F>(&self, f: F) -> R where
-        F: FnOnce(&CombinedSnapshot) -> R,
+        F: FnOnce(&CombinedSnapshot<'a, 'tcx>) -> R,
     {
         debug!("probe()");
         let snapshot = self.start_snapshot();
@@ -953,18 +942,25 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         })
     }
 
-    pub fn next_ty_var_id(&self, diverging: bool, origin: TypeVariableOrigin) -> TyVid {
+    pub fn next_ty_var_id(&self,
+                          universe: ty::UniverseIndex,
+                          diverging: bool,
+                          origin: TypeVariableOrigin)
+                          -> TyVid {
         self.type_variables
             .borrow_mut()
-            .new_var(diverging, origin, None)
+            .new_var(universe, diverging, origin)
     }
 
-    pub fn next_ty_var(&self, origin: TypeVariableOrigin) -> Ty<'tcx> {
-        self.tcx.mk_var(self.next_ty_var_id(false, origin))
+    pub fn next_ty_var(&self, universe: ty::UniverseIndex, origin: TypeVariableOrigin) -> Ty<'tcx> {
+        self.tcx.mk_var(self.next_ty_var_id(universe, false, origin))
     }
 
-    pub fn next_diverging_ty_var(&self, origin: TypeVariableOrigin) -> Ty<'tcx> {
-        self.tcx.mk_var(self.next_ty_var_id(true, origin))
+    pub fn next_diverging_ty_var(&self,
+                                 universe: ty::UniverseIndex,
+                                 origin: TypeVariableOrigin)
+                                 -> Ty<'tcx> {
+        self.tcx.mk_var(self.next_ty_var_id(universe, true, origin))
     }
 
     pub fn next_int_var_id(&self) -> IntVid {
@@ -1002,27 +998,15 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     /// use an inference variable for `C` with `[T, U]`
     /// as the substitutions for the default, `(T, U)`.
     pub fn type_var_for_def(&self,
+                            universe: ty::UniverseIndex,
                             span: Span,
-                            def: &ty::TypeParameterDef,
-                            substs: &[Kind<'tcx>])
+                            def: &ty::TypeParameterDef)
                             -> Ty<'tcx> {
-        let default = if def.has_default {
-            let default = self.tcx.type_of(def.def_id);
-            Some(type_variable::Default {
-                ty: default.subst_spanned(self.tcx, substs, Some(span)),
-                origin_span: span,
-                def_id: def.def_id
-            })
-        } else {
-            None
-        };
-
-
         let ty_var_id = self.type_variables
                             .borrow_mut()
-                            .new_var(false,
-                                     TypeVariableOrigin::TypeParameterDefinition(span, def.name),
-                                     default);
+                            .new_var(universe,
+                                     false,
+                                     TypeVariableOrigin::TypeParameterDefinition(span, def.name));
 
         self.tcx.mk_var(ty_var_id)
     }
@@ -1030,13 +1014,14 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
     /// Given a set of generics defined on a type or impl, returns a substitution mapping each
     /// type/region parameter to a fresh inference variable.
     pub fn fresh_substs_for_item(&self,
+                                 universe: ty::UniverseIndex,
                                  span: Span,
                                  def_id: DefId)
                                  -> &'tcx Substs<'tcx> {
         Substs::for_item(self.tcx, def_id, |def, _| {
             self.region_var_for_def(span, def)
-        }, |def, substs| {
-            self.type_var_for_def(span, def, substs)
+        }, |def, _| {
+            self.type_var_for_def(universe, span, def)
         })
     }
 
@@ -1115,15 +1100,16 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
                 // so this recursion should always be of very limited
                 // depth.
                 self.type_variables.borrow_mut()
-                    .probe(v)
-                    .map(|t| self.shallow_resolve(t))
-                    .unwrap_or(typ)
+                                   .probe(v)
+                                   .known()
+                                   .map(|t| self.shallow_resolve(t))
+                                   .unwrap_or(typ)
             }
 
             ty::TyInfer(ty::IntVar(v)) => {
                 self.int_unification_table
                     .borrow_mut()
-                    .probe(v)
+                    .probe_value(v)
                     .map(|v| v.to_type(self.tcx))
                     .unwrap_or(typ)
             }
@@ -1131,7 +1117,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
             ty::TyInfer(ty::FloatVar(v)) => {
                 self.float_unification_table
                     .borrow_mut()
-                    .probe(v)
+                    .probe_value(v)
                     .map(|v| v.to_type(self.tcx))
                     .unwrap_or(typ)
             }
@@ -1233,28 +1219,6 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         self.report_and_explain_type_error(trace, &err)
     }
 
-    pub fn report_conflicting_default_types(&self,
-                                            span: Span,
-                                            body_id: ast::NodeId,
-                                            expected: type_variable::Default<'tcx>,
-                                            actual: type_variable::Default<'tcx>) {
-        let trace = TypeTrace {
-            cause: ObligationCause::misc(span, body_id),
-            values: Types(ExpectedFound {
-                expected: expected.ty,
-                found: actual.ty
-            })
-        };
-
-        self.report_and_explain_type_error(
-            trace,
-            &TypeError::TyParamDefaultMismatch(ExpectedFound {
-                expected,
-                found: actual
-            }))
-            .emit();
-    }
-
     pub fn replace_late_bound_regions_with_fresh_var<T>(
         &self,
         span: Span,
diff --git a/src/librustc/infer/region_inference/mod.rs b/src/librustc/infer/region_inference/mod.rs
index 8351be490767a..b197344bda914 100644
--- a/src/librustc/infer/region_inference/mod.rs
+++ b/src/librustc/infer/region_inference/mod.rs
@@ -21,7 +21,7 @@ use super::unify_key;
 
 use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_data_structures::graph::{self, Direction, NodeIndex, OUTGOING};
-use rustc_data_structures::unify::{self, UnificationTable};
+use rustc_data_structures::unify as ut;
 use middle::free_region::RegionRelations;
 use ty::{self, Ty, TyCtxt};
 use ty::{Region, RegionVid};
@@ -216,7 +216,7 @@ pub struct RegionVarBindings<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
 
     lubs: RefCell<CombineMap<'tcx>>,
     glbs: RefCell<CombineMap<'tcx>>,
-    skolemization_count: Cell<u32>,
+    skolemization_count: Cell<ty::UniverseIndex>,
     bound_count: Cell<u32>,
 
     /// The undo log records actions that might later be undone.
@@ -230,7 +230,7 @@ pub struct RegionVarBindings<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
     /// back.
     undo_log: RefCell<Vec<UndoLogEntry<'tcx>>>,
 
-    unification_table: RefCell<UnificationTable<ty::RegionVid>>,
+    unification_table: RefCell<ut::UnificationTable<ut::InPlace<ty::RegionVid>>>,
 
     /// This contains the results of inference.  It begins as an empty
     /// option and only acquires a value after inference is complete.
@@ -239,8 +239,8 @@ pub struct RegionVarBindings<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
 
 pub struct RegionSnapshot {
     length: usize,
-    region_snapshot: unify::Snapshot<ty::RegionVid>,
-    skolemization_count: u32,
+    region_snapshot: ut::Snapshot<ut::InPlace<ty::RegionVid>>,
+    skolemization_count: ty::UniverseIndex,
 }
 
 /// When working with skolemized regions, we often wish to find all of
@@ -362,10 +362,10 @@ impl<'a, 'gcx, 'tcx> RegionVarBindings<'a, 'gcx, 'tcx> {
             givens: RefCell::new(FxHashSet()),
             lubs: RefCell::new(FxHashMap()),
             glbs: RefCell::new(FxHashMap()),
-            skolemization_count: Cell::new(0),
+            skolemization_count: Cell::new(ty::UniverseIndex::ROOT),
             bound_count: Cell::new(0),
             undo_log: RefCell::new(Vec::new()),
-            unification_table: RefCell::new(UnificationTable::new()),
+            unification_table: RefCell::new(ut::UnificationTable::new()),
         }
     }
 
@@ -389,7 +389,7 @@ impl<'a, 'gcx, 'tcx> RegionVarBindings<'a, 'gcx, 'tcx> {
         assert!(self.undo_log.borrow().len() > snapshot.length);
         assert!((*self.undo_log.borrow())[snapshot.length] == OpenSnapshot);
         assert!(self.skolemization_count.get() == snapshot.skolemization_count,
-                "failed to pop skolemized regions: {} now vs {} at start",
+                "failed to pop skolemized regions: {:?} now vs {:?} at start",
                 self.skolemization_count.get(),
                 snapshot.skolemization_count);
 
@@ -501,9 +501,9 @@ impl<'a, 'gcx, 'tcx> RegionVarBindings<'a, 'gcx, 'tcx> {
         assert!(self.in_snapshot());
         assert!(self.undo_log.borrow()[snapshot.length] == OpenSnapshot);
 
-        let sc = self.skolemization_count.get();
-        self.skolemization_count.set(sc + 1);
-        self.tcx.mk_region(ReSkolemized(ty::SkolemizedRegionVid { index: sc }, br))
+        let universe = self.skolemization_count.get().subuniverse();
+        self.skolemization_count.set(universe);
+        self.tcx.mk_region(ReSkolemized(universe, br))
     }
 
     /// Removes all the edges to/from the skolemized regions that are
@@ -517,31 +517,31 @@ impl<'a, 'gcx, 'tcx> RegionVarBindings<'a, 'gcx, 'tcx> {
 
         assert!(self.in_snapshot());
         assert!(self.undo_log.borrow()[snapshot.length] == OpenSnapshot);
-        assert!(self.skolemization_count.get() as usize >= skols.len(),
+        assert!(self.skolemization_count.get().as_usize() >= skols.len(),
                 "popping more skolemized variables than actually exist, \
                  sc now = {}, skols.len = {}",
-                self.skolemization_count.get(),
+                self.skolemization_count.get().as_usize(),
                 skols.len());
 
-        let last_to_pop = self.skolemization_count.get();
-        let first_to_pop = last_to_pop - (skols.len() as u32);
+        let last_to_pop = self.skolemization_count.get().subuniverse();
+        let first_to_pop = ty::UniverseIndex::from(last_to_pop.as_u32() - (skols.len() as u32));
 
         assert!(first_to_pop >= snapshot.skolemization_count,
                 "popping more regions than snapshot contains, \
-                 sc now = {}, sc then = {}, skols.len = {}",
+                 sc now = {:?}, sc then = {:?}, skols.len = {}",
                 self.skolemization_count.get(),
                 snapshot.skolemization_count,
                 skols.len());
         debug_assert! {
             skols.iter()
                  .all(|&k| match *k {
-                     ty::ReSkolemized(index, _) =>
-                         index.index >= first_to_pop &&
-                         index.index < last_to_pop,
+                     ty::ReSkolemized(universe, _) =>
+                         universe >= first_to_pop &&
+                         universe < last_to_pop,
                      _ =>
                          false
                  }),
-            "invalid skolemization keys or keys out of range ({}..{}): {:?}",
+            "invalid skolemization keys or keys out of range ({:?}..{:?}): {:?}",
             snapshot.skolemization_count,
             self.skolemization_count.get(),
             skols
@@ -808,7 +808,7 @@ impl<'a, 'gcx, 'tcx> RegionVarBindings<'a, 'gcx, 'tcx> {
     }
 
     pub fn opportunistic_resolve_var(&self, rid: RegionVid) -> ty::Region<'tcx> {
-        let vid = self.unification_table.borrow_mut().find_value(rid).min_vid;
+        let vid = self.unification_table.borrow_mut().probe_value(rid).min_vid;
         self.tcx.mk_region(ty::ReVar(vid))
     }
 
@@ -1523,7 +1523,7 @@ impl<'tcx> fmt::Debug for RegionAndOrigin<'tcx> {
 
 impl fmt::Debug for RegionSnapshot {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "RegionSnapshot(length={},skolemization={})",
+        write!(f, "RegionSnapshot(length={},skolemization={:?})",
                self.length, self.skolemization_count)
     }
 }
diff --git a/src/librustc/infer/type_variable.rs b/src/librustc/infer/type_variable.rs
index cc91a637b8931..4ee23d2647fa2 100644
--- a/src/librustc/infer/type_variable.rs
+++ b/src/librustc/infer/type_variable.rs
@@ -8,26 +8,28 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-use self::TypeVariableValue::*;
-use hir::def_id::{DefId};
 use syntax::ast;
 use syntax_pos::Span;
 use ty::{self, Ty};
 
-use std::cmp::min;
+use std::cmp;
 use std::marker::PhantomData;
-use std::mem;
 use std::u32;
 use rustc_data_structures::fx::FxHashMap;
-use rustc_data_structures::snapshot_vec as sv;
 use rustc_data_structures::unify as ut;
 
 pub struct TypeVariableTable<'tcx> {
-    values: sv::SnapshotVec<Delegate<'tcx>>,
+    /// Extra data for each type variable, such as the origin. This is
+    /// not stored in the unification table since, when we inquire
+    /// after the origin of a variable X, we want the origin of **that
+    /// variable X**, not the origin of some other variable Y with
+    /// which X has been unified.
+    var_data: Vec<TypeVariableData>,
 
     /// Two variables are unified in `eq_relations` when we have a
-    /// constraint `?X == ?Y`.
-    eq_relations: ut::UnificationTable<ty::TyVid>,
+    /// constraint `?X == ?Y`. This table also stores, for each key,
+    /// the known value.
+    eq_relations: ut::UnificationTable<ut::InPlace<TyVidEqKey<'tcx>>>,
 
     /// Two variables are unified in `eq_relations` when we have a
     /// constraint `?X <: ?Y` *or* a constraint `?Y <: ?X`. This second
@@ -46,7 +48,7 @@ pub struct TypeVariableTable<'tcx> {
     /// This is reasonable because, in Rust, subtypes have the same
     /// "skeleton" and hence there is no possible type such that
     /// (e.g.)  `Box<?3> <: ?3` for any `?3`.
-    sub_relations: ut::UnificationTable<ty::TyVid>,
+    sub_relations: ut::UnificationTable<ut::InPlace<ty::TyVid>>,
 }
 
 /// Reasons to create a type inference variable
@@ -69,73 +71,91 @@ pub enum TypeVariableOrigin {
 
 pub type TypeVariableMap = FxHashMap<ty::TyVid, TypeVariableOrigin>;
 
-struct TypeVariableData<'tcx> {
-    value: TypeVariableValue<'tcx>,
+struct TypeVariableData {
     origin: TypeVariableOrigin,
     diverging: bool
 }
 
-enum TypeVariableValue<'tcx> {
-    Known(Ty<'tcx>),
-    Bounded {
-        default: Option<Default<'tcx>>
-    }
+#[derive(Copy, Clone, Debug)]
+pub enum TypeVariableValue<'tcx> {
+    Known { value: Ty<'tcx> },
+    Unknown { universe: ty::UniverseIndex },
 }
 
-// We will use this to store the required information to recapitulate what happened when
-// an error occurs.
-#[derive(Clone, Debug, PartialEq, Eq, Hash)]
-pub struct Default<'tcx> {
-    pub ty: Ty<'tcx>,
-    /// The span where the default was incurred
-    pub origin_span: Span,
-    /// The definition that the default originates from
-    pub def_id: DefId
+#[derive(Copy, Clone, Debug)]
+pub enum ProbeTyValue<'tcx> {
+    Ty(Ty<'tcx>),
+    Vid(ty::TyVid),
 }
 
-pub struct Snapshot {
-    snapshot: sv::Snapshot,
-    eq_snapshot: ut::Snapshot<ty::TyVid>,
-    sub_snapshot: ut::Snapshot<ty::TyVid>,
-}
+impl<'tcx> TypeVariableValue<'tcx> {
+    /// If this value is known, returns the type it is known to be.
+    /// Otherwise, `None`.
+    pub fn known(&self) -> Option<Ty<'tcx>> {
+        match *self {
+            TypeVariableValue::Unknown { .. } => None,
+            TypeVariableValue::Known { value } => Some(value),
+        }
+    }
 
-struct Instantiate<'tcx> {
-    vid: ty::TyVid,
-    default: Option<Default<'tcx>>,
+    /// If this value is unknown, returns the universe, otherwise `None`.
+    pub fn universe(&self) -> Option<ty::UniverseIndex> {
+        match *self {
+            TypeVariableValue::Unknown { universe } => Some(universe),
+            TypeVariableValue::Known { .. } => None,
+        }
+    }
+
+    pub fn is_unknown(&self) -> bool {
+        match *self {
+            TypeVariableValue::Unknown { .. } => true,
+            TypeVariableValue::Known { .. } => false,
+        }
+    }
 }
 
-struct Delegate<'tcx>(PhantomData<&'tcx ()>);
+pub struct Snapshot<'tcx> {
+    /// number of variables at the time of the snapshot
+    num_vars: usize,
+
+    /// snapshot from the `eq_relations` table
+    eq_snapshot: ut::Snapshot<ut::InPlace<TyVidEqKey<'tcx>>>,
+
+    /// snapshot from the `sub_relations` table
+    sub_snapshot: ut::Snapshot<ut::InPlace<ty::TyVid>>,
+}
 
 impl<'tcx> TypeVariableTable<'tcx> {
     pub fn new() -> TypeVariableTable<'tcx> {
         TypeVariableTable {
-            values: sv::SnapshotVec::new(),
+            var_data: Vec::new(),
             eq_relations: ut::UnificationTable::new(),
             sub_relations: ut::UnificationTable::new(),
         }
     }
 
-    pub fn default(&self, vid: ty::TyVid) -> Option<Default<'tcx>> {
-        match &self.values.get(vid.index as usize).value {
-            &Known(_) => None,
-            &Bounded { ref default, .. } => default.clone()
-        }
-    }
-
+    /// Returns the diverges flag given when `vid` was created.
+    ///
+    /// Note that this function does not return care whether
+    /// `vid` has been unified with something else or not.
     pub fn var_diverges<'a>(&'a self, vid: ty::TyVid) -> bool {
-        self.values.get(vid.index as usize).diverging
+        self.var_data[vid.index as usize].diverging
     }
 
+    /// Returns the origin that was given when `vid` was created.
+    ///
+    /// Note that this function does not return care whether
+    /// `vid` has been unified with something else or not.
     pub fn var_origin(&self, vid: ty::TyVid) -> &TypeVariableOrigin {
-        &self.values.get(vid.index as usize).origin
+        &self.var_data[vid.index as usize].origin
     }
 
     /// Records that `a == b`, depending on `dir`.
     ///
     /// Precondition: neither `a` nor `b` are known.
     pub fn equate(&mut self, a: ty::TyVid, b: ty::TyVid) {
-        debug_assert!(self.probe(a).is_none());
-        debug_assert!(self.probe(b).is_none());
+        debug_assert!(self.probe(a).is_unknown());
+        debug_assert!(self.probe(b).is_unknown());
         self.eq_relations.union(a, b);
         self.sub_relations.union(a, b);
     }
@@ -144,8 +164,8 @@ impl<'tcx> TypeVariableTable<'tcx> {
     ///
     /// Precondition: neither `a` nor `b` are known.
     pub fn sub(&mut self, a: ty::TyVid, b: ty::TyVid) {
-        debug_assert!(self.probe(a).is_none());
-        debug_assert!(self.probe(b).is_none());
+        debug_assert!(self.probe(a).is_unknown());
+        debug_assert!(self.probe(b).is_unknown());
         self.sub_relations.union(a, b);
     }
 
@@ -154,43 +174,44 @@ impl<'tcx> TypeVariableTable<'tcx> {
     /// Precondition: `vid` must not have been previously instantiated.
     pub fn instantiate(&mut self, vid: ty::TyVid, ty: Ty<'tcx>) {
         let vid = self.root_var(vid);
-        debug_assert!(self.probe_root(vid).is_none());
-
-        let old_value = {
-            let vid_data = &mut self.values[vid.index as usize];
-            mem::replace(&mut vid_data.value, TypeVariableValue::Known(ty))
-        };
-
-        match old_value {
-            TypeVariableValue::Bounded { default } => {
-                self.values.record(Instantiate { vid: vid, default: default });
-            }
-            TypeVariableValue::Known(old_ty) => {
-                bug!("instantiating type variable `{:?}` twice: new-value = {:?}, old-value={:?}",
-                     vid, ty, old_ty)
-            }
-        }
+        debug_assert!(self.probe(vid).is_unknown());
+        debug_assert!(self.eq_relations.probe_value(vid).is_unknown(),
+                      "instantiating type variable `{:?}` twice: new-value = {:?}, old-value={:?}",
+                      vid, ty, self.eq_relations.probe_value(vid));
+        self.eq_relations.union_value(vid, TypeVariableValue::Known { value: ty });
     }
 
+    /// Creates a new type variable.
+    ///
+    /// - `diverging`: indicates if this is a "diverging" type
+    ///   variable, e.g.  one created as the type of a `return`
+    ///   expression. The code in this module doesn't care if a
+    ///   variable is diverging, but the main Rust type-checker will
+    ///   sometimes "unify" such variables with the `!` or `()` types.
+    /// - `origin`: indicates *why* the type variable was created.
+    ///   The code in this module doesn't care, but it can be useful
+    ///   for improving error messages.
     pub fn new_var(&mut self,
+                   universe: ty::UniverseIndex,
                    diverging: bool,
-                   origin: TypeVariableOrigin,
-                   default: Option<Default<'tcx>>,) -> ty::TyVid {
-        debug!("new_var(diverging={:?}, origin={:?})", diverging, origin);
-        self.eq_relations.new_key(());
-        self.sub_relations.new_key(());
-        let index = self.values.push(TypeVariableData {
-            value: Bounded { default: default },
-            origin,
-            diverging,
-        });
-        let v = ty::TyVid { index: index as u32 };
-        debug!("new_var: diverging={:?} index={:?}", diverging, v);
-        v
+                   origin: TypeVariableOrigin)
+                   -> ty::TyVid {
+        let eq_key = self.eq_relations.new_key(TypeVariableValue::Unknown { universe });
+
+        let sub_key = self.sub_relations.new_key(());
+        assert_eq!(eq_key.vid, sub_key);
+
+        assert_eq!(self.var_data.len(), sub_key.index as usize);
+        self.var_data.push(TypeVariableData { origin, diverging });
+
+        debug!("new_var(index={:?}, diverging={:?}, origin={:?}", eq_key.vid, diverging, origin);
+
+        eq_key.vid
     }
 
+    /// Returns the number of type variables created thus far.
     pub fn num_vars(&self) -> usize {
-        self.values.len()
+        self.var_data.len()
     }
 
     /// Returns the "root" variable of `vid` in the `eq_relations`
@@ -199,7 +220,7 @@ impl<'tcx> TypeVariableTable<'tcx> {
     /// algorithm), so `root_var(a) == root_var(b)` implies that `a ==
     /// b` (transitively).
     pub fn root_var(&mut self, vid: ty::TyVid) -> ty::TyVid {
-        self.eq_relations.find(vid)
+        self.eq_relations.find(vid).vid
     }
 
     /// Returns the "root" variable of `vid` in the `sub_relations`
@@ -219,65 +240,58 @@ impl<'tcx> TypeVariableTable<'tcx> {
         self.sub_root_var(a) == self.sub_root_var(b)
     }
 
-    pub fn probe(&mut self, vid: ty::TyVid) -> Option<Ty<'tcx>> {
-        let vid = self.root_var(vid);
-        self.probe_root(vid)
-    }
-
-    pub fn origin(&self, vid: ty::TyVid) -> TypeVariableOrigin {
-        self.values.get(vid.index as usize).origin.clone()
-    }
-
-    /// Retrieves the type of `vid` given that it is currently a root in the unification table
-    pub fn probe_root(&mut self, vid: ty::TyVid) -> Option<Ty<'tcx>> {
-        debug_assert!(self.root_var(vid) == vid);
-        match self.values.get(vid.index as usize).value {
-            Bounded { .. } => None,
-            Known(t) => Some(t)
-        }
+    /// Retrieves the type to which `vid` has been instantiated, if
+    /// any.
+    pub fn probe(&mut self, vid: ty::TyVid) -> TypeVariableValue<'tcx> {
+        self.eq_relations.probe_value(vid)
     }
 
+    /// If `t` is a type-inference variable, and it has been
+    /// instantiated, then return the with which it was
+    /// instantiated. Otherwise, returns `t`.
     pub fn replace_if_possible(&mut self, t: Ty<'tcx>) -> Ty<'tcx> {
         match t.sty {
             ty::TyInfer(ty::TyVar(v)) => {
                 match self.probe(v) {
-                    None => t,
-                    Some(u) => u
+                    TypeVariableValue::Unknown { .. } => t,
+                    TypeVariableValue::Known { value } => value,
                 }
             }
             _ => t,
         }
     }
 
-    pub fn snapshot(&mut self) -> Snapshot {
+    /// Creates a snapshot of the type variable state.  This snapshot
+    /// must later be committed (`commit()`) or rolled back
+    /// (`rollback_to()`).  Nested snapshots are permitted, but must
+    /// be processed in a stack-like fashion.
+    pub fn snapshot(&mut self) -> Snapshot<'tcx> {
         Snapshot {
-            snapshot: self.values.start_snapshot(),
+            num_vars: self.var_data.len(),
             eq_snapshot: self.eq_relations.snapshot(),
             sub_snapshot: self.sub_relations.snapshot(),
         }
     }
 
-    pub fn rollback_to(&mut self, s: Snapshot) {
-        debug!("rollback_to{:?}", {
-            for action in self.values.actions_since_snapshot(&s.snapshot) {
-                match *action {
-                    sv::UndoLog::NewElem(index) => {
-                        debug!("inference variable _#{}t popped", index)
-                    }
-                    _ => { }
-                }
-            }
-        });
-
-        let Snapshot { snapshot, eq_snapshot, sub_snapshot } = s;
-        self.values.rollback_to(snapshot);
+    /// Undoes all changes since the snapshot was created. Any
+    /// snapshots created since that point must already have been
+    /// committed or rolled back.
+    pub fn rollback_to(&mut self, s: Snapshot<'tcx>) {
+        let Snapshot { num_vars, eq_snapshot, sub_snapshot } = s;
+        debug!("type_variables::rollback_to(num_vars = {})", num_vars);
+        assert!(self.var_data.len() >= num_vars);
         self.eq_relations.rollback_to(eq_snapshot);
         self.sub_relations.rollback_to(sub_snapshot);
+        self.var_data.truncate(num_vars);
     }
 
-    pub fn commit(&mut self, s: Snapshot) {
-        let Snapshot { snapshot, eq_snapshot, sub_snapshot } = s;
-        self.values.commit(snapshot);
+    /// Commits all changes since the snapshot was created, making
+    /// them permanent (unless this snapshot was created within
+    /// another snapshot). Any snapshots created since that point
+    /// must already have been committed or rolled back.
+    pub fn commit(&mut self, s: Snapshot<'tcx>) {
+        let Snapshot { num_vars, eq_snapshot, sub_snapshot } = s;
+        debug!("type_variables::commit(num_vars = {})", num_vars);
         self.eq_relations.commit(eq_snapshot);
         self.sub_relations.commit(sub_snapshot);
     }
@@ -286,90 +300,125 @@ impl<'tcx> TypeVariableTable<'tcx> {
     /// ty-variables created during the snapshot, and the values
     /// `{V2}` are the root variables that they were unified with,
     /// along with their origin.
-    pub fn types_created_since_snapshot(&mut self, s: &Snapshot) -> TypeVariableMap {
-        let actions_since_snapshot = self.values.actions_since_snapshot(&s.snapshot);
-
-        actions_since_snapshot
+    pub fn types_created_since_snapshot(&mut self, snapshot: &Snapshot<'tcx>) -> TypeVariableMap {
+        self.var_data
             .iter()
-            .filter_map(|action| match action {
-                &sv::UndoLog::NewElem(index) => Some(ty::TyVid { index: index as u32 }),
-                _ => None,
-            })
-            .map(|vid| {
-                let origin = self.values.get(vid.index as usize).origin.clone();
-                (vid, origin)
-            })
+            .enumerate()
+            .skip(snapshot.num_vars) // skip those that existed when snapshot was taken
+            .map(|(index, data)| (ty::TyVid { index: index as u32 }, data.origin))
             .collect()
     }
 
-    pub fn types_escaping_snapshot(&mut self, s: &Snapshot) -> Vec<Ty<'tcx>> {
-        /*!
-         * Find the set of type variables that existed *before* `s`
-         * but which have only been unified since `s` started, and
-         * return the types with which they were unified. So if we had
-         * a type variable `V0`, then we started the snapshot, then we
-         * created a type variable `V1`, unifed `V0` with `T0`, and
-         * unified `V1` with `T1`, this function would return `{T0}`.
-         */
-
-        let mut new_elem_threshold = u32::MAX;
-        let mut escaping_types = Vec::new();
-        let actions_since_snapshot = self.values.actions_since_snapshot(&s.snapshot);
-        debug!("actions_since_snapshot.len() = {}", actions_since_snapshot.len());
-        for action in actions_since_snapshot {
-            match *action {
-                sv::UndoLog::NewElem(index) => {
-                    // if any new variables were created during the
-                    // snapshot, remember the lower index (which will
-                    // always be the first one we see). Note that this
-                    // action must precede those variables being
-                    // specified.
-                    new_elem_threshold = min(new_elem_threshold, index as u32);
-                    debug!("NewElem({}) new_elem_threshold={}", index, new_elem_threshold);
-                }
-
-                sv::UndoLog::Other(Instantiate { vid, .. }) => {
-                    if vid.index < new_elem_threshold {
-                        // quick check to see if this variable was
-                        // created since the snapshot started or not.
-                        let escaping_type = match self.values.get(vid.index as usize).value {
-                            Bounded { .. } => bug!(),
-                            Known(ty) => ty,
-                        };
-                        escaping_types.push(escaping_type);
-                    }
-                    debug!("SpecifyVar({:?}) new_elem_threshold={}", vid, new_elem_threshold);
-                }
-
-                _ => { }
-            }
-        }
-
+    /// Find the set of type variables that existed *before* `s`
+    /// but which have only been unified since `s` started, and
+    /// return the types with which they were unified. So if we had
+    /// a type variable `V0`, then we started the snapshot, then we
+    /// created a type variable `V1`, unifed `V0` with `T0`, and
+    /// unified `V1` with `T1`, this function would return `{T0}`.
+    pub fn types_escaping_snapshot(&mut self, snapshot: &Snapshot<'tcx>) -> Vec<Ty<'tcx>> {
+        // We want to select only those instantiations that have
+        // occurred since the snapshot *and* which affect some
+        // variable that existed prior to the snapshot. This code just
+        // affects all instantiatons that ever occurred which affect
+        // variables prior to the snapshot.
+        //
+        // It's hard to do better than this, though, without changing
+        // the unification table to prefer "lower" vids -- the problem
+        // is that we may have a variable X (from before the snapshot)
+        // and Y (from after the snapshot) which get unified, with Y
+        // chosen as the new root. Now we are "instantiating" Y with a
+        // value, but it escapes into X, but we wouldn't readily see
+        // that. (In fact, earlier revisions of this code had this
+        // bug; it was introduced when we added the `eq_relations`
+        // table, but it's hard to create rust code that triggers it.)
+        //
+        // We could tell the table to prefer lower vids, and then we would
+        // see the case above, but we would get less-well-balanced trees.
+        //
+        // Since I hope to kill the leak-check in this branch, and
+        // that's the code which uses this logic anyway, I'm going to
+        // use the less efficient algorithm for now.
+        let mut escaping_types = Vec::with_capacity(snapshot.num_vars);
+        escaping_types.extend(
+            (0..snapshot.num_vars) // for all variables that pre-exist the snapshot, collect..
+                .map(|i| ty::TyVid { index: i as u32 })
+                .filter_map(|vid| self.probe(vid).known())); // ..types they are instantiated with.
+        debug!("types_escaping_snapshot = {:?}", escaping_types);
         escaping_types
     }
 
+    /// Returns indices of all variables that are not yet
+    /// instantiated.
     pub fn unsolved_variables(&mut self) -> Vec<ty::TyVid> {
-        (0..self.values.len())
+        (0..self.var_data.len())
             .filter_map(|i| {
                 let vid = ty::TyVid { index: i as u32 };
-                if self.probe(vid).is_some() {
-                    None
-                } else {
-                    Some(vid)
+                match self.probe(vid) {
+                    TypeVariableValue::Unknown { .. } => Some(vid),
+                    TypeVariableValue::Known { .. } => None,
                 }
             })
             .collect()
     }
 }
+///////////////////////////////////////////////////////////////////////////
 
-impl<'tcx> sv::SnapshotVecDelegate for Delegate<'tcx> {
-    type Value = TypeVariableData<'tcx>;
-    type Undo = Instantiate<'tcx>;
+/// These structs (a newtyped TyVid) are used as the unification key
+/// for the `eq_relations`; they carry a `TypeVariableValue` along
+/// with them.
+#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+struct TyVidEqKey<'tcx> {
+    vid: ty::TyVid,
 
-    fn reverse(values: &mut Vec<TypeVariableData<'tcx>>, action: Instantiate<'tcx>) {
-        let Instantiate { vid, default } = action;
-        values[vid.index as usize].value = Bounded {
-            default,
-        };
+    // in the table, we map each ty-vid to one of these:
+    phantom: PhantomData<TypeVariableValue<'tcx>>,
+}
+
+impl<'tcx> From<ty::TyVid> for TyVidEqKey<'tcx> {
+    fn from(vid: ty::TyVid) -> Self {
+        TyVidEqKey { vid, phantom: PhantomData }
+    }
+}
+
+impl<'tcx> ut::UnifyKey for TyVidEqKey<'tcx> {
+    type Value = TypeVariableValue<'tcx>;
+    fn index(&self) -> u32 { self.vid.index }
+    fn from_index(i: u32) -> Self { TyVidEqKey::from(ty::TyVid { index: i }) }
+    fn tag() -> &'static str { "TyVidEqKey" }
+}
+
+impl<'tcx> ut::UnifyValue for TypeVariableValue<'tcx> {
+    type Error = ut::NoError;
+
+    fn unify_values(value1: &Self, value2: &Self) -> Result<Self, ut::NoError> {
+        match (value1, value2) {
+            // We never equate two type variables, both of which
+            // have known types.  Instead, we recursively equate
+            // those types.
+            (&TypeVariableValue::Known { .. }, &TypeVariableValue::Known { .. }) => {
+                bug!("equating two type variables, both of which have known types")
+            }
+
+            // If one side is known, prefer that one.
+            (&TypeVariableValue::Known { .. }, &TypeVariableValue::Unknown { .. }) => Ok(*value1),
+            (&TypeVariableValue::Unknown { .. }, &TypeVariableValue::Known { .. }) => Ok(*value2),
+
+            // If both sides are unknown, we need to pick the most restrictive universe.
+            (&TypeVariableValue::Unknown { universe: universe1 },
+             &TypeVariableValue::Unknown { universe: universe2 }) => {
+                let universe = cmp::min(universe1, universe2);
+                Ok(TypeVariableValue::Unknown { universe })
+            }
+        }
     }
 }
+
+/// Raw `TyVid` are used as the unification key for `sub_relations`;
+/// they carry no values.
+impl ut::UnifyKey for ty::TyVid {
+    type Value = ();
+    fn index(&self) -> u32 { self.index }
+    fn from_index(i: u32) -> ty::TyVid { ty::TyVid { index: i } }
+    fn tag() -> &'static str { "TyVid" }
+}
+
diff --git a/src/librustc/infer/unify_key.rs b/src/librustc/infer/unify_key.rs
index d7e3a53ff25c9..24e3aa51e290a 100644
--- a/src/librustc/infer/unify_key.rs
+++ b/src/librustc/infer/unify_key.rs
@@ -8,9 +8,8 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-use syntax::ast;
-use ty::{self, IntVarValue, Ty, TyCtxt};
-use rustc_data_structures::unify::{Combine, UnifyKey};
+use ty::{self, FloatVarValue, IntVarValue, Ty, TyCtxt};
+use rustc_data_structures::unify::{NoError, EqUnifyValue, UnifyKey, UnifyValue};
 
 pub trait ToType {
     fn to_type<'a, 'gcx, 'tcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Ty<'tcx>;
@@ -20,7 +19,10 @@ impl UnifyKey for ty::IntVid {
     type Value = Option<IntVarValue>;
     fn index(&self) -> u32 { self.index }
     fn from_index(i: u32) -> ty::IntVid { ty::IntVid { index: i } }
-    fn tag(_: Option<ty::IntVid>) -> &'static str { "IntVid" }
+    fn tag() -> &'static str { "IntVid" }
+}
+
+impl EqUnifyValue for IntVarValue {
 }
 
 #[derive(PartialEq, Copy, Clone, Debug)]
@@ -31,15 +33,17 @@ pub struct RegionVidKey {
     pub min_vid: ty::RegionVid
 }
 
-impl Combine for RegionVidKey {
-    fn combine(&self, other: &RegionVidKey) -> RegionVidKey {
-        let min_vid = if self.min_vid.index < other.min_vid.index {
-            self.min_vid
+impl UnifyValue for RegionVidKey {
+    type Error = NoError;
+
+    fn unify_values(value1: &Self, value2: &Self) -> Result<Self, NoError> {
+        let min_vid = if value1.min_vid.index < value2.min_vid.index {
+            value1.min_vid
         } else {
-            other.min_vid
+            value2.min_vid
         };
 
-        RegionVidKey { min_vid: min_vid }
+        Ok(RegionVidKey { min_vid: min_vid })
     }
 }
 
@@ -47,7 +51,7 @@ impl UnifyKey for ty::RegionVid {
     type Value = RegionVidKey;
     fn index(&self) -> u32 { self.index }
     fn from_index(i: u32) -> ty::RegionVid { ty::RegionVid { index: i } }
-    fn tag(_: Option<ty::RegionVid>) -> &'static str { "RegionVid" }
+    fn tag() -> &'static str { "RegionVid" }
 }
 
 impl ToType for IntVarValue {
@@ -62,21 +66,17 @@ impl ToType for IntVarValue {
 // Floating point type keys
 
 impl UnifyKey for ty::FloatVid {
-    type Value = Option<ast::FloatTy>;
+    type Value = Option<FloatVarValue>;
     fn index(&self) -> u32 { self.index }
     fn from_index(i: u32) -> ty::FloatVid { ty::FloatVid { index: i } }
-    fn tag(_: Option<ty::FloatVid>) -> &'static str { "FloatVid" }
+    fn tag() -> &'static str { "FloatVid" }
 }
 
-impl ToType for ast::FloatTy {
-    fn to_type<'a, 'gcx, 'tcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Ty<'tcx> {
-        tcx.mk_mach_float(*self)
-    }
+impl EqUnifyValue for FloatVarValue {
 }
 
-impl UnifyKey for ty::TyVid {
-    type Value = ();
-    fn index(&self) -> u32 { self.index }
-    fn from_index(i: u32) -> ty::TyVid { ty::TyVid { index: i } }
-    fn tag(_: Option<ty::TyVid>) -> &'static str { "TyVid" }
+impl ToType for FloatVarValue {
+    fn to_type<'a, 'gcx, 'tcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Ty<'tcx> {
+        tcx.mk_mach_float(self.0)
+    }
 }
diff --git a/src/librustc/traits/coherence.rs b/src/librustc/traits/coherence.rs
index 10a32c26e741d..bc805e85f7baa 100644
--- a/src/librustc/traits/coherence.rs
+++ b/src/librustc/traits/coherence.rs
@@ -50,7 +50,9 @@ fn with_fresh_ty_vars<'cx, 'gcx, 'tcx>(selcx: &mut SelectionContext<'cx, 'gcx, '
                                        -> ty::ImplHeader<'tcx>
 {
     let tcx = selcx.tcx();
-    let impl_substs = selcx.infcx().fresh_substs_for_item(DUMMY_SP, impl_def_id);
+    let impl_substs = selcx.infcx().fresh_substs_for_item(param_env.universe,
+                                                          DUMMY_SP,
+                                                          impl_def_id);
 
     let header = ty::ImplHeader {
         impl_def_id,
diff --git a/src/librustc/traits/error_reporting.rs b/src/librustc/traits/error_reporting.rs
index e2b23c12cf1f3..e4e53a6692751 100644
--- a/src/librustc/traits/error_reporting.rs
+++ b/src/librustc/traits/error_reporting.rs
@@ -285,7 +285,9 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
 
         self.tcx.for_each_relevant_impl(
             trait_ref.def_id, trait_self_ty, |def_id| {
-                let impl_substs = self.fresh_substs_for_item(obligation.cause.span, def_id);
+                let impl_substs = self.fresh_substs_for_item(param_env.universe,
+                                                             obligation.cause.span,
+                                                             def_id);
                 let impl_trait_ref = tcx
                     .impl_trait_ref(def_id)
                     .unwrap()
@@ -1134,6 +1136,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
                            -> bool {
         struct ParamToVarFolder<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
             infcx: &'a InferCtxt<'a, 'gcx, 'tcx>,
+            param_env: ty::ParamEnv<'tcx>,
             var_map: FxHashMap<Ty<'tcx>, Ty<'tcx>>
         }
 
@@ -1143,9 +1146,14 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
             fn fold_ty(&mut self, ty: Ty<'tcx>) -> Ty<'tcx> {
                 if let ty::TyParam(ty::ParamTy {name, ..}) = ty.sty {
                     let infcx = self.infcx;
-                    self.var_map.entry(ty).or_insert_with(||
-                        infcx.next_ty_var(
-                            TypeVariableOrigin::TypeParameterDefinition(DUMMY_SP, name)))
+                    let param_env = self.param_env;
+                    self.var_map
+                        .entry(ty)
+                        .or_insert_with(|| {
+                            let origin = TypeVariableOrigin::TypeParameterDefinition(DUMMY_SP,
+                                                                                     name);
+                            infcx.next_ty_var(param_env.universe, origin)
+                        })
                 } else {
                     ty.super_fold_with(self)
                 }
@@ -1157,6 +1165,7 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
 
             let cleaned_pred = pred.fold_with(&mut ParamToVarFolder {
                 infcx: self,
+                param_env,
                 var_map: FxHashMap()
             });
 
diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs
index c08fe187f99bf..09c7d7316baa2 100644
--- a/src/librustc/traits/mod.rs
+++ b/src/librustc/traits/mod.rs
@@ -68,10 +68,21 @@ mod util;
 /// scope. The eventual result is usually a `Selection` (defined below).
 #[derive(Clone, PartialEq, Eq)]
 pub struct Obligation<'tcx, T> {
+    /// Why do we have to prove this thing?
     pub cause: ObligationCause<'tcx>,
+
+    /// In which environment should we prove this thing?
     pub param_env: ty::ParamEnv<'tcx>,
-    pub recursion_depth: usize,
+
+    /// What are we trying to prove?
     pub predicate: T,
+
+    /// If we started proving this as a result of trying to prove
+    /// something else, track the total depth to ensure termination.
+    /// If this goes over a certain threshold, we abort compilation --
+    /// in such cases, we can not say whether or not the predicate
+    /// holds for certain. Stupid halting problem. Such a drag.
+    pub recursion_depth: usize,
 }
 
 pub type PredicateObligation<'tcx> = Obligation<'tcx, ty::Predicate<'tcx>>;
@@ -509,7 +520,8 @@ pub fn normalize_param_env_or_error<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
            predicates);
 
     let elaborated_env = ty::ParamEnv::new(tcx.intern_predicates(&predicates),
-                                           unnormalized_env.reveal);
+                                           unnormalized_env.reveal,
+                                           unnormalized_env.universe);
 
     tcx.infer_ctxt().enter(|infcx| {
         let predicates = match fully_normalize(
@@ -562,7 +574,9 @@ pub fn normalize_param_env_or_error<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
         debug!("normalize_param_env_or_error: resolved predicates={:?}",
                predicates);
 
-        ty::ParamEnv::new(tcx.intern_predicates(&predicates), unnormalized_env.reveal)
+        ty::ParamEnv::new(tcx.intern_predicates(&predicates),
+                          unnormalized_env.reveal,
+                          unnormalized_env.universe)
     })
 }
 
diff --git a/src/librustc/traits/project.rs b/src/librustc/traits/project.rs
index 9c56df058c3dd..6cb556cc99aa5 100644
--- a/src/librustc/traits/project.rs
+++ b/src/librustc/traits/project.rs
@@ -404,6 +404,7 @@ pub fn normalize_projection_type<'a, 'b, 'gcx, 'tcx>(
             let tcx = selcx.infcx().tcx;
             let def_id = projection_ty.item_def_id;
             let ty_var = selcx.infcx().next_ty_var(
+                param_env.universe,
                 TypeVariableOrigin::NormalizeProjectionType(tcx.def_span(def_id)));
             let projection = ty::Binder(ty::ProjectionPredicate {
                 projection_ty,
@@ -724,6 +725,7 @@ fn normalize_to_error<'a, 'gcx, 'tcx>(selcx: &mut SelectionContext<'a, 'gcx, 'tc
     let tcx = selcx.infcx().tcx;
     let def_id = projection_ty.item_def_id;
     let new_value = selcx.infcx().next_ty_var(
+        param_env.universe,
         TypeVariableOrigin::NormalizeProjectionType(tcx.def_span(def_id)));
     Normalized {
         value: new_value,
diff --git a/src/librustc/traits/select.rs b/src/librustc/traits/select.rs
index 7716770d318ba..ec911911a07ba 100644
--- a/src/librustc/traits/select.rs
+++ b/src/librustc/traits/select.rs
@@ -452,7 +452,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
     /// Wraps the inference context's in_snapshot s.t. snapshot handling is only from the selection
     /// context's self.
     fn in_snapshot<R, F>(&mut self, f: F) -> R
-        where F: FnOnce(&mut Self, &infer::CombinedSnapshot) -> R
+        where F: FnOnce(&mut Self, &infer::CombinedSnapshot<'cx, 'tcx>) -> R
     {
         // The irrefutable nature of the operation means we don't need to snapshot the
         // inferred_obligations vector.
@@ -462,7 +462,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
     /// Wraps a probe s.t. obligations collected during it are ignored and old obligations are
     /// retained.
     fn probe<R, F>(&mut self, f: F) -> R
-        where F: FnOnce(&mut Self, &infer::CombinedSnapshot) -> R
+        where F: FnOnce(&mut Self, &infer::CombinedSnapshot<'cx, 'tcx>) -> R
     {
         let inferred_obligations_snapshot = self.inferred_obligations.start_snapshot();
         let result = self.infcx.probe(|snapshot| f(self, snapshot));
@@ -1407,7 +1407,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
     fn match_projection_obligation_against_definition_bounds(
         &mut self,
         obligation: &TraitObligation<'tcx>,
-        snapshot: &infer::CombinedSnapshot)
+        snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
         -> bool
     {
         let poly_trait_predicate =
@@ -1478,7 +1478,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
                         trait_bound: ty::PolyTraitRef<'tcx>,
                         skol_trait_ref: ty::TraitRef<'tcx>,
                         skol_map: &infer::SkolemizationMap<'tcx>,
-                        snapshot: &infer::CombinedSnapshot)
+                        snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
                         -> bool
     {
         assert!(!skol_trait_ref.has_escaping_regions());
@@ -2507,7 +2507,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
                    recursion_depth: usize,
                    param_env: ty::ParamEnv<'tcx>,
                    skol_map: infer::SkolemizationMap<'tcx>,
-                   snapshot: &infer::CombinedSnapshot)
+                   snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
                    -> VtableImplData<'tcx, PredicateObligation<'tcx>>
     {
         debug!("vtable_impl(impl_def_id={:?}, substs={:?}, recursion_depth={}, skol_map={:?})",
@@ -2996,7 +2996,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
     fn rematch_impl(&mut self,
                     impl_def_id: DefId,
                     obligation: &TraitObligation<'tcx>,
-                    snapshot: &infer::CombinedSnapshot)
+                    snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
                     -> (Normalized<'tcx, &'tcx Substs<'tcx>>,
                         infer::SkolemizationMap<'tcx>)
     {
@@ -3013,7 +3013,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
     fn match_impl(&mut self,
                   impl_def_id: DefId,
                   obligation: &TraitObligation<'tcx>,
-                  snapshot: &infer::CombinedSnapshot)
+                  snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
                   -> Result<(Normalized<'tcx, &'tcx Substs<'tcx>>,
                              infer::SkolemizationMap<'tcx>), ()>
     {
@@ -3031,7 +3031,8 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
             snapshot);
         let skol_obligation_trait_ref = skol_obligation.trait_ref;
 
-        let impl_substs = self.infcx.fresh_substs_for_item(obligation.cause.span,
+        let impl_substs = self.infcx.fresh_substs_for_item(obligation.param_env.universe,
+                                                           obligation.cause.span,
                                                            impl_def_id);
 
         let impl_trait_ref = impl_trait_ref.subst(self.tcx(),
@@ -3210,7 +3211,7 @@ impl<'cx, 'gcx, 'tcx> SelectionContext<'cx, 'gcx, 'tcx> {
                                  def_id: DefId, // of impl or trait
                                  substs: &Substs<'tcx>, // for impl or trait
                                  skol_map: infer::SkolemizationMap<'tcx>,
-                                 snapshot: &infer::CombinedSnapshot)
+                                 snapshot: &infer::CombinedSnapshot<'cx, 'tcx>)
                                  -> Vec<PredicateObligation<'tcx>>
     {
         debug!("impl_or_trait_obligations(def_id={:?})", def_id);
diff --git a/src/librustc/traits/specialize/mod.rs b/src/librustc/traits/specialize/mod.rs
index d8d0715ff3957..5f2136ef9c8cf 100644
--- a/src/librustc/traits/specialize/mod.rs
+++ b/src/librustc/traits/specialize/mod.rs
@@ -217,7 +217,7 @@ fn fulfill_implication<'a, 'gcx, 'tcx>(infcx: &InferCtxt<'a, 'gcx, 'tcx>,
                                        target_impl: DefId)
                                        -> Result<&'tcx Substs<'tcx>, ()> {
     let selcx = &mut SelectionContext::new(&infcx);
-    let target_substs = infcx.fresh_substs_for_item(DUMMY_SP, target_impl);
+    let target_substs = infcx.fresh_substs_for_item(param_env.universe, DUMMY_SP, target_impl);
     let (target_trait_ref, mut obligations) = impl_trait_ref_and_oblig(selcx,
                                                                        param_env,
                                                                        target_impl,
diff --git a/src/librustc/ty/error.rs b/src/librustc/ty/error.rs
index 5cfa72c07126f..7b46525544bfd 100644
--- a/src/librustc/ty/error.rs
+++ b/src/librustc/ty/error.rs
@@ -9,9 +9,8 @@
 // except according to those terms.
 
 use hir::def_id::DefId;
-use infer::type_variable;
 use middle::const_val::ConstVal;
-use ty::{self, BoundRegion, DefIdTree, Region, Ty, TyCtxt};
+use ty::{self, BoundRegion, Region, Ty, TyCtxt};
 
 use std::fmt;
 use syntax::abi;
@@ -52,7 +51,6 @@ pub enum TypeError<'tcx> {
     CyclicTy,
     ProjectionMismatched(ExpectedFound<DefId>),
     ProjectionBoundsLength(ExpectedFound<usize>),
-    TyParamDefaultMismatch(ExpectedFound<type_variable::Default<'tcx>>),
     ExistentialMismatch(ExpectedFound<&'tcx ty::Slice<ty::ExistentialPredicate<'tcx>>>),
 }
 
@@ -161,11 +159,6 @@ impl<'tcx> fmt::Display for TypeError<'tcx> {
                        values.expected,
                        values.found)
             },
-            TyParamDefaultMismatch(ref values) => {
-                write!(f, "conflicting type parameter defaults `{}` and `{}`",
-                       values.expected.ty,
-                       values.found.ty)
-            }
             ExistentialMismatch(ref values) => {
                 report_maybe_different(f, format!("trait `{}`", values.expected),
                                        format!("trait `{}`", values.found))
@@ -257,42 +250,6 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
                         "consider boxing your closure and/or using it as a trait object");
                 }
             },
-            TyParamDefaultMismatch(values) => {
-                let expected = values.expected;
-                let found = values.found;
-                db.span_note(sp, &format!("conflicting type parameter defaults `{}` and `{}`",
-                                          expected.ty,
-                                          found.ty));
-
-                match self.hir.span_if_local(expected.def_id) {
-                    Some(span) => {
-                        db.span_note(span, "a default was defined here...");
-                    }
-                    None => {
-                        let item_def_id = self.parent(expected.def_id).unwrap();
-                        db.note(&format!("a default is defined on `{}`",
-                                         self.item_path_str(item_def_id)));
-                    }
-                }
-
-                db.span_note(
-                    expected.origin_span,
-                    "...that was applied to an unconstrained type variable here");
-
-                match self.hir.span_if_local(found.def_id) {
-                    Some(span) => {
-                        db.span_note(span, "a second default was defined here...");
-                    }
-                    None => {
-                        let item_def_id = self.parent(found.def_id).unwrap();
-                        db.note(&format!("a second default is defined on `{}`",
-                                         self.item_path_str(item_def_id)));
-                    }
-                }
-
-                db.span_note(found.origin_span,
-                             "...that also applies to the same type variable here");
-            }
             _ => {}
         }
     }
diff --git a/src/librustc/ty/mod.rs b/src/librustc/ty/mod.rs
index 0deababd21829..af2bb1b1e7fab 100644
--- a/src/librustc/ty/mod.rs
+++ b/src/librustc/ty/mod.rs
@@ -68,7 +68,7 @@ pub use self::sty::{ExistentialTraitRef, PolyExistentialTraitRef};
 pub use self::sty::{ExistentialProjection, PolyExistentialProjection, Const};
 pub use self::sty::{BoundRegion, EarlyBoundRegion, FreeRegion, Region};
 pub use self::sty::RegionKind;
-pub use self::sty::{TyVid, IntVid, FloatVid, RegionVid, SkolemizedRegionVid};
+pub use self::sty::{TyVid, IntVid, FloatVid, RegionVid};
 pub use self::sty::BoundRegion::*;
 pub use self::sty::InferTy::*;
 pub use self::sty::RegionKind::*;
@@ -655,12 +655,15 @@ pub struct ClosureUpvar<'tcx> {
     pub ty: Ty<'tcx>,
 }
 
-#[derive(Clone, Copy, PartialEq)]
+#[derive(Clone, Copy, PartialEq, Eq)]
 pub enum IntVarValue {
     IntType(ast::IntTy),
     UintType(ast::UintTy),
 }
 
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct FloatVarValue(pub ast::FloatTy);
+
 #[derive(Copy, Clone, RustcEncodable, RustcDecodable)]
 pub struct TypeParameterDef {
     pub name: Name,
@@ -1236,6 +1239,85 @@ impl<'tcx> InstantiatedPredicates<'tcx> {
     }
 }
 
+/// "Universes" are used during type- and trait-checking in the
+/// presence of `for<..>` binders to control what sets of names are
+/// visible. Universes are arranged into a tree: the root universe
+/// contains names that are always visible. But when you enter into
+/// some subuniverse, then it may add names that are only visible
+/// within that subtree (but it can still name the names of its
+/// ancestor universes).
+///
+/// To make this more concrete, consider this program:
+///
+/// ```
+/// struct Foo { }
+/// fn bar<T>(x: T) {
+///   let y: for<'a> fn(&'a u8, Foo) = ...;
+/// }
+/// ```
+///
+/// The struct name `Foo` is in the root universe U0. But the type
+/// parameter `T`, introduced on `bar`, is in a subuniverse U1 --
+/// i.e., within `bar`, we can name both `T` and `Foo`, but outside of
+/// `bar`, we cannot name `T`. Then, within the type of `y`, the
+/// region `'a` is in a subuniverse U2 of U1, because we can name it
+/// inside the fn type but not outside.
+///
+/// Universes are related to **skolemization** -- which is a way of
+/// doing type- and trait-checking around these "forall" binders (also
+/// called **universal quantification**). The idea is that when, in
+/// the body of `bar`, we refer to `T` as a type, we aren't referring
+/// to any type in particular, but rather a kind of "fresh" type that
+/// is distinct from all other types we have actually declared. This
+/// is called a **skolemized** type, and we use universes to talk
+/// about this. In other words, a type name in universe 0 always
+/// corresponds to some "ground" type that the user declared, but a
+/// type name in a non-zero universe is a skolemized type -- an
+/// idealized representative of "types in general" that we use for
+/// checking generic functions.
+#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, RustcEncodable, RustcDecodable)]
+pub struct UniverseIndex(u32);
+
+impl UniverseIndex {
+    /// The root universe, where things that the user defined are
+    /// visible.
+    pub const ROOT: UniverseIndex = UniverseIndex(0);
+
+    /// A "subuniverse" corresponds to being inside a `forall` quantifier.
+    /// So, for example, suppose we have this type in universe `U`:
+    ///
+    /// ```
+    /// for<'a> fn(&'a u32)
+    /// ```
+    ///
+    /// Once we "enter" into this `for<'a>` quantifier, we are in a
+    /// subuniverse of `U` -- in this new universe, we can name the
+    /// region `'a`, but that region was not nameable from `U` because
+    /// it was not in scope there.
+    pub fn subuniverse(self) -> UniverseIndex {
+        UniverseIndex(self.0.checked_add(1).unwrap())
+    }
+
+    pub fn from(v: u32) -> UniverseIndex {
+        UniverseIndex(v)
+    }
+
+    pub fn as_u32(&self) -> u32 {
+        self.0
+    }
+
+    pub fn as_usize(&self) -> usize {
+        self.0 as usize
+    }
+
+    /// Gets the "depth" of this universe in the universe tree. This
+    /// is not really useful except for e.g. the `HashStable`
+    /// implementation
+    pub fn depth(&self) -> u32 {
+        self.0
+    }
+}
+
 /// When type checking, we use the `ParamEnv` to track
 /// details about the set of where-clauses that are in scope at this
 /// particular point.
@@ -1250,6 +1332,17 @@ pub struct ParamEnv<'tcx> {
     /// want `Reveal::All` -- note that this is always paired with an
     /// empty environment. To get that, use `ParamEnv::reveal()`.
     pub reveal: traits::Reveal,
+
+    /// What is the innermost universe we have created? Starts out as
+    /// `UniverseIndex::root()` but grows from there as we enter
+    /// universal quantifiers.
+    ///
+    /// NB: At present, we exclude the universal quantifiers on the
+    /// item we are type-checking, and just consider those names as
+    /// part of the root universe. So this would only get incremented
+    /// when we enter into a higher-ranked (`for<..>`) type or trait
+    /// bound.
+    pub universe: UniverseIndex,
 }
 
 impl<'tcx> ParamEnv<'tcx> {
@@ -2565,7 +2658,8 @@ fn param_env<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     // sure that this will succeed without errors anyway.
 
     let unnormalized_env = ty::ParamEnv::new(tcx.intern_predicates(&predicates),
-                                             traits::Reveal::UserFacing);
+                                             traits::Reveal::UserFacing,
+                                             ty::UniverseIndex::ROOT);
 
     let body_id = tcx.hir.as_local_node_id(def_id).map_or(DUMMY_NODE_ID, |id| {
         tcx.hir.maybe_body_owned_by(id).map_or(id, |body| body.node_id)
diff --git a/src/librustc/ty/structural_impls.rs b/src/librustc/ty/structural_impls.rs
index 5f1448cd1f18e..15257fc5a277e 100644
--- a/src/librustc/ty/structural_impls.rs
+++ b/src/librustc/ty/structural_impls.rs
@@ -8,7 +8,6 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-use infer::type_variable;
 use middle::const_val::{self, ConstVal, ConstAggregate, ConstEvalErr};
 use ty::{self, Lift, Ty, TyCtxt};
 use ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
@@ -239,6 +238,7 @@ impl<'a, 'tcx> Lift<'tcx> for ty::ParamEnv<'a> {
         tcx.lift(&self.caller_bounds).map(|caller_bounds| {
             ty::ParamEnv {
                 reveal: self.reveal,
+                universe: self.universe,
                 caller_bounds,
             }
         })
@@ -381,19 +381,6 @@ impl<'tcx, T: Lift<'tcx>> Lift<'tcx> for ty::error::ExpectedFound<T> {
     }
 }
 
-impl<'a, 'tcx> Lift<'tcx> for type_variable::Default<'a> {
-    type Lifted = type_variable::Default<'tcx>;
-    fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
-        tcx.lift(&self.ty).map(|ty| {
-            type_variable::Default {
-                ty,
-                origin_span: self.origin_span,
-                def_id: self.def_id
-            }
-        })
-    }
-}
-
 impl<'a, 'tcx> Lift<'tcx> for ty::error::TypeError<'a> {
     type Lifted = ty::error::TypeError<'tcx>;
     fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
@@ -425,9 +412,6 @@ impl<'a, 'tcx> Lift<'tcx> for ty::error::TypeError<'a> {
             ProjectionBoundsLength(x) => ProjectionBoundsLength(x),
 
             Sorts(ref x) => return tcx.lift(x).map(Sorts),
-            TyParamDefaultMismatch(ref x) => {
-                return tcx.lift(x).map(TyParamDefaultMismatch)
-            }
             ExistentialMismatch(ref x) => return tcx.lift(x).map(ExistentialMismatch)
         })
     }
@@ -601,12 +585,23 @@ impl<'tcx> TypeFoldable<'tcx> for ty::ParamEnv<'tcx> {
         ty::ParamEnv {
             reveal: self.reveal,
             caller_bounds: self.caller_bounds.fold_with(folder),
+            universe: self.universe.fold_with(folder),
         }
     }
 
     fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
-        let &ty::ParamEnv { reveal: _, ref caller_bounds } = self;
-        caller_bounds.super_visit_with(visitor)
+        let &ty::ParamEnv { reveal: _, ref universe, ref caller_bounds } = self;
+        universe.super_visit_with(visitor) || caller_bounds.super_visit_with(visitor)
+    }
+}
+
+impl<'tcx> TypeFoldable<'tcx> for ty::UniverseIndex {
+    fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, _folder: &mut F) -> Self {
+        *self
+    }
+
+    fn super_visit_with<V: TypeVisitor<'tcx>>(&self, _visitor: &mut V) -> bool {
+        false
     }
 }
 
@@ -1119,20 +1114,6 @@ impl<'tcx, T: TypeFoldable<'tcx>> TypeFoldable<'tcx> for ty::error::ExpectedFoun
     }
 }
 
-impl<'tcx> TypeFoldable<'tcx> for type_variable::Default<'tcx> {
-    fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
-        type_variable::Default {
-            ty: self.ty.fold_with(folder),
-            origin_span: self.origin_span,
-            def_id: self.def_id
-        }
-    }
-
-    fn super_visit_with<V: TypeVisitor<'tcx>>(&self, visitor: &mut V) -> bool {
-        self.ty.visit_with(visitor)
-    }
-}
-
 impl<'tcx, T: TypeFoldable<'tcx>, I: Idx> TypeFoldable<'tcx> for IndexVec<I, T> {
     fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
         self.iter().map(|x| x.fold_with(folder)).collect()
@@ -1172,7 +1153,6 @@ impl<'tcx> TypeFoldable<'tcx> for ty::error::TypeError<'tcx> {
             ProjectionMismatched(x) => ProjectionMismatched(x),
             ProjectionBoundsLength(x) => ProjectionBoundsLength(x),
             Sorts(x) => Sorts(x.fold_with(folder)),
-            TyParamDefaultMismatch(ref x) => TyParamDefaultMismatch(x.fold_with(folder)),
             ExistentialMismatch(x) => ExistentialMismatch(x.fold_with(folder)),
         }
     }
@@ -1191,7 +1171,6 @@ impl<'tcx> TypeFoldable<'tcx> for ty::error::TypeError<'tcx> {
                 b.visit_with(visitor)
             },
             Sorts(x) => x.visit_with(visitor),
-            TyParamDefaultMismatch(ref x) => x.visit_with(visitor),
             ExistentialMismatch(x) => x.visit_with(visitor),
             Mismatch |
             Mutability |
diff --git a/src/librustc/ty/sty.rs b/src/librustc/ty/sty.rs
index d0ac7d0183a58..c1328552ccb4e 100644
--- a/src/librustc/ty/sty.rs
+++ b/src/librustc/ty/sty.rs
@@ -854,7 +854,7 @@ pub enum RegionKind {
 
     /// A skolemized region - basically the higher-ranked version of ReFree.
     /// Should not exist after typeck.
-    ReSkolemized(SkolemizedRegionVid, BoundRegion),
+    ReSkolemized(ty::UniverseIndex, BoundRegion),
 
     /// Empty lifetime is for data that is never accessed.
     /// Bottom in the region lattice. We treat ReEmpty somewhat
@@ -898,11 +898,6 @@ pub struct RegionVid {
     pub index: u32,
 }
 
-#[derive(Clone, Copy, PartialEq, Eq, Hash, RustcEncodable, RustcDecodable)]
-pub struct SkolemizedRegionVid {
-    pub index: u32,
-}
-
 #[derive(Clone, Copy, PartialEq, Eq, Hash, RustcEncodable, RustcDecodable)]
 pub enum InferTy {
     TyVar(TyVid),
diff --git a/src/librustc/ty/util.rs b/src/librustc/ty/util.rs
index 39842a543b54b..2a7b0fb20e9fa 100644
--- a/src/librustc/ty/util.rs
+++ b/src/librustc/ty/util.rs
@@ -153,14 +153,15 @@ impl<'tcx> ty::ParamEnv<'tcx> {
     /// Construct a trait environment suitable for contexts where
     /// there are no where clauses in scope.
     pub fn empty(reveal: Reveal) -> Self {
-        Self::new(ty::Slice::empty(), reveal)
+        Self::new(ty::Slice::empty(), reveal, ty::UniverseIndex::ROOT)
     }
 
     /// Construct a trait environment with the given set of predicates.
     pub fn new(caller_bounds: &'tcx ty::Slice<ty::Predicate<'tcx>>,
-               reveal: Reveal)
+               reveal: Reveal,
+               universe: ty::UniverseIndex)
                -> Self {
-        ty::ParamEnv { caller_bounds, reveal }
+        ty::ParamEnv { caller_bounds, reveal, universe }
     }
 
     /// Returns a new parameter environment with the same clauses, but
diff --git a/src/librustc/util/ppaux.rs b/src/librustc/util/ppaux.rs
index acb929981fbf2..ba147443a71dc 100644
--- a/src/librustc/util/ppaux.rs
+++ b/src/librustc/util/ppaux.rs
@@ -762,7 +762,7 @@ define_print! {
                 }
 
                 ty::ReSkolemized(id, ref bound_region) => {
-                    write!(f, "ReSkolemized({}, {:?})", id.index, bound_region)
+                    write!(f, "ReSkolemized({:?}, {:?})", id, bound_region)
                 }
 
                 ty::ReEmpty => write!(f, "ReEmpty"),
@@ -888,6 +888,12 @@ impl fmt::Debug for ty::IntVarValue {
     }
 }
 
+impl fmt::Debug for ty::FloatVarValue {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        self.0.fmt(f)
+    }
+}
+
 // The generic impl doesn't work yet because projections are not
 // normalized under HRTB.
 /*impl<T> fmt::Display for ty::Binder<T>
diff --git a/src/librustc_data_structures/Cargo.toml b/src/librustc_data_structures/Cargo.toml
index 343b1ed68b804..381b89a238fd6 100644
--- a/src/librustc_data_structures/Cargo.toml
+++ b/src/librustc_data_structures/Cargo.toml
@@ -9,5 +9,6 @@ path = "lib.rs"
 crate-type = ["dylib"]
 
 [dependencies]
+ena = "0.8.0"
 log = "0.3"
 serialize = { path = "../libserialize" }
diff --git a/src/librustc_data_structures/lib.rs b/src/librustc_data_structures/lib.rs
index 3a20343033c23..e32ab10de4824 100644
--- a/src/librustc_data_structures/lib.rs
+++ b/src/librustc_data_structures/lib.rs
@@ -36,6 +36,7 @@
 #![cfg_attr(test, feature(test))]
 
 extern crate core;
+extern crate ena;
 #[macro_use]
 extern crate log;
 extern crate serialize as rustc_serialize; // used by deriving
@@ -57,10 +58,10 @@ pub mod indexed_vec;
 pub mod obligation_forest;
 pub mod sip128;
 pub mod snapshot_map;
-pub mod snapshot_vec;
+pub use ena::snapshot_vec;
 pub mod stable_hasher;
 pub mod transitive_relation;
-pub mod unify;
+pub use ena::unify;
 pub mod fx;
 pub mod tuple_slice;
 pub mod veccell;
diff --git a/src/librustc_driver/test.rs b/src/librustc_driver/test.rs
index 5ff75351b635b..201b6e40b0426 100644
--- a/src/librustc_driver/test.rs
+++ b/src/librustc_driver/test.rs
@@ -503,7 +503,8 @@ fn sub_free_bound_false_infer() {
     //! does NOT hold for any instantiation of `_#1`.
 
     test_env(EMPTY_SOURCE_STR, errors(&[]), |env| {
-        let t_infer1 = env.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
+        let t_infer1 = env.infcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                             TypeVariableOrigin::MiscVariable(DUMMY_SP));
         let t_rptr_bound1 = env.t_rptr_late_bound(1);
         env.check_not_sub(env.t_fn(&[t_infer1], env.tcx().types.isize),
                           env.t_fn(&[t_rptr_bound1], env.tcx().types.isize));
@@ -522,7 +523,8 @@ fn lub_free_bound_infer() {
 
     test_env(EMPTY_SOURCE_STR, errors(&[]), |mut env| {
         env.create_simple_region_hierarchy();
-        let t_infer1 = env.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
+        let t_infer1 = env.infcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                             TypeVariableOrigin::MiscVariable(DUMMY_SP));
         let t_rptr_bound1 = env.t_rptr_late_bound(1);
         let t_rptr_free1 = env.t_rptr_free(1);
         env.check_lub(env.t_fn(&[t_infer1], env.tcx().types.isize),
@@ -642,7 +644,8 @@ fn glb_bound_free() {
 fn glb_bound_free_infer() {
     test_env(EMPTY_SOURCE_STR, errors(&[]), |env| {
         let t_rptr_bound1 = env.t_rptr_late_bound(1);
-        let t_infer1 = env.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
+        let t_infer1 = env.infcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                             TypeVariableOrigin::MiscVariable(DUMMY_SP));
 
         // compute GLB(fn(_) -> isize, for<'b> fn(&'b isize) -> isize),
         // which should yield for<'b> fn(&'b isize) -> isize
diff --git a/src/librustc_typeck/astconv.rs b/src/librustc_typeck/astconv.rs
index 1471e235156eb..bbde41a3f4d83 100644
--- a/src/librustc_typeck/astconv.rs
+++ b/src/librustc_typeck/astconv.rs
@@ -19,7 +19,7 @@ use hir::def::Def;
 use hir::def_id::DefId;
 use middle::resolve_lifetime as rl;
 use namespace::Namespace;
-use rustc::ty::subst::{Kind, Subst, Substs};
+use rustc::ty::subst::{Subst, Substs};
 use rustc::traits;
 use rustc::ty::{self, Ty, TyCtxt, ToPredicate, TypeFoldable};
 use rustc::ty::wf::object_region_bounds;
@@ -51,7 +51,6 @@ pub trait AstConv<'gcx, 'tcx> {
     /// Same as ty_infer, but with a known type parameter definition.
     fn ty_infer_for_def(&self,
                         _def: &ty::TypeParameterDef,
-                        _substs: &[Kind<'tcx>],
                         span: Span) -> Ty<'tcx> {
         self.ty_infer(span)
     }
@@ -250,7 +249,7 @@ impl<'o, 'gcx: 'tcx, 'tcx> AstConv<'gcx, 'tcx>+'o {
             } else if infer_types {
                 // No type parameters were provided, we can infer all.
                 let ty_var = if !default_needs_object_self(def) {
-                    self.ty_infer_for_def(def, substs, span)
+                    self.ty_infer_for_def(def, span)
                 } else {
                     self.ty_infer(span)
                 };
diff --git a/src/librustc_typeck/check/_match.rs b/src/librustc_typeck/check/_match.rs
index 272f13b28030e..2fbdc3c236ede 100644
--- a/src/librustc_typeck/check/_match.rs
+++ b/src/librustc_typeck/check/_match.rs
@@ -285,6 +285,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 let element_tys_iter = (0..max_len).map(|_| self.next_ty_var(
                     // FIXME: MiscVariable for now, obtaining the span and name information
                     //       from all tuple elements isn't trivial.
+                    ty::UniverseIndex::ROOT,
                     TypeVariableOrigin::TypeInference(pat.span)));
                 let element_tys = tcx.mk_type_list(element_tys_iter);
                 let pat_ty = tcx.mk_ty(ty::TyTuple(element_tys, false));
@@ -295,7 +296,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 pat_ty
             }
             PatKind::Box(ref inner) => {
-                let inner_ty = self.next_ty_var(TypeVariableOrigin::TypeInference(inner.span));
+                let inner_ty = self.next_ty_var(ty::UniverseIndex::ROOT,
+                                                TypeVariableOrigin::TypeInference(inner.span));
                 let uniq_ty = tcx.mk_box(inner_ty);
 
                 if self.check_dereferencable(pat.span, expected, &inner) {
@@ -328,6 +330,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                         }
                         _ => {
                             let inner_ty = self.next_ty_var(
+                                ty::UniverseIndex::ROOT,
                                 TypeVariableOrigin::TypeInference(inner.span));
                             let mt = ty::TypeAndMut { ty: inner_ty, mutbl: mutbl };
                             let region = self.next_region_var(infer::PatternRegion(pat.span));
@@ -571,7 +574,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
             // ...but otherwise we want to use any supertype of the
             // discriminant. This is sort of a workaround, see note (*) in
             // `check_pat` for some details.
-            discrim_ty = self.next_ty_var(TypeVariableOrigin::TypeInference(discrim.span));
+            discrim_ty = self.next_ty_var(ty::UniverseIndex::ROOT,
+                                          TypeVariableOrigin::TypeInference(discrim.span));
             self.check_expr_has_type_or_error(discrim, discrim_ty);
         };
 
@@ -632,7 +636,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 // arm for inconsistent arms or to the whole match when a `()` type
                 // is required).
                 Expectation::ExpectHasType(ety) if ety != self.tcx.mk_nil() => ety,
-                _ => self.next_ty_var(TypeVariableOrigin::MiscVariable(expr.span)),
+                _ => self.next_ty_var(ty::UniverseIndex::ROOT,
+                                      TypeVariableOrigin::MiscVariable(expr.span)),
             };
             CoerceMany::with_coercion_sites(coerce_first, arms)
         };
diff --git a/src/librustc_typeck/check/closure.rs b/src/librustc_typeck/check/closure.rs
index d475fb0cf1a14..f7a086c160b64 100644
--- a/src/librustc_typeck/check/closure.rs
+++ b/src/librustc_typeck/check/closure.rs
@@ -100,7 +100,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
             |_, _| span_bug!(expr.span, "closure has region param"),
             |_, _| {
                 self.infcx
-                    .next_ty_var(TypeVariableOrigin::TransformedUpvar(expr.span))
+                    .next_ty_var(ty::UniverseIndex::ROOT,
+                                 TypeVariableOrigin::TransformedUpvar(expr.span))
             },
         );
         let closure_type = self.tcx.mk_closure(expr_def_id, substs);
diff --git a/src/librustc_typeck/check/coercion.rs b/src/librustc_typeck/check/coercion.rs
index 94422f93e5922..3941b3c8f1b5a 100644
--- a/src/librustc_typeck/check/coercion.rs
+++ b/src/librustc_typeck/check/coercion.rs
@@ -179,6 +179,7 @@ impl<'f, 'gcx, 'tcx> Coerce<'f, 'gcx, 'tcx> {
                 // micro-optimization: no need for this if `b` is
                 // already resolved in some way.
                 let diverging_ty = self.next_diverging_ty_var(
+                    ty::UniverseIndex::ROOT,
                     TypeVariableOrigin::AdjustmentType(self.cause.span));
                 self.unify_and(&b, &diverging_ty, simple(Adjust::NeverToAny))
             } else {
@@ -497,7 +498,7 @@ impl<'f, 'gcx, 'tcx> Coerce<'f, 'gcx, 'tcx> {
         // We only have the latter, so we use an inference variable
         // for the former and let type inference do the rest.
         let origin = TypeVariableOrigin::MiscVariable(self.cause.span);
-        let coerce_target = self.next_ty_var(origin);
+        let coerce_target = self.next_ty_var(ty::UniverseIndex::ROOT, origin);
         let mut coercion = self.unify_and(coerce_target, target, |target| {
             let unsize = Adjustment {
                 kind: Adjust::Unsize,
diff --git a/src/librustc_typeck/check/compare_method.rs b/src/librustc_typeck/check/compare_method.rs
index 554a858bcc173..d6c0156cbfec2 100644
--- a/src/librustc_typeck/check/compare_method.rs
+++ b/src/librustc_typeck/check/compare_method.rs
@@ -213,7 +213,8 @@ fn compare_predicate_entailment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
     // the new hybrid bounds we computed.
     let normalize_cause = traits::ObligationCause::misc(impl_m_span, impl_m_node_id);
     let param_env = ty::ParamEnv::new(tcx.intern_predicates(&hybrid_preds.predicates),
-                                      Reveal::UserFacing);
+                                      Reveal::UserFacing,
+                                      ty::UniverseIndex::ROOT);
     let param_env = traits::normalize_param_env_or_error(tcx,
                                                          impl_m.def_id,
                                                          param_env,
diff --git a/src/librustc_typeck/check/dropck.rs b/src/librustc_typeck/check/dropck.rs
index 610d07efa359d..0a5f3c76aec98 100644
--- a/src/librustc_typeck/check/dropck.rs
+++ b/src/librustc_typeck/check/dropck.rs
@@ -88,7 +88,7 @@ fn ensure_drop_params_and_item_params_correspond<'a, 'tcx>(
 
         let drop_impl_span = tcx.def_span(drop_impl_did);
         let fresh_impl_substs =
-            infcx.fresh_substs_for_item(drop_impl_span, drop_impl_did);
+            infcx.fresh_substs_for_item(ty::UniverseIndex::ROOT, drop_impl_span, drop_impl_did);
         let fresh_impl_self_ty = drop_impl_ty.subst(tcx, fresh_impl_substs);
 
         let cause = &ObligationCause::misc(drop_impl_span, drop_impl_node_id);
diff --git a/src/librustc_typeck/check/method/confirm.rs b/src/librustc_typeck/check/method/confirm.rs
index a9830dd5ddece..b6b39a807563a 100644
--- a/src/librustc_typeck/check/method/confirm.rs
+++ b/src/librustc_typeck/check/method/confirm.rs
@@ -240,7 +240,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
                 // the process we will unify the transformed-self-type
                 // of the method with the actual type in order to
                 // unify some of these variables.
-                self.fresh_substs_for_item(self.span, trait_def_id)
+                self.fresh_substs_for_item(ty::UniverseIndex::ROOT, self.span, trait_def_id)
             }
 
             probe::WhereClausePick(ref poly_trait_ref) => {
@@ -305,7 +305,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
             } else {
                 self.region_var_for_def(self.span, def)
             }
-        }, |def, cur_substs| {
+        }, |def, _cur_substs| {
             let i = def.index as usize;
             if i < parent_substs.len() {
                 parent_substs.type_at(i)
@@ -316,7 +316,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
             {
                 self.to_ty(ast_ty)
             } else {
-                self.type_var_for_def(self.span, def, cur_substs)
+                self.type_var_for_def(ty::UniverseIndex::ROOT, self.span, def)
             }
         })
     }
diff --git a/src/librustc_typeck/check/method/mod.rs b/src/librustc_typeck/check/method/mod.rs
index 58d72e37d51cf..af86570309dfd 100644
--- a/src/librustc_typeck/check/method/mod.rs
+++ b/src/librustc_typeck/check/method/mod.rs
@@ -249,13 +249,13 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         let substs = Substs::for_item(self.tcx,
                                       trait_def_id,
                                       |def, _| self.region_var_for_def(span, def),
-                                      |def, substs| {
+                                      |def, _substs| {
             if def.index == 0 {
                 self_ty
             } else if let Some(ref input_types) = opt_input_types {
                 input_types[def.index as usize - 1]
             } else {
-                self.type_var_for_def(span, def, substs)
+                self.type_var_for_def(ty::UniverseIndex::ROOT, span, def)
             }
         });
 
diff --git a/src/librustc_typeck/check/method/probe.rs b/src/librustc_typeck/check/method/probe.rs
index 81e5b2fe00a6a..646867283e23b 100644
--- a/src/librustc_typeck/check/method/probe.rs
+++ b/src/librustc_typeck/check/method/probe.rs
@@ -693,7 +693,9 @@ impl<'a, 'gcx, 'tcx> ProbeContext<'a, 'gcx, 'tcx> {
             Def::Method(def_id) => {
                 let fty = self.tcx.fn_sig(def_id);
                 self.probe(|_| {
-                    let substs = self.fresh_substs_for_item(self.span, method.def_id);
+                    let substs = self.fresh_substs_for_item(ty::UniverseIndex::ROOT,
+                                                            self.span,
+                                                            method.def_id);
                     let fty = fty.subst(self.tcx, substs);
                     let (fty, _) = self.replace_late_bound_regions_with_fresh_var(
                         self.span, infer::FnCall, &fty);
@@ -1265,12 +1267,12 @@ impl<'a, 'gcx, 'tcx> ProbeContext<'a, 'gcx, 'tcx> {
                     // `impl_self_ty()` for an explanation.
                     self.tcx.types.re_erased
                 }
-            }, |def, cur_substs| {
+            }, |def, _cur_substs| {
                 let i = def.index as usize;
                 if i < substs.len() {
                     substs.type_at(i)
                 } else {
-                    self.type_var_for_def(self.span, def, cur_substs)
+                    self.type_var_for_def(ty::UniverseIndex::ROOT, self.span, def)
                 }
             });
             xform_fn_sig.subst(self.tcx, substs)
@@ -1287,6 +1289,7 @@ impl<'a, 'gcx, 'tcx> ProbeContext<'a, 'gcx, 'tcx> {
                          def_id,
                          |_, _| self.tcx.types.re_erased,
                          |_, _| self.next_ty_var(
+                             ty::UniverseIndex::ROOT,
                              TypeVariableOrigin::SubstitutionPlaceholder(
                                  self.tcx.def_span(def_id))))
     }
diff --git a/src/librustc_typeck/check/method/suggest.rs b/src/librustc_typeck/check/method/suggest.rs
index 8613ec86b4a73..bdb56b7da94e6 100644
--- a/src/librustc_typeck/check/method/suggest.rs
+++ b/src/librustc_typeck/check/method/suggest.rs
@@ -54,7 +54,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 self.autoderef(span, ty).any(|(ty, _)| {
                     self.probe(|_| {
                         let fn_once_substs = tcx.mk_substs_trait(ty,
-                            &[self.next_ty_var(TypeVariableOrigin::MiscVariable(span))]);
+                            &[self.next_ty_var(ty::UniverseIndex::ROOT,
+                                               TypeVariableOrigin::MiscVariable(span))]);
                         let trait_ref = ty::TraitRef::new(fn_once, fn_once_substs);
                         let poly_trait_ref = trait_ref.to_poly_trait_ref();
                         let obligation =
diff --git a/src/librustc_typeck/check/mod.rs b/src/librustc_typeck/check/mod.rs
index 82d59ecfc92cf..a1f2a0f3a5461 100644
--- a/src/librustc_typeck/check/mod.rs
+++ b/src/librustc_typeck/check/mod.rs
@@ -92,7 +92,7 @@ use namespace::Namespace;
 use rustc::infer::{self, InferCtxt, InferOk, RegionVariableOrigin};
 use rustc::infer::type_variable::{TypeVariableOrigin};
 use rustc::middle::region;
-use rustc::ty::subst::{Kind, Subst, Substs};
+use rustc::ty::subst::{Subst, Substs};
 use rustc::traits::{self, FulfillmentContext, ObligationCause, ObligationCauseCode};
 use rustc::ty::{ParamTy, LvaluePreference, NoPreference, PreferMutLvalue};
 use rustc::ty::{self, Ty, TyCtxt, Visibility};
@@ -360,7 +360,8 @@ impl<'a, 'gcx, 'tcx> Expectation<'tcx> {
     /// hard constraint exists, creates a fresh type variable.
     fn coercion_target_type(self, fcx: &FnCtxt<'a, 'gcx, 'tcx>, span: Span) -> Ty<'tcx> {
         self.only_has_type(fcx)
-            .unwrap_or_else(|| fcx.next_ty_var(TypeVariableOrigin::MiscVariable(span)))
+            .unwrap_or_else(|| fcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                               TypeVariableOrigin::MiscVariable(span)))
     }
 }
 
@@ -945,7 +946,8 @@ impl<'a, 'gcx, 'tcx> GatherLocalsVisitor<'a, 'gcx, 'tcx> {
         match ty_opt {
             None => {
                 // infer the variable's type
-                let var_ty = self.fcx.next_ty_var(TypeVariableOrigin::TypeInference(span));
+                let var_ty = self.fcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                                  TypeVariableOrigin::TypeInference(span));
                 self.fcx.locals.borrow_mut().insert(nid, var_ty);
                 var_ty
             }
@@ -1038,7 +1040,8 @@ fn check_fn<'a, 'gcx, 'tcx>(inherited: &'a Inherited<'a, 'gcx, 'tcx>,
     let span = body.value.span;
 
     if body.is_generator && can_be_generator {
-        fcx.yield_ty = Some(fcx.next_ty_var(TypeVariableOrigin::TypeInference(span)));
+        fcx.yield_ty = Some(fcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                            TypeVariableOrigin::TypeInference(span)));
     }
 
     GatherLocalsVisitor { fcx: &fcx, }.visit_body(body);
@@ -1068,7 +1071,8 @@ fn check_fn<'a, 'gcx, 'tcx>(inherited: &'a Inherited<'a, 'gcx, 'tcx>,
         };
         inherited.tables.borrow_mut().generator_sigs_mut().insert(fn_hir_id, Some(gen_sig));
 
-        let witness = fcx.next_ty_var(TypeVariableOrigin::MiscVariable(span));
+        let witness = fcx.next_ty_var(ty::UniverseIndex::ROOT,
+                                      TypeVariableOrigin::MiscVariable(span));
         fcx.deferred_generator_interiors.borrow_mut().push((body.id(), witness));
         let interior = ty::GeneratorInterior::new(witness);
 
@@ -1110,6 +1114,7 @@ fn check_fn<'a, 'gcx, 'tcx>(inherited: &'a Inherited<'a, 'gcx, 'tcx>,
     let mut actual_return_ty = coercion.complete(&fcx);
     if actual_return_ty.is_never() {
         actual_return_ty = fcx.next_diverging_ty_var(
+            ty::UniverseIndex::ROOT,
             TypeVariableOrigin::DivergingFn(span));
     }
     fcx.demand_suptype(span, ret_ty, actual_return_ty);
@@ -1647,14 +1652,14 @@ impl<'a, 'gcx, 'tcx> AstConv<'gcx, 'tcx> for FnCtxt<'a, 'gcx, 'tcx> {
     }
 
     fn ty_infer(&self, span: Span) -> Ty<'tcx> {
-        self.next_ty_var(TypeVariableOrigin::TypeInference(span))
+        self.next_ty_var(ty::UniverseIndex::ROOT,
+                         TypeVariableOrigin::TypeInference(span))
     }
 
     fn ty_infer_for_def(&self,
                         ty_param_def: &ty::TypeParameterDef,
-                        substs: &[Kind<'tcx>],
                         span: Span) -> Ty<'tcx> {
-        self.type_var_for_def(span, ty_param_def, substs)
+        self.type_var_for_def(ty::UniverseIndex::ROOT, span, ty_param_def)
     }
 
     fn projected_ty_from_poly_trait_ref(&self,
@@ -1945,7 +1950,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                     return ty_var;
                 }
                 let span = self.tcx.def_span(def_id);
-                let ty_var = self.next_ty_var(TypeVariableOrigin::TypeInference(span));
+                let ty_var = self.next_ty_var(ty::UniverseIndex::ROOT,
+                                              TypeVariableOrigin::TypeInference(span));
                 self.anon_types.borrow_mut().insert(id, ty_var);
 
                 let predicates_of = self.tcx.predicates_of(def_id);
@@ -2279,7 +2285,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
             // If some lookup succeeds, write callee into table and extract index/element
             // type from the method signature.
             // If some lookup succeeded, install method in table
-            let input_ty = self.next_ty_var(TypeVariableOrigin::AutoDeref(base_expr.span));
+            let input_ty = self.next_ty_var(ty::UniverseIndex::ROOT,
+                                            TypeVariableOrigin::AutoDeref(base_expr.span));
             let method = self.try_overloaded_lvalue_op(
                 expr.span, self_ty, &[input_ty], lvalue_pref, LvalueOp::Index);
 
@@ -2723,6 +2730,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
             assert!(!self.tables.borrow().adjustments().contains_key(expr.hir_id),
                     "expression with never type wound up being adjusted");
             let adj_ty = self.next_diverging_ty_var(
+                ty::UniverseIndex::ROOT,
                 TypeVariableOrigin::AdjustmentType(expr.span));
             self.apply_adjustments(expr, vec![Adjustment {
                 kind: Adjust::NeverToAny,
@@ -2801,7 +2809,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         let ity = self.tcx.type_of(did);
         debug!("impl_self_ty: ity={:?}", ity);
 
-        let substs = self.fresh_substs_for_item(span, did);
+        let substs = self.fresh_substs_for_item(ty::UniverseIndex::ROOT, span, did);
         let substd_ty = self.instantiate_type_scheme(span, &substs, &ity);
 
         TypeAndSubsts { substs: substs, ty: substd_ty }
@@ -3932,7 +3940,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
 
               let element_ty = if !args.is_empty() {
                   let coerce_to = uty.unwrap_or_else(
-                      || self.next_ty_var(TypeVariableOrigin::TypeInference(expr.span)));
+                      || self.next_ty_var(ty::UniverseIndex::ROOT,
+                                          TypeVariableOrigin::TypeInference(expr.span)));
                   let mut coerce = CoerceMany::with_coercion_sites(coerce_to, args);
                   assert_eq!(self.diverges.get(), Diverges::Maybe);
                   for e in args {
@@ -3942,7 +3951,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                   }
                   coerce.complete(self)
               } else {
-                  self.next_ty_var(TypeVariableOrigin::TypeInference(expr.span))
+                  self.next_ty_var(ty::UniverseIndex::ROOT,
+                                   TypeVariableOrigin::TypeInference(expr.span))
               };
               tcx.mk_array(element_ty, args.len() as u64)
           }
@@ -3972,7 +3982,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                     (uty, uty)
                 }
                 None => {
-                    let t: Ty = self.next_ty_var(TypeVariableOrigin::MiscVariable(element.span));
+                    let t: Ty = self.next_ty_var(ty::UniverseIndex::ROOT,
+                                                 TypeVariableOrigin::MiscVariable(element.span));
                     let element_ty = self.check_expr_has_type_or_error(&element, t);
                     (element_ty, t)
                 }
@@ -4747,7 +4758,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 // Handle Self first, so we can adjust the index to match the AST.
                 if has_self && i == 0 {
                     return opt_self_ty.unwrap_or_else(|| {
-                        self.type_var_for_def(span, def, substs)
+                        self.type_var_for_def(ty::UniverseIndex::ROOT, span, def)
                     });
                 }
                 i -= has_self as usize;
@@ -4780,7 +4791,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 // This can also be reached in some error cases:
                 // We prefer to use inference variables instead of
                 // TyError to let type inference recover somewhat.
-                self.type_var_for_def(span, def, substs)
+                self.type_var_for_def(ty::UniverseIndex::ROOT, span, def)
             }
         });
 
diff --git a/src/librustc_typeck/check/op.rs b/src/librustc_typeck/check/op.rs
index 2d45f797ecb4d..987fead48c474 100644
--- a/src/librustc_typeck/check/op.rs
+++ b/src/librustc_typeck/check/op.rs
@@ -175,8 +175,10 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         // trait matching creating lifetime constraints that are too strict.
         // E.g. adding `&'a T` and `&'b T`, given `&'x T: Add<&'x T>`, will result
         // in `&'a T <: &'x T` and `&'b T <: &'x T`, instead of `'a = 'b = 'x`.
-        let lhs_ty = self.check_expr_coercable_to_type_with_lvalue_pref(lhs_expr,
-            self.next_ty_var(TypeVariableOrigin::MiscVariable(lhs_expr.span)),
+        let lhs_ty = self.check_expr_coercable_to_type_with_lvalue_pref(
+            lhs_expr,
+            self.next_ty_var(ty::UniverseIndex::ROOT,
+                             TypeVariableOrigin::MiscVariable(lhs_expr.span)),
             lhs_pref);
         let lhs_ty = self.resolve_type_vars_with_obligations(lhs_ty);
 
@@ -186,7 +188,8 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         // using this variable as the expected type, which sometimes lets
         // us do better coercions than we would be able to do otherwise,
         // particularly for things like `String + &String`.
-        let rhs_ty_var = self.next_ty_var(TypeVariableOrigin::MiscVariable(rhs_expr.span));
+        let rhs_ty_var = self.next_ty_var(ty::UniverseIndex::ROOT,
+                         TypeVariableOrigin::MiscVariable(rhs_expr.span));
 
         let result = self.lookup_op_method(lhs_ty, &[rhs_ty_var], Op::Binary(op, is_assign));