diff --git a/src/librustc/middle/ty.rs b/src/librustc/middle/ty.rs
index c5e84b8e0c8..766cb06907e 100644
--- a/src/librustc/middle/ty.rs
+++ b/src/librustc/middle/ty.rs
@@ -850,17 +850,23 @@ impl CLike for BuiltinBound {
 }
 
 #[deriving(Clone, PartialEq, Eq, Hash)]
-pub struct TyVid(pub uint);
+pub struct TyVid {
+    pub index: uint
+}
 
 #[deriving(Clone, PartialEq, Eq, Hash)]
-pub struct IntVid(pub uint);
+pub struct IntVid {
+    pub index: uint
+}
 
 #[deriving(Clone, PartialEq, Eq, Hash)]
-pub struct FloatVid(pub uint);
+pub struct FloatVid {
+    pub index: uint
+}
 
 #[deriving(Clone, PartialEq, Eq, Encodable, Decodable, Hash)]
 pub struct RegionVid {
-    pub id: uint
+    pub index: uint
 }
 
 #[deriving(Clone, PartialEq, Eq, Hash)]
@@ -893,47 +899,27 @@ impl cmp::PartialEq for InferRegion {
     }
 }
 
-pub trait Vid {
-    fn to_uint(&self) -> uint;
-}
-
-impl Vid for TyVid {
-    fn to_uint(&self) -> uint { let TyVid(v) = *self; v }
-}
-
 impl fmt::Show for TyVid {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result{
-        write!(f, "<generic #{}>", self.to_uint())
+        write!(f, "<generic #{}>", self.index)
     }
 }
 
-impl Vid for IntVid {
-    fn to_uint(&self) -> uint { let IntVid(v) = *self; v }
-}
-
 impl fmt::Show for IntVid {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "<generic integer #{}>", self.to_uint())
+        write!(f, "<generic integer #{}>", self.index)
     }
 }
 
-impl Vid for FloatVid {
-    fn to_uint(&self) -> uint { let FloatVid(v) = *self; v }
-}
-
 impl fmt::Show for FloatVid {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        write!(f, "<generic float #{}>", self.to_uint())
+        write!(f, "<generic float #{}>", self.index)
     }
 }
 
-impl Vid for RegionVid {
-    fn to_uint(&self) -> uint { self.id }
-}
-
 impl fmt::Show for RegionVid {
     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
-        self.id.fmt(f)
+        write!(f, "'<generic lifetime #{}>", self.index)
     }
 }
 
diff --git a/src/librustc/middle/typeck/coherence.rs b/src/librustc/middle/typeck/coherence.rs
index b12e3b614d1..71bc2f0374c 100644
--- a/src/librustc/middle/typeck/coherence.rs
+++ b/src/librustc/middle/typeck/coherence.rs
@@ -519,7 +519,8 @@ impl<'a> CoherenceChecker<'a> {
     fn can_unify_universally_quantified<'a>(&self,
                                             a: &'a UniversalQuantificationResult,
                                             b: &'a UniversalQuantificationResult)
-                                            -> bool {
+                                            -> bool
+    {
         infer::can_mk_subty(&self.inference_context,
                             a.monotype,
                             b.monotype).is_ok()
diff --git a/src/librustc/middle/typeck/infer/coercion.rs b/src/librustc/middle/typeck/infer/coercion.rs
index 0568542472b..9317563da93 100644
--- a/src/librustc/middle/typeck/infer/coercion.rs
+++ b/src/librustc/middle/typeck/infer/coercion.rs
@@ -71,9 +71,9 @@ use middle::ty;
 use middle::typeck::infer::{CoerceResult, resolve_type, Coercion};
 use middle::typeck::infer::combine::{CombineFields, Combine};
 use middle::typeck::infer::sub::Sub;
-use middle::typeck::infer::to_str::InferStr;
 use middle::typeck::infer::resolve::try_resolve_tvar_shallow;
 use util::common::indenter;
+use util::ppaux::Repr;
 
 use syntax::abi;
 use syntax::ast::MutImmutable;
@@ -91,8 +91,8 @@ impl<'f> Coerce<'f> {
 
     pub fn tys(&self, a: ty::t, b: ty::t) -> CoerceResult {
         debug!("Coerce.tys({} => {})",
-               a.inf_str(self.get_ref().infcx),
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx),
+               b.repr(self.get_ref().infcx.tcx));
         let _indent = indenter();
 
         // Examine the supertype and consider auto-borrowing.
@@ -233,8 +233,8 @@ impl<'f> Coerce<'f> {
                                    mt_b: ty::mt)
                                    -> CoerceResult {
         debug!("coerce_borrowed_pointer(a={}, sty_a={:?}, b={}, mt_b={:?})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx), mt_b);
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx), mt_b);
 
         // If we have a parameter of type `&M T_a` and the value
         // provided is `expr`, we will be adding an implicit borrow,
@@ -270,8 +270,8 @@ impl<'f> Coerce<'f> {
                                   b: ty::t)
                                   -> CoerceResult {
         debug!("coerce_borrowed_string(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         match *sty_a {
             ty::ty_uniq(t) => match ty::get(t).sty {
@@ -300,8 +300,8 @@ impl<'f> Coerce<'f> {
                                   mutbl_b: ast::Mutability)
                                   -> CoerceResult {
         debug!("coerce_borrowed_vector(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         let sub = Sub(self.get_ref().clone());
         let coercion = Coercion(self.get_ref().trace.clone());
@@ -336,8 +336,8 @@ impl<'f> Coerce<'f> {
                               b_mutbl: ast::Mutability) -> CoerceResult
     {
         debug!("coerce_borrowed_object(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         let tcx = self.get_ref().infcx.tcx;
         let coercion = Coercion(self.get_ref().trace.clone());
@@ -376,8 +376,8 @@ impl<'f> Coerce<'f> {
                               b: ty::t)
                               -> CoerceResult {
         debug!("coerce_borrowed_fn(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         match *sty_a {
             ty::ty_bare_fn(ref f) => {
@@ -400,7 +400,7 @@ impl<'f> Coerce<'f> {
         self.unpack_actual_value(b, |sty_b| {
 
             debug!("coerce_from_bare_fn(a={}, b={})",
-                   a.inf_str(self.get_ref().infcx), b.inf_str(self.get_ref().infcx));
+                   a.repr(self.get_ref().infcx.tcx), b.repr(self.get_ref().infcx.tcx));
 
             if fn_ty_a.abi != abi::Rust || fn_ty_a.fn_style != ast::NormalFn {
                 return self.subtype(a, b);
@@ -429,8 +429,8 @@ impl<'f> Coerce<'f> {
                              mt_b: ty::mt)
                              -> CoerceResult {
         debug!("coerce_unsafe_ptr(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         let mt_a = match *sty_a {
             ty::ty_rptr(_, mt) => mt,
@@ -462,8 +462,8 @@ impl<'f> Coerce<'f> {
                          bounds: ty::BuiltinBounds) -> CoerceResult {
 
         debug!("coerce_object(a={}, sty_a={:?}, b={})",
-               a.inf_str(self.get_ref().infcx), sty_a,
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), sty_a,
+               b.repr(self.get_ref().infcx.tcx));
 
         Ok(Some(ty::AutoObject(trait_store, bounds,
                                trait_def_id, trait_substs.clone())))
diff --git a/src/librustc/middle/typeck/infer/combine.rs b/src/librustc/middle/typeck/infer/combine.rs
index cc898ab9c66..844a37d366e 100644
--- a/src/librustc/middle/typeck/infer/combine.rs
+++ b/src/librustc/middle/typeck/infer/combine.rs
@@ -57,8 +57,7 @@ use middle::typeck::infer::{ToUres};
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lub::Lub;
 use middle::typeck::infer::sub::Sub;
-use middle::typeck::infer::to_str::InferStr;
-use middle::typeck::infer::unify::InferCtxtMethods;
+use middle::typeck::infer::unify::InferCtxtMethodsForSimplyUnifiableTypes;
 use middle::typeck::infer::{InferCtxt, cres, ures};
 use middle::typeck::infer::{TypeTrace};
 use util::common::indent;
@@ -263,7 +262,7 @@ pub trait Combine {
                     a: ty::TraitStore,
                     b: ty::TraitStore)
                     -> cres<ty::TraitStore> {
-        debug!("{}.trait_stores(a={:?}, b={:?})", self.tag(), a, b);
+        debug!("{}.trait_stores(a={}, b={})", self.tag(), a, b);
 
         match (a, b) {
             (ty::RegionTraitStore(a_r, a_m),
@@ -409,8 +408,8 @@ pub fn super_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> cres<ty::t> {
         tcx.sess.bug(
             format!("{}: bot and var types should have been handled ({},{})",
                     this.tag(),
-                    a.inf_str(this.infcx()),
-                    b.inf_str(this.infcx())).as_slice());
+                    a.repr(this.infcx().tcx),
+                    b.repr(this.infcx().tcx)).as_slice());
       }
 
         // Relate integral variables to other types
diff --git a/src/librustc/middle/typeck/infer/glb.rs b/src/librustc/middle/typeck/infer/glb.rs
index 18cfd259513..d2c27330a94 100644
--- a/src/librustc/middle/typeck/infer/glb.rs
+++ b/src/librustc/middle/typeck/infer/glb.rs
@@ -17,16 +17,17 @@ use middle::typeck::infer::combine::*;
 use middle::typeck::infer::lattice::*;
 use middle::typeck::infer::lub::Lub;
 use middle::typeck::infer::sub::Sub;
-use middle::typeck::infer::to_str::InferStr;
 use middle::typeck::infer::{cres, InferCtxt};
 use middle::typeck::infer::{TypeTrace, Subtype};
 use middle::typeck::infer::fold_regions_in_sig;
+use middle::typeck::infer::region_inference::RegionMark;
 use syntax::ast::{Many, Once, MutImmutable, MutMutable};
 use syntax::ast::{NormalFn, UnsafeFn, NodeId};
 use syntax::ast::{Onceness, FnStyle};
 use std::collections::HashMap;
 use util::common::{indenter};
 use util::ppaux::mt_to_str;
+use util::ppaux::Repr;
 
 pub struct Glb<'f>(pub CombineFields<'f>);  // "greatest lower bound" (common subtype)
 
@@ -104,8 +105,8 @@ impl<'f> Combine for Glb<'f> {
     fn regions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
         debug!("{}.regions({:?}, {:?})",
                self.tag(),
-               a.inf_str(self.get_ref().infcx),
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx),
+               b.repr(self.get_ref().infcx.tcx));
 
         Ok(self.get_ref().infcx.region_vars.glb_regions(Subtype(self.trace()), a, b))
     }
@@ -124,14 +125,12 @@ impl<'f> Combine for Glb<'f> {
         // please see the large comment in `region_inference.rs`.
 
         debug!("{}.fn_sigs({:?}, {:?})",
-               self.tag(), a.inf_str(self.get_ref().infcx), b.inf_str(self.get_ref().infcx));
+               self.tag(), a.repr(self.get_ref().infcx.tcx), b.repr(self.get_ref().infcx.tcx));
         let _indenter = indenter();
 
-        // Take a snapshot.  We'll never roll this back, but in later
-        // phases we do want to be able to examine "all bindings that
-        // were created as part of this type comparison", and making a
-        // snapshot is a convenient way to do that.
-        let snapshot = self.get_ref().infcx.region_vars.start_snapshot();
+        // Make a mark so we can examine "all bindings that were
+        // created as part of this type comparison".
+        let mark = self.get_ref().infcx.region_vars.mark();
 
         // Instantiate each bound region with a fresh region variable.
         let (a_with_fresh, a_map) =
@@ -145,18 +144,18 @@ impl<'f> Combine for Glb<'f> {
 
         // Collect constraints.
         let sig0 = if_ok!(super_fn_sigs(self, &a_with_fresh, &b_with_fresh));
-        debug!("sig0 = {}", sig0.inf_str(self.get_ref().infcx));
+        debug!("sig0 = {}", sig0.repr(self.get_ref().infcx.tcx));
 
         // Generalize the regions appearing in fn_ty0 if possible
         let new_vars =
-            self.get_ref().infcx.region_vars.vars_created_since_snapshot(snapshot);
+            self.get_ref().infcx.region_vars.vars_created_since_mark(mark);
         let sig1 =
             fold_regions_in_sig(
                 self.get_ref().infcx.tcx,
                 &sig0,
                 |r| {
                 generalize_region(self,
-                                  snapshot,
+                                  mark,
                                   new_vars.as_slice(),
                                   sig0.binder_id,
                                   &a_map,
@@ -164,11 +163,11 @@ impl<'f> Combine for Glb<'f> {
                                   b_vars.as_slice(),
                                   r)
             });
-        debug!("sig1 = {}", sig1.inf_str(self.get_ref().infcx));
+        debug!("sig1 = {}", sig1.repr(self.get_ref().infcx.tcx));
         return Ok(sig1);
 
         fn generalize_region(this: &Glb,
-                             snapshot: uint,
+                             mark: RegionMark,
                              new_vars: &[RegionVid],
                              new_binder_id: NodeId,
                              a_map: &HashMap<ty::BoundRegion, ty::Region>,
@@ -180,7 +179,7 @@ impl<'f> Combine for Glb<'f> {
                 return r0;
             }
 
-            let tainted = this.get_ref().infcx.region_vars.tainted(snapshot, r0);
+            let tainted = this.get_ref().infcx.region_vars.tainted(mark, r0);
 
             let mut a_r = None;
             let mut b_r = None;
diff --git a/src/librustc/middle/typeck/infer/lattice.rs b/src/librustc/middle/typeck/infer/lattice.rs
index 6455344cb13..1b3d96e474e 100644
--- a/src/librustc/middle/typeck/infer/lattice.rs
+++ b/src/librustc/middle/typeck/infer/lattice.rs
@@ -32,22 +32,20 @@
  * a lattice.
  */
 
-
-use middle::ty::{RegionVid, TyVar, Vid};
+use middle::ty::{RegionVid, TyVar};
 use middle::ty;
-use middle::typeck::infer::{then, ToUres};
+use middle::typeck::infer::{ToUres};
 use middle::typeck::infer::*;
 use middle::typeck::infer::combine::*;
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lub::Lub;
-use middle::typeck::infer::unify::*;
+use middle::typeck::infer::unify::{Root, UnifyKey};
 use middle::typeck::infer::sub::Sub;
-use middle::typeck::infer::to_str::InferStr;
-use util::common::indenter;
+use util::ppaux::Repr;
 
 use std::collections::HashMap;
 
-trait LatticeValue {
+trait LatticeValue : Clone + Repr + PartialEq {
     fn sub(cf: CombineFields, a: &Self, b: &Self) -> ures;
     fn lub(cf: CombineFields, a: &Self, b: &Self) -> cres<Self>;
     fn glb(cf: CombineFields, a: &Self, b: &Self) -> cres<Self>;
@@ -70,72 +68,73 @@ impl LatticeValue for ty::t {
     }
 }
 
-pub trait CombineFieldsLatticeMethods {
-    fn var_sub_var<T:Clone + InferStr + LatticeValue,
-                   V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(&self,
-                                                                     a_id: V,
-                                                                     b_id: V)
-                                                                     -> ures;
+pub trait CombineFieldsLatticeMethods<T:LatticeValue, K:UnifyKey<Bounds<T>>> {
+    /// make variable a subtype of variable
+    fn var_sub_var(&self,
+                   a_id: K,
+                   b_id: K)
+                   -> ures;
+
     /// make variable a subtype of T
-    fn var_sub_t<T:Clone + InferStr + LatticeValue,
-                 V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
-                 &self,
-                 a_id: V,
+    fn var_sub_t(&self,
+                 a_id: K,
                  b: T)
                  -> ures;
-    fn t_sub_var<T:Clone + InferStr + LatticeValue,
-                 V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
-                 &self,
+
+    /// make T a subtype of variable
+    fn t_sub_var(&self,
                  a: T,
-                 b_id: V)
+                 b_id: K)
                  -> ures;
-    fn merge_bnd<T:Clone + InferStr + LatticeValue>(
-                 &self,
-                 a: &Bound<T>,
-                 b: &Bound<T>,
-                 lattice_op: LatticeOp<T>)
-                 -> cres<Bound<T>>;
-    fn set_var_to_merged_bounds<T:Clone + InferStr + LatticeValue,
-                                V:Clone+PartialEq+ToStr+Vid+UnifyVid<Bounds<T>>>(
-                                &self,
-                                v_id: V,
+
+    fn set_var_to_merged_bounds(&self,
+                                v_id: K,
                                 a: &Bounds<T>,
                                 b: &Bounds<T>,
                                 rank: uint)
                                 -> ures;
-    fn bnds<T:Clone + InferStr + LatticeValue>(
-            &self,
-            a: &Bound<T>,
-            b: &Bound<T>)
-            -> ures;
 }
 
-impl<'f> CombineFieldsLatticeMethods for CombineFields<'f> {
-    fn var_sub_var<T:Clone + InferStr + LatticeValue,
-                   V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
-                   &self,
-                   a_id: V,
-                   b_id: V)
-                   -> ures {
+pub trait CombineFieldsLatticeMethods2<T:LatticeValue> {
+    fn merge_bnd(&self,
+                 a: &Bound<T>,
+                 b: &Bound<T>,
+                 lattice_op: LatticeOp<T>)
+                 -> cres<Bound<T>>;
+
+    fn bnds(&self, a: &Bound<T>, b: &Bound<T>) -> ures;
+}
+
+impl<'f,T:LatticeValue, K:UnifyKey<Bounds<T>>>
+    CombineFieldsLatticeMethods<T,K> for CombineFields<'f>
+{
+    fn var_sub_var(&self,
+                   a_id: K,
+                   b_id: K)
+                   -> ures
+    {
         /*!
-         *
          * Make one variable a subtype of another variable.  This is a
          * subtle and tricky process, as described in detail at the
-         * top of infer.rs*/
+         * top of infer.rs.
+         */
+
+        let tcx = self.infcx.tcx;
+        let table = UnifyKey::unification_table(self.infcx);
 
         // Need to make sub_id a subtype of sup_id.
-        let node_a = self.infcx.get(a_id);
-        let node_b = self.infcx.get(b_id);
-        let a_id = node_a.root.clone();
-        let b_id = node_b.root.clone();
-        let a_bounds = node_a.possible_types.clone();
-        let b_bounds = node_b.possible_types.clone();
+        let node_a = table.borrow_mut().get(tcx, a_id);
+        let node_b = table.borrow_mut().get(tcx, b_id);
+        let a_id = node_a.key.clone();
+        let b_id = node_b.key.clone();
+        let a_bounds = node_a.value.clone();
+        let b_bounds = node_b.value.clone();
 
         debug!("vars({}={} <: {}={})",
-               a_id.to_str(), a_bounds.inf_str(self.infcx),
-               b_id.to_str(), b_bounds.inf_str(self.infcx));
+               a_id, a_bounds.repr(tcx),
+               b_id, b_bounds.repr(tcx));
 
-        if a_id == b_id { return uok(); }
+        if a_id == b_id { return Ok(()); }
 
         // If both A's UB and B's LB have already been bound to types,
         // see if we can make those types subtypes.
@@ -157,96 +156,72 @@ impl<'f> CombineFieldsLatticeMethods for CombineFields<'f> {
         // A remains a subtype of B.  Actually, there are other options,
         // but that's the route we choose to take.
 
-        let (new_root, new_rank) = self.infcx.unify(&node_a, &node_b);
+        let (new_root, new_rank) =
+            table.borrow_mut().unify(tcx, &node_a, &node_b);
         self.set_var_to_merged_bounds(new_root,
                                       &a_bounds, &b_bounds,
                                       new_rank)
     }
 
     /// make variable a subtype of T
-    fn var_sub_t<T:Clone + InferStr + LatticeValue,
-                 V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
-                 &self,
-                 a_id: V,
+    fn var_sub_t(&self,
+                 a_id: K,
                  b: T)
-                 -> ures {
+                 -> ures
+    {
         /*!
-         *
-         * Make a variable (`a_id`) a subtype of the concrete type `b` */
+         * Make a variable (`a_id`) a subtype of the concrete type `b`.
+         */
 
-        let node_a = self.infcx.get(a_id);
-        let a_id = node_a.root.clone();
-        let a_bounds = &node_a.possible_types;
+        let tcx = self.infcx.tcx;
+        let table = UnifyKey::unification_table(self.infcx);
+        let node_a = table.borrow_mut().get(tcx, a_id);
+        let a_id = node_a.key.clone();
+        let a_bounds = &node_a.value;
         let b_bounds = &Bounds { lb: None, ub: Some(b.clone()) };
 
         debug!("var_sub_t({}={} <: {})",
-               a_id.to_str(),
-               a_bounds.inf_str(self.infcx),
-               b.inf_str(self.infcx));
+               a_id,
+               a_bounds.repr(self.infcx.tcx),
+               b.repr(self.infcx.tcx));
 
         self.set_var_to_merged_bounds(
             a_id, a_bounds, b_bounds, node_a.rank)
     }
 
-    fn t_sub_var<T:Clone + InferStr + LatticeValue,
-                 V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
-                 &self,
+    fn t_sub_var(&self,
                  a: T,
-                 b_id: V)
-                 -> ures {
+                 b_id: K)
+                 -> ures
+    {
         /*!
-         *
-         * Make a concrete type (`a`) a subtype of the variable `b_id` */
+         * Make a concrete type (`a`) a subtype of the variable `b_id`
+         */
 
+        let tcx = self.infcx.tcx;
+        let table = UnifyKey::unification_table(self.infcx);
         let a_bounds = &Bounds { lb: Some(a.clone()), ub: None };
-        let node_b = self.infcx.get(b_id);
-        let b_id = node_b.root.clone();
-        let b_bounds = &node_b.possible_types;
+        let node_b = table.borrow_mut().get(tcx, b_id);
+        let b_id = node_b.key.clone();
+        let b_bounds = &node_b.value;
 
         debug!("t_sub_var({} <: {}={})",
-               a.inf_str(self.infcx),
-               b_id.to_str(),
-               b_bounds.inf_str(self.infcx));
+               a.repr(self.infcx.tcx),
+               b_id,
+               b_bounds.repr(self.infcx.tcx));
 
         self.set_var_to_merged_bounds(
             b_id, a_bounds, b_bounds, node_b.rank)
     }
 
-    fn merge_bnd<T:Clone + InferStr + LatticeValue>(
-                 &self,
-                 a: &Bound<T>,
-                 b: &Bound<T>,
-                 lattice_op: LatticeOp<T>)
-                 -> cres<Bound<T>> {
-        /*!
-         *
-         * Combines two bounds into a more general bound. */
-
-        debug!("merge_bnd({},{})",
-               a.inf_str(self.infcx),
-               b.inf_str(self.infcx));
-        let _r = indenter();
-
-        match (a, b) {
-            (&None,          &None) => Ok(None),
-            (&Some(_),       &None) => Ok((*a).clone()),
-            (&None,          &Some(_)) => Ok((*b).clone()),
-            (&Some(ref v_a), &Some(ref v_b)) => {
-                lattice_op(self.clone(), v_a, v_b).and_then(|v| Ok(Some(v)))
-            }
-        }
-    }
-
-    fn set_var_to_merged_bounds<T:Clone + InferStr + LatticeValue,
-                                V:Clone+PartialEq+ToStr+Vid+UnifyVid<Bounds<T>>>(
-                                &self,
-                                v_id: V,
+    fn set_var_to_merged_bounds(&self,
+                                v_id: K,
                                 a: &Bounds<T>,
                                 b: &Bounds<T>,
                                 rank: uint)
-                                -> ures {
+                                -> ures
+    {
         /*!
-         *
          * Updates the bounds for the variable `v_id` to be the intersection
          * of `a` and `b`.  That is, the new bounds for `v_id` will be
          * a bounds c such that:
@@ -254,7 +229,8 @@ impl<'f> CombineFieldsLatticeMethods for CombineFields<'f> {
          *    c.ub <: b.ub
          *    a.lb <: c.lb
          *    b.lb <: c.lb
-         * If this cannot be achieved, the result is failure. */
+         * If this cannot be achieved, the result is failure.
+         */
 
         // Think of the two diamonds, we want to find the
         // intersection.  There are basically four possibilities (you
@@ -271,11 +247,13 @@ impl<'f> CombineFieldsLatticeMethods for CombineFields<'f> {
         //       A     \ / A
         //              B
 
+        let tcx = self.infcx.tcx;
+        let table = UnifyKey::unification_table(self.infcx);
+
         debug!("merge({},{},{})",
-               v_id.to_str(),
-               a.inf_str(self.infcx),
-               b.inf_str(self.infcx));
-        let _indent = indenter();
+               v_id,
+               a.repr(self.infcx.tcx),
+               b.repr(self.infcx.tcx));
 
         // First, relate the lower/upper bounds of A and B.
         // Note that these relations *must* hold for us
@@ -289,29 +267,57 @@ impl<'f> CombineFieldsLatticeMethods for CombineFields<'f> {
         let lb = if_ok!(self.merge_bnd(&a.lb, &b.lb, LatticeValue::lub));
         let bounds = Bounds { lb: lb, ub: ub };
         debug!("merge({}): bounds={}",
-               v_id.to_str(),
-               bounds.inf_str(self.infcx));
+               v_id,
+               bounds.repr(self.infcx.tcx));
 
         // the new bounds must themselves
         // be relatable:
         let () = if_ok!(self.bnds(&bounds.lb, &bounds.ub));
-        self.infcx.set(v_id, Root(bounds, rank));
-        uok()
+        table.borrow_mut().set(tcx, v_id, Root(bounds, rank));
+        Ok(())
+    }
+}
+
+impl<'f,T:LatticeValue>
+    CombineFieldsLatticeMethods2<T> for CombineFields<'f>
+{
+    fn merge_bnd(&self,
+                 a: &Bound<T>,
+                 b: &Bound<T>,
+                 lattice_op: LatticeOp<T>)
+                 -> cres<Bound<T>>
+    {
+        /*!
+         * Combines two bounds into a more general bound.
+         */
+
+        debug!("merge_bnd({},{})",
+               a.repr(self.infcx.tcx),
+               b.repr(self.infcx.tcx));
+        match (a, b) {
+            (&None,          &None) => Ok(None),
+            (&Some(_),       &None) => Ok((*a).clone()),
+            (&None,          &Some(_)) => Ok((*b).clone()),
+            (&Some(ref v_a), &Some(ref v_b)) => {
+                lattice_op(self.clone(), v_a, v_b).and_then(|v| Ok(Some(v)))
+            }
+        }
     }
 
-    fn bnds<T:Clone + InferStr + LatticeValue>(&self,
-                                               a: &Bound<T>,
-                                               b: &Bound<T>)
-                                               -> ures {
-        debug!("bnds({} <: {})", a.inf_str(self.infcx),
-               b.inf_str(self.infcx));
-        let _r = indenter();
+    fn bnds(&self,
+            a: &Bound<T>,
+            b: &Bound<T>)
+            -> ures
+    {
+        debug!("bnds({} <: {})",
+               a.repr(self.infcx.tcx),
+               b.repr(self.infcx.tcx));
 
         match (a, b) {
             (&None, &None) |
             (&Some(_), &None) |
             (&None, &Some(_)) => {
-                uok()
+                Ok(())
             }
             (&Some(ref t_a), &Some(ref t_b)) => {
                 LatticeValue::sub(self.clone(), t_a, t_b)
@@ -368,9 +374,10 @@ pub fn super_lattice_tys<L:LatticeDir+TyLatticeDir+Combine>(this: &L,
                                                             a: ty::t,
                                                             b: ty::t)
                                                             -> cres<ty::t> {
-    debug!("{}.lattice_tys({}, {})", this.tag(),
-           a.inf_str(this.infcx()),
-           b.inf_str(this.infcx()));
+    debug!("{}.lattice_tys({}, {})",
+           this.tag(),
+           a.repr(this.infcx().tcx),
+           b.repr(this.infcx().tcx));
 
     if a == b {
         return Ok(a);
@@ -410,8 +417,8 @@ pub fn super_lattice_tys<L:LatticeDir+TyLatticeDir+Combine>(this: &L,
 pub type LatticeDirOp<'a, T> = |a: &T, b: &T|: 'a -> cres<T>;
 
 #[deriving(Clone)]
-pub enum LatticeVarResult<V,T> {
-    VarResult(V),
+pub enum LatticeVarResult<K,T> {
+    VarResult(K),
     ValueResult(T)
 }
 
@@ -429,26 +436,31 @@ pub enum LatticeVarResult<V,T> {
  * - If the variables do not both have an upper bound, we will unify
  *   the variables and return the unified variable, in which case the
  *   result is a variable.  This is indicated with a `VarResult`
- *   return. */
-pub fn lattice_vars<L:LatticeDir + Combine,
-                    T:Clone + InferStr + LatticeValue,
-                    V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
+ *   return.
+ */
+pub fn lattice_vars<L:LatticeDir+Combine,
+                    T:LatticeValue,
+                    K:UnifyKey<Bounds<T>>>(
     this: &L,                           // defines whether we want LUB or GLB
-    a_vid: V,                          // first variable
-    b_vid: V,                          // second variable
+    a_vid: K,                           // first variable
+    b_vid: K,                           // second variable
     lattice_dir_op: LatticeDirOp<T>)    // LUB or GLB operation on types
-    -> cres<LatticeVarResult<V,T>> {
-    let nde_a = this.infcx().get(a_vid);
-    let nde_b = this.infcx().get(b_vid);
-    let a_vid = nde_a.root.clone();
-    let b_vid = nde_b.root.clone();
-    let a_bounds = &nde_a.possible_types;
-    let b_bounds = &nde_b.possible_types;
+    -> cres<LatticeVarResult<K,T>>
+{
+    let tcx = this.infcx().tcx;
+    let table = UnifyKey::unification_table(this.infcx());
+
+    let node_a = table.borrow_mut().get(tcx, a_vid);
+    let node_b = table.borrow_mut().get(tcx, b_vid);
+    let a_vid = node_a.key.clone();
+    let b_vid = node_b.key.clone();
+    let a_bounds = &node_a.value;
+    let b_bounds = &node_b.value;
 
     debug!("{}.lattice_vars({}={} <: {}={})",
            this.tag(),
-           a_vid.to_str(), a_bounds.inf_str(this.infcx()),
-           b_vid.to_str(), b_bounds.inf_str(this.infcx()));
+           a_vid, a_bounds.repr(tcx),
+           b_vid, b_bounds.repr(tcx));
 
     // Same variable: the easy case.
     if a_vid == b_vid {
@@ -471,36 +483,39 @@ pub fn lattice_vars<L:LatticeDir + Combine,
     // Otherwise, we need to merge A and B into one variable.  We can
     // then use either variable as an upper bound:
     let cf = this.combine_fields();
-    cf.var_sub_var(a_vid.clone(), b_vid.clone()).then(|| {
-        Ok(VarResult(a_vid.clone()))
-    })
+    let () = try!(cf.var_sub_var(a_vid.clone(), b_vid.clone()));
+    Ok(VarResult(a_vid.clone()))
 }
 
-pub fn lattice_var_and_t<L:LatticeDir + Combine,
-                         T:Clone + InferStr + LatticeValue,
-                         V:Clone + PartialEq + ToStr + Vid + UnifyVid<Bounds<T>>>(
+pub fn lattice_var_and_t<L:LatticeDir+Combine,
+                         T:LatticeValue,
+                         K:UnifyKey<Bounds<T>>>(
     this: &L,
-    a_id: V,
+    a_id: K,
     b: &T,
     lattice_dir_op: LatticeDirOp<T>)
-    -> cres<T> {
-    let nde_a = this.infcx().get(a_id);
-    let a_id = nde_a.root.clone();
-    let a_bounds = &nde_a.possible_types;
+    -> cres<T>
+{
+    let tcx = this.infcx().tcx;
+    let table = UnifyKey::unification_table(this.infcx());
+
+    let node_a = table.borrow_mut().get(tcx, a_id);
+    let a_id = node_a.key.clone();
+    let a_bounds = &node_a.value;
 
     // The comments in this function are written for LUB, but they
     // apply equally well to GLB if you inverse upper/lower/sub/super/etc.
 
     debug!("{}.lattice_var_and_t({}={} <: {})",
            this.tag(),
-           a_id.to_str(),
-           a_bounds.inf_str(this.infcx()),
-           b.inf_str(this.infcx()));
+           a_id,
+           a_bounds.repr(this.infcx().tcx),
+           b.repr(this.infcx().tcx));
 
     match this.bnd(a_bounds) {
         Some(ref a_bnd) => {
             // If a has an upper bound, return the LUB(a.ub, b)
-            debug!("bnd=Some({})", a_bnd.inf_str(this.infcx()));
+            debug!("bnd=Some({})", a_bnd.repr(this.infcx().tcx));
             lattice_dir_op(a_bnd, b)
         }
         None => {
@@ -508,11 +523,12 @@ pub fn lattice_var_and_t<L:LatticeDir + Combine,
             // and then return b.
             debug!("bnd=None");
             let a_bounds = this.with_bnd(a_bounds, (*b).clone());
-            this.combine_fields().bnds(&a_bounds.lb, &a_bounds.ub).then(|| {
-                this.infcx().set(a_id.clone(),
-                                 Root(a_bounds.clone(), nde_a.rank));
-                Ok((*b).clone())
-            })
+            let () = try!(this.combine_fields().bnds(&a_bounds.lb,
+                                                     &a_bounds.ub));
+            table.borrow_mut().set(tcx,
+                                   a_id.clone(),
+                                   Root(a_bounds.clone(), node_a.rank));
+            Ok((*b).clone())
         }
     }
 }
diff --git a/src/librustc/middle/typeck/infer/lub.rs b/src/librustc/middle/typeck/infer/lub.rs
index 41784c9b8d9..7ccffdfeb06 100644
--- a/src/librustc/middle/typeck/infer/lub.rs
+++ b/src/librustc/middle/typeck/infer/lub.rs
@@ -16,16 +16,17 @@ use middle::typeck::infer::combine::*;
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lattice::*;
 use middle::typeck::infer::sub::Sub;
-use middle::typeck::infer::to_str::InferStr;
 use middle::typeck::infer::{cres, InferCtxt};
 use middle::typeck::infer::fold_regions_in_sig;
 use middle::typeck::infer::{TypeTrace, Subtype};
+use middle::typeck::infer::region_inference::RegionMark;
 use std::collections::HashMap;
 use syntax::ast::{Many, Once, NodeId};
 use syntax::ast::{NormalFn, UnsafeFn};
 use syntax::ast::{Onceness, FnStyle};
 use syntax::ast::{MutMutable, MutImmutable};
 use util::ppaux::mt_to_str;
+use util::ppaux::Repr;
 
 pub struct Lub<'f>(pub CombineFields<'f>);  // least-upper-bound: common supertype
 
@@ -101,10 +102,10 @@ impl<'f> Combine for Lub<'f> {
     }
 
     fn regions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
-        debug!("{}.regions({:?}, {:?})",
+        debug!("{}.regions({}, {})",
                self.tag(),
-               a.inf_str(self.get_ref().infcx),
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx),
+               b.repr(self.get_ref().infcx.tcx));
 
         Ok(self.get_ref().infcx.region_vars.lub_regions(Subtype(self.trace()), a, b))
     }
@@ -113,11 +114,9 @@ impl<'f> Combine for Lub<'f> {
         // Note: this is a subtle algorithm.  For a full explanation,
         // please see the large comment in `region_inference.rs`.
 
-        // Take a snapshot.  We'll never roll this back, but in later
-        // phases we do want to be able to examine "all bindings that
-        // were created as part of this type comparison", and making a
-        // snapshot is a convenient way to do that.
-        let snapshot = self.get_ref().infcx.region_vars.start_snapshot();
+        // Make a mark so we can examine "all bindings that were
+        // created as part of this type comparison".
+        let mark = self.get_ref().infcx.region_vars.mark();
 
         // Instantiate each bound region with a fresh region variable.
         let (a_with_fresh, a_map) =
@@ -129,21 +128,21 @@ impl<'f> Combine for Lub<'f> {
 
         // Collect constraints.
         let sig0 = if_ok!(super_fn_sigs(self, &a_with_fresh, &b_with_fresh));
-        debug!("sig0 = {}", sig0.inf_str(self.get_ref().infcx));
+        debug!("sig0 = {}", sig0.repr(self.get_ref().infcx.tcx));
 
         // Generalize the regions appearing in sig0 if possible
         let new_vars =
-            self.get_ref().infcx.region_vars.vars_created_since_snapshot(snapshot);
+            self.get_ref().infcx.region_vars.vars_created_since_mark(mark);
         let sig1 =
             fold_regions_in_sig(
                 self.get_ref().infcx.tcx,
                 &sig0,
-                |r| generalize_region(self, snapshot, new_vars.as_slice(),
+                |r| generalize_region(self, mark, new_vars.as_slice(),
                                       sig0.binder_id, &a_map, r));
         return Ok(sig1);
 
         fn generalize_region(this: &Lub,
-                             snapshot: uint,
+                             mark: RegionMark,
                              new_vars: &[RegionVid],
                              new_scope: NodeId,
                              a_map: &HashMap<ty::BoundRegion, ty::Region>,
@@ -156,7 +155,7 @@ impl<'f> Combine for Lub<'f> {
                 return r0;
             }
 
-            let tainted = this.get_ref().infcx.region_vars.tainted(snapshot, r0);
+            let tainted = this.get_ref().infcx.region_vars.tainted(mark, r0);
 
             // Variables created during LUB computation which are
             // *related* to regions that pre-date the LUB computation
diff --git a/src/librustc/middle/typeck/infer/mod.rs b/src/librustc/middle/typeck/infer/mod.rs
index 7a7dbaa549a..bb458d27d17 100644
--- a/src/librustc/middle/typeck/infer/mod.rs
+++ b/src/librustc/middle/typeck/infer/mod.rs
@@ -23,21 +23,21 @@ pub use middle::typeck::infer::resolve::{resolve_rvar};
 
 use middle::subst;
 use middle::subst::Substs;
-use middle::ty::{TyVid, IntVid, FloatVid, RegionVid, Vid};
+use middle::ty::{TyVid, IntVid, FloatVid, RegionVid};
 use middle::ty;
 use middle::ty_fold;
 use middle::ty_fold::TypeFolder;
 use middle::typeck::check::regionmanip::replace_late_bound_regions_in_fn_sig;
 use middle::typeck::infer::coercion::Coerce;
 use middle::typeck::infer::combine::{Combine, CombineFields, eq_tys};
-use middle::typeck::infer::region_inference::{RegionVarBindings};
+use middle::typeck::infer::region_inference::{RegionVarBindings,
+                                              RegionSnapshot};
 use middle::typeck::infer::resolve::{resolver};
 use middle::typeck::infer::sub::Sub;
 use middle::typeck::infer::lub::Lub;
-use middle::typeck::infer::to_str::InferStr;
-use middle::typeck::infer::unify::{ValsAndBindings, Root};
+use middle::typeck::infer::unify::{UnificationTable, Snapshot};
 use middle::typeck::infer::error_reporting::ErrorReporting;
-use std::cell::{Cell, RefCell};
+use std::cell::{RefCell};
 use std::collections::HashMap;
 use std::rc::Rc;
 use syntax::ast;
@@ -55,17 +55,17 @@ pub mod lub;
 pub mod region_inference;
 pub mod resolve;
 pub mod sub;
-pub mod to_str;
 pub mod unify;
 pub mod coercion;
 pub mod error_reporting;
+pub mod test;
 
 pub type Bound<T> = Option<T>;
 
-#[deriving(Clone)]
+#[deriving(PartialEq,Clone)]
 pub struct Bounds<T> {
-    lb: Bound<T>,
-    ub: Bound<T>
+    pub lb: Bound<T>,
+    pub ub: Bound<T>
 }
 
 pub type cres<T> = Result<T,ty::type_err>; // "combine result"
@@ -76,24 +76,23 @@ pub type CoerceResult = cres<Option<ty::AutoAdjustment>>;
 pub struct InferCtxt<'a> {
     pub tcx: &'a ty::ctxt,
 
-    // We instantiate ValsAndBindings with bounds<ty::t> because the
+    // We instantiate UnificationTable with bounds<ty::t> because the
     // types that might instantiate a general type variable have an
     // order, represented by its upper and lower bounds.
-    pub ty_var_bindings: RefCell<ValsAndBindings<ty::TyVid, Bounds<ty::t>>>,
-    pub ty_var_counter: Cell<uint>,
+    type_unification_table:
+        RefCell<UnificationTable<ty::TyVid, Bounds<ty::t>>>,
 
     // Map from integral variable to the kind of integer it represents
-    pub int_var_bindings: RefCell<ValsAndBindings<ty::IntVid,
-                                              Option<IntVarValue>>>,
-    pub int_var_counter: Cell<uint>,
+    int_unification_table:
+        RefCell<UnificationTable<ty::IntVid, Option<IntVarValue>>>,
 
     // Map from floating variable to the kind of float it represents
-    pub float_var_bindings: RefCell<ValsAndBindings<ty::FloatVid,
-                                                Option<ast::FloatTy>>>,
-    pub float_var_counter: Cell<uint>,
+    float_unification_table:
+        RefCell<UnificationTable<ty::FloatVid, Option<ast::FloatTy>>>,
 
     // For region variables.
-    pub region_vars: RegionVarBindings<'a>,
+    region_vars:
+        RegionVarBindings<'a>,
 }
 
 /// Why did we require that the two types be related?
@@ -261,16 +260,9 @@ pub fn fixup_err_to_str(f: fixup_err) -> String {
 pub fn new_infer_ctxt<'a>(tcx: &'a ty::ctxt) -> InferCtxt<'a> {
     InferCtxt {
         tcx: tcx,
-
-        ty_var_bindings: RefCell::new(ValsAndBindings::new()),
-        ty_var_counter: Cell::new(0),
-
-        int_var_bindings: RefCell::new(ValsAndBindings::new()),
-        int_var_counter: Cell::new(0),
-
-        float_var_bindings: RefCell::new(ValsAndBindings::new()),
-        float_var_counter: Cell::new(0),
-
+        type_unification_table: RefCell::new(UnificationTable::new()),
+        int_unification_table: RefCell::new(UnificationTable::new()),
+        float_unification_table: RefCell::new(UnificationTable::new()),
         region_vars: RegionVarBindings::new(tcx),
     }
 }
@@ -280,20 +272,23 @@ pub fn common_supertype(cx: &InferCtxt,
                         a_is_expected: bool,
                         a: ty::t,
                         b: ty::t)
-                        -> ty::t {
+                        -> ty::t
+{
     /*!
      * Computes the least upper-bound of `a` and `b`. If this is
      * not possible, reports an error and returns ty::err.
      */
 
-    debug!("common_supertype({}, {})", a.inf_str(cx), b.inf_str(cx));
+    debug!("common_supertype({}, {})",
+           a.repr(cx.tcx), b.repr(cx.tcx));
 
     let trace = TypeTrace {
         origin: origin,
         values: Types(expected_found(a_is_expected, a, b))
     };
 
-    let result = cx.commit(|| cx.lub(a_is_expected, trace.clone()).tys(a, b));
+    let result =
+        cx.commit_if_ok(|| cx.lub(a_is_expected, trace.clone()).tys(a, b));
     match result {
         Ok(t) => t,
         Err(ref err) => {
@@ -309,9 +304,9 @@ pub fn mk_subty(cx: &InferCtxt,
                 a: ty::t,
                 b: ty::t)
              -> ures {
-    debug!("mk_subty({} <: {})", a.inf_str(cx), b.inf_str(cx));
+    debug!("mk_subty({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
     indent(|| {
-        cx.commit(|| {
+        cx.commit_if_ok(|| {
             let trace = TypeTrace {
                 origin: origin,
                 values: Types(expected_found(a_is_expected, a, b))
@@ -322,15 +317,13 @@ pub fn mk_subty(cx: &InferCtxt,
 }
 
 pub fn can_mk_subty(cx: &InferCtxt, a: ty::t, b: ty::t) -> ures {
-    debug!("can_mk_subty({} <: {})", a.inf_str(cx), b.inf_str(cx));
-    indent(|| {
-        cx.probe(|| {
-            let trace = TypeTrace {
-                origin: Misc(codemap::DUMMY_SP),
-                values: Types(expected_found(true, a, b))
-            };
-            cx.sub(true, trace).tys(a, b)
-        })
+    debug!("can_mk_subty({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
+    cx.probe(|| {
+        let trace = TypeTrace {
+            origin: Misc(codemap::DUMMY_SP),
+            values: Types(expected_found(true, a, b))
+        };
+        cx.sub(true, trace).tys(a, b)
     }).to_ures()
 }
 
@@ -339,10 +332,10 @@ pub fn mk_subr(cx: &InferCtxt,
                origin: SubregionOrigin,
                a: ty::Region,
                b: ty::Region) {
-    debug!("mk_subr({} <: {})", a.inf_str(cx), b.inf_str(cx));
-    cx.region_vars.start_snapshot();
+    debug!("mk_subr({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
+    let snapshot = cx.region_vars.start_snapshot();
     cx.region_vars.make_subregion(origin, a, b);
-    cx.region_vars.commit();
+    cx.region_vars.commit(snapshot);
 }
 
 pub fn mk_eqty(cx: &InferCtxt,
@@ -350,18 +343,17 @@ pub fn mk_eqty(cx: &InferCtxt,
                origin: TypeOrigin,
                a: ty::t,
                b: ty::t)
-            -> ures {
-    debug!("mk_eqty({} <: {})", a.inf_str(cx), b.inf_str(cx));
-    indent(|| {
-        cx.commit(|| {
-            let trace = TypeTrace {
-                origin: origin,
-                values: Types(expected_found(a_is_expected, a, b))
-            };
-            let suber = cx.sub(a_is_expected, trace);
-            eq_tys(&suber, a, b)
-        })
-    }).to_ures()
+            -> ures
+{
+    debug!("mk_eqty({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
+    cx.commit_if_ok(|| {
+        let trace = TypeTrace {
+            origin: origin,
+            values: Types(expected_found(a_is_expected, a, b))
+        };
+        let suber = cx.sub(a_is_expected, trace);
+        eq_tys(&suber, a, b)
+    })
 }
 
 pub fn mk_sub_trait_refs(cx: &InferCtxt,
@@ -372,9 +364,9 @@ pub fn mk_sub_trait_refs(cx: &InferCtxt,
     -> ures
 {
     debug!("mk_sub_trait_refs({} <: {})",
-           a.inf_str(cx), b.inf_str(cx));
+           a.repr(cx.tcx), b.repr(cx.tcx));
     indent(|| {
-        cx.commit(|| {
+        cx.commit_if_ok(|| {
             let trace = TypeTrace {
                 origin: origin,
                 values: TraitRefs(expected_found(a_is_expected, a.clone(), b.clone()))
@@ -401,9 +393,9 @@ pub fn mk_coercety(cx: &InferCtxt,
                    a: ty::t,
                    b: ty::t)
                 -> CoerceResult {
-    debug!("mk_coercety({} -> {})", a.inf_str(cx), b.inf_str(cx));
+    debug!("mk_coercety({} -> {})", a.repr(cx.tcx), b.repr(cx.tcx));
     indent(|| {
-        cx.commit(|| {
+        cx.commit_if_ok(|| {
             let trace = TypeTrace {
                 origin: origin,
                 values: Types(expected_found(a_is_expected, a, b))
@@ -417,13 +409,15 @@ pub fn mk_coercety(cx: &InferCtxt,
 pub fn resolve_type(cx: &InferCtxt,
                     a: ty::t,
                     modes: uint)
-                 -> fres<ty::t> {
+                 -> fres<ty::t>
+{
     let mut resolver = resolver(cx, modes);
-    resolver.resolve_type_chk(a)
+    cx.commit_unconditionally(|| resolver.resolve_type_chk(a))
 }
 
 pub fn resolve_region(cx: &InferCtxt, r: ty::Region, modes: uint)
-                   -> fres<ty::Region> {
+                   -> fres<ty::Region>
+{
     let mut resolver = resolver(cx, modes);
     resolver.resolve_region_chk(r)
 }
@@ -473,19 +467,11 @@ pub fn uok() -> ures {
     Ok(())
 }
 
-fn rollback_to<V:Clone + Vid,T:Clone>(vb: &mut ValsAndBindings<V, T>,
-                                      len: uint) {
-    while vb.bindings.len() != len {
-        let (vid, old_v) = vb.bindings.pop().unwrap();
-        vb.vals.insert(vid.to_uint(), old_v);
-    }
-}
-
-pub struct Snapshot {
-    ty_var_bindings_len: uint,
-    int_var_bindings_len: uint,
-    float_var_bindings_len: uint,
-    region_vars_snapshot: uint,
+pub struct CombinedSnapshot {
+    type_snapshot: Snapshot<ty::TyVid>,
+    int_snapshot: Snapshot<ty::IntVid>,
+    float_snapshot: Snapshot<ty::FloatVid>,
+    region_vars_snapshot: RegionSnapshot,
 }
 
 impl<'a> InferCtxt<'a> {
@@ -508,40 +494,67 @@ impl<'a> InferCtxt<'a> {
         self.region_vars.in_snapshot()
     }
 
-    pub fn start_snapshot(&self) -> Snapshot {
-        Snapshot {
-            ty_var_bindings_len: self.ty_var_bindings.borrow().bindings.len(),
-            int_var_bindings_len: self.int_var_bindings.borrow().bindings.len(),
-            float_var_bindings_len: self.float_var_bindings.borrow().bindings.len(),
+    fn start_snapshot(&self) -> CombinedSnapshot {
+        CombinedSnapshot {
+            type_snapshot: self.type_unification_table.borrow_mut().snapshot(),
+            int_snapshot: self.int_unification_table.borrow_mut().snapshot(),
+            float_snapshot: self.float_unification_table.borrow_mut().snapshot(),
             region_vars_snapshot: self.region_vars.start_snapshot(),
         }
     }
 
-    pub fn rollback_to(&self, snapshot: &Snapshot) {
+    fn rollback_to(&self, snapshot: CombinedSnapshot) {
         debug!("rollback!");
-        rollback_to(&mut *self.ty_var_bindings.borrow_mut(),
-                    snapshot.ty_var_bindings_len);
-        rollback_to(&mut *self.int_var_bindings.borrow_mut(),
-                    snapshot.int_var_bindings_len);
-        rollback_to(&mut *self.float_var_bindings.borrow_mut(),
-                    snapshot.float_var_bindings_len);
+        let CombinedSnapshot { type_snapshot,
+                               int_snapshot,
+                               float_snapshot,
+                               region_vars_snapshot } = snapshot;
 
-        self.region_vars.rollback_to(snapshot.region_vars_snapshot);
+        self.type_unification_table
+            .borrow_mut()
+            .rollback_to(self.tcx, type_snapshot);
+        self.int_unification_table
+            .borrow_mut()
+            .rollback_to(self.tcx, int_snapshot);
+        self.float_unification_table
+            .borrow_mut()
+            .rollback_to(self.tcx, float_snapshot);
+        self.region_vars
+            .rollback_to(region_vars_snapshot);
+    }
+
+    fn commit_from(&self, snapshot: CombinedSnapshot) {
+        debug!("commit_from!");
+        let CombinedSnapshot { type_snapshot,
+                               int_snapshot,
+                               float_snapshot,
+                               region_vars_snapshot } = snapshot;
+
+        self.type_unification_table
+            .borrow_mut()
+            .commit(type_snapshot);
+        self.int_unification_table
+            .borrow_mut()
+            .commit(int_snapshot);
+        self.float_unification_table
+            .borrow_mut()
+            .commit(float_snapshot);
+        self.region_vars
+            .commit(region_vars_snapshot);
+    }
+
+    /// Execute `f` and commit the bindings
+    pub fn commit_unconditionally<R>(&self, f: || -> R) -> R {
+        debug!("commit()");
+        let snapshot = self.start_snapshot();
+        let r = f();
+        self.commit_from(snapshot);
+        r
     }
 
     /// Execute `f` and commit the bindings if successful
-    pub fn commit<T,E>(&self, f: || -> Result<T,E>) -> Result<T,E> {
-        assert!(!self.in_snapshot());
-
-        debug!("commit()");
-        indent(|| {
-            let r = self.try(|| f());
-
-            self.ty_var_bindings.borrow_mut().bindings.truncate(0);
-            self.int_var_bindings.borrow_mut().bindings.truncate(0);
-            self.region_vars.commit();
-            r
-        })
+    pub fn commit_if_ok<T,E>(&self, f: || -> Result<T,E>) -> Result<T,E> {
+        self.commit_unconditionally(|| self.try(|| f()))
     }
 
     /// Execute `f`, unroll bindings on failure
@@ -549,11 +562,13 @@ impl<'a> InferCtxt<'a> {
         debug!("try()");
         let snapshot = self.start_snapshot();
         let r = f();
+        debug!("try() -- r.is_ok() = {}", r.is_ok());
         match r {
-            Ok(_) => { debug!("success"); }
-            Err(ref e) => {
-                debug!("error: {:?}", *e);
-                self.rollback_to(&snapshot)
+            Ok(_) => {
+                self.commit_from(snapshot);
+            }
+            Err(_) => {
+                self.rollback_to(snapshot);
             }
         }
         r
@@ -562,36 +577,18 @@ impl<'a> InferCtxt<'a> {
     /// Execute `f` then unroll any bindings it creates
     pub fn probe<T,E>(&self, f: || -> Result<T,E>) -> Result<T,E> {
         debug!("probe()");
-        indent(|| {
-            let snapshot = self.start_snapshot();
-            let r = f();
-            self.rollback_to(&snapshot);
-            r
-        })
+        let snapshot = self.start_snapshot();
+        let r = f();
+        self.rollback_to(snapshot);
+        r
     }
 }
 
-fn next_simple_var<V:Clone,T:Clone>(counter: &mut uint,
-                                    bindings: &mut ValsAndBindings<V,
-                                                                   Option<T>>)
-                                    -> uint {
-    let id = *counter;
-    *counter += 1;
-    bindings.vals.insert(id, Root(None, 0));
-    return id;
-}
-
 impl<'a> InferCtxt<'a> {
     pub fn next_ty_var_id(&self) -> TyVid {
-        let id = self.ty_var_counter.get();
-        self.ty_var_counter.set(id + 1);
-        {
-            let mut ty_var_bindings = self.ty_var_bindings.borrow_mut();
-            let vals = &mut ty_var_bindings.vals;
-            vals.insert(id, Root(Bounds { lb: None, ub: None }, 0u));
-        }
-        debug!("created type variable {}", TyVid(id));
-        return TyVid(id);
+        self.type_unification_table
+            .borrow_mut()
+            .new_key(Bounds { lb: None, ub: None })
     }
 
     pub fn next_ty_var(&self) -> ty::t {
@@ -603,21 +600,15 @@ impl<'a> InferCtxt<'a> {
     }
 
     pub fn next_int_var_id(&self) -> IntVid {
-        let mut int_var_counter = self.int_var_counter.get();
-        let mut int_var_bindings = self.int_var_bindings.borrow_mut();
-        let result = IntVid(next_simple_var(&mut int_var_counter,
-                                            &mut *int_var_bindings));
-        self.int_var_counter.set(int_var_counter);
-        result
+        self.int_unification_table
+            .borrow_mut()
+            .new_key(None)
     }
 
     pub fn next_float_var_id(&self) -> FloatVid {
-        let mut float_var_counter = self.float_var_counter.get();
-        let mut float_var_bindings = self.float_var_bindings.borrow_mut();
-        let result = FloatVid(next_simple_var(&mut float_var_counter,
-                                              &mut *float_var_bindings));
-        self.float_var_counter.set(float_var_counter);
-        result
+        self.float_unification_table
+            .borrow_mut()
+            .new_key(None)
     }
 
     pub fn next_region_var(&self, origin: RegionVariableOrigin) -> ty::Region {
diff --git a/src/librustc/middle/typeck/infer/region_inference/mod.rs b/src/librustc/middle/typeck/infer/region_inference/mod.rs
index 8ea15d25420..c81d4b17d9b 100644
--- a/src/librustc/middle/typeck/infer/region_inference/mod.rs
+++ b/src/librustc/middle/typeck/infer/region_inference/mod.rs
@@ -12,7 +12,7 @@
 
 
 use middle::ty;
-use middle::ty::{BoundRegion, FreeRegion, Region, RegionVid, Vid};
+use middle::ty::{BoundRegion, FreeRegion, Region, RegionVid};
 use middle::ty::{ReEmpty, ReStatic, ReInfer, ReFree, ReEarlyBound,
                  ReLateBound};
 use middle::ty::{ReScope, ReVar, ReSkolemized, BrFresh};
@@ -45,13 +45,17 @@ pub struct TwoRegions {
     b: Region,
 }
 
+#[deriving(PartialEq)]
 pub enum UndoLogEntry {
-    Snapshot,
+    OpenSnapshot,
+    CommitedSnapshot,
+    Mark,
     AddVar(RegionVid),
     AddConstraint(Constraint),
     AddCombination(CombineMapType, TwoRegions)
 }
 
+#[deriving(PartialEq)]
 pub enum CombineMapType {
     Lub, Glb
 }
@@ -131,16 +135,27 @@ pub struct RegionVarBindings<'a> {
     // The undo log records actions that might later be undone.
     //
     // Note: when the undo_log is empty, we are not actively
-    // snapshotting.  When the `start_snapshot()` method is called, we
-    // push a Snapshot entry onto the list to indicate that we are now
-    // actively snapshotting.  The reason for this is that otherwise
-    // we end up adding entries for things like the lower bound on
-    // a variable and so forth, which can never be rolled back.
-    undo_log: RefCell<Vec<UndoLogEntry> >,
+    // snapshotting. When the `start_snapshot()` method is called, we
+    // push an OpenSnapshot entry onto the list to indicate that we
+    // are now actively snapshotting. The reason for this is that
+    // otherwise we end up adding entries for things like the lower
+    // bound on a variable and so forth, which can never be rolled
+    // back.
+    undo_log: RefCell<Vec<UndoLogEntry>>,
 
     // This contains the results of inference.  It begins as an empty
     // option and only acquires a value after inference is complete.
-    values: RefCell<Option<Vec<VarValue> >>,
+    values: RefCell<Option<Vec<VarValue>>>,
+}
+
+#[deriving(Show)]
+pub struct RegionSnapshot {
+    length: uint
+}
+
+#[deriving(Show)]
+pub struct RegionMark {
+    length: uint
 }
 
 impl<'a> RegionVarBindings<'a> {
@@ -162,48 +177,62 @@ impl<'a> RegionVarBindings<'a> {
         self.undo_log.borrow().len() > 0
     }
 
-    pub fn start_snapshot(&self) -> uint {
-        debug!("RegionVarBindings: start_snapshot()");
-        if self.in_snapshot() {
-            self.undo_log.borrow().len()
-        } else {
-            self.undo_log.borrow_mut().push(Snapshot);
-            0
-        }
+    pub fn start_snapshot(&self) -> RegionSnapshot {
+        let length = self.undo_log.borrow().len();
+        debug!("RegionVarBindings: start_snapshot({})", length);
+        self.undo_log.borrow_mut().push(OpenSnapshot);
+        RegionSnapshot { length: length }
     }
 
-    pub fn commit(&self) {
+    pub fn mark(&self) -> RegionMark {
+        let length = self.undo_log.borrow().len();
+        debug!("RegionVarBindings: mark({})", length);
+        self.undo_log.borrow_mut().push(Mark);
+        RegionMark { length: length }
+    }
+
+    pub fn commit(&self, snapshot: RegionSnapshot) {
         debug!("RegionVarBindings: commit()");
+        assert!(self.undo_log.borrow().len() > snapshot.length);
+        assert!(*self.undo_log.borrow().get(snapshot.length) == OpenSnapshot);
+
         let mut undo_log = self.undo_log.borrow_mut();
-        while undo_log.len() > 0 {
-            undo_log.pop().unwrap();
+        if snapshot.length == 0 {
+            undo_log.truncate(0);
+        } else {
+            *undo_log.get_mut(snapshot.length) = CommitedSnapshot;
         }
     }
 
-    pub fn rollback_to(&self, snapshot: uint) {
+    pub fn rollback_to(&self, snapshot: RegionSnapshot) {
         debug!("RegionVarBindings: rollback_to({})", snapshot);
         let mut undo_log = self.undo_log.borrow_mut();
-        while undo_log.len() > snapshot {
-            let undo_item = undo_log.pop().unwrap();
-            debug!("undo_item={:?}", undo_item);
-            match undo_item {
-              Snapshot => {}
-              AddVar(vid) => {
-                let mut var_origins = self.var_origins.borrow_mut();
-                assert_eq!(var_origins.len(), vid.to_uint() + 1);
-                var_origins.pop().unwrap();
-              }
-              AddConstraint(ref constraint) => {
-                self.constraints.borrow_mut().remove(constraint);
-              }
-              AddCombination(Glb, ref regions) => {
-                self.glbs.borrow_mut().remove(regions);
-              }
-              AddCombination(Lub, ref regions) => {
-                self.lubs.borrow_mut().remove(regions);
-              }
+        assert!(undo_log.len() > snapshot.length);
+        assert!(*undo_log.get(snapshot.length) == OpenSnapshot);
+        while undo_log.len() > snapshot.length + 1 {
+            match undo_log.pop().unwrap() {
+                OpenSnapshot => {
+                    fail!("Failure to observe stack discipline");
+                }
+                Mark | CommitedSnapshot => { }
+                AddVar(vid) => {
+                    let mut var_origins = self.var_origins.borrow_mut();
+                    assert_eq!(var_origins.len(), vid.index + 1);
+                    var_origins.pop().unwrap();
+                }
+                AddConstraint(ref constraint) => {
+                    self.constraints.borrow_mut().remove(constraint);
+                }
+                AddCombination(Glb, ref regions) => {
+                    self.glbs.borrow_mut().remove(regions);
+                }
+                AddCombination(Lub, ref regions) => {
+                    self.lubs.borrow_mut().remove(regions);
+                }
             }
         }
+        let c = undo_log.pop().unwrap();
+        assert!(c == OpenSnapshot);
     }
 
     pub fn num_vars(&self) -> uint {
@@ -213,7 +242,7 @@ impl<'a> RegionVarBindings<'a> {
     pub fn new_region_var(&self, origin: RegionVariableOrigin) -> RegionVid {
         let id = self.num_vars();
         self.var_origins.borrow_mut().push(origin.clone());
-        let vid = RegionVid { id: id };
+        let vid = RegionVid { index: id };
         if self.in_snapshot() {
             self.undo_log.borrow_mut().push(AddVar(vid));
         }
@@ -368,15 +397,15 @@ impl<'a> RegionVarBindings<'a> {
         let v = match *self.values.borrow() {
             None => {
                 self.tcx.sess.span_bug(
-                    self.var_origins.borrow().get(rid.to_uint()).span(),
+                    self.var_origins.borrow().get(rid.index).span(),
                     "attempt to resolve region variable before values have \
                      been computed!")
             }
-            Some(ref values) => *values.get(rid.to_uint())
+            Some(ref values) => *values.get(rid.index)
         };
 
         debug!("RegionVarBindings: resolve_var({:?}={})={:?}",
-               rid, rid.to_uint(), v);
+               rid, rid.index, v);
         match v {
             Value(r) => r,
 
@@ -427,9 +456,12 @@ impl<'a> RegionVarBindings<'a> {
         ReInfer(ReVar(c))
     }
 
-    pub fn vars_created_since_snapshot(&self, snapshot: uint)
-                                       -> Vec<RegionVid> {
-        self.undo_log.borrow().slice_from(snapshot).iter()
+    pub fn vars_created_since_mark(&self, mark: RegionMark)
+                                   -> Vec<RegionVid>
+    {
+        self.undo_log.borrow()
+            .slice_from(mark.length)
+            .iter()
             .filter_map(|&elt| match elt {
                 AddVar(vid) => Some(vid),
                 _ => None
@@ -437,20 +469,18 @@ impl<'a> RegionVarBindings<'a> {
             .collect()
     }
 
-    pub fn tainted(&self, snapshot: uint, r0: Region) -> Vec<Region> {
+    pub fn tainted(&self, mark: RegionMark, r0: Region) -> Vec<Region> {
         /*!
          * Computes all regions that have been related to `r0` in any
-         * way since the snapshot `snapshot` was taken---`r0` itself
-         * will be the first entry. This is used when checking whether
+         * way since the mark `mark` was made---`r0` itself will be
+         * the first entry. This is used when checking whether
          * skolemized regions are being improperly related to other
          * regions.
          */
 
-        debug!("tainted(snapshot={}, r0={:?})", snapshot, r0);
+        debug!("tainted(mark={}, r0={})", mark, r0.repr(self.tcx));
         let _indenter = indenter();
 
-        let undo_len = self.undo_log.borrow().len();
-
         // `result_set` acts as a worklist: we explore all outgoing
         // edges and add any new regions we find to result_set.  This
         // is not a terribly efficient implementation.
@@ -459,16 +489,14 @@ impl<'a> RegionVarBindings<'a> {
         while result_index < result_set.len() {
             // nb: can't use uint::range() here because result_set grows
             let r = *result_set.get(result_index);
-
             debug!("result_index={}, r={:?}", result_index, r);
 
-            let mut undo_index = snapshot;
-            while undo_index < undo_len {
-                // nb: can't use uint::range() here as we move result_set
-                let regs = match self.undo_log.borrow().get(undo_index) {
+            for undo_entry in
+                self.undo_log.borrow().slice_from(mark.length).iter()
+            {
+                let regs = match undo_entry {
                     &AddConstraint(ConstrainVarSubVar(ref a, ref b)) => {
-                        Some((ReInfer(ReVar(*a)),
-                              ReInfer(ReVar(*b))))
+                        Some((ReInfer(ReVar(*a)), ReInfer(ReVar(*b))))
                     }
                     &AddConstraint(ConstrainRegSubVar(ref a, ref b)) => {
                         Some((*a, ReInfer(ReVar(*b))))
@@ -479,7 +507,11 @@ impl<'a> RegionVarBindings<'a> {
                     &AddConstraint(ConstrainRegSubReg(a, b)) => {
                         Some((a, b))
                     }
-                    _ => {
+                    &AddCombination(..) |
+                    &Mark |
+                    &AddVar(..) |
+                    &OpenSnapshot |
+                    &CommitedSnapshot => {
                         None
                     }
                 };
@@ -493,8 +525,6 @@ impl<'a> RegionVarBindings<'a> {
                             consider_adding_edge(result_set, r, r2, r1);
                     }
                 }
-
-                undo_index += 1;
             }
 
             result_index += 1;
@@ -559,7 +589,7 @@ impl<'a> RegionVarBindings<'a> {
 
           (ReInfer(ReVar(v_id)), _) | (_, ReInfer(ReVar(v_id))) => {
             self.tcx.sess.span_bug(
-                self.var_origins.borrow().get(v_id.to_uint()).span(),
+                self.var_origins.borrow().get(v_id.index).span(),
                 format!("lub_concrete_regions invoked with \
                          non-concrete regions: {:?}, {:?}",
                         a,
@@ -665,7 +695,7 @@ impl<'a> RegionVarBindings<'a> {
             (ReInfer(ReVar(v_id)), _) |
             (_, ReInfer(ReVar(v_id))) => {
                 self.tcx.sess.span_bug(
-                    self.var_origins.borrow().get(v_id.to_uint()).span(),
+                    self.var_origins.borrow().get(v_id.index).span(),
                     format!("glb_concrete_regions invoked with \
                              non-concrete regions: {:?}, {:?}",
                             a,
@@ -804,14 +834,14 @@ impl<'a> RegionVarBindings<'a> {
         self.iterate_until_fixed_point("Expansion", |constraint| {
             match *constraint {
               ConstrainRegSubVar(a_region, b_vid) => {
-                let b_data = &mut var_data[b_vid.to_uint()];
+                let b_data = &mut var_data[b_vid.index];
                 self.expand_node(a_region, b_vid, b_data)
               }
               ConstrainVarSubVar(a_vid, b_vid) => {
-                match var_data[a_vid.to_uint()].value {
+                match var_data[a_vid.index].value {
                   NoValue | ErrorValue => false,
                   Value(a_region) => {
-                    let b_node = &mut var_data[b_vid.to_uint()];
+                    let b_node = &mut var_data[b_vid.index];
                     self.expand_node(a_region, b_vid, b_node)
                   }
                 }
@@ -873,16 +903,16 @@ impl<'a> RegionVarBindings<'a> {
                 false
               }
               ConstrainVarSubVar(a_vid, b_vid) => {
-                match var_data[b_vid.to_uint()].value {
+                match var_data[b_vid.index].value {
                   NoValue | ErrorValue => false,
                   Value(b_region) => {
-                    let a_data = &mut var_data[a_vid.to_uint()];
+                    let a_data = &mut var_data[a_vid.index];
                     self.contract_node(a_vid, a_data, b_region)
                   }
                 }
               }
               ConstrainVarSubReg(a_vid, b_region) => {
-                let a_data = &mut var_data[a_vid.to_uint()];
+                let a_data = &mut var_data[a_vid.index];
                 self.contract_node(a_vid, a_data, b_region)
               }
               ConstrainRegSubReg(..) => {
@@ -1054,7 +1084,7 @@ impl<'a> RegionVarBindings<'a> {
                     }
                     let graph = opt_graph.get_ref();
 
-                    let node_vid = RegionVid { id: idx };
+                    let node_vid = RegionVid { index: idx };
                     match var_data[idx].classification {
                         Expanding => {
                             self.collect_error_for_expanding_node(
@@ -1091,17 +1121,17 @@ impl<'a> RegionVarBindings<'a> {
         for (constraint, _) in constraints.iter() {
             match *constraint {
                 ConstrainVarSubVar(a_id, b_id) => {
-                    graph.add_edge(NodeIndex(a_id.to_uint()),
-                                   NodeIndex(b_id.to_uint()),
+                    graph.add_edge(NodeIndex(a_id.index),
+                                   NodeIndex(b_id.index),
                                    *constraint);
                 }
                 ConstrainRegSubVar(_, b_id) => {
                     graph.add_edge(dummy_idx,
-                                   NodeIndex(b_id.to_uint()),
+                                   NodeIndex(b_id.index),
                                    *constraint);
                 }
                 ConstrainVarSubReg(a_id, _) => {
-                    graph.add_edge(NodeIndex(a_id.to_uint()),
+                    graph.add_edge(NodeIndex(a_id.index),
                                    dummy_idx,
                                    *constraint);
                 }
@@ -1157,7 +1187,7 @@ impl<'a> RegionVarBindings<'a> {
                 if !self.is_subregion_of(lower_bound.region,
                                          upper_bound.region) {
                     errors.push(SubSupConflict(
-                        self.var_origins.borrow().get(node_idx.to_uint()).clone(),
+                        self.var_origins.borrow().get(node_idx.index).clone(),
                         lower_bound.origin.clone(),
                         lower_bound.region,
                         upper_bound.origin.clone(),
@@ -1168,7 +1198,7 @@ impl<'a> RegionVarBindings<'a> {
         }
 
         self.tcx.sess.span_bug(
-            self.var_origins.borrow().get(node_idx.to_uint()).span(),
+            self.var_origins.borrow().get(node_idx.index).span(),
             format!("collect_error_for_expanding_node() could not find error \
                   for var {:?}, lower_bounds={}, upper_bounds={}",
                  node_idx,
@@ -1207,7 +1237,7 @@ impl<'a> RegionVarBindings<'a> {
                   Ok(_) => {}
                   Err(_) => {
                     errors.push(SupSupConflict(
-                        self.var_origins.borrow().get(node_idx.to_uint()).clone(),
+                        self.var_origins.borrow().get(node_idx.index).clone(),
                         upper_bound_1.origin.clone(),
                         upper_bound_1.region,
                         upper_bound_2.origin.clone(),
@@ -1219,7 +1249,7 @@ impl<'a> RegionVarBindings<'a> {
         }
 
         self.tcx.sess.span_bug(
-            self.var_origins.borrow().get(node_idx.to_uint()).span(),
+            self.var_origins.borrow().get(node_idx.index).span(),
             format!("collect_error_for_contracting_node() could not find error \
                   for var {:?}, upper_bounds={}",
                  node_idx,
@@ -1256,12 +1286,12 @@ impl<'a> RegionVarBindings<'a> {
 
         while !state.stack.is_empty() {
             let node_idx = state.stack.pop().unwrap();
-            let classification = var_data[node_idx.to_uint()].classification;
+            let classification = var_data[node_idx.index].classification;
 
             // check whether we've visited this node on some previous walk
-            if dup_vec[node_idx.to_uint()] == uint::MAX {
-                dup_vec[node_idx.to_uint()] = orig_node_idx.to_uint();
-            } else if dup_vec[node_idx.to_uint()] != orig_node_idx.to_uint() {
+            if dup_vec[node_idx.index] == uint::MAX {
+                dup_vec[node_idx.index] = orig_node_idx.index;
+            } else if dup_vec[node_idx.index] != orig_node_idx.index {
                 state.dup_found = true;
             }
 
@@ -1289,7 +1319,7 @@ impl<'a> RegionVarBindings<'a> {
                          dir: Direction) {
             debug!("process_edges(source_vid={:?}, dir={:?})", source_vid, dir);
 
-            let source_node_index = NodeIndex(source_vid.to_uint());
+            let source_node_index = NodeIndex(source_vid.index);
             graph.each_adjacent_edge(source_node_index, dir, |_, edge| {
                 match edge.data {
                     ConstrainVarSubVar(from_vid, to_vid) => {
diff --git a/src/librustc/middle/typeck/infer/resolve.rs b/src/librustc/middle/typeck/infer/resolve.rs
index 9df610dc7bc..ae7578957f8 100644
--- a/src/librustc/middle/typeck/infer/resolve.rs
+++ b/src/librustc/middle/typeck/infer/resolve.rs
@@ -53,10 +53,9 @@ use middle::ty;
 use middle::ty_fold;
 use middle::typeck::infer::{Bounds, cyclic_ty, fixup_err, fres, InferCtxt};
 use middle::typeck::infer::unresolved_ty;
-use middle::typeck::infer::to_str::InferStr;
-use middle::typeck::infer::unify::{Root, UnifyInferCtxtMethods};
-use util::common::{indent, indenter};
-use util::ppaux::ty_to_str;
+use middle::typeck::infer::unify::Root;
+use util::common::{indent};
+use util::ppaux::{ty_to_str, Repr};
 
 use syntax::ast;
 
@@ -150,8 +149,7 @@ impl<'a> ResolveState<'a> {
     }
 
     pub fn resolve_type(&mut self, typ: ty::t) -> ty::t {
-        debug!("resolve_type({})", typ.inf_str(self.infcx));
-        let _i = indenter();
+        debug!("resolve_type({})", typ.repr(self.infcx.tcx));
 
         if !ty::type_needs_infer(typ) {
             return typ;
@@ -188,7 +186,7 @@ impl<'a> ResolveState<'a> {
     }
 
     pub fn resolve_region(&mut self, orig: ty::Region) -> ty::Region {
-        debug!("Resolve_region({})", orig.inf_str(self.infcx));
+        debug!("Resolve_region({})", orig.repr(self.infcx.tcx));
         match orig {
           ty::ReInfer(ty::ReVar(rid)) => self.resolve_region_var(rid),
           _ => orig
@@ -216,14 +214,15 @@ impl<'a> ResolveState<'a> {
             // tend to carry more restrictions or higher
             // perf. penalties, so it pays to know more.
 
-            let nde = self.infcx.get(vid);
-            let bounds = nde.possible_types;
-
-            let t1 = match bounds {
-              Bounds { ub:_, lb:Some(t) } if !type_is_bot(t)
-                => self.resolve_type(t),
-              Bounds { ub:Some(t), lb:_ } => self.resolve_type(t),
-              Bounds { ub:_, lb:Some(t) } => self.resolve_type(t),
+            let node =
+                self.infcx.type_unification_table.borrow_mut().get(tcx, vid);
+            let t1 = match node.value {
+              Bounds { ub:_, lb:Some(t) } if !type_is_bot(t) => {
+                  self.resolve_type(t)
+              }
+              Bounds { ub:Some(t), lb:_ } | Bounds { ub:_, lb:Some(t) } => {
+                  self.resolve_type(t)
+              }
               Bounds { ub:None, lb:None } => {
                 if self.should(force_tvar) {
                     self.err = Some(unresolved_ty(vid));
@@ -241,15 +240,18 @@ impl<'a> ResolveState<'a> {
             return ty::mk_int_var(self.infcx.tcx, vid);
         }
 
-        let node = self.infcx.get(vid);
-        match node.possible_types {
+        let tcx = self.infcx.tcx;
+        let table = &self.infcx.int_unification_table;
+        let node = table.borrow_mut().get(tcx, vid);
+        match node.value {
           Some(IntType(t)) => ty::mk_mach_int(t),
           Some(UintType(t)) => ty::mk_mach_uint(t),
           None => {
             if self.should(force_ivar) {
                 // As a last resort, default to int.
                 let ty = ty::mk_int();
-                self.infcx.set(vid, Root(Some(IntType(ast::TyI)), node.rank));
+                table.borrow_mut().set(
+                    tcx, node.key, Root(Some(IntType(ast::TyI)), node.rank));
                 ty
             } else {
                 ty::mk_int_var(self.infcx.tcx, vid)
@@ -263,14 +265,17 @@ impl<'a> ResolveState<'a> {
             return ty::mk_float_var(self.infcx.tcx, vid);
         }
 
-        let node = self.infcx.get(vid);
-        match node.possible_types {
+        let tcx = self.infcx.tcx;
+        let table = &self.infcx.float_unification_table;
+        let node = table.borrow_mut().get(tcx, vid);
+        match node.value {
           Some(t) => ty::mk_mach_float(t),
           None => {
             if self.should(force_fvar) {
                 // As a last resort, default to f64.
                 let ty = ty::mk_f64();
-                self.infcx.set(vid, Root(Some(ast::TyF64), node.rank));
+                table.borrow_mut().set(
+                    tcx, node.key, Root(Some(ast::TyF64), node.rank));
                 ty
             } else {
                 ty::mk_float_var(self.infcx.tcx, vid)
diff --git a/src/librustc/middle/typeck/infer/sub.rs b/src/librustc/middle/typeck/infer/sub.rs
index a543cf18d56..856237c4bca 100644
--- a/src/librustc/middle/typeck/infer/sub.rs
+++ b/src/librustc/middle/typeck/infer/sub.rs
@@ -20,10 +20,9 @@ use middle::typeck::infer::InferCtxt;
 use middle::typeck::infer::lattice::CombineFieldsLatticeMethods;
 use middle::typeck::infer::lub::Lub;
 use middle::typeck::infer::then;
-use middle::typeck::infer::to_str::InferStr;
 use middle::typeck::infer::{TypeTrace, Subtype};
 use util::common::{indenter};
-use util::ppaux::bound_region_to_str;
+use util::ppaux::{bound_region_to_str, Repr};
 
 use syntax::ast::{Onceness, FnStyle, MutImmutable, MutMutable};
 
@@ -63,14 +62,16 @@ impl<'f> Combine for Sub<'f> {
     fn regions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
         debug!("{}.regions({}, {})",
                self.tag(),
-               a.inf_str(self.get_ref().infcx),
-               b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx),
+               b.repr(self.get_ref().infcx.tcx));
         self.get_ref().infcx.region_vars.make_subregion(Subtype(self.trace()), a, b);
         Ok(a)
     }
 
     fn mts(&self, a: &ty::mt, b: &ty::mt) -> cres<ty::mt> {
-        debug!("mts({} <: {})", a.inf_str(self.get_ref().infcx), b.inf_str(self.get_ref().infcx));
+        debug!("mts({} <: {})",
+               a.repr(self.get_ref().infcx.tcx),
+               b.repr(self.get_ref().infcx.tcx));
 
         if a.mutbl != b.mutbl {
             return Err(ty::terr_mutability);
@@ -116,7 +117,7 @@ impl<'f> Combine for Sub<'f> {
 
     fn tys(&self, a: ty::t, b: ty::t) -> cres<ty::t> {
         debug!("{}.tys({}, {})", self.tag(),
-               a.inf_str(self.get_ref().infcx), b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), b.repr(self.get_ref().infcx.tcx));
         if a == b { return Ok(a); }
         let _indenter = indenter();
         match (&ty::get(a).sty, &ty::get(b).sty) {
@@ -149,7 +150,7 @@ impl<'f> Combine for Sub<'f> {
 
     fn fn_sigs(&self, a: &ty::FnSig, b: &ty::FnSig) -> cres<ty::FnSig> {
         debug!("fn_sigs(a={}, b={})",
-               a.inf_str(self.get_ref().infcx), b.inf_str(self.get_ref().infcx));
+               a.repr(self.get_ref().infcx.tcx), b.repr(self.get_ref().infcx.tcx));
         let _indenter = indenter();
 
         // Rather than checking the subtype relationship between `a` and `b`
@@ -159,11 +160,9 @@ impl<'f> Combine for Sub<'f> {
         // Note: this is a subtle algorithm.  For a full explanation,
         // please see the large comment in `region_inference.rs`.
 
-        // Take a snapshot.  We'll never roll this back, but in later
-        // phases we do want to be able to examine "all bindings that
-        // were created as part of this type comparison", and making a
-        // snapshot is a convenient way to do that.
-        let snapshot = self.get_ref().infcx.region_vars.start_snapshot();
+        // Make a mark so we can examine "all bindings that were
+        // created as part of this type comparison".
+        let mark = self.get_ref().infcx.region_vars.mark();
 
         // First, we instantiate each bound region in the subtype with a fresh
         // region variable.
@@ -183,8 +182,8 @@ impl<'f> Combine for Sub<'f> {
             })
         };
 
-        debug!("a_sig={}", a_sig.inf_str(self.get_ref().infcx));
-        debug!("b_sig={}", b_sig.inf_str(self.get_ref().infcx));
+        debug!("a_sig={}", a_sig.repr(self.get_ref().infcx.tcx));
+        debug!("b_sig={}", b_sig.repr(self.get_ref().infcx.tcx));
 
         // Compare types now that bound regions have been replaced.
         let sig = if_ok!(super_fn_sigs(self, &a_sig, &b_sig));
@@ -192,9 +191,9 @@ impl<'f> Combine for Sub<'f> {
         // Presuming type comparison succeeds, we need to check
         // that the skolemized regions do not "leak".
         let new_vars =
-            self.get_ref().infcx.region_vars.vars_created_since_snapshot(snapshot);
+            self.get_ref().infcx.region_vars.vars_created_since_mark(mark);
         for (&skol_br, &skol) in skol_map.iter() {
-            let tainted = self.get_ref().infcx.region_vars.tainted(snapshot, skol);
+            let tainted = self.get_ref().infcx.region_vars.tainted(mark, skol);
             for tainted_region in tainted.iter() {
                 // Each skolemized should only be relatable to itself
                 // or new variables:
@@ -209,9 +208,11 @@ impl<'f> Combine for Sub<'f> {
 
                 // A is not as polymorphic as B:
                 if self.a_is_expected() {
+                    debug!("Not as polymorphic!");
                     return Err(ty::terr_regions_insufficiently_polymorphic(
                             skol_br, *tainted_region));
                 } else {
+                    debug!("Overly polymorphic!");
                     return Err(ty::terr_regions_overly_polymorphic(
                             skol_br, *tainted_region));
                 }
diff --git a/src/librustc/middle/typeck/infer/test.rs b/src/librustc/middle/typeck/infer/test.rs
index e4636e1c7c6..f08cbb06c9e 100644
--- a/src/librustc/middle/typeck/infer/test.rs
+++ b/src/librustc/middle/typeck/infer/test.rs
@@ -8,77 +8,144 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-/**
+/*!
 
 # Standalone Tests for the Inference Module
 
-Note: This module is only compiled when doing unit testing.
-
 */
 
+// This is only used by tests, hence allow dead code.
+#![allow(dead_code)]
+
+use driver::config;
 use driver::diagnostic;
-use driver::driver::{optgroups, build_session_options, build_session};
-use driver::driver::{str_input, build_configuration};
-use middle::lang_items::{LanguageItems, language_items};
-use middle::ty::{FnTyBase, FnMeta, FnSig};
-use util::ppaux::ty_to_str;
+use driver::diagnostic::Emitter;
+use driver::driver;
+use driver::session;
+use middle::freevars;
+use middle::lang_items;
+use middle::region;
+use middle::resolve;
+use middle::resolve_lifetime;
+use middle::stability;
+use middle::ty;
+use middle::typeck::infer::combine::Combine;
+use middle::typeck::infer;
+use middle::typeck::infer::lub::Lub;
+use middle::typeck::infer::glb::Glb;
+use syntax::codemap;
+use syntax::codemap::{Span, CodeMap, DUMMY_SP};
+use syntax::diagnostic::{Level, RenderSpan, Bug, Fatal, Error, Warning, Note};
+use syntax::ast;
+use syntax::crateid::CrateId;
+use util::ppaux::{ty_to_str, UserString};
 
-use extra::oldmap::HashMap;
-use getopts::{optopt, optmulti, optflag, optflagopt, getopts};
-use getopts::opt_present;
-use syntax::codemap::DUMMY_SP;
-use syntax::parse::parse_crate_from_source_str;
-use syntax::{ast, attr, parse};
-
-struct Env {
-    krate: @ast::Crate,
-    tcx: ty::ctxt,
-    infcx: infer::infer_ctxt,
-    err_messages: @DVec<String>
+struct Env<'a> {
+    krate: ast::Crate,
+    tcx: &'a ty::ctxt,
+    infcx: &'a infer::InferCtxt<'a>,
 }
 
-struct RH {
-    id: ast::node_id,
-    sub: &[RH]
+struct RH<'a> {
+    id: ast::NodeId,
+    sub: &'a [RH<'a>]
 }
 
-static EMPTY_SOURCE_STR: &str = "/* Hello, world! */";
+static EMPTY_SOURCE_STR: &'static str = "#![no_std]";
 
-fn setup_env(test_name: &str, source_string: &str) -> Env {
-    let messages = @DVec();
-    let matches = getopts(vec!("-Z".to_string(), "verbose".to_string()), optgroups()).get();
-    let diag = diagnostic::collect(messages);
-    let sessopts = build_session_options("rustc".to_string(), &matches, diag);
-    let sess = build_session(sessopts, None, diag);
-    let cfg = build_configuration(sess, "whatever".to_string(), str_input("".to_string()));
-    let dm = HashMap();
-    let amap = HashMap();
-    let freevars = HashMap();
-    let region_paramd_items = HashMap();
-    let region_map = HashMap();
-    let lang_items = LanguageItems::new();
-
-    let parse_sess = parse::new_parse_sess(None);
-    let krate = parse_crate_from_source_str(
-        test_name.to_str(), @source_string.to_str(),
-        cfg, parse_sess);
-
-    let tcx = ty::mk_ctxt(sess, dm, amap, freevars, region_map,
-                          region_paramd_items, lang_items);
-
-    let infcx = infer::new_infer_ctxt(tcx);
-
-    return Env {krate: krate,
-                tcx: tcx,
-                infcx: infcx,
-                err_messages: messages};
+struct ExpectErrorEmitter {
+    messages: Vec<String>
 }
 
-impl Env {
+fn remove_message(e: &mut ExpectErrorEmitter, msg: &str, lvl: Level) {
+    match lvl {
+        Bug | Fatal | Error => { }
+        Warning | Note => { return; }
+    }
+
+    debug!("Error: {}", msg);
+    match e.messages.iter().position(|m| msg.contains(m.as_slice())) {
+        Some(i) => {
+            e.messages.remove(i);
+        }
+        None => {
+            fail!("Unexpected error: {} Expected: {}",
+                  msg, e.messages);
+        }
+    }
+}
+
+impl Emitter for ExpectErrorEmitter {
+    fn emit(&mut self,
+            _cmsp: Option<(&codemap::CodeMap, Span)>,
+            msg: &str,
+            lvl: Level)
+    {
+        remove_message(self, msg, lvl);
+    }
+
+    fn custom_emit(&mut self,
+                   _cm: &codemap::CodeMap,
+                   _sp: RenderSpan,
+                   msg: &str,
+                   lvl: Level)
+    {
+        remove_message(self, msg, lvl);
+    }
+}
+
+fn errors(msgs: &[&str]) -> (Box<Emitter+Send>, uint) {
+    let v = Vec::from_fn(msgs.len(), |i| msgs[i].to_owned());
+    (box ExpectErrorEmitter { messages: v } as Box<Emitter+Send>, msgs.len())
+}
+
+fn test_env(_test_name: &str,
+            source_string: &str,
+            (emitter, expected_err_count): (Box<Emitter+Send>, uint),
+            body: |Env|) {
+    let options =
+        config::basic_options();
+    let codemap =
+        CodeMap::new();
+    let diagnostic_handler =
+        diagnostic::mk_handler(emitter);
+    let span_diagnostic_handler =
+        diagnostic::mk_span_handler(diagnostic_handler, codemap);
+
+    let sess = session::build_session_(options, None, span_diagnostic_handler);
+    let krate_config = Vec::new();
+    let input = driver::StrInput(source_string.to_owned());
+    let krate = driver::phase_1_parse_input(&sess, krate_config, &input);
+    let krate_id = CrateId { path: "test".to_owned(),
+                             name: "test".to_owned(),
+                             version: None };
+    let (krate, ast_map) =
+        driver::phase_2_configure_and_expand(&sess, krate, &krate_id);
+
+    // run just enough stuff to build a tcx:
+    let lang_items = lang_items::collect_language_items(&krate, &sess);
+    let resolve::CrateMap { def_map: def_map, .. } =
+        resolve::resolve_crate(&sess, &lang_items, &krate);
+    let freevars_map = freevars::annotate_freevars(&def_map, &krate);
+    let named_region_map = resolve_lifetime::krate(&sess, &krate);
+    let region_map = region::resolve_crate(&sess, &krate);
+    let stability_index = stability::Index::build(&krate);
+    let tcx = ty::mk_ctxt(sess, def_map, named_region_map, ast_map,
+                          freevars_map, region_map, lang_items, stability_index);
+    let infcx = infer::new_infer_ctxt(&tcx);
+    let env = Env {krate: krate,
+                   tcx: &tcx,
+                   infcx: &infcx};
+    body(env);
+    infcx.resolve_regions_and_report_errors();
+    assert_eq!(tcx.sess.err_count(), expected_err_count);
+}
+
+impl<'a> Env<'a> {
     pub fn create_region_hierarchy(&self, rh: &RH) {
         for child_rh in rh.sub.iter() {
             self.create_region_hierarchy(child_rh);
-            self.tcx.region_map.insert(child_rh.id, rh.id);
+            self.tcx.region_maps.record_encl_scope(child_rh.id, rh.id);
         }
     }
 
@@ -93,37 +160,39 @@ impl Env {
                             sub: &[]}]});
     }
 
-    pub fn lookup_item(&self, names: &[String]) -> ast::node_id {
-        return match search_mod(self, &self.krate.node.module, 0, names) {
+    pub fn lookup_item(&self, names: &[String]) -> ast::NodeId {
+        return match search_mod(self, &self.krate.module, 0, names) {
             Some(id) => id,
             None => {
-                fail!("no item found: `%s`", names.connect("::"));
+                fail!("no item found: `{}`", names.connect("::"));
             }
         };
 
-        fn search_mod(self: &Env,
+        fn search_mod(this: &Env,
                       m: &ast::Mod,
                       idx: uint,
-                      names: &[String]) -> Option<ast::node_id> {
+                      names: &[String])
+                      -> Option<ast::NodeId> {
             assert!(idx < names.len());
             for item in m.items.iter() {
-                if self.tcx.sess.str_of(item.ident) == names[idx] {
-                    return search(self, *item, idx+1, names);
+                if item.ident.user_string(this.tcx) == names[idx] {
+                    return search(this, *item, idx+1, names);
                 }
             }
             return None;
         }
 
-        fn search(self: &Env,
-                  it: @ast::Item,
+        fn search(this: &Env,
+                  it: &ast::Item,
                   idx: uint,
-                  names: &[String]) -> Option<ast::node_id> {
+                  names: &[String])
+                  -> Option<ast::NodeId> {
             if idx == names.len() {
                 return Some(it.id);
             }
 
             return match it.node {
-                ast::ItemConst(..) | ast::ItemFn(..) |
+                ast::ItemStatic(..) | ast::ItemFn(..) |
                 ast::ItemForeignMod(..) | ast::ItemTy(..) => {
                     None
                 }
@@ -135,12 +204,20 @@ impl Env {
                 }
 
                 ast::ItemMod(ref m) => {
-                    search_mod(self, m, idx, names)
+                    search_mod(this, m, idx, names)
                 }
             };
         }
     }
 
+    pub fn make_subtype(&self, a: ty::t, b: ty::t) -> bool {
+        match infer::mk_subty(self.infcx, true, infer::Misc(DUMMY_SP), a, b) {
+            Ok(_) => true,
+            Err(ref e) => fail!("Encountered error: {}",
+                                ty::type_err_to_str(self.tcx, e))
+        }
+    }
+
     pub fn is_subtype(&self, a: ty::t, b: ty::t) -> bool {
         match infer::can_mk_subty(self.infcx, a, b) {
             Ok(_) => true,
@@ -150,7 +227,7 @@ impl Env {
 
     pub fn assert_subtype(&self, a: ty::t, b: ty::t) {
         if !self.is_subtype(a, b) {
-            fail!("%s is not a subtype of %s, but it should be",
+            fail!("{} is not a subtype of {}, but it should be",
                   self.ty_to_str(a),
                   self.ty_to_str(b));
         }
@@ -158,17 +235,12 @@ impl Env {
 
     pub fn assert_not_subtype(&self, a: ty::t, b: ty::t) {
         if self.is_subtype(a, b) {
-            fail!("%s is a subtype of %s, but it shouldn't be",
+            fail!("{} is a subtype of {}, but it shouldn't be",
                   self.ty_to_str(a),
                   self.ty_to_str(b));
         }
     }
 
-    pub fn assert_strict_subtype(&self, a: ty::t, b: ty::t) {
-        self.assert_subtype(a, b);
-        self.assert_not_subtype(b, a);
-    }
-
     pub fn assert_eq(&self, a: ty::t, b: ty::t) {
         self.assert_subtype(a, b);
         self.assert_subtype(b, a);
@@ -178,36 +250,29 @@ impl Env {
         ty_to_str(self.tcx, a)
     }
 
-    pub fn t_fn(&self, input_tys: &[ty::t], output_ty: ty::t) -> ty::t {
-        let inputs = input_tys.map(|t| {mode: ast::expl(ast::by_copy),
-                                        ty: *t});
-        ty::mk_fn(self.tcx, FnTyBase {
-            meta: FnMeta {fn_style: ast::NormalFn,
-                          proto: ast::ProtoBare,
-                          onceness: ast::Many,
-                          region: ty::ReStatic,
-                          bounds: @Vec::new()},
-            sig: FnSig {
-                inputs: inputs,
-                output: output_ty,
-                variadic: false
-            }
-        })
+    pub fn t_fn(&self,
+                binder_id: ast::NodeId,
+                input_tys: &[ty::t],
+                output_ty: ty::t)
+                -> ty::t
+    {
+        ty::mk_ctor_fn(self.tcx, binder_id, input_tys, output_ty)
     }
 
     pub fn t_int(&self) -> ty::t {
-        ty::mk_int(self.tcx)
+        ty::mk_int()
     }
 
-    pub fn t_rptr_bound(&self, id: uint) -> ty::t {
-        ty::mk_imm_rptr(self.tcx, ty::re_bound(ty::BrAnon(id)), self.t_int())
+    pub fn t_rptr_late_bound(&self, binder_id: ast::NodeId, id: uint) -> ty::t {
+        ty::mk_imm_rptr(self.tcx, ty::ReLateBound(binder_id, ty::BrAnon(id)),
+                        self.t_int())
     }
 
-    pub fn t_rptr_scope(&self, id: ast::node_id) -> ty::t {
+    pub fn t_rptr_scope(&self, id: ast::NodeId) -> ty::t {
         ty::mk_imm_rptr(self.tcx, ty::ReScope(id), self.t_int())
     }
 
-    pub fn t_rptr_free(&self, nid: ast::node_id, id: uint) -> ty::t {
+    pub fn t_rptr_free(&self, nid: ast::NodeId, id: uint) -> ty::t {
         ty::mk_imm_rptr(self.tcx,
                         ty::ReFree(ty::FreeRegion {scope_id: nid,
                                                     bound_region: ty::BrAnon(id)}),
@@ -218,51 +283,60 @@ impl Env {
         ty::mk_imm_rptr(self.tcx, ty::ReStatic, self.t_int())
     }
 
-    pub fn lub() -> Lub { Lub(self.infcx.combine_fields(true, DUMMY_SP)) }
+    pub fn dummy_type_trace(&self) -> infer::TypeTrace {
+        infer::TypeTrace {
+            origin: infer::Misc(DUMMY_SP),
+            values: infer::Types(ty::expected_found {
+                expected: ty::mk_err(),
+                found: ty::mk_err(),
+            })
+        }
+    }
 
-    pub fn glb() -> Glb { Glb(self.infcx.combine_fields(true, DUMMY_SP)) }
+    pub fn lub(&self) -> Lub<'a> {
+        let trace = self.dummy_type_trace();
+        Lub(self.infcx.combine_fields(true, trace))
+    }
 
-    pub fn resolve_regions(exp_count: uint) {
-        debug!("resolve_regions(%u)", exp_count);
+    pub fn glb(&self) -> Glb<'a> {
+        let trace = self.dummy_type_trace();
+        Glb(self.infcx.combine_fields(true, trace))
+    }
 
-        self.infcx.resolve_regions();
-        if self.err_messages.len() != exp_count {
-            for msg in self.err_messages.iter() {
-                debug!("Error encountered: %s", *msg);
-            }
-            format!("resolving regions encountered %u errors but expected %u!",
-                 self.err_messages.len(),
-                 exp_count);
+    pub fn resolve_regions(&self) {
+        self.infcx.resolve_regions_and_report_errors();
+    }
+
+    pub fn make_lub_ty(&self, t1: ty::t, t2: ty::t) -> ty::t {
+        match self.lub().tys(t1, t2) {
+            Ok(t) => t,
+            Err(ref e) => fail!("unexpected error computing LUB: {:?}",
+                                ty::type_err_to_str(self.tcx, e))
         }
     }
 
     /// Checks that `LUB(t1,t2) == t_lub`
     pub fn check_lub(&self, t1: ty::t, t2: ty::t, t_lub: ty::t) {
         match self.lub().tys(t1, t2) {
-            Err(e) => {
-                fail!("unexpected error computing LUB: %?", e)
-            }
             Ok(t) => {
                 self.assert_eq(t, t_lub);
-
-                // sanity check for good measure:
-                self.assert_subtype(t1, t);
-                self.assert_subtype(t2, t);
-
-                self.resolve_regions(0);
+            }
+            Err(ref e) => {
+                fail!("unexpected error in LUB: {}",
+                      ty::type_err_to_str(self.tcx, e))
             }
         }
     }
 
     /// Checks that `GLB(t1,t2) == t_glb`
     pub fn check_glb(&self, t1: ty::t, t2: ty::t, t_glb: ty::t) {
-        debug!("check_glb(t1=%s, t2=%s, t_glb=%s)",
+        debug!("check_glb(t1={}, t2={}, t_glb={})",
                self.ty_to_str(t1),
                self.ty_to_str(t2),
                self.ty_to_str(t_glb));
         match self.glb().tys(t1, t2) {
             Err(e) => {
-                fail!("unexpected error computing LUB: %?", e)
+                fail!("unexpected error computing LUB: {:?}", e)
             }
             Ok(t) => {
                 self.assert_eq(t, t_glb);
@@ -270,8 +344,6 @@ impl Env {
                 // sanity check for good measure:
                 self.assert_subtype(t, t1);
                 self.assert_subtype(t, t2);
-
-                self.resolve_regions(0);
             }
         }
     }
@@ -281,7 +353,7 @@ impl Env {
         match self.lub().tys(t1, t2) {
             Err(_) => {}
             Ok(t) => {
-                fail!("unexpected success computing LUB: %?", self.ty_to_str(t))
+                fail!("unexpected success computing LUB: {}", self.ty_to_str(t))
             }
         }
     }
@@ -291,120 +363,151 @@ impl Env {
         match self.glb().tys(t1, t2) {
             Err(_) => {}
             Ok(t) => {
-                fail!("unexpected success computing GLB: %?", self.ty_to_str(t))
+                fail!("unexpected success computing GLB: {}", self.ty_to_str(t))
             }
         }
     }
 }
 
 #[test]
-fn contravariant_region_ptr() {
-    let env = setup_env("contravariant_region_ptr", EMPTY_SOURCE_STR);
-    env.create_simple_region_hierarchy();
-    let t_rptr1 = env.t_rptr_scope(1);
-    let t_rptr10 = env.t_rptr_scope(10);
-    env.assert_eq(t_rptr1, t_rptr1);
-    env.assert_eq(t_rptr10, t_rptr10);
-    env.assert_strict_subtype(t_rptr1, t_rptr10);
+fn contravariant_region_ptr_ok() {
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        env.create_simple_region_hierarchy();
+        let t_rptr1 = env.t_rptr_scope(1);
+        let t_rptr10 = env.t_rptr_scope(10);
+        env.assert_eq(t_rptr1, t_rptr1);
+        env.assert_eq(t_rptr10, t_rptr10);
+        env.make_subtype(t_rptr1, t_rptr10);
+    })
+}
+
+#[test]
+fn contravariant_region_ptr_err() {
+    test_env("contravariant_region_ptr",
+             EMPTY_SOURCE_STR,
+             errors(["lifetime mismatch"]),
+             |env| {
+                 env.create_simple_region_hierarchy();
+                 let t_rptr1 = env.t_rptr_scope(1);
+                 let t_rptr10 = env.t_rptr_scope(10);
+                 env.assert_eq(t_rptr1, t_rptr1);
+                 env.assert_eq(t_rptr10, t_rptr10);
+
+                 // will cause an error when regions are resolved
+                 env.make_subtype(t_rptr10, t_rptr1);
+             })
 }
 
 #[test]
 fn lub_bound_bound() {
-    let env = setup_env("lub_bound_bound", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_bound2 = env.t_rptr_bound(2);
-    env.check_lub(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_bound2], env.t_int()),
-                  env.t_fn([t_rptr_bound1], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_bound2 = env.t_rptr_late_bound(22, 2);
+        env.check_lub(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound2], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound1], env.t_int()));
+    })
 }
 
 #[test]
 fn lub_bound_free() {
-    let env = setup_env("lub_bound_free", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_free1 = env.t_rptr_free(0, 1);
-    env.check_lub(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_free1], env.t_int()),
-                  env.t_fn([t_rptr_free1], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_free1 = env.t_rptr_free(0, 1);
+        env.check_lub(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_free1], env.t_int()),
+                      env.t_fn(22, [t_rptr_free1], env.t_int()));
+    })
 }
 
 #[test]
 fn lub_bound_static() {
-    let env = setup_env("lub_bound_static", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_static = env.t_rptr_static();
-    env.check_lub(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_static], env.t_int()),
-                  env.t_fn([t_rptr_static], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_static = env.t_rptr_static();
+        env.check_lub(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_static], env.t_int()),
+                      env.t_fn(22, [t_rptr_static], env.t_int()));
+    })
 }
 
 #[test]
 fn lub_bound_bound_inverse_order() {
-    let env = setup_env("lub_bound_bound_inverse_order", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_bound2 = env.t_rptr_bound(2);
-    env.check_lub(env.t_fn([t_rptr_bound1, t_rptr_bound2], t_rptr_bound1),
-                  env.t_fn([t_rptr_bound2, t_rptr_bound1], t_rptr_bound1),
-                  env.t_fn([t_rptr_bound1, t_rptr_bound1], t_rptr_bound1));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_bound2 = env.t_rptr_late_bound(22, 2);
+        env.check_lub(env.t_fn(22, [t_rptr_bound1, t_rptr_bound2], t_rptr_bound1),
+                      env.t_fn(22, [t_rptr_bound2, t_rptr_bound1], t_rptr_bound1),
+                      env.t_fn(22, [t_rptr_bound1, t_rptr_bound1], t_rptr_bound1));
+    })
 }
 
 #[test]
 fn lub_free_free() {
-    let env = setup_env("lub_free_free", EMPTY_SOURCE_STR);
-    let t_rptr_free1 = env.t_rptr_free(0, 1);
-    let t_rptr_free2 = env.t_rptr_free(0, 2);
-    let t_rptr_static = env.t_rptr_static();
-    env.check_lub(env.t_fn([t_rptr_free1], env.t_int()),
-                  env.t_fn([t_rptr_free2], env.t_int()),
-                  env.t_fn([t_rptr_static], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_free1 = env.t_rptr_free(0, 1);
+        let t_rptr_free2 = env.t_rptr_free(0, 2);
+        let t_rptr_static = env.t_rptr_static();
+        env.check_lub(env.t_fn(22, [t_rptr_free1], env.t_int()),
+                      env.t_fn(22, [t_rptr_free2], env.t_int()),
+                      env.t_fn(22, [t_rptr_static], env.t_int()));
+    })
 }
 
 #[test]
 fn lub_returning_scope() {
-    let env = setup_env("lub_returning_scope", EMPTY_SOURCE_STR);
-    let t_rptr_scope10 = env.t_rptr_scope(10);
-    let t_rptr_scope11 = env.t_rptr_scope(11);
-    env.check_no_lub(env.t_fn([], t_rptr_scope10),
-                     env.t_fn([], t_rptr_scope11));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR,
+             errors(["cannot infer an appropriate lifetime"]), |env| {
+                 let t_rptr_scope10 = env.t_rptr_scope(10);
+                 let t_rptr_scope11 = env.t_rptr_scope(11);
+
+                 // this should generate an error when regions are resolved
+                 env.make_lub_ty(env.t_fn(22, [], t_rptr_scope10),
+                                 env.t_fn(22, [], t_rptr_scope11));
+             })
 }
 
 #[test]
 fn glb_free_free_with_common_scope() {
-    let env = setup_env("glb_free_free", EMPTY_SOURCE_STR);
-    let t_rptr_free1 = env.t_rptr_free(0, 1);
-    let t_rptr_free2 = env.t_rptr_free(0, 2);
-    let t_rptr_scope = env.t_rptr_scope(0);
-    env.check_glb(env.t_fn([t_rptr_free1], env.t_int()),
-                  env.t_fn([t_rptr_free2], env.t_int()),
-                  env.t_fn([t_rptr_scope], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_free1 = env.t_rptr_free(0, 1);
+        let t_rptr_free2 = env.t_rptr_free(0, 2);
+        let t_rptr_scope = env.t_rptr_scope(0);
+        env.check_glb(env.t_fn(22, [t_rptr_free1], env.t_int()),
+                      env.t_fn(22, [t_rptr_free2], env.t_int()),
+                      env.t_fn(22, [t_rptr_scope], env.t_int()));
+    })
 }
 
 #[test]
 fn glb_bound_bound() {
-    let env = setup_env("glb_bound_bound", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_bound2 = env.t_rptr_bound(2);
-    env.check_glb(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_bound2], env.t_int()),
-                  env.t_fn([t_rptr_bound1], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_bound2 = env.t_rptr_late_bound(22, 2);
+        env.check_glb(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound2], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound1], env.t_int()));
+    })
 }
 
 #[test]
 fn glb_bound_free() {
-    let env = setup_env("glb_bound_free", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_free1 = env.t_rptr_free(0, 1);
-    env.check_glb(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_free1], env.t_int()),
-                  env.t_fn([t_rptr_bound1], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_free1 = env.t_rptr_free(0, 1);
+        env.check_glb(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_free1], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound1], env.t_int()));
+    })
 }
 
 #[test]
 fn glb_bound_static() {
-    let env = setup_env("glb_bound_static", EMPTY_SOURCE_STR);
-    let t_rptr_bound1 = env.t_rptr_bound(1);
-    let t_rptr_static = env.t_rptr_static();
-    env.check_glb(env.t_fn([t_rptr_bound1], env.t_int()),
-                  env.t_fn([t_rptr_static], env.t_int()),
-                  env.t_fn([t_rptr_bound1], env.t_int()));
+    test_env("contravariant_region_ptr", EMPTY_SOURCE_STR, errors([]), |env| {
+        let t_rptr_bound1 = env.t_rptr_late_bound(22, 1);
+        let t_rptr_static = env.t_rptr_static();
+        env.check_glb(env.t_fn(22, [t_rptr_bound1], env.t_int()),
+                      env.t_fn(22, [t_rptr_static], env.t_int()),
+                      env.t_fn(22, [t_rptr_bound1], env.t_int()));
+    })
 }
diff --git a/src/librustc/middle/typeck/infer/to_str.rs b/src/librustc/middle/typeck/infer/to_str.rs
deleted file mode 100644
index 097c5dcfeda..00000000000
--- a/src/librustc/middle/typeck/infer/to_str.rs
+++ /dev/null
@@ -1,96 +0,0 @@
-// Copyright 2012 The Rust Project Developers. See the COPYRIGHT
-// file at the top-level directory of this distribution and at
-// http://rust-lang.org/COPYRIGHT.
-//
-// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
-// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
-// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
-// option. This file may not be copied, modified, or distributed
-// except according to those terms.
-
-
-use middle::ty::{FnSig, Vid};
-use middle::ty::IntVarValue;
-use middle::ty;
-use middle::typeck::infer::{Bound, Bounds};
-use middle::typeck::infer::InferCtxt;
-use middle::typeck::infer::unify::{Redirect, Root, VarValue};
-use util::ppaux::{mt_to_str, ty_to_str, trait_ref_to_str};
-
-use syntax::ast;
-
-pub trait InferStr {
-    fn inf_str(&self, cx: &InferCtxt) -> String;
-}
-
-impl InferStr for ty::t {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        ty_to_str(cx.tcx, *self)
-    }
-}
-
-impl InferStr for FnSig {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        format!("({}) -> {}",
-                self.inputs.iter()
-                    .map(|a| a.inf_str(cx))
-                    .collect::<Vec<String>>().connect(", "),
-                self.output.inf_str(cx))
-    }
-}
-
-impl InferStr for ty::mt {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        mt_to_str(cx.tcx, self)
-    }
-}
-
-impl InferStr for ty::Region {
-    fn inf_str(&self, _cx: &InferCtxt) -> String {
-        format!("{:?}", *self)
-    }
-}
-
-impl<V:InferStr> InferStr for Bound<V> {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        match *self {
-            Some(ref v) => v.inf_str(cx),
-            None => "none".to_string()
-        }
-    }
-}
-
-impl<T:InferStr> InferStr for Bounds<T> {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        format!("{{{} <: {}}}", self.lb.inf_str(cx), self.ub.inf_str(cx))
-    }
-}
-
-impl<V:Vid + ToStr,T:InferStr> InferStr for VarValue<V, T> {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        match *self {
-          Redirect(ref vid) => format!("Redirect({})", vid.to_str()),
-          Root(ref pt, rk) => {
-              format!("Root({}, {})", pt.inf_str(cx), rk)
-          }
-        }
-    }
-}
-
-impl InferStr for IntVarValue {
-    fn inf_str(&self, _cx: &InferCtxt) -> String {
-        self.to_str()
-    }
-}
-
-impl InferStr for ast::FloatTy {
-    fn inf_str(&self, _cx: &InferCtxt) -> String {
-        self.to_str()
-    }
-}
-
-impl InferStr for ty::TraitRef {
-    fn inf_str(&self, cx: &InferCtxt) -> String {
-        trait_ref_to_str(cx.tcx, self)
-    }
-}
diff --git a/src/librustc/middle/typeck/infer/unify.rs b/src/librustc/middle/typeck/infer/unify.rs
index 78c841afa60..f106ce18a4a 100644
--- a/src/librustc/middle/typeck/infer/unify.rs
+++ b/src/librustc/middle/typeck/infer/unify.rs
@@ -8,179 +8,372 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
+use std::kinds::marker;
 
-use std::collections::SmallIntMap;
-
-use middle::ty::{Vid, expected_found, IntVarValue};
+use middle::ty::{expected_found, IntVarValue};
 use middle::ty;
 use middle::typeck::infer::{Bounds, uok, ures};
 use middle::typeck::infer::InferCtxt;
-use middle::typeck::infer::to_str::InferStr;
 use std::cell::RefCell;
+use std::fmt::Show;
+use std::mem;
 use syntax::ast;
+use util::ppaux::Repr;
 
-#[deriving(Clone)]
-pub enum VarValue<V, T> {
-    Redirect(V),
-    Root(T, uint),
+/**
+ * This trait is implemented by any type that can serve as a type
+ * variable. We call such variables *unification keys*. For example,
+ * this trait is implemented by `TyVid`, which represents normal
+ * type variables, and `IntVid`, which represents integral variables.
+ *
+ * Each key type has an associated value type `V`. For example,
+ * for `TyVid`, this is `Bounds<ty::t>`, representing a pair of
+ * upper- and lower-bound types.
+ *
+ * Implementations of this trait are at the end of this file.
+ */
+pub trait UnifyKey<V> : Clone + Show + PartialEq + Repr {
+    fn index(&self) -> uint;
+
+    fn from_index(u: uint) -> Self;
+
+    /**
+     * Given an inference context, returns the unification table
+     * appropriate to this key type.
+     */
+    fn unification_table<'v>(infcx: &'v InferCtxt)
+                             -> &'v RefCell<UnificationTable<Self,V>>;
+
+    fn tag(k: Option<Self>) -> &'static str;
 }
 
-pub struct ValsAndBindings<V, T> {
-    pub vals: SmallIntMap<VarValue<V, T>>,
-    pub bindings: Vec<(V, VarValue<V, T>)> ,
+/**
+ * Trait for valid types that a type variable can be set to.  Note
+ * that this is typically not the end type that the value will
+ * take on, but rather some wrapper: for example, for normal type
+ * variables, the associated type is not `ty::t` but rather
+ * `Bounds<ty::t>`.
+ *
+ * Implementations of this trait are at the end of this file.
+ */
+pub trait UnifyValue : Clone + Repr + PartialEq {
 }
 
-impl<V:Clone, T:Clone> ValsAndBindings<V, T> {
-    pub fn new() -> ValsAndBindings<V, T> {
-        ValsAndBindings {
-            vals: SmallIntMap::new(),
-            bindings: Vec::new()
-        }
-    }
+/**
+ * Value of a unification key. We implement Tarjan's union-find
+ * algorithm: when two keys are unified, one of them is converted
+ * into a "redirect" pointing at the other. These redirects form a
+ * DAG: the roots of the DAG (nodes that are not redirected) are each
+ * associated with a value of type `V` and a rank. The rank is used
+ * to keep the DAG relatively balanced, which helps keep the running
+ * time of the algorithm under control. For more information, see
+ * <http://en.wikipedia.org/wiki/Disjoint-set_data_structure>.
+ */
+#[deriving(PartialEq,Clone)]
+pub enum VarValue<K,V> {
+    Redirect(K),
+    Root(V, uint),
 }
 
-pub struct Node<V, T> {
-    pub root: V,
-    pub possible_types: T,
+/**
+ * Table of unification keys and their values.
+ */
+pub struct UnificationTable<K,V> {
+    /**
+     * Indicates the current value of each key.
+     */
+    values: Vec<VarValue<K,V>>,
+
+    /**
+     * When a snapshot is active, logs each change made to the table
+     * so that they can be unrolled.
+     */
+    undo_log: Vec<UndoLog<K,V>>,
+}
+
+/**
+ * At any time, users may snapshot a unification table.  The changes
+ * made during the snapshot may either be *commited* or *rolled back*.
+ */
+pub struct Snapshot<K> {
+    // Ensure that this snapshot is keyed to the table type.
+    marker1: marker::CovariantType<K>,
+
+    // Snapshots are tokens that should be created/consumed linearly.
+    marker2: marker::NoCopy,
+
+    // Length of the undo log at the time the snapshot was taken.
+    length: uint,
+}
+
+#[deriving(PartialEq)]
+enum UndoLog<K,V> {
+    /// Indicates where a snapshot started.
+    OpenSnapshot,
+
+    /// Indicates a snapshot that has been committed.
+    CommittedSnapshot,
+
+    /// New variable with given index was created.
+    NewVar(uint),
+
+    /// Variable with given index was changed *from* the given value.
+    SetVar(uint, VarValue<K,V>),
+}
+
+/**
+ * Internal type used to represent the result of a `get()` operation.
+ * Conveys the current root and value of the key.
+ */
+pub struct Node<K,V> {
+    pub key: K,
+    pub value: V,
     pub rank: uint,
 }
 
-pub trait UnifyVid<T> {
-    fn appropriate_vals_and_bindings<'v>(infcx: &'v InferCtxt)
-                                     -> &'v RefCell<ValsAndBindings<Self, T>>;
-}
+// We can't use V:LatticeValue, much as I would like to,
+// because frequently the pattern is that V=Bounds<U> for some
+// other type parameter U, and we have no way to say
+// Bounds<U>:
 
-pub trait UnifyInferCtxtMethods {
-    fn get<T:Clone,
-           V:Clone + PartialEq + Vid + UnifyVid<T>>(
-           &self,
-           vid: V)
-           -> Node<V, T>;
-    fn set<T:Clone + InferStr,
-           V:Clone + Vid + ToStr + UnifyVid<T>>(
-           &self,
-           vid: V,
-           new_v: VarValue<V, T>);
-    fn unify<T:Clone + InferStr,
-             V:Clone + Vid + ToStr + UnifyVid<T>>(
-             &self,
-             node_a: &Node<V, T>,
-             node_b: &Node<V, T>)
-             -> (V, uint);
-}
+impl<V:PartialEq+Clone+Repr,K:UnifyKey<V>> UnificationTable<K,V> {
+    pub fn new() -> UnificationTable<K,V> {
+        UnificationTable {
+            values: Vec::new(),
+            undo_log: Vec::new()
+        }
+    }
 
-impl<'a> UnifyInferCtxtMethods for InferCtxt<'a> {
-    fn get<T:Clone,
-           V:Clone + PartialEq + Vid + UnifyVid<T>>(
-           &self,
-           vid: V)
-           -> Node<V, T> {
+    pub fn in_snapshot(&self) -> bool {
+        /*! True if a snapshot has been started. */
+
+        self.undo_log.len() > 0
+    }
+
+    /**
+     * Starts a new snapshot. Each snapshot must be either
+     * rolled back or commited in a "LIFO" (stack) order.
+     */
+    pub fn snapshot(&mut self) -> Snapshot<K> {
+        let length = self.undo_log.len();
+        debug!("{}: snapshot at length {}",
+               UnifyKey::tag(None::<K>),
+               length);
+        self.undo_log.push(OpenSnapshot);
+        Snapshot { length: length,
+                   marker1: marker::CovariantType,
+                   marker2: marker::NoCopy }
+    }
+
+    fn assert_open_snapshot(&self, snapshot: &Snapshot<K>) {
+        // Or else there was a failure to follow a stack discipline:
+        assert!(self.undo_log.len() > snapshot.length);
+
+        // Invariant established by start_snapshot():
+        assert!(*self.undo_log.get(snapshot.length) == OpenSnapshot);
+    }
+
+    /**
+     * Reverses all changes since the last snapshot. Also
+     * removes any keys that have been created since then.
+     */
+    pub fn rollback_to(&mut self, tcx: &ty::ctxt, snapshot: Snapshot<K>) {
+        debug!("{}: rollback_to({})",
+               UnifyKey::tag(None::<K>),
+               snapshot.length);
+
+        self.assert_open_snapshot(&snapshot);
+
+        while self.undo_log.len() > snapshot.length + 1 {
+            match self.undo_log.pop().unwrap() {
+                OpenSnapshot => {
+                    // This indicates a failure to obey the stack discipline.
+                    tcx.sess.bug("Cannot rollback an uncommited snapshot");
+                }
+
+                CommittedSnapshot => {
+                    // This occurs when there are nested snapshots and
+                    // the inner is commited but outer is rolled back.
+                }
+
+                NewVar(i) => {
+                    assert!(self.values.len() == i);
+                    self.values.pop();
+                }
+
+                SetVar(i, v) => {
+                    *self.values.get_mut(i) = v;
+                }
+            }
+        }
+
+        let v = self.undo_log.pop().unwrap();
+        assert!(v == OpenSnapshot);
+        assert!(self.undo_log.len() == snapshot.length);
+    }
+
+    /**
+     * Commits all changes since the last snapshot. Of course, they
+     * can still be undone if there is a snapshot further out.
+     */
+    pub fn commit(&mut self, snapshot: Snapshot<K>) {
+        debug!("{}: commit({})",
+               UnifyKey::tag(None::<K>),
+               snapshot.length);
+
+        self.assert_open_snapshot(&snapshot);
+
+        if snapshot.length == 0 {
+            // The root snapshot.
+            self.undo_log.truncate(0);
+        } else {
+            *self.undo_log.get_mut(snapshot.length) = CommittedSnapshot;
+        }
+    }
+
+    pub fn new_key(&mut self, value: V) -> K {
+        let index = self.values.len();
+
+        if self.in_snapshot() {
+            self.undo_log.push(NewVar(index));
+        }
+
+        self.values.push(Root(value, 0));
+        let k = UnifyKey::from_index(index);
+        debug!("{}: created new key: {}",
+               UnifyKey::tag(None::<K>),
+               k);
+        k
+    }
+
+    fn swap_value(&mut self,
+                  index: uint,
+                  new_value: VarValue<K,V>)
+                  -> VarValue<K,V>
+    {
+        /*!
+         * Primitive operation to swap a value in the var array.
+         * Caller should update the undo log if we are in a snapshot.
+         */
+
+        let loc = self.values.get_mut(index);
+        mem::replace(loc, new_value)
+    }
+
+    pub fn get(&mut self, tcx: &ty::ctxt, vid: K) -> Node<K,V> {
         /*!
-         *
          * Find the root node for `vid`. This uses the standard
          * union-find algorithm with path compression:
          * http://en.wikipedia.org/wiki/Disjoint-set_data_structure
          */
 
-        let tcx = self.tcx;
-        let vb = UnifyVid::appropriate_vals_and_bindings(self);
-        return helper(tcx, &mut *vb.borrow_mut(), vid);
+        let index = vid.index();
+        let value = (*self.values.get(index)).clone();
+        match value {
+            Redirect(redirect) => {
+                let node: Node<K,V> = self.get(tcx, redirect.clone());
+                if node.key != redirect {
+                    // Path compression
+                    let old_value =
+                        self.swap_value(index, Redirect(node.key.clone()));
 
-        fn helper<T:Clone, V:Clone+PartialEq+Vid>(
-            tcx: &ty::ctxt,
-            vb: &mut ValsAndBindings<V,T>,
-            vid: V) -> Node<V, T>
-        {
-            let vid_u = vid.to_uint();
-            let var_val = match vb.vals.find(&vid_u) {
-                Some(&ref var_val) => (*var_val).clone(),
-                None => {
-                    tcx.sess.bug(format!(
-                        "failed lookup of vid `{}`", vid_u).as_slice());
-                }
-            };
-            match var_val {
-                Redirect(vid) => {
-                    let node: Node<V,T> = helper(tcx, vb, vid.clone());
-                    if node.root != vid {
-                        // Path compression
-                        vb.vals.insert(vid.to_uint(),
-                                       Redirect(node.root.clone()));
+                    // If we are in a snapshot, record this compression,
+                    // because it's possible that the unification which
+                    // caused it will be rolled back later.
+                    if self.in_snapshot() {
+                        self.undo_log.push(SetVar(index, old_value));
                     }
-                    node
-                }
-                Root(pt, rk) => {
-                    Node {root: vid, possible_types: pt, rank: rk}
                 }
+                node
+            }
+            Root(value, rank) => {
+                Node { key: vid, value: value, rank: rank }
             }
         }
     }
 
-    fn set<T:Clone + InferStr,
-           V:Clone + Vid + ToStr + UnifyVid<T>>(
-           &self,
-           vid: V,
-           new_v: VarValue<V, T>) {
-        /*!
-         *
-         * Sets the value for `vid` to `new_v`.  `vid` MUST be a root node!
-         */
-
-        debug!("Updating variable {} to {}",
-               vid.to_str(), new_v.inf_str(self));
-
-        let vb = UnifyVid::appropriate_vals_and_bindings(self);
-        let mut vb = vb.borrow_mut();
-        let old_v = (*vb.vals.get(&vid.to_uint())).clone();
-        vb.bindings.push((vid.clone(), old_v));
-        vb.vals.insert(vid.to_uint(), new_v);
+    fn is_root(&self, key: &K) -> bool {
+        match *self.values.get(key.index()) {
+            Redirect(..) => false,
+            Root(..) => true,
+        }
     }
 
-    fn unify<T:Clone + InferStr,
-             V:Clone + Vid + ToStr + UnifyVid<T>>(
-             &self,
-             node_a: &Node<V, T>,
-             node_b: &Node<V, T>)
-             -> (V, uint) {
-        // Rank optimization: if you don't know what it is, check
-        // out <http://en.wikipedia.org/wiki/Disjoint-set_data_structure>
+    pub fn set(&mut self,
+               tcx: &ty::ctxt,
+               key: K,
+               new_value: VarValue<K,V>)
+    {
+        /*!
+         * Sets the value for `vid` to `new_value`. `vid` MUST be a
+         * root node! Also, we must be in the middle of a snapshot.
+         */
 
-        debug!("unify(node_a(id={:?}, rank={:?}), \
-                node_b(id={:?}, rank={:?}))",
-               node_a.root, node_a.rank,
-               node_b.root, node_b.rank);
+        assert!(self.is_root(&key));
+        assert!(self.in_snapshot());
+
+        debug!("Updating variable {} to {}",
+               key.repr(tcx),
+               new_value.repr(tcx));
+
+        let index = key.index();
+        let old_value = self.swap_value(index, new_value);
+        self.undo_log.push(SetVar(index, old_value));
+    }
+
+    pub fn unify(&mut self,
+                 tcx: &ty::ctxt,
+                 node_a: &Node<K,V>,
+                 node_b: &Node<K,V>)
+                 -> (K, uint)
+    {
+        /*!
+         * Either redirects node_a to node_b or vice versa, depending
+         * on the relative rank. Returns the new root and rank.  You
+         * should then update the value of the new root to something
+         * suitable.
+         */
+
+        debug!("unify(node_a(id={}, rank={}), node_b(id={}, rank={}))",
+               node_a.key.repr(tcx),
+               node_a.rank,
+               node_b.key.repr(tcx),
+               node_b.rank);
 
         if node_a.rank > node_b.rank {
             // a has greater rank, so a should become b's parent,
             // i.e., b should redirect to a.
-            self.set(node_b.root.clone(), Redirect(node_a.root.clone()));
-            (node_a.root.clone(), node_a.rank)
+            self.set(tcx, node_b.key.clone(), Redirect(node_a.key.clone()));
+            (node_a.key.clone(), node_a.rank)
         } else if node_a.rank < node_b.rank {
             // b has greater rank, so a should redirect to b.
-            self.set(node_a.root.clone(), Redirect(node_b.root.clone()));
-            (node_b.root.clone(), node_b.rank)
+            self.set(tcx, node_a.key.clone(), Redirect(node_b.key.clone()));
+            (node_b.key.clone(), node_b.rank)
         } else {
             // If equal, redirect one to the other and increment the
             // other's rank.
             assert_eq!(node_a.rank, node_b.rank);
-            self.set(node_b.root.clone(), Redirect(node_a.root.clone()));
-            (node_a.root.clone(), node_a.rank + 1)
+            self.set(tcx, node_b.key.clone(), Redirect(node_a.key.clone()));
+            (node_a.key.clone(), node_a.rank + 1)
         }
     }
-
 }
 
-// ______________________________________________________________________
-// Code to handle simple variables like ints, floats---anything that
+///////////////////////////////////////////////////////////////////////////
+// Code to handle simple keys like ints, floats---anything that
 // doesn't have a subtyping relationship we need to worry about.
 
-pub trait SimplyUnifiable {
+/**
+ * Indicates a type that does not have any kind of subtyping
+ * relationship.
+ */
+pub trait SimplyUnifiable : Clone + PartialEq + Repr {
     fn to_type_err(expected_found<Self>) -> ty::type_err;
 }
 
-pub fn mk_err<T:SimplyUnifiable>(a_is_expected: bool,
-                                 a_t: T,
-                                 b_t: T) -> ures {
+pub fn err<V:SimplyUnifiable>(a_is_expected: bool,
+                              a_t: V,
+                              b_t: V) -> ures {
     if a_is_expected {
         Err(SimplyUnifiable::to_type_err(
             ty::expected_found {expected: a_t, found: b_t}))
@@ -190,111 +383,141 @@ pub fn mk_err<T:SimplyUnifiable>(a_is_expected: bool,
     }
 }
 
-pub trait InferCtxtMethods {
-    fn simple_vars<T:Clone + PartialEq + InferStr + SimplyUnifiable,
-                   V:Clone + PartialEq + Vid + ToStr + UnifyVid<Option<T>>>(
-                   &self,
+pub trait InferCtxtMethodsForSimplyUnifiableTypes<V:SimplyUnifiable,
+                                                  K:UnifyKey<Option<V>>> {
+    fn simple_vars(&self,
                    a_is_expected: bool,
-                   a_id: V,
-                   b_id: V)
+                   a_id: K,
+                   b_id: K)
                    -> ures;
-    fn simple_var_t<T:Clone + PartialEq + InferStr + SimplyUnifiable,
-                    V:Clone + PartialEq + Vid + ToStr + UnifyVid<Option<T>>>(
-                    &self,
+    fn simple_var_t(&self,
                     a_is_expected: bool,
-                    a_id: V,
-                    b: T)
+                    a_id: K,
+                    b: V)
                     -> ures;
 }
 
-impl<'a> InferCtxtMethods for InferCtxt<'a> {
-    fn simple_vars<T:Clone + PartialEq + InferStr + SimplyUnifiable,
-                   V:Clone + PartialEq + Vid + ToStr + UnifyVid<Option<T>>>(
-                   &self,
+impl<'tcx,V:SimplyUnifiable,K:UnifyKey<Option<V>>>
+    InferCtxtMethodsForSimplyUnifiableTypes<V,K> for InferCtxt<'tcx>
+{
+    fn simple_vars(&self,
                    a_is_expected: bool,
-                   a_id: V,
-                   b_id: V)
-                   -> ures {
+                   a_id: K,
+                   b_id: K)
+                   -> ures
+    {
         /*!
-         *
-         * Unifies two simple variables.  Because simple variables do
-         * not have any subtyping relationships, if both variables
+         * Unifies two simple keys.  Because simple keys do
+         * not have any subtyping relationships, if both keys
          * have already been associated with a value, then those two
-         * values must be the same. */
+         * values must be the same.
+         */
 
-        let node_a = self.get(a_id);
-        let node_b = self.get(b_id);
-        let a_id = node_a.root.clone();
-        let b_id = node_b.root.clone();
+        let tcx = self.tcx;
+        let table = UnifyKey::unification_table(self);
+        let node_a = table.borrow_mut().get(tcx, a_id);
+        let node_b = table.borrow_mut().get(tcx, b_id);
+        let a_id = node_a.key.clone();
+        let b_id = node_b.key.clone();
 
         if a_id == b_id { return uok(); }
 
-        let combined = match (&node_a.possible_types, &node_b.possible_types)
-        {
-            (&None, &None) => None,
-            (&Some(ref v), &None) | (&None, &Some(ref v)) => {
-                Some((*v).clone())
-            }
-            (&Some(ref v1), &Some(ref v2)) => {
-                if *v1 != *v2 {
-                    return mk_err(a_is_expected, (*v1).clone(), (*v2).clone())
+        let combined = {
+            match (&node_a.value, &node_b.value) {
+                (&None, &None) => {
+                    None
+                }
+                (&Some(ref v), &None) | (&None, &Some(ref v)) => {
+                    Some((*v).clone())
+                }
+                (&Some(ref v1), &Some(ref v2)) => {
+                    if *v1 != *v2 {
+                        return err(a_is_expected, (*v1).clone(), (*v2).clone())
+                    }
+                    Some((*v1).clone())
                 }
-                Some((*v1).clone())
             }
         };
 
-        let (new_root, new_rank) = self.unify(&node_a, &node_b);
-        self.set(new_root, Root(combined, new_rank));
-        return uok();
+        let (new_root, new_rank) = table.borrow_mut().unify(tcx,
+                                                            &node_a,
+                                                            &node_b);
+        table.borrow_mut().set(tcx, new_root, Root(combined, new_rank));
+        return Ok(())
     }
 
-    fn simple_var_t<T:Clone + PartialEq + InferStr + SimplyUnifiable,
-                    V:Clone + PartialEq + Vid + ToStr + UnifyVid<Option<T>>>(
-                    &self,
+    fn simple_var_t(&self,
                     a_is_expected: bool,
-                    a_id: V,
-                    b: T)
-                    -> ures {
+                    a_id: K,
+                    b: V)
+                    -> ures
+    {
         /*!
-         *
-         * Sets the value of the variable `a_id` to `b`.  Because
-         * simple variables do not have any subtyping relationships,
+         * Sets the value of the key `a_id` to `b`.  Because
+         * simple keys do not have any subtyping relationships,
          * if `a_id` already has a value, it must be the same as
-         * `b`. */
+         * `b`.
+         */
 
-        let node_a = self.get(a_id);
-        let a_id = node_a.root.clone();
+        let tcx = self.tcx;
+        let table = UnifyKey::unification_table(self);
+        let node_a = table.borrow_mut().get(tcx, a_id);
+        let a_id = node_a.key.clone();
 
-        match node_a.possible_types {
+        match node_a.value {
             None => {
-                self.set(a_id, Root(Some(b), node_a.rank));
-                return uok();
+                table.borrow_mut().set(tcx, a_id, Root(Some(b), node_a.rank));
+                return Ok(());
             }
 
             Some(ref a_t) => {
                 if *a_t == b {
-                    return uok();
+                    return Ok(());
                 } else {
-                    return mk_err(a_is_expected, (*a_t).clone(), b);
+                    return err(a_is_expected, (*a_t).clone(), b);
                 }
             }
         }
     }
 }
 
-// ______________________________________________________________________
+///////////////////////////////////////////////////////////////////////////
 
-impl UnifyVid<Bounds<ty::t>> for ty::TyVid {
-    fn appropriate_vals_and_bindings<'v>(infcx: &'v InferCtxt)
-        -> &'v RefCell<ValsAndBindings<ty::TyVid, Bounds<ty::t>>> {
-        return &infcx.ty_var_bindings;
+// General type keys
+
+impl UnifyKey<Bounds<ty::t>> for ty::TyVid {
+    fn index(&self) -> uint { self.index }
+
+    fn from_index(i: uint) -> ty::TyVid { ty::TyVid { index: i } }
+
+    fn unification_table<'v>(infcx: &'v InferCtxt)
+        -> &'v RefCell<UnificationTable<ty::TyVid, Bounds<ty::t>>>
+    {
+        return &infcx.type_unification_table;
+    }
+
+    fn tag(_: Option<ty::TyVid>) -> &'static str {
+        "TyVid"
     }
 }
 
-impl UnifyVid<Option<IntVarValue>> for ty::IntVid {
-    fn appropriate_vals_and_bindings<'v>(infcx: &'v InferCtxt)
-        -> &'v RefCell<ValsAndBindings<ty::IntVid, Option<IntVarValue>>> {
-        return &infcx.int_var_bindings;
+impl UnifyValue for Bounds<ty::t> { }
+
+// Integral type keys
+
+impl UnifyKey<Option<IntVarValue>> for ty::IntVid {
+    fn index(&self) -> uint { self.index }
+
+    fn from_index(i: uint) -> ty::IntVid { ty::IntVid { index: i } }
+
+    fn unification_table<'v>(infcx: &'v InferCtxt)
+        -> &'v RefCell<UnificationTable<ty::IntVid, Option<IntVarValue>>>
+    {
+        return &infcx.int_unification_table;
+    }
+
+    fn tag(_: Option<ty::IntVid>) -> &'static str {
+        "IntVid"
     }
 }
 
@@ -304,11 +527,27 @@ impl SimplyUnifiable for IntVarValue {
     }
 }
 
-impl UnifyVid<Option<ast::FloatTy>> for ty::FloatVid {
-    fn appropriate_vals_and_bindings<'v>(infcx: &'v InferCtxt)
-        -> &'v RefCell<ValsAndBindings<ty::FloatVid, Option<ast::FloatTy>>> {
-        return &infcx.float_var_bindings;
+impl UnifyValue for Option<IntVarValue> { }
+
+// Floating point type keys
+
+impl UnifyKey<Option<ast::FloatTy>> for ty::FloatVid {
+    fn index(&self) -> uint { self.index }
+
+    fn from_index(i: uint) -> ty::FloatVid { ty::FloatVid { index: i } }
+
+    fn unification_table<'v>(infcx: &'v InferCtxt)
+        -> &'v RefCell<UnificationTable<ty::FloatVid, Option<ast::FloatTy>>>
+    {
+        return &infcx.float_unification_table;
     }
+
+    fn tag(_: Option<ty::FloatVid>) -> &'static str {
+        "FloatVid"
+    }
+}
+
+impl UnifyValue for Option<ast::FloatTy> {
 }
 
 impl SimplyUnifiable for ast::FloatTy {
diff --git a/src/librustc/util/ppaux.rs b/src/librustc/util/ppaux.rs
index 6e9ee92c0a3..d08dd4f6cbc 100644
--- a/src/librustc/util/ppaux.rs
+++ b/src/librustc/util/ppaux.rs
@@ -24,6 +24,10 @@ use middle::ty::{ty_nil, ty_param, ty_ptr, ty_rptr, ty_tup};
 use middle::ty::{ty_uniq, ty_trait, ty_int, ty_uint, ty_infer};
 use middle::ty;
 use middle::typeck;
+use middle::typeck::infer;
+use middle::typeck::infer::unify;
+use VV = middle::typeck::infer::unify::VarValue;
+use middle::typeck::infer::region_inference;
 
 use std::rc::Rc;
 use std::gc::Gc;
@@ -574,6 +578,12 @@ impl Repr for ty::t {
     }
 }
 
+impl Repr for ty::mt {
+    fn repr(&self, tcx: &ctxt) -> String {
+        mt_to_str(tcx, self)
+    }
+}
+
 impl Repr for subst::Substs {
     fn repr(&self, tcx: &ctxt) -> String {
         format!("Substs[types={}, regions={}]",
@@ -707,7 +717,7 @@ impl Repr for ty::Region {
             }
 
             ty::ReInfer(ReVar(ref vid)) => {
-                format!("ReInfer({})", vid.id)
+                format!("ReInfer({})", vid.index)
             }
 
             ty::ReInfer(ReSkolemized(id, ref bound_region)) => {
@@ -878,13 +888,6 @@ impl Repr for typeck::MethodObject {
     }
 }
 
-
-impl Repr for ty::RegionVid {
-    fn repr(&self, _tcx: &ctxt) -> String {
-        format!("{:?}", *self)
-    }
-}
-
 impl Repr for ty::TraitStore {
     fn repr(&self, tcx: &ctxt) -> String {
         trait_store_to_str(tcx, *self)
@@ -998,3 +1001,83 @@ impl Repr for ty::UpvarBorrow {
                 self.region.repr(tcx))
     }
 }
+
+impl Repr for ty::IntVid {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{}", self)
+    }
+}
+
+impl Repr for ty::FloatVid {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{}", self)
+    }
+}
+
+impl Repr for ty::RegionVid {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{}", self)
+    }
+}
+
+impl Repr for ty::TyVid {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{}", self)
+    }
+}
+
+impl Repr for ty::IntVarValue {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{:?}", *self)
+    }
+}
+
+impl Repr for ast::IntTy {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{:?}", *self)
+    }
+}
+
+impl Repr for ast::UintTy {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{:?}", *self)
+    }
+}
+
+impl Repr for ast::FloatTy {
+    fn repr(&self, _tcx: &ctxt) -> String {
+        format!("{:?}", *self)
+    }
+}
+
+impl<T:Repr> Repr for infer::Bounds<T> {
+    fn repr(&self, tcx: &ctxt) -> String {
+        format!("({} <= {})",
+                self.lb.repr(tcx),
+                self.ub.repr(tcx))
+    }
+}
+
+impl<K:Repr,V:Repr> Repr for VV<K,V> {
+    fn repr(&self, tcx: &ctxt) -> String {
+        match *self {
+            unify::Redirect(ref k) =>
+                format!("Redirect({})", k.repr(tcx)),
+            unify::Root(ref v, r) =>
+                format!("Root({}, {})", v.repr(tcx), r)
+        }
+    }
+}
+
+impl Repr for region_inference::VarValue {
+    fn repr(&self, tcx: &ctxt) -> String {
+        match *self {
+            infer::region_inference::NoValue =>
+                format!("NoValue"),
+            infer::region_inference::Value(r) =>
+                format!("Value({})", r.repr(tcx)),
+            infer::region_inference::ErrorValue =>
+                format!("ErrorValue"),
+        }
+    }
+}