diff --git a/src/librustc/middle/typeck/infer/combine.rs b/src/librustc/middle/typeck/infer/combine.rs
index c6506b145214f..0c6143ea73376 100644
--- a/src/librustc/middle/typeck/infer/combine.rs
+++ b/src/librustc/middle/typeck/infer/combine.rs
@@ -8,43 +8,29 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-// ______________________________________________________________________
-// Type combining
+///////////////////////////////////////////////////////////////////////////
+// # Type combining
 //
-// There are three type combiners: sub, lub, and glb.  Each implements
-// the trait `Combine` and contains methods for combining two
-// instances of various things and yielding a new instance.  These
-// combiner methods always yield a `result<T>`---failure is propagated
-// upward using `and_then()` methods.  There is a lot of common code for
-// these operations, implemented as default methods on the `Combine`
-// trait.
+// There are four type combiners: equate, sub, lub, and glb.  Each
+// implements the trait `Combine` and contains methods for combining
+// two instances of various things and yielding a new instance.  These
+// combiner methods always yield a `Result<T>`.  There is a lot of
+// common code for these operations, implemented as default methods on
+// the `Combine` trait.
 //
-// In reality, the sub operation is rather different from lub/glb, but
-// they are combined into one trait to avoid duplication (they used to
-// be separate but there were many bugs because there were two copies
-// of most routines).
+// Each operation may have side-effects on the inference context,
+// though these can be unrolled using snapshots. On success, the
+// LUB/GLB operations return the appropriate bound. The Eq and Sub
+// operations generally return the first operand.
 //
-// The differences are:
-//
-// - when making two things have a sub relationship, the order of the
-//   arguments is significant (a <: b) and the return value of the
-//   combine functions is largely irrelevant.  The important thing is
-//   whether the action succeeds or fails.  If it succeeds, then side
-//   effects have been committed into the type variables.
-//
-// - for GLB/LUB, the order of arguments is not significant (GLB(a,b) ==
-//   GLB(b,a)) and the return value is important (it is the GLB).  Of
-//   course GLB/LUB may also have side effects.
-//
-// Contravariance
+// ## Contravariance
 //
 // When you are relating two things which have a contravariant
 // relationship, you should use `contratys()` or `contraregions()`,
 // rather than inversing the order of arguments!  This is necessary
 // because the order of arguments is not relevant for LUB and GLB.  It
 // is also useful to track which value is the "expected" value in
-// terms of error reporting, although we do not do that properly right
-// now.
+// terms of error reporting.
 
 
 use middle::subst;
@@ -53,14 +39,16 @@ use middle::ty::{FloatVar, FnSig, IntVar, TyVar};
 use middle::ty::{IntType, UintType};
 use middle::ty::{BuiltinBounds};
 use middle::ty;
-use middle::typeck::infer::{ToUres};
+use middle::typeck::infer::equate::Equate;
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lub::Lub;
 use middle::typeck::infer::sub::Sub;
 use middle::typeck::infer::unify::InferCtxtMethodsForSimplyUnifiableTypes;
-use middle::typeck::infer::{InferCtxt, cres, ures};
-use middle::typeck::infer::{TypeTrace};
-use util::common::indent;
+use middle::typeck::infer::{InferCtxt, cres};
+use middle::typeck::infer::{MiscVariable, TypeTrace};
+use middle::typeck::infer::type_variable::{RelationDir, EqTo,
+                                           SubtypeOf, SupertypeOf};
+use middle::ty_fold::{RegionFolder, TypeFoldable};
 use util::ppaux::Repr;
 
 use std::result;
@@ -75,6 +63,7 @@ pub trait Combine {
     fn a_is_expected(&self) -> bool;
     fn trace(&self) -> TypeTrace;
 
+    fn equate<'a>(&'a self) -> Equate<'a>;
     fn sub<'a>(&'a self) -> Sub<'a>;
     fn lub<'a>(&'a self) -> Lub<'a>;
     fn glb<'a>(&'a self) -> Glb<'a>;
@@ -101,7 +90,7 @@ pub trait Combine {
         try!(result::fold_(as_
                           .iter()
                           .zip(bs.iter())
-                          .map(|(a, b)| eq_tys(self, *a, *b))));
+                          .map(|(a, b)| self.equate().tys(*a, *b))));
         Ok(Vec::from_slice(as_))
     }
 
@@ -177,10 +166,7 @@ pub trait Combine {
                 let b_r = b_rs[i];
                 let variance = variances[i];
                 let r = match variance {
-                    ty::Invariant => {
-                        eq_regions(this, a_r, b_r)
-                            .and_then(|()| Ok(a_r))
-                    }
+                    ty::Invariant => this.equate().regions(a_r, b_r),
                     ty::Covariant => this.regions(a_r, b_r),
                     ty::Contravariant => this.contraregions(a_r, b_r),
                     ty::Bivariant => Ok(a_r),
@@ -334,34 +320,6 @@ pub fn expected_found<C:Combine,T>(
     }
 }
 
-pub fn eq_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> ures {
-    let suber = this.sub();
-    this.infcx().try(|| {
-        suber.tys(a, b).and_then(|_ok| suber.contratys(a, b)).to_ures()
-    })
-}
-
-pub fn eq_regions<C:Combine>(this: &C, a: ty::Region, b: ty::Region)
-                          -> ures {
-    debug!("eq_regions({}, {})",
-            a.repr(this.infcx().tcx),
-            b.repr(this.infcx().tcx));
-    let sub = this.sub();
-    indent(|| {
-        this.infcx().try(|| {
-            sub.regions(a, b).and_then(|_r| sub.contraregions(a, b))
-        }).or_else(|e| {
-            // substitute a better error, but use the regions
-            // found in the original error
-            match e {
-              ty::terr_regions_does_not_outlive(a1, b1) =>
-                Err(ty::terr_regions_not_same(a1, b1)),
-              _ => Err(e)
-            }
-        }).to_ures()
-    })
-}
-
 pub fn super_fn_sigs<C:Combine>(this: &C, a: &ty::FnSig, b: &ty::FnSig) -> cres<ty::FnSig> {
 
     fn argvecs<C:Combine>(this: &C, a_args: &[ty::t], b_args: &[ty::t]) -> cres<Vec<ty::t> > {
@@ -453,8 +411,7 @@ pub fn super_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> cres<ty::t> {
 
         // Relate floating-point variables to other types
         (&ty::ty_infer(FloatVar(a_id)), &ty::ty_infer(FloatVar(b_id))) => {
-            try!(this.infcx().simple_vars(this.a_is_expected(),
-                                            a_id, b_id));
+            try!(this.infcx().simple_vars(this.a_is_expected(), a_id, b_id));
             Ok(a)
         }
         (&ty::ty_infer(FloatVar(v_id)), &ty::ty_float(v)) => {
@@ -469,7 +426,8 @@ pub fn super_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> cres<ty::t> {
       (&ty::ty_bool, _) |
       (&ty::ty_int(_), _) |
       (&ty::ty_uint(_), _) |
-      (&ty::ty_float(_), _) => {
+      (&ty::ty_float(_), _) |
+      (&ty::ty_err, _) => {
         if ty::get(a).sty == ty::get(b).sty {
             Ok(a)
         } else {
@@ -512,7 +470,10 @@ pub fn super_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> cres<ty::t> {
       (&ty::ty_unboxed_closure(a_id, a_region),
        &ty::ty_unboxed_closure(b_id, b_region))
       if a_id == b_id => {
-          let region = if_ok!(this.regions(a_region, b_region));
+          // All ty_unboxed_closure types with the same id represent
+          // the (anonymous) type of the same closure expression. So
+          // all of their regions should be equated.
+          let region = try!(this.equate().regions(a_region, b_region));
           Ok(ty::mk_unboxed_closure(tcx, a_id, region))
       }
 
@@ -609,3 +570,118 @@ pub fn super_tys<C:Combine>(this: &C, a: ty::t, b: ty::t) -> cres<ty::t> {
         Ok(ty::mk_mach_float(val))
     }
 }
+
+impl<'f> CombineFields<'f> {
+    pub fn switch_expected(&self) -> CombineFields<'f> {
+        CombineFields {
+            a_is_expected: !self.a_is_expected,
+            ..(*self).clone()
+        }
+    }
+
+    fn equate(&self) -> Equate<'f> {
+        Equate((*self).clone())
+    }
+
+    fn sub(&self) -> Sub<'f> {
+        Sub((*self).clone())
+    }
+
+    pub fn instantiate(&self,
+                       a_ty: ty::t,
+                       dir: RelationDir,
+                       b_vid: ty::TyVid)
+                       -> cres<()>
+    {
+        let tcx = self.infcx.tcx;
+        let mut stack = Vec::new();
+        stack.push((a_ty, dir, b_vid));
+        loop {
+            // For each turn of the loop, we extract a tuple
+            //
+            //     (a_ty, dir, b_vid)
+            //
+            // to relate. Here dir is either SubtypeOf or
+            // SupertypeOf. The idea is that we should ensure that
+            // the type `a_ty` is a subtype or supertype (respectively) of the
+            // type to which `b_vid` is bound.
+            //
+            // If `b_vid` has not yet been instantiated with a type
+            // (which is always true on the first iteration, but not
+            // necessarily true on later iterations), we will first
+            // instantiate `b_vid` with a *generalized* version of
+            // `a_ty`. Generalization introduces other inference
+            // variables wherever subtyping could occur (at time of
+            // this writing, this means replacing free regions with
+            // region variables).
+            let (a_ty, dir, b_vid) = match stack.pop() {
+                None => break,
+                Some(e) => e,
+            };
+
+            debug!("instantiate(a_ty={} dir={} b_vid={})",
+                   a_ty.repr(tcx),
+                   dir,
+                   b_vid.repr(tcx));
+
+            // Check whether `vid` has been instantiated yet.  If not,
+            // make a generalized form of `ty` and instantiate with
+            // that.
+            let b_ty = self.infcx.type_variables.borrow().probe(b_vid);
+            let b_ty = match b_ty {
+                Some(t) => t, // ...already instantiated.
+                None => {     // ...not yet instantiated:
+                    // Generalize type if necessary.
+                    let generalized_ty = match dir {
+                        EqTo => a_ty,
+                        SupertypeOf | SubtypeOf => self.generalize(a_ty)
+                    };
+                    debug!("instantiate(a_ty={}, dir={}, \
+                                        b_vid={}, generalized_ty={})",
+                           a_ty.repr(tcx), dir, b_vid.repr(tcx),
+                           generalized_ty.repr(tcx));
+                    self.infcx.type_variables
+                        .borrow_mut()
+                        .instantiate_and_push(
+                            b_vid, generalized_ty, &mut stack);
+                    generalized_ty
+                }
+            };
+
+            // The original triple was `(a_ty, dir, b_vid)` -- now we have
+            // resolved `b_vid` to `b_ty`, so apply `(a_ty, dir, b_ty)`:
+            //
+            // FIXME: This code is non-ideal because all these subtype
+            // relations wind up attributed to the same spans. We need
+            // to associate causes/spans with each of the relations in
+            // the stack to get this right.
+            match dir {
+                EqTo => {
+                    try!(self.equate().tys(a_ty, b_ty));
+                }
+
+                SubtypeOf => {
+                    try!(self.sub().tys(a_ty, b_ty));
+                }
+
+                SupertypeOf => {
+                    try!(self.sub().contratys(a_ty, b_ty));
+                }
+            }
+        }
+
+        Ok(())
+    }
+
+    fn generalize(&self, t: ty::t) -> ty::t {
+        // FIXME: This is non-ideal because we don't give a very descriptive
+        // origin for this region variable.
+
+        let infcx = self.infcx;
+        let span = self.trace.origin.span();
+        t.fold_with(
+            &mut RegionFolder::regions(
+                self.infcx.tcx,
+                |_| infcx.next_region_var(MiscVariable(span))))
+    }
+}
diff --git a/src/librustc/middle/typeck/infer/equate.rs b/src/librustc/middle/typeck/infer/equate.rs
new file mode 100644
index 0000000000000..391027f9c4bf9
--- /dev/null
+++ b/src/librustc/middle/typeck/infer/equate.rs
@@ -0,0 +1,149 @@
+// Copyright 2014 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::{BuiltinBounds};
+use middle::ty;
+use middle::ty::TyVar;
+use middle::typeck::infer::combine::*;
+use middle::typeck::infer::{cres};
+use middle::typeck::infer::glb::Glb;
+use middle::typeck::infer::InferCtxt;
+use middle::typeck::infer::lub::Lub;
+use middle::typeck::infer::sub::Sub;
+use middle::typeck::infer::{TypeTrace, Subtype};
+use middle::typeck::infer::type_variable::{EqTo};
+use util::ppaux::{Repr};
+
+use syntax::ast::{Onceness, FnStyle};
+
+pub struct Equate<'f> {
+    fields: CombineFields<'f>
+}
+
+#[allow(non_snake_case_functions)]
+pub fn Equate<'f>(cf: CombineFields<'f>) -> Equate<'f> {
+    Equate { fields: cf }
+}
+
+impl<'f> Combine for Equate<'f> {
+    fn infcx<'a>(&'a self) -> &'a InferCtxt<'a> { self.fields.infcx }
+    fn tag(&self) -> String { "eq".to_string() }
+    fn a_is_expected(&self) -> bool { self.fields.a_is_expected }
+    fn trace(&self) -> TypeTrace { self.fields.trace.clone() }
+
+    fn equate<'a>(&'a self) -> Equate<'a> { Equate(self.fields.clone()) }
+    fn sub<'a>(&'a self) -> Sub<'a> { Sub(self.fields.clone()) }
+    fn lub<'a>(&'a self) -> Lub<'a> { Lub(self.fields.clone()) }
+    fn glb<'a>(&'a self) -> Glb<'a> { Glb(self.fields.clone()) }
+
+    fn contratys(&self, a: ty::t, b: ty::t) -> cres<ty::t> {
+        self.tys(a, b)
+    }
+
+    fn contraregions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
+        self.regions(a, b)
+    }
+
+    fn regions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
+        debug!("{}.regions({}, {})",
+               self.tag(),
+               a.repr(self.fields.infcx.tcx),
+               b.repr(self.fields.infcx.tcx));
+        self.infcx().region_vars.make_eqregion(Subtype(self.trace()), a, b);
+        Ok(a)
+    }
+
+    fn mts(&self, a: &ty::mt, b: &ty::mt) -> cres<ty::mt> {
+        debug!("mts({} <: {})",
+               a.repr(self.fields.infcx.tcx),
+               b.repr(self.fields.infcx.tcx));
+
+        if a.mutbl != b.mutbl { return Err(ty::terr_mutability); }
+        let t = try!(self.tys(a.ty, b.ty));
+        Ok(ty::mt { mutbl: a.mutbl, ty: t })
+    }
+
+    fn fn_styles(&self, a: FnStyle, b: FnStyle) -> cres<FnStyle> {
+        if a != b {
+            Err(ty::terr_fn_style_mismatch(expected_found(self, a, b)))
+        } else {
+            Ok(a)
+        }
+    }
+
+    fn oncenesses(&self, a: Onceness, b: Onceness) -> cres<Onceness> {
+        if a != b {
+            Err(ty::terr_onceness_mismatch(expected_found(self, a, b)))
+        } else {
+            Ok(a)
+        }
+    }
+
+    fn builtin_bounds(&self,
+                      a: BuiltinBounds,
+                      b: BuiltinBounds)
+                      -> cres<BuiltinBounds>
+    {
+        // More bounds is a subtype of fewer bounds.
+        //
+        // e.g., fn:Copy() <: fn(), because the former is a function
+        // that only closes over copyable things, but the latter is
+        // any function at all.
+        if a != b {
+            Err(ty::terr_builtin_bounds(expected_found(self, a, b)))
+        } else {
+            Ok(a)
+        }
+    }
+
+    fn tys(&self, a: ty::t, b: ty::t) -> cres<ty::t> {
+        debug!("{}.tys({}, {})", self.tag(),
+               a.repr(self.fields.infcx.tcx), b.repr(self.fields.infcx.tcx));
+        if a == b { return Ok(a); }
+
+        let infcx = self.fields.infcx;
+        let a = infcx.type_variables.borrow().replace_if_possible(a);
+        let b = infcx.type_variables.borrow().replace_if_possible(b);
+        match (&ty::get(a).sty, &ty::get(b).sty) {
+            (&ty::ty_bot, &ty::ty_bot) => {
+                Ok(a)
+            }
+
+            (&ty::ty_bot, _) |
+            (_, &ty::ty_bot) => {
+                Err(ty::terr_sorts(expected_found(self, a, b)))
+            }
+
+            (&ty::ty_infer(TyVar(a_id)), &ty::ty_infer(TyVar(b_id))) => {
+                infcx.type_variables.borrow_mut().relate_vars(a_id, EqTo, b_id);
+                Ok(a)
+            }
+
+            (&ty::ty_infer(TyVar(a_id)), _) => {
+                try!(self.fields.instantiate(b, EqTo, a_id));
+                Ok(a)
+            }
+
+            (_, &ty::ty_infer(TyVar(b_id))) => {
+                try!(self.fields.instantiate(a, EqTo, b_id));
+                Ok(a)
+            }
+
+            _ => {
+                super_tys(self, a, b)
+            }
+        }
+    }
+
+    fn fn_sigs(&self, a: &ty::FnSig, b: &ty::FnSig) -> cres<ty::FnSig> {
+        try!(self.sub().fn_sigs(a, b));
+        self.sub().fn_sigs(b, a)
+    }
+}
diff --git a/src/librustc/middle/typeck/infer/glb.rs b/src/librustc/middle/typeck/infer/glb.rs
index 0b89e7274e727..68b8031a04b68 100644
--- a/src/librustc/middle/typeck/infer/glb.rs
+++ b/src/librustc/middle/typeck/infer/glb.rs
@@ -12,9 +12,9 @@
 use middle::ty::{BuiltinBounds};
 use middle::ty::RegionVid;
 use middle::ty;
-use middle::typeck::infer::then;
 use middle::typeck::infer::combine::*;
 use middle::typeck::infer::lattice::*;
+use middle::typeck::infer::equate::Equate;
 use middle::typeck::infer::lub::Lub;
 use middle::typeck::infer::sub::Sub;
 use middle::typeck::infer::{cres, InferCtxt};
@@ -31,7 +31,7 @@ use util::ppaux::Repr;
 
 /// "Greatest lower bound" (common subtype)
 pub struct Glb<'f> {
-    pub fields: CombineFields<'f>
+    fields: CombineFields<'f>
 }
 
 #[allow(non_snake_case_functions)]
@@ -45,6 +45,7 @@ impl<'f> Combine for Glb<'f> {
     fn a_is_expected(&self) -> bool { self.fields.a_is_expected }
     fn trace(&self) -> TypeTrace { self.fields.trace.clone() }
 
+    fn equate<'a>(&'a self) -> Equate<'a> { Equate(self.fields.clone()) }
     fn sub<'a>(&'a self) -> Sub<'a> { Sub(self.fields.clone()) }
     fn lub<'a>(&'a self) -> Lub<'a> { Lub(self.fields.clone()) }
     fn glb<'a>(&'a self) -> Glb<'a> { Glb(self.fields.clone()) }
@@ -58,27 +59,25 @@ impl<'f> Combine for Glb<'f> {
                mt_to_string(tcx, b));
 
         match (a.mutbl, b.mutbl) {
-          // If one side or both is mut, then the GLB must use
-          // the precise type from the mut side.
-          (MutMutable, MutMutable) => {
-            eq_tys(self, a.ty, b.ty).then(|| {
-                Ok(ty::mt {ty: a.ty, mutbl: MutMutable})
-            })
-          }
-
-          // If one side or both is immutable, we can use the GLB of
-          // both sides but mutbl must be `MutImmutable`.
-          (MutImmutable, MutImmutable) => {
-            self.tys(a.ty, b.ty).and_then(|t| {
+            // If one side or both is mut, then the GLB must use
+            // the precise type from the mut side.
+            (MutMutable, MutMutable) => {
+                let t = try!(self.equate().tys(a.ty, b.ty));
+                Ok(ty::mt {ty: t, mutbl: MutMutable})
+            }
+
+            // If one side or both is immutable, we can use the GLB of
+            // both sides but mutbl must be `MutImmutable`.
+            (MutImmutable, MutImmutable) => {
+                let t = try!(self.tys(a.ty, b.ty));
                 Ok(ty::mt {ty: t, mutbl: MutImmutable})
-            })
-          }
-
-          // There is no mutual subtype of these combinations.
-          (MutMutable, MutImmutable) |
-          (MutImmutable, MutMutable) => {
-              Err(ty::terr_mutability)
-          }
+            }
+
+            // There is no mutual subtype of these combinations.
+            (MutMutable, MutImmutable) |
+            (MutImmutable, MutMutable) => {
+                Err(ty::terr_mutability)
+            }
         }
     }
 
diff --git a/src/librustc/middle/typeck/infer/lattice.rs b/src/librustc/middle/typeck/infer/lattice.rs
index 8a40021ea9676..f09773d30b514 100644
--- a/src/librustc/middle/typeck/infer/lattice.rs
+++ b/src/librustc/middle/typeck/infer/lattice.rs
@@ -33,346 +33,55 @@
 
 use middle::ty::{RegionVid, TyVar};
 use middle::ty;
-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::sub::Sub;
 use util::ppaux::Repr;
 
 use std::collections::HashMap;
 
-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>;
-}
-
-pub type LatticeOp<'a, T> =
-    |cf: CombineFields, a: &T, b: &T|: 'a -> cres<T>;
-
-impl LatticeValue for ty::t {
-    fn sub(cf: CombineFields, a: &ty::t, b: &ty::t) -> ures {
-        Sub(cf).tys(*a, *b).to_ures()
-    }
-
-    fn lub(cf: CombineFields, a: &ty::t, b: &ty::t) -> cres<ty::t> {
-        Lub(cf).tys(*a, *b)
-    }
-
-    fn glb(cf: CombineFields, a: &ty::t, b: &ty::t) -> cres<ty::t> {
-        Glb(cf).tys(*a, *b)
-    }
-}
-
-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(&self,
-                 a_id: K,
-                 b: T)
-                 -> ures;
-
-    /// make T a subtype of variable
-    fn t_sub_var(&self,
-                 a: T,
-                 b_id: K)
-                 -> ures;
-
-    fn set_var_to_merged_bounds(&self,
-                                v_id: K,
-                                a: &Bounds<T>,
-                                b: &Bounds<T>,
-                                rank: uint)
-                                -> 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.
-         */
-
-        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 = 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, a_bounds.repr(tcx),
-               b_id, b_bounds.repr(tcx));
-
-        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.
-        match (&a_bounds.ub, &b_bounds.lb) {
-            (&Some(ref a_ub), &Some(ref b_lb)) => {
-                let r = self.infcx.try(
-                    || LatticeValue::sub(self.clone(), a_ub, b_lb));
-                match r {
-                    Ok(()) => {
-                        return Ok(());
-                    }
-                    Err(_) => { /*fallthrough */ }
-                }
-            }
-            _ => { /*fallthrough*/ }
-        }
-
-        // Otherwise, we need to merge A and B so as to guarantee that
-        // 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) =
-            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(&self,
-                 a_id: K,
-                 b: T)
-                 -> ures
-    {
-        /*!
-         * Make a variable (`a_id`) a subtype of the concrete type `b`.
-         */
-
-        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,
-               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(&self,
-                 a: T,
-                 b_id: K)
-                 -> ures
-    {
-        /*!
-         * 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 = 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.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 set_var_to_merged_bounds(&self,
-                                v_id: K,
-                                a: &Bounds<T>,
-                                b: &Bounds<T>,
-                                rank: uint)
-                                -> 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:
-         *    c.ub <: a.ub
-         *    c.ub <: b.ub
-         *    a.lb <: c.lb
-         *    b.lb <: c.lb
-         * 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
-        // can swap A/B in these pictures):
-        //
-        //       A         A
-        //      / \       / \
-        //     / B \     / B \
-        //    / / \ \   / / \ \
-        //   * *   * * * /   * *
-        //    \ \ / /   \   / /
-        //     \ B /   / \ / /
-        //      \ /   *   \ /
-        //       A     \ / A
-        //              B
-
-        let tcx = self.infcx.tcx;
-        let table = UnifyKey::unification_table(self.infcx);
-
-        debug!("merge({},{},{})",
-               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
-        // to be able to merge A and B at all, and relating
-        // them explicitly gives the type inferencer more
-        // information and helps to produce tighter bounds
-        // when necessary.
-        let () = if_ok!(self.bnds(&a.lb, &b.ub));
-        let () = if_ok!(self.bnds(&b.lb, &a.ub));
-        let ub = if_ok!(self.merge_bnd(&a.ub, &b.ub, LatticeValue::glb));
-        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,
-               bounds.repr(self.infcx.tcx));
-
-        // the new bounds must themselves
-        // be relatable:
-        let () = if_ok!(self.bnds(&bounds.lb, &bounds.ub));
-        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(&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(_)) => {
-                Ok(())
-            }
-            (&Some(ref t_a), &Some(ref t_b)) => {
-                LatticeValue::sub(self.clone(), t_a, t_b)
-            }
-        }
-    }
-}
-
-// ______________________________________________________________________
-// Lattice operations on variables
-//
-// This is common code used by both LUB and GLB to compute the LUB/GLB
-// for pairs of variables or for variables and values.
-
 pub trait LatticeDir {
-    fn combine_fields<'a>(&'a self) -> CombineFields<'a>;
-    fn bnd<T:Clone>(&self, b: &Bounds<T>) -> Option<T>;
-    fn with_bnd<T:Clone>(&self, b: &Bounds<T>, t: T) -> Bounds<T>;
-}
-
-pub trait TyLatticeDir {
+    // Relates the bottom type to `t` and returns LUB(t, _|_) or
+    // GLB(t, _|_) as appropriate.
     fn ty_bot(&self, t: ty::t) -> cres<ty::t>;
-}
 
-impl<'f> LatticeDir for Lub<'f> {
-    fn combine_fields<'a>(&'a self) -> CombineFields<'a> { self.fields.clone() }
-    fn bnd<T:Clone>(&self, b: &Bounds<T>) -> Option<T> { b.ub.clone() }
-    fn with_bnd<T:Clone>(&self, b: &Bounds<T>, t: T) -> Bounds<T> {
-        Bounds { ub: Some(t), ..(*b).clone() }
-    }
+    // Relates the type `v` to `a` and `b` such that `v` represents
+    // the LUB/GLB of `a` and `b` as appropriate.
+    fn relate_bound<'a>(&'a self, v: ty::t, a: ty::t, b: ty::t) -> cres<()>;
 }
 
-impl<'f> TyLatticeDir for Lub<'f> {
+impl<'a> LatticeDir for Lub<'a> {
     fn ty_bot(&self, t: ty::t) -> cres<ty::t> {
         Ok(t)
     }
-}
 
-impl<'f> LatticeDir for Glb<'f> {
-    fn combine_fields<'a>(&'a self) -> CombineFields<'a> { self.fields.clone() }
-    fn bnd<T:Clone>(&self, b: &Bounds<T>) -> Option<T> { b.lb.clone() }
-    fn with_bnd<T:Clone>(&self, b: &Bounds<T>, t: T) -> Bounds<T> {
-        Bounds { lb: Some(t), ..(*b).clone() }
+    fn relate_bound<'a>(&'a self, v: ty::t, a: ty::t, b: ty::t) -> cres<()> {
+        let sub = self.sub();
+        try!(sub.tys(a, v));
+        try!(sub.tys(b, v));
+        Ok(())
     }
 }
 
-impl<'f> TyLatticeDir for Glb<'f> {
-    fn ty_bot(&self, _t: ty::t) -> cres<ty::t> {
+impl<'a> LatticeDir for Glb<'a> {
+    fn ty_bot(&self, _: ty::t) -> cres<ty::t> {
         Ok(ty::mk_bot())
     }
+
+    fn relate_bound<'a>(&'a self, v: ty::t, a: ty::t, b: ty::t) -> cres<()> {
+        let sub = self.sub();
+        try!(sub.tys(v, a));
+        try!(sub.tys(v, b));
+        Ok(())
+    }
 }
 
-pub fn super_lattice_tys<L:LatticeDir+TyLatticeDir+Combine>(this: &L,
-                                                            a: ty::t,
-                                                            b: ty::t)
-                                                            -> cres<ty::t> {
+pub fn super_lattice_tys<L:LatticeDir+Combine>(this: &L,
+                                               a: ty::t,
+                                               b: ty::t)
+                                               -> cres<ty::t>
+{
     debug!("{}.lattice_tys({}, {})",
            this.tag(),
            a.repr(this.infcx().tcx),
@@ -382,156 +91,27 @@ pub fn super_lattice_tys<L:LatticeDir+TyLatticeDir+Combine>(this: &L,
         return Ok(a);
     }
 
-    let tcx = this.infcx().tcx;
-
+    let infcx = this.infcx();
+    let a = infcx.type_variables.borrow().replace_if_possible(a);
+    let b = infcx.type_variables.borrow().replace_if_possible(b);
     match (&ty::get(a).sty, &ty::get(b).sty) {
-        (&ty::ty_bot, _) => { return this.ty_bot(b); }
-        (_, &ty::ty_bot) => { return this.ty_bot(a); }
-
-        (&ty::ty_infer(TyVar(a_id)), &ty::ty_infer(TyVar(b_id))) => {
-            let r = if_ok!(lattice_vars(this, a_id, b_id,
-                                        |x, y| this.tys(*x, *y)));
-            return match r {
-                VarResult(v) => Ok(ty::mk_var(tcx, v)),
-                ValueResult(t) => Ok(t)
-            };
-        }
-
-        (&ty::ty_infer(TyVar(a_id)), _) => {
-            return lattice_var_and_t(this, a_id, &b,
-                                     |x, y| this.tys(*x, *y));
-        }
-
-        (_, &ty::ty_infer(TyVar(b_id))) => {
-            return lattice_var_and_t(this, b_id, &a,
-                                     |x, y| this.tys(*x, *y));
+        (&ty::ty_bot, _) => { this.ty_bot(b) }
+        (_, &ty::ty_bot) => { this.ty_bot(a) }
+
+        (&ty::ty_infer(TyVar(..)), _) |
+        (_, &ty::ty_infer(TyVar(..))) => {
+            let v = infcx.next_ty_var();
+            try!(this.relate_bound(v, a, b));
+            Ok(v)
         }
 
         _ => {
-            return super_tys(this, a, b);
-        }
-    }
-}
-
-pub type LatticeDirOp<'a, T> = |a: &T, b: &T|: 'a -> cres<T>;
-
-#[deriving(Clone)]
-pub enum LatticeVarResult<K,T> {
-    VarResult(K),
-    ValueResult(T)
-}
-
-/**
- * Computes the LUB or GLB of two bounded variables.  These could be any
- * sort of variables, but in the comments on this function I'll assume
- * we are doing an LUB on two type variables.
- *
- * This computation can be done in one of two ways:
- *
- * - If both variables have an upper bound, we may just compute the
- *   LUB of those bounds and return that, in which case we are
- *   returning a type.  This is indicated with a `ValueResult` return.
- *
- * - 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:LatticeValue,
-                    K:UnifyKey<Bounds<T>>>(
-    this: &L,                           // defines whether we want LUB or GLB
-    a_vid: K,                           // first variable
-    b_vid: K,                           // second variable
-    lattice_dir_op: LatticeDirOp<T>)    // LUB or GLB operation on 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, a_bounds.repr(tcx),
-           b_vid, b_bounds.repr(tcx));
-
-    // Same variable: the easy case.
-    if a_vid == b_vid {
-        return Ok(VarResult(a_vid));
-    }
-
-    // If both A and B have an UB type, then we can just compute the
-    // LUB of those types:
-    let (a_bnd, b_bnd) = (this.bnd(a_bounds), this.bnd(b_bounds));
-    match (a_bnd, b_bnd) {
-        (Some(ref a_ty), Some(ref b_ty)) => {
-            match this.infcx().try(|| lattice_dir_op(a_ty, b_ty) ) {
-                Ok(t) => return Ok(ValueResult(t)),
-                Err(_) => { /*fallthrough */ }
-            }
-        }
-        _ => {/*fallthrough*/}
-    }
-
-    // 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();
-    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:LatticeValue,
-                         K:UnifyKey<Bounds<T>>>(
-    this: &L,
-    a_id: K,
-    b: &T,
-    lattice_dir_op: LatticeDirOp<T>)
-    -> 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,
-           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.repr(this.infcx().tcx));
-            lattice_dir_op(a_bnd, b)
-        }
-        None => {
-            // If a does not have an upper bound, make b the upper bound of a
-            // and then return b.
-            debug!("bnd=None");
-            let a_bounds = this.with_bnd(a_bounds, (*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())
+            super_tys(this, a, b)
         }
     }
 }
 
-// ___________________________________________________________________________
+///////////////////////////////////////////////////////////////////////////
 // Random utility functions used by LUB/GLB when computing LUB/GLB of
 // fn types
 
diff --git a/src/librustc/middle/typeck/infer/lub.rs b/src/librustc/middle/typeck/infer/lub.rs
index 650987612accf..9c6c0763ad45e 100644
--- a/src/librustc/middle/typeck/infer/lub.rs
+++ b/src/librustc/middle/typeck/infer/lub.rs
@@ -11,8 +11,8 @@
 use middle::ty::{BuiltinBounds};
 use middle::ty::RegionVid;
 use middle::ty;
-use middle::typeck::infer::then;
 use middle::typeck::infer::combine::*;
+use middle::typeck::infer::equate::Equate;
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lattice::*;
 use middle::typeck::infer::sub::Sub;
@@ -30,7 +30,7 @@ use util::ppaux::Repr;
 
 /// "Least upper bound" (common supertype)
 pub struct Lub<'f> {
-    pub fields: CombineFields<'f>
+    fields: CombineFields<'f>
 }
 
 #[allow(non_snake_case_functions)]
@@ -44,6 +44,7 @@ impl<'f> Combine for Lub<'f> {
     fn a_is_expected(&self) -> bool { self.fields.a_is_expected }
     fn trace(&self) -> TypeTrace { self.fields.trace.clone() }
 
+    fn equate<'a>(&'a self) -> Equate<'a> { Equate(self.fields.clone()) }
     fn sub<'a>(&'a self) -> Sub<'a> { Sub(self.fields.clone()) }
     fn lub<'a>(&'a self) -> Lub<'a> { Lub(self.fields.clone()) }
     fn glb<'a>(&'a self) -> Glb<'a> { Glb(self.fields.clone()) }
@@ -62,17 +63,15 @@ impl<'f> Combine for Lub<'f> {
 
         let m = a.mutbl;
         match m {
-          MutImmutable => {
-            self.tys(a.ty, b.ty).and_then(|t| Ok(ty::mt {ty: t, mutbl: m}) )
-          }
-
-          MutMutable => {
-            self.fields.infcx.try(|| {
-                eq_tys(self, a.ty, b.ty).then(|| {
-                    Ok(ty::mt {ty: a.ty, mutbl: m})
-                })
-            }).or_else(|e| Err(e))
-          }
+            MutImmutable => {
+                let t = try!(self.tys(a.ty, b.ty));
+                Ok(ty::mt {ty: t, mutbl: m})
+            }
+
+            MutMutable => {
+                let t = try!(self.equate().tys(a.ty, b.ty));
+                Ok(ty::mt {ty: t, mutbl: m})
+            }
         }
     }
 
diff --git a/src/librustc/middle/typeck/infer/mod.rs b/src/librustc/middle/typeck/infer/mod.rs
index e672b8b310f5d..f86857f97f654 100644
--- a/src/librustc/middle/typeck/infer/mod.rs
+++ b/src/librustc/middle/typeck/infer/mod.rs
@@ -29,13 +29,14 @@ 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::{RegionSnapshot};
-use middle::typeck::infer::region_inference::{RegionVarBindings};
+use middle::typeck::infer::combine::{Combine, CombineFields};
+use middle::typeck::infer::region_inference::{RegionVarBindings,
+                                              RegionSnapshot};
 use middle::typeck::infer::resolve::{resolver};
+use middle::typeck::infer::equate::Equate;
 use middle::typeck::infer::sub::Sub;
 use middle::typeck::infer::lub::Lub;
-use middle::typeck::infer::unify::{UnificationTable, Snapshot};
+use middle::typeck::infer::unify::{UnificationTable};
 use middle::typeck::infer::error_reporting::ErrorReporting;
 use std::cell::{RefCell};
 use std::collections::HashMap;
@@ -46,19 +47,20 @@ use syntax::codemap::Span;
 use util::common::indent;
 use util::ppaux::{bound_region_to_string, ty_to_string, trait_ref_to_string, Repr};
 
-pub mod doc;
-pub mod macros;
+pub mod coercion;
 pub mod combine;
+pub mod doc;
+pub mod equate;
+pub mod error_reporting;
 pub mod glb;
 pub mod lattice;
 pub mod lub;
 pub mod region_inference;
 pub mod resolve;
 pub mod sub;
-pub mod unify;
-pub mod coercion;
-pub mod error_reporting;
 pub mod test;
+pub mod type_variable;
+pub mod unify;
 
 pub type Bound<T> = Option<T>;
 
@@ -79,8 +81,7 @@ pub struct InferCtxt<'a> {
     // 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.
-    type_unification_table:
-        RefCell<UnificationTable<ty::TyVid, Bounds<ty::t>>>,
+    type_variables: RefCell<type_variable::TypeVariableTable>,
 
     // Map from integral variable to the kind of integer it represents
     int_unification_table:
@@ -293,7 +294,7 @@ pub fn fixup_err_to_string(f: fixup_err) -> String {
 pub fn new_infer_ctxt<'a>(tcx: &'a ty::ctxt) -> InferCtxt<'a> {
     InferCtxt {
         tcx: tcx,
-        type_unification_table: RefCell::new(UnificationTable::new()),
+        type_variables: RefCell::new(type_variable::TypeVariableTable::new()),
         int_unification_table: RefCell::new(UnificationTable::new()),
         float_unification_table: RefCell::new(UnificationTable::new()),
         region_vars: RegionVarBindings::new(tcx),
@@ -395,8 +396,8 @@ pub fn mk_eqty(cx: &InferCtxt,
             origin: origin,
             values: Types(expected_found(a_is_expected, a, b))
         };
-        let suber = cx.sub(a_is_expected, trace);
-        eq_tys(&suber, a, b)
+        try!(cx.equate(a_is_expected, trace).tys(a, b));
+        Ok(())
     })
 }
 
@@ -511,9 +512,9 @@ pub fn uok() -> ures {
 }
 
 pub struct CombinedSnapshot {
-    type_snapshot: Snapshot<ty::TyVid>,
-    int_snapshot: Snapshot<ty::IntVid>,
-    float_snapshot: Snapshot<ty::FloatVid>,
+    type_snapshot: type_variable::Snapshot,
+    int_snapshot: unify::Snapshot<ty::IntVid>,
+    float_snapshot: unify::Snapshot<ty::FloatVid>,
     region_vars_snapshot: RegionSnapshot,
 }
 
@@ -525,6 +526,10 @@ impl<'a> InferCtxt<'a> {
                        trace: trace}
     }
 
+    pub fn equate<'a>(&'a self, a_is_expected: bool, trace: TypeTrace) -> Equate<'a> {
+        Equate(self.combine_fields(a_is_expected, trace))
+    }
+
     pub fn sub<'a>(&'a self, a_is_expected: bool, trace: TypeTrace) -> Sub<'a> {
         Sub(self.combine_fields(a_is_expected, trace))
     }
@@ -533,13 +538,9 @@ impl<'a> InferCtxt<'a> {
         Lub(self.combine_fields(a_is_expected, trace))
     }
 
-    pub fn in_snapshot(&self) -> bool {
-        self.region_vars.in_snapshot()
-    }
-
     fn start_snapshot(&self) -> CombinedSnapshot {
         CombinedSnapshot {
-            type_snapshot: self.type_unification_table.borrow_mut().snapshot(),
+            type_snapshot: self.type_variables.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(),
@@ -553,7 +554,7 @@ impl<'a> InferCtxt<'a> {
                                float_snapshot,
                                region_vars_snapshot } = snapshot;
 
-        self.type_unification_table
+        self.type_variables
             .borrow_mut()
             .rollback_to(type_snapshot);
         self.int_unification_table
@@ -573,7 +574,7 @@ impl<'a> InferCtxt<'a> {
                                float_snapshot,
                                region_vars_snapshot } = snapshot;
 
-        self.type_unification_table
+        self.type_variables
             .borrow_mut()
             .commit(type_snapshot);
         self.int_unification_table
@@ -636,9 +637,9 @@ impl<'a> InferCtxt<'a> {
 
 impl<'a> InferCtxt<'a> {
     pub fn next_ty_var_id(&self) -> TyVid {
-        self.type_unification_table
+        self.type_variables
             .borrow_mut()
-            .new_key(Bounds { lb: None, ub: None })
+            .new_var()
     }
 
     pub fn next_ty_var(&self) -> ty::t {
diff --git a/src/librustc/middle/typeck/infer/region_inference/mod.rs b/src/librustc/middle/typeck/infer/region_inference/mod.rs
index ff42dd817fb94..f34894346f64a 100644
--- a/src/librustc/middle/typeck/infer/region_inference/mod.rs
+++ b/src/librustc/middle/typeck/infer/region_inference/mod.rs
@@ -234,7 +234,7 @@ impl<'a> RegionVarBindings<'a> {
         }
     }
 
-    pub fn in_snapshot(&self) -> bool {
+    fn in_snapshot(&self) -> bool {
         self.undo_log.borrow().len() > 0
     }
 
@@ -406,6 +406,18 @@ impl<'a> RegionVarBindings<'a> {
         }
     }
 
+    pub fn make_eqregion(&self,
+                         origin: SubregionOrigin,
+                         sub: Region,
+                         sup: Region) {
+        if sub != sup {
+            // Eventually, it would be nice to add direct support for
+            // equating regions.
+            self.make_subregion(origin.clone(), sub, sup);
+            self.make_subregion(origin, sup, sub);
+        }
+    }
+
     pub fn make_subregion(&self,
                           origin: SubregionOrigin,
                           sub: Region,
diff --git a/src/librustc/middle/typeck/infer/resolve.rs b/src/librustc/middle/typeck/infer/resolve.rs
index 2ae95309d41d9..f9742c522dac4 100644
--- a/src/librustc/middle/typeck/infer/resolve.rs
+++ b/src/librustc/middle/typeck/infer/resolve.rs
@@ -48,12 +48,11 @@
 
 
 use middle::ty::{FloatVar, FloatVid, IntVar, IntVid, RegionVid, TyVar, TyVid};
-use middle::ty::{type_is_bot, IntType, UintType};
+use middle::ty::{IntType, UintType};
 use middle::ty;
 use middle::ty_fold;
-use middle::typeck::infer::{Bounds, cyclic_ty, fixup_err, fres, InferCtxt};
-use middle::typeck::infer::{unresolved_float_ty, unresolved_int_ty};
-use middle::typeck::infer::{unresolved_ty};
+use middle::typeck::infer::{cyclic_ty, fixup_err, fres, InferCtxt};
+use middle::typeck::infer::{unresolved_int_ty,unresolved_float_ty,unresolved_ty};
 use syntax::codemap::Span;
 use util::common::indent;
 use util::ppaux::{Repr, ty_to_string};
@@ -132,8 +131,8 @@ impl<'a> ResolveState<'a> {
         assert!(self.v_seen.is_empty());
         match self.err {
           None => {
-            debug!("Resolved to {} + {} (modes={:x})",
-                   ty_to_string(self.infcx.tcx, rty),
+            debug!("Resolved {} to {} (modes={:x})",
+                   ty_to_string(self.infcx.tcx, typ),
                    ty_to_string(self.infcx.tcx, rty),
                    self.modes);
             return Ok(rty);
@@ -219,21 +218,16 @@ impl<'a> ResolveState<'a> {
             // tend to carry more restrictions or higher
             // perf. penalties, so it pays to know more.
 
-            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));
+            let t1 = match self.infcx.type_variables.borrow().probe(vid) {
+                Some(t) => {
+                    self.resolve_type(t)
+                }
+                None => {
+                    if self.should(force_tvar) {
+                        self.err = Some(unresolved_ty(vid));
+                    }
+                    ty::mk_var(tcx, vid)
                 }
-                ty::mk_var(tcx, vid)
-              }
             };
             self.v_seen.pop().unwrap();
             return t1;
diff --git a/src/librustc/middle/typeck/infer/sub.rs b/src/librustc/middle/typeck/infer/sub.rs
index 1b83ee299bc7c..cc3abc279bf34 100644
--- a/src/librustc/middle/typeck/infer/sub.rs
+++ b/src/librustc/middle/typeck/infer/sub.rs
@@ -15,12 +15,12 @@ use middle::ty::TyVar;
 use middle::typeck::check::regionmanip::replace_late_bound_regions_in_fn_sig;
 use middle::typeck::infer::combine::*;
 use middle::typeck::infer::{cres, CresCompare};
+use middle::typeck::infer::equate::Equate;
 use middle::typeck::infer::glb::Glb;
 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::{TypeTrace, Subtype};
+use middle::typeck::infer::type_variable::{SubtypeOf, SupertypeOf};
 use util::common::{indenter};
 use util::ppaux::{bound_region_to_string, Repr};
 
@@ -43,27 +43,23 @@ impl<'f> Combine for Sub<'f> {
     fn a_is_expected(&self) -> bool { self.fields.a_is_expected }
     fn trace(&self) -> TypeTrace { self.fields.trace.clone() }
 
+    fn equate<'a>(&'a self) -> Equate<'a> { Equate(self.fields.clone()) }
     fn sub<'a>(&'a self) -> Sub<'a> { Sub(self.fields.clone()) }
     fn lub<'a>(&'a self) -> Lub<'a> { Lub(self.fields.clone()) }
     fn glb<'a>(&'a self) -> Glb<'a> { Glb(self.fields.clone()) }
 
     fn contratys(&self, a: ty::t, b: ty::t) -> cres<ty::t> {
-        let opp = CombineFields {
-            a_is_expected: !self.fields.a_is_expected,
-            ..self.fields.clone()
-        };
-        Sub(opp).tys(b, a)
+        Sub(self.fields.switch_expected()).tys(b, a)
     }
 
     fn contraregions(&self, a: ty::Region, b: ty::Region)
-                     -> cres<ty::Region>
-    {
-        let opp = CombineFields {
-            a_is_expected: !self.fields.a_is_expected,
-            ..self.fields.clone()
-        };
-        Sub(opp).regions(b, a)
-    }
+                     -> cres<ty::Region> {
+                         let opp = CombineFields {
+                             a_is_expected: !self.fields.a_is_expected,
+                             ..self.fields.clone()
+                         };
+                         Sub(opp).regions(b, a)
+                     }
 
     fn regions(&self, a: ty::Region, b: ty::Region) -> cres<ty::Region> {
         debug!("{}.regions({}, {})",
@@ -84,16 +80,18 @@ impl<'f> Combine for Sub<'f> {
         }
 
         match b.mutbl {
-          MutMutable => {
-            // If supertype is mut, subtype must match exactly
-            // (i.e., invariant if mut):
-            eq_tys(self, a.ty, b.ty).then(|| Ok(*a))
-          }
-          MutImmutable => {
-            // Otherwise we can be covariant:
-            self.tys(a.ty, b.ty).and_then(|_t| Ok(*a) )
-          }
+            MutMutable => {
+                // If supertype is mut, subtype must match exactly
+                // (i.e., invariant if mut):
+                try!(self.equate().tys(a.ty, b.ty));
+            }
+            MutImmutable => {
+                // Otherwise we can be covariant:
+                try!(self.tys(a.ty, b.ty));
+            }
         }
+
+        Ok(*a) // return is meaningless in sub, just return *a
     }
 
     fn fn_styles(&self, a: FnStyle, b: FnStyle) -> cres<FnStyle> {
@@ -126,14 +124,19 @@ impl<'f> Combine for Sub<'f> {
         debug!("{}.tys({}, {})", self.tag(),
                a.repr(self.fields.infcx.tcx), b.repr(self.fields.infcx.tcx));
         if a == b { return Ok(a); }
-        let _indenter = indenter();
+
+        let infcx = self.fields.infcx;
+        let a = infcx.type_variables.borrow().replace_if_possible(a);
+        let b = infcx.type_variables.borrow().replace_if_possible(b);
         match (&ty::get(a).sty, &ty::get(b).sty) {
             (&ty::ty_bot, _) => {
                 Ok(a)
             }
 
             (&ty::ty_infer(TyVar(a_id)), &ty::ty_infer(TyVar(b_id))) => {
-                if_ok!(self.fields.var_sub_var(a_id, b_id));
+                infcx.type_variables
+                    .borrow_mut()
+                    .relate_vars(a_id, SubtypeOf, b_id);
                 Ok(a)
             }
             // The vec/str check here and below is so that we don't unify
@@ -145,7 +148,9 @@ impl<'f> Combine for Sub<'f> {
                 Err(ty::terr_sorts(expected_found(self, a, b)))
             }
             (&ty::ty_infer(TyVar(a_id)), _) => {
-                if_ok!(self.fields.var_sub_t(a_id, b));
+                try!(self.fields
+                       .switch_expected()
+                       .instantiate(b, SupertypeOf, a_id));
                 Ok(a)
             }
 
@@ -154,7 +159,7 @@ impl<'f> Combine for Sub<'f> {
                 Err(ty::terr_sorts(expected_found(self, a, b)))
             }
             (_, &ty::ty_infer(TyVar(b_id))) => {
-                if_ok!(self.fields.t_sub_var(a, b_id));
+                try!(self.fields.instantiate(a, SubtypeOf, b_id));
                 Ok(a)
             }
 
diff --git a/src/librustc/middle/typeck/infer/type_variable.rs b/src/librustc/middle/typeck/infer/type_variable.rs
new file mode 100644
index 0000000000000..5f67f8a048aa4
--- /dev/null
+++ b/src/librustc/middle/typeck/infer/type_variable.rs
@@ -0,0 +1,173 @@
+// Copyright 2014 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;
+use std::mem;
+use util::snapshot_vec as sv;
+
+pub struct TypeVariableTable {
+    values: sv::SnapshotVec<TypeVariableData,UndoEntry,Delegate>,
+}
+
+struct TypeVariableData {
+    value: TypeVariableValue
+}
+
+enum TypeVariableValue {
+    Known(ty::t),
+    Bounded(Vec<Relation>),
+}
+
+pub struct Snapshot {
+    snapshot: sv::Snapshot
+}
+
+enum UndoEntry {
+    // The type of the var was specified.
+    SpecifyVar(ty::TyVid, Vec<Relation>),
+    Relate(ty::TyVid, ty::TyVid),
+}
+
+struct Delegate;
+
+type Relation = (RelationDir, ty::TyVid);
+
+#[deriving(PartialEq,Show)]
+pub enum RelationDir {
+    SubtypeOf, SupertypeOf, EqTo
+}
+
+impl RelationDir {
+    fn opposite(self) -> RelationDir {
+        match self {
+            SubtypeOf => SupertypeOf,
+            SupertypeOf => SubtypeOf,
+            EqTo => EqTo
+        }
+    }
+}
+
+impl TypeVariableTable {
+    pub fn new() -> TypeVariableTable {
+        TypeVariableTable { values: sv::SnapshotVec::new(Delegate) }
+    }
+
+    fn relations<'a>(&'a mut self, a: ty::TyVid) -> &'a mut Vec<Relation> {
+        relations(self.values.get_mut(a.index))
+    }
+
+    pub fn relate_vars(&mut self, a: ty::TyVid, dir: RelationDir, b: ty::TyVid) {
+        /*!
+         * Records that `a <: b`, `a :> b`, or `a == b`, depending on `dir`.
+         *
+         * Precondition: neither `a` nor `b` are known.
+         */
+
+        if a != b {
+            self.relations(a).push((dir, b));
+            self.relations(b).push((dir.opposite(), a));
+            self.values.record(Relate(a, b));
+        }
+    }
+
+    pub fn instantiate_and_push(
+        &mut self,
+        vid: ty::TyVid,
+        ty: ty::t,
+        stack: &mut Vec<(ty::t, RelationDir, ty::TyVid)>)
+    {
+        /*!
+         * Instantiates `vid` with the type `ty` and then pushes an
+         * entry onto `stack` for each of the relations of `vid` to
+         * other variables. The relations will have the form `(ty,
+         * dir, vid1)` where `vid1` is some other variable id.
+         */
+
+        let old_value = {
+            let value_ptr = &mut self.values.get_mut(vid.index).value;
+            mem::replace(value_ptr, Known(ty))
+        };
+
+        let relations = match old_value {
+            Bounded(b) => b,
+            Known(_) => fail!("Asked to instantiate variable that is \
+                               already instantiated")
+        };
+
+        for &(dir, vid) in relations.iter() {
+            stack.push((ty, dir, vid));
+        }
+
+        self.values.record(SpecifyVar(vid, relations));
+    }
+
+    pub fn new_var(&mut self) -> ty::TyVid {
+        let index =
+            self.values.push(
+                TypeVariableData { value: Bounded(Vec::new()) });
+        ty::TyVid { index: index }
+    }
+
+    pub fn probe(&self, vid: ty::TyVid) -> Option<ty::t> {
+        match self.values.get(vid.index).value {
+            Bounded(..) => None,
+            Known(t) => Some(t)
+        }
+    }
+
+    pub fn replace_if_possible(&self, t: ty::t) -> ty::t {
+        match ty::get(t).sty {
+            ty::ty_infer(ty::TyVar(v)) => {
+                match self.probe(v) {
+                    None => t,
+                    Some(u) => u
+                }
+            }
+            _ => t,
+        }
+    }
+
+    pub fn snapshot(&mut self) -> Snapshot {
+        Snapshot { snapshot: self.values.start_snapshot() }
+    }
+
+    pub fn rollback_to(&mut self, s: Snapshot) {
+        self.values.rollback_to(s.snapshot);
+    }
+
+    pub fn commit(&mut self, s: Snapshot) {
+        self.values.commit(s.snapshot);
+    }
+}
+
+impl sv::SnapshotVecDelegate<TypeVariableData,UndoEntry> for Delegate {
+    fn reverse(&mut self,
+               values: &mut Vec<TypeVariableData>,
+               action: UndoEntry) {
+        match action {
+            SpecifyVar(vid, relations) => {
+                values.get_mut(vid.index).value = Bounded(relations);
+            }
+
+            Relate(a, b) => {
+                relations(values.get_mut(a.index)).pop();
+                relations(values.get_mut(b.index)).pop();
+            }
+        }
+    }
+}
+
+fn relations<'a>(v: &'a mut TypeVariableData) -> &'a mut Vec<Relation> {
+    match v.value {
+        Known(_) => fail!("var_sub_var: variable is known"),
+        Bounded(ref mut relations) => relations
+    }
+}
+
diff --git a/src/librustc/middle/typeck/infer/unify.rs b/src/librustc/middle/typeck/infer/unify.rs
index fd722d3696638..adf0a25ce4002 100644
--- a/src/librustc/middle/typeck/infer/unify.rs
+++ b/src/librustc/middle/typeck/infer/unify.rs
@@ -12,7 +12,7 @@ use std::kinds::marker;
 
 use middle::ty::{expected_found, IntVarValue};
 use middle::ty;
-use middle::typeck::infer::{Bounds, uok, ures};
+use middle::typeck::infer::{uok, ures};
 use middle::typeck::infer::InferCtxt;
 use std::cell::RefCell;
 use std::fmt::Show;
@@ -23,12 +23,12 @@ use util::snapshot_vec as sv;
 /**
  * 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.
+ * this trait is implemented by `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.
+ * Each key type has an associated value type `V`. For example, for
+ * `IntVid`, this is `Option<IntVarValue>`, representing some
+ * (possibly not yet known) sort of integer.
  *
  * Implementations of this trait are at the end of this file.
  */
@@ -48,11 +48,10 @@ pub trait UnifyKey<V> : Clone + Show + PartialEq + Repr {
 }
 
 /**
- * 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>`.
+ * 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 an `Option` wrapper (where `None` represents a variable
+ * whose value is not yet set).
  *
  * Implementations of this trait are at the end of this file.
  */
@@ -109,9 +108,9 @@ pub struct Node<K,V> {
 pub struct Delegate;
 
 // We can't use V:LatticeValue, much as I would like to,
-// because frequently the pattern is that V=Bounds<U> for some
+// because frequently the pattern is that V=Option<U> for some
 // other type parameter U, and we have no way to say
-// Bounds<U>:
+// Option<U>:LatticeValue.
 
 impl<V:PartialEq+Clone+Repr,K:UnifyKey<V>> UnificationTable<K,V> {
     pub fn new() -> UnificationTable<K,V> {
@@ -375,26 +374,6 @@ impl<'tcx,V:SimplyUnifiable,K:UnifyKey<Option<V>>>
 
 ///////////////////////////////////////////////////////////////////////////
 
-// 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 UnifyValue for Bounds<ty::t> { }
-
 // Integral type keys
 
 impl UnifyKey<Option<IntVarValue>> for ty::IntVid {
diff --git a/src/test/compile-fail/issue-10291.rs b/src/test/compile-fail/issue-10291.rs
index 8ae20dfde9123..995ae7b3d44e7 100644
--- a/src/test/compile-fail/issue-10291.rs
+++ b/src/test/compile-fail/issue-10291.rs
@@ -9,7 +9,7 @@
 // except according to those terms.
 
 fn test<'x>(x: &'x int) {
-    drop::< <'z>|&'z int| -> &'z int>(|z| {
+    drop::< <'z>|&'z int| -> &'z int >(|z| {
         x
         //~^ ERROR cannot infer an appropriate lifetime
     });
diff --git a/src/test/compile-fail/issue-13482.rs b/src/test/compile-fail/issue-13482.rs
index 7159aa17623c0..2d7458944269c 100644
--- a/src/test/compile-fail/issue-13482.rs
+++ b/src/test/compile-fail/issue-13482.rs
@@ -12,7 +12,7 @@ fn main() {
   let x = [1,2];
   let y = match x {
     [] => None,
-//~^ ERROR expected `[<generic integer #1>, .. 2]`, found a fixed vector pattern of size 0
+//~^ ERROR expected `[<generic integer #0>, .. 2]`, found a fixed vector pattern of size 0
     [a,_] => Some(a)
   };
 }
diff --git a/src/test/compile-fail/issue-16338.rs b/src/test/compile-fail/issue-16338.rs
index d4b31066e5ac2..305b1fe2ad7de 100644
--- a/src/test/compile-fail/issue-16338.rs
+++ b/src/test/compile-fail/issue-16338.rs
@@ -12,6 +12,6 @@ use std::raw::Slice;
 
 fn main() {
     let Slice { data: data, len: len } = "foo";
-    //~^ ERROR mismatched types: expected `&'static str`, found a structure pattern
+    //~^ ERROR mismatched types: expected `&str`, found a structure pattern
 }
 
diff --git a/src/test/compile-fail/issue-2149.rs b/src/test/compile-fail/issue-2149.rs
index afb413584a481..5d07472afbb25 100644
--- a/src/test/compile-fail/issue-2149.rs
+++ b/src/test/compile-fail/issue-2149.rs
@@ -22,5 +22,5 @@ impl<A> vec_monad<A> for Vec<A> {
 }
 fn main() {
     ["hi"].bind(|x| [x] );
-    //~^ ERROR type `[&'static str, .. 1]` does not implement any method in scope named `bind`
+    //~^ ERROR type `[&str, .. 1]` does not implement any method in scope named `bind`
 }
diff --git a/src/test/compile-fail/kindck-send-object1.rs b/src/test/compile-fail/kindck-send-object1.rs
new file mode 100644
index 0000000000000..6a90fd5535604
--- /dev/null
+++ b/src/test/compile-fail/kindck-send-object1.rs
@@ -0,0 +1,44 @@
+// Copyright 2014 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.
+
+// Test which object types are considered sendable. This test
+// is broken into two parts because some errors occur in distinct
+// phases in the compiler. See kindck-send-object2.rs as well!
+
+fn assert_send<T:Send>() { }
+trait Dummy { }
+
+// careful with object types, who knows what they close over...
+fn test51<'a>() {
+    assert_send::<&'a Dummy>(); //~ ERROR does not fulfill the required lifetime
+}
+fn test52<'a>() {
+    assert_send::<&'a Dummy+Send>(); //~ ERROR does not fulfill the required lifetime
+}
+
+// ...unless they are properly bounded
+fn test60() {
+    assert_send::<&'static Dummy+Send>();
+}
+fn test61() {
+    assert_send::<Box<Dummy+Send>>();
+}
+
+// closure and object types can have lifetime bounds which make
+// them not ok
+fn test_70<'a>() {
+    assert_send::<proc():'a>(); //~ ERROR does not fulfill the required lifetime
+}
+
+fn test_71<'a>() {
+    assert_send::<Box<Dummy+'a>>(); //~ ERROR does not fulfill the required lifetime
+}
+
+fn main() { }
diff --git a/src/test/compile-fail/kindck-send-object2.rs b/src/test/compile-fail/kindck-send-object2.rs
new file mode 100644
index 0000000000000..75006477837c2
--- /dev/null
+++ b/src/test/compile-fail/kindck-send-object2.rs
@@ -0,0 +1,32 @@
+// Copyright 2014 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.
+
+// Continue kindck-send-object1.rs.
+
+fn assert_send<T:Send>() { }
+trait Dummy { }
+
+fn test50() {
+    assert_send::<&'static Dummy>(); //~ ERROR does not fulfill `Send`
+}
+
+fn test53() {
+    assert_send::<Box<Dummy>>(); //~ ERROR does not fulfill `Send`
+}
+
+// ...unless they are properly bounded
+fn test60() {
+    assert_send::<&'static Dummy+Send>();
+}
+fn test61() {
+    assert_send::<Box<Dummy+Send>>();
+}
+
+fn main() { }
diff --git a/src/test/compile-fail/kindck-send-owned.rs b/src/test/compile-fail/kindck-send-owned.rs
new file mode 100644
index 0000000000000..0eed05692b9c5
--- /dev/null
+++ b/src/test/compile-fail/kindck-send-owned.rs
@@ -0,0 +1,25 @@
+// Copyright 2014 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.
+
+// Test which of the builtin types are considered sendable.
+
+fn assert_send<T:Send>() { }
+
+// owned content are ok
+fn test30() { assert_send::<Box<int>>(); }
+fn test31() { assert_send::<String>(); }
+fn test32() { assert_send::<Vec<int> >(); }
+
+// but not if they own a bad thing
+fn test40<'a>(_: &'a int) {
+    assert_send::<Box<&'a int>>(); //~ ERROR does not fulfill the required lifetime
+}
+
+fn main() { }
diff --git a/src/test/compile-fail/kindck-send-region-pointers.rs b/src/test/compile-fail/kindck-send-region-pointers.rs
new file mode 100644
index 0000000000000..cc46d7f4de9c0
--- /dev/null
+++ b/src/test/compile-fail/kindck-send-region-pointers.rs
@@ -0,0 +1,34 @@
+// Copyright 2014 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.
+
+// Test that borrowed pointers are not sendable unless 'static.
+
+fn assert_send<T:Send>() { }
+
+// lifetime pointers with 'static lifetime are ok
+fn test01() { assert_send::<&'static int>(); }
+fn test02() { assert_send::<&'static str>(); }
+fn test03() { assert_send::<&'static [int]>(); }
+
+// whether or not they are mutable
+fn test10() { assert_send::<&'static mut int>(); }
+
+// otherwise lifetime pointers are not ok
+fn test20<'a>(_: &'a int) {
+    assert_send::<&'a int>(); //~ ERROR does not fulfill the required lifetime
+}
+fn test21<'a>(_: &'a int) {
+    assert_send::<&'a str>(); //~ ERROR does not fulfill the required lifetime
+}
+fn test22<'a>(_: &'a int) {
+    assert_send::<&'a [int]>(); //~ ERROR does not fulfill the required lifetime
+}
+
+fn main() { }
diff --git a/src/librustc/middle/typeck/infer/macros.rs b/src/test/compile-fail/kindck-send-unsafe.rs
similarity index 55%
rename from src/librustc/middle/typeck/infer/macros.rs
rename to src/test/compile-fail/kindck-send-unsafe.rs
index d3e81f07f7dc1..a9bbfcfa26263 100644
--- a/src/librustc/middle/typeck/infer/macros.rs
+++ b/src/test/compile-fail/kindck-send-unsafe.rs
@@ -1,4 +1,4 @@
-// Copyright 2012 The Rust Project Developers. See the COPYRIGHT
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
 // file at the top-level directory of this distribution and at
 // http://rust-lang.org/COPYRIGHT.
 //
@@ -8,13 +8,15 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-#![macro_escape]
+fn assert_send<T:Send>() { }
 
-macro_rules! if_ok(
-    ($inp: expr) => (
-        match $inp {
-            Ok(v) => { v }
-            Err(e) => { return Err(e); }
-        }
-    )
-)
+// unsafe ptrs are ok unless they point at unsendable things
+fn test70() {
+    assert_send::<*mut int>();
+}
+fn test71<'a>() {
+    assert_send::<*mut &'a int>(); //~ ERROR does not fulfill the required lifetime
+}
+
+fn main() {
+}
diff --git a/src/test/compile-fail/regions-bounds.rs b/src/test/compile-fail/regions-bounds.rs
index 68e198ea5b7a0..e13a6b211a503 100644
--- a/src/test/compile-fail/regions-bounds.rs
+++ b/src/test/compile-fail/regions-bounds.rs
@@ -17,12 +17,10 @@ struct a_class<'a> { x:&'a int }
 
 fn a_fn1<'a,'b>(e: an_enum<'a>) -> an_enum<'b> {
     return e; //~ ERROR mismatched types: expected `an_enum<'b>`, found `an_enum<'a>`
-    //~^ ERROR cannot infer
 }
 
 fn a_fn3<'a,'b>(e: a_class<'a>) -> a_class<'b> {
     return e; //~ ERROR mismatched types: expected `a_class<'b>`, found `a_class<'a>`
-    //~^ ERROR cannot infer
 }
 
 fn main() { }
diff --git a/src/test/compile-fail/regions-escape-bound-fn-2.rs b/src/test/compile-fail/regions-escape-bound-fn-2.rs
index d752bc97cac79..66103eb95888a 100644
--- a/src/test/compile-fail/regions-escape-bound-fn-2.rs
+++ b/src/test/compile-fail/regions-escape-bound-fn-2.rs
@@ -15,7 +15,6 @@ fn with_int(f: |x: &int|) {
 
 fn main() {
     let mut x = None;
-         //~^ ERROR lifetime of variable does not enclose its declaration
-         //~^^ ERROR type of expression contains references that are not valid during the expression
     with_int(|y| x = Some(y));
+         //~^ ERROR cannot infer
 }
diff --git a/src/test/compile-fail/regions-escape-bound-fn.rs b/src/test/compile-fail/regions-escape-bound-fn.rs
index eb72b4b0c5321..fee84cf9656d1 100644
--- a/src/test/compile-fail/regions-escape-bound-fn.rs
+++ b/src/test/compile-fail/regions-escape-bound-fn.rs
@@ -14,6 +14,6 @@ fn with_int(f: |x: &int|) {
 }
 
 fn main() {
-    let mut x: Option<&int> = None;   //~ ERROR cannot infer
-    with_int(|y| x = Some(y));
+    let mut x: Option<&int> = None;
+    with_int(|y| x = Some(y));   //~ ERROR cannot infer
 }
diff --git a/src/test/compile-fail/regions-escape-via-trait-or-not.rs b/src/test/compile-fail/regions-escape-via-trait-or-not.rs
index adef1f901fd0a..b73b5e0649ff5 100644
--- a/src/test/compile-fail/regions-escape-via-trait-or-not.rs
+++ b/src/test/compile-fail/regions-escape-via-trait-or-not.rs
@@ -27,7 +27,7 @@ fn with<R:Deref>(f: |x: &int| -> R) -> int {
 }
 
 fn return_it() -> int {
-    with(|o| o) //~ ERROR cannot infer an appropriate lifetime
+    with(|o| o) //~ ERROR cannot infer
 }
 
 fn main() {
diff --git a/src/test/compile-fail/regions-infer-at-fn-not-param.rs b/src/test/compile-fail/regions-infer-at-fn-not-param.rs
index e5444aadc1ca6..8af341e3ace42 100644
--- a/src/test/compile-fail/regions-infer-at-fn-not-param.rs
+++ b/src/test/compile-fail/regions-infer-at-fn-not-param.rs
@@ -22,7 +22,6 @@ struct not_parameterized2 {
 
 fn take1<'a>(p: parameterized1) -> parameterized1<'a> { p }
 //~^ ERROR mismatched types
-//~^^ ERROR cannot infer
 
 fn take3(p: not_parameterized1) -> not_parameterized1 { p }
 fn take4(p: not_parameterized2) -> not_parameterized2 { p }
diff --git a/src/test/compile-fail/regions-infer-contravariance-due-to-decl.rs b/src/test/compile-fail/regions-infer-contravariance-due-to-decl.rs
index d3e9c1f6ea848..4dd028b788459 100644
--- a/src/test/compile-fail/regions-infer-contravariance-due-to-decl.rs
+++ b/src/test/compile-fail/regions-infer-contravariance-due-to-decl.rs
@@ -33,7 +33,6 @@ fn use_<'short,'long>(c: Contravariant<'short>,
     // covariant with respect to its parameter 'a.
 
     let _: Contravariant<'long> = c; //~ ERROR mismatched types
-    //~^ ERROR  cannot infer an appropriate lifetime
 }
 
 fn main() {}
diff --git a/src/test/compile-fail/regions-infer-covariance-due-to-decl.rs b/src/test/compile-fail/regions-infer-covariance-due-to-decl.rs
index 2d3ca17301220..93c06aecd30ec 100644
--- a/src/test/compile-fail/regions-infer-covariance-due-to-decl.rs
+++ b/src/test/compile-fail/regions-infer-covariance-due-to-decl.rs
@@ -30,7 +30,6 @@ fn use_<'short,'long>(c: Covariant<'long>,
     // contravariant with respect to its parameter 'a.
 
     let _: Covariant<'short> = c; //~ ERROR mismatched types
-    //~^ ERROR  cannot infer an appropriate lifetime
 }
 
 fn main() {}
diff --git a/src/test/compile-fail/regions-infer-not-param.rs b/src/test/compile-fail/regions-infer-not-param.rs
index cadf66c328686..b84f13ec37feb 100644
--- a/src/test/compile-fail/regions-infer-not-param.rs
+++ b/src/test/compile-fail/regions-infer-not-param.rs
@@ -23,11 +23,9 @@ struct indirect2<'a> {
 }
 
 fn take_direct<'a,'b>(p: direct<'a>) -> direct<'b> { p } //~ ERROR mismatched types
-//~^ ERROR cannot infer
 
 fn take_indirect1(p: indirect1) -> indirect1 { p }
 
 fn take_indirect2<'a,'b>(p: indirect2<'a>) -> indirect2<'b> { p } //~ ERROR mismatched types
-//~^ ERROR cannot infer
 
 fn main() {}
diff --git a/src/test/compile-fail/regions-infer-paramd-indirect.rs b/src/test/compile-fail/regions-infer-paramd-indirect.rs
index 519223e97535e..e862b36dcd168 100644
--- a/src/test/compile-fail/regions-infer-paramd-indirect.rs
+++ b/src/test/compile-fail/regions-infer-paramd-indirect.rs
@@ -22,18 +22,17 @@ struct c<'a> {
 }
 
 trait set_f<'a> {
-    fn set_f_ok(&self, b: Gc<b<'a>>);
-    fn set_f_bad(&self, b: Gc<b>);
+    fn set_f_ok(&mut self, b: Gc<b<'a>>);
+    fn set_f_bad(&mut self, b: Gc<b>);
 }
 
 impl<'a> set_f<'a> for c<'a> {
-    fn set_f_ok(&self, b: Gc<b<'a>>) {
+    fn set_f_ok(&mut self, b: Gc<b<'a>>) {
         self.f = b;
     }
 
-    fn set_f_bad(&self, b: Gc<b>) {
+    fn set_f_bad(&mut self, b: Gc<b>) {
         self.f = b; //~ ERROR mismatched types: expected `Gc<Gc<&'a int>>`, found `Gc<Gc<&int>>`
-        //~^ ERROR cannot infer
     }
 }
 
diff --git a/src/test/compile-fail/regions-reborrow-from-shorter-mut-ref-mut-ref.rs b/src/test/compile-fail/regions-reborrow-from-shorter-mut-ref-mut-ref.rs
index 50ea8b1f2ed12..783009f6dcbfc 100644
--- a/src/test/compile-fail/regions-reborrow-from-shorter-mut-ref-mut-ref.rs
+++ b/src/test/compile-fail/regions-reborrow-from-shorter-mut-ref-mut-ref.rs
@@ -11,7 +11,7 @@
 // Issue #8624. Test for reborrowing with 3 levels, not just two.
 
 fn copy_borrowed_ptr<'a, 'b, 'c>(p: &'a mut &'b mut &'c mut int) -> &'b mut int {
-    &mut ***p //~ ERROR lifetime of `p` is too short to guarantee its contents
+    &mut ***p //~ ERROR cannot infer
 }
 
 fn main() {
diff --git a/src/test/compile-fail/regions-ret-borrowed-1.rs b/src/test/compile-fail/regions-ret-borrowed-1.rs
index aac81a2af6b1f..6d9b261917105 100644
--- a/src/test/compile-fail/regions-ret-borrowed-1.rs
+++ b/src/test/compile-fail/regions-ret-borrowed-1.rs
@@ -19,8 +19,6 @@ fn with<R>(f: <'a>|x: &'a int| -> R) -> R {
 fn return_it<'a>() -> &'a int {
     with(|o| o)
         //~^ ERROR cannot infer
-        //~^^ ERROR not valid during the expression
-        //~^^^ ERROR not valid at this point
 }
 
 fn main() {
diff --git a/src/test/compile-fail/regions-ret-borrowed.rs b/src/test/compile-fail/regions-ret-borrowed.rs
index dd9421ee2ef2c..465f4410fbbcc 100644
--- a/src/test/compile-fail/regions-ret-borrowed.rs
+++ b/src/test/compile-fail/regions-ret-borrowed.rs
@@ -22,8 +22,6 @@ fn with<R>(f: |x: &int| -> R) -> R {
 fn return_it<'a>() -> &'a int {
     with(|o| o)
         //~^ ERROR cannot infer
-        //~^^ ERROR not valid during the expression
-        //~^^^ ERROR not valid at this point
 }
 
 fn main() {
diff --git a/src/test/compile-fail/regions-variance-contravariant-use-covariant-in-second-position.rs b/src/test/compile-fail/regions-variance-contravariant-use-covariant-in-second-position.rs
index 77a54fec7bf7c..14ead8da1587b 100644
--- a/src/test/compile-fail/regions-variance-contravariant-use-covariant-in-second-position.rs
+++ b/src/test/compile-fail/regions-variance-contravariant-use-covariant-in-second-position.rs
@@ -33,7 +33,6 @@ fn use_<'short,'long>(c: S<'long, 'short>,
     // covariant with respect to its parameter 'a.
 
     let _: S<'long, 'long> = c; //~ ERROR mismatched types
-    //~^ ERROR  cannot infer an appropriate lifetime
 }
 
 fn main() {}
diff --git a/src/test/compile-fail/regions-variance-contravariant-use-covariant.rs b/src/test/compile-fail/regions-variance-contravariant-use-covariant.rs
index 0fab89264606b..3fc58071d2ce8 100644
--- a/src/test/compile-fail/regions-variance-contravariant-use-covariant.rs
+++ b/src/test/compile-fail/regions-variance-contravariant-use-covariant.rs
@@ -31,7 +31,6 @@ fn use_<'short,'long>(c: Contravariant<'short>,
     // covariant with respect to its parameter 'a.
 
     let _: Contravariant<'long> = c; //~ ERROR mismatched types
-    //~^ ERROR  cannot infer an appropriate lifetime
 }
 
 fn main() {}
diff --git a/src/test/compile-fail/regions-variance-covariant-use-contravariant.rs b/src/test/compile-fail/regions-variance-covariant-use-contravariant.rs
index 7dcdc9875e395..844c8151a642a 100644
--- a/src/test/compile-fail/regions-variance-covariant-use-contravariant.rs
+++ b/src/test/compile-fail/regions-variance-covariant-use-contravariant.rs
@@ -31,7 +31,6 @@ fn use_<'short,'long>(c: Covariant<'long>,
     // contravariant with respect to its parameter 'a.
 
     let _: Covariant<'short> = c; //~ ERROR mismatched types
-    //~^ ERROR cannot infer an appropriate lifetime
 }
 
 fn main() {}
diff --git a/src/test/run-pass/regions-scope-chain-example.rs b/src/test/run-pass/regions-scope-chain-example.rs
new file mode 100644
index 0000000000000..0eacb27a600bd
--- /dev/null
+++ b/src/test/run-pass/regions-scope-chain-example.rs
@@ -0,0 +1,48 @@
+// Copyright 2014 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.
+
+// This is an example where the older inference algorithm failed. The
+// specifics of why it failed are somewhat, but not entirely, tailed
+// to the algorithm. Ultimately the problem is that when computing the
+// mutual supertype of both sides of the `if` it would be faced with a
+// choice of tightening bounds or unifying variables and it took the
+// wrong path. The new algorithm avoids this problem and hence this
+// example typechecks correctly.
+
+enum ScopeChain<'a> {
+    Link(Scope<'a>),
+    End
+}
+
+type Scope<'a> = &'a ScopeChain<'a>;
+
+struct OuterContext;
+
+struct Context<'a> {
+    foo: &'a OuterContext
+}
+
+impl<'a> Context<'a> {
+    fn foo(&mut self, scope: Scope) {
+        let link = if 1i < 2 {
+            let l = Link(scope);
+            self.take_scope(&l);
+            l
+        } else {
+            Link(scope)
+        };
+        self.take_scope(&link);
+    }
+
+    fn take_scope(&mut self, x: Scope) {
+    }
+}
+
+fn main() { }