diff --git a/src/librustc/middle/ty.rs b/src/librustc/middle/ty.rs
index 840726b80417..0726104788cd 100644
--- a/src/librustc/middle/ty.rs
+++ b/src/librustc/middle/ty.rs
@@ -55,7 +55,7 @@ export ProvidedMethodSource;
 export ProvidedMethodInfo;
 export ProvidedMethodsMap;
 export InstantiatedTraitRef;
-export TyVid, IntVid, FloatVid, FnVid, RegionVid, Vid;
+export TyVid, IntVid, FloatVid, RegionVid, Vid;
 export br_hashmap;
 export is_instantiable;
 export node_id_to_type;
@@ -215,7 +215,7 @@ export ty_sort_str;
 export normalize_ty;
 export to_str;
 export bound_const;
-export terr_no_integral_type, terr_no_floating_point_type;
+export terr_int_mismatch, terr_float_mismatch, terr_sigil_mismatch;
 export terr_ty_param_size, terr_self_substs;
 export terr_in_field, terr_record_fields, terr_vstores_differ, terr_arg_count;
 export terr_sorts, terr_vec, terr_str, terr_record_size, terr_tuple_size;
@@ -241,6 +241,7 @@ export AutoRef;
 export AutoRefKind, AutoPtr, AutoBorrowVec, AutoBorrowVecRef, AutoBorrowFn;
 export iter_bound_traits_and_supertraits;
 export count_traits_and_supertraits;
+export IntVarValue, IntType, UintType;
 
 // Data types
 
@@ -703,6 +704,12 @@ enum sty {
     ty_unboxed_vec(mt),
 }
 
+#[deriving_eq]
+enum IntVarValue {
+    IntType(ast::int_ty),
+    UintType(ast::uint_ty),
+}
+
 enum terr_vstore_kind {
     terr_vec, terr_str, terr_fn, terr_trait
 }
@@ -740,8 +747,8 @@ enum type_err {
     terr_sorts(expected_found<t>),
     terr_self_substs,
     terr_integer_as_char,
-    terr_no_integral_type,
-    terr_no_floating_point_type,
+    terr_int_mismatch(expected_found<IntVarValue>),
+    terr_float_mismatch(expected_found<ast::float_ty>)
 }
 
 enum param_bound {
@@ -752,10 +759,16 @@ enum param_bound {
     bound_trait(t),
 }
 
+#[deriving_eq]
 enum TyVid = uint;
+
+#[deriving_eq]
 enum IntVid = uint;
+
+#[deriving_eq]
 enum FloatVid = uint;
-enum FnVid = uint;
+
+#[deriving_eq]
 #[auto_encode]
 #[auto_decode]
 enum RegionVid = uint;
@@ -851,14 +864,6 @@ impl FloatVid: ToStr {
     pure fn to_str() -> ~str { fmt!("<VF%u>", self.to_uint()) }
 }
 
-impl FnVid: Vid {
-    pure fn to_uint() -> uint { *self }
-}
-
-impl FnVid: ToStr {
-    pure fn to_str() -> ~str { fmt!("<F%u>", self.to_uint()) }
-}
-
 impl RegionVid: Vid {
     pure fn to_uint() -> uint { *self }
 }
@@ -884,33 +889,36 @@ impl InferTy: ToStr {
     }
 }
 
-impl RegionVid : to_bytes::IterBytes {
-    pure fn iter_bytes(&self, +lsb0: bool, f: to_bytes::Cb) {
-        (**self).iter_bytes(lsb0, f)
+impl IntVarValue : ToStr {
+    pure fn to_str() -> ~str {
+        match self {
+            IntType(ref v) => v.to_str(),
+            UintType(ref v) => v.to_str(),
+        }
     }
 }
 
 impl TyVid : to_bytes::IterBytes {
     pure fn iter_bytes(&self, +lsb0: bool, f: to_bytes::Cb) {
-        (**self).iter_bytes(lsb0, f)
+        self.to_uint().iter_bytes(lsb0, f)
     }
 }
 
 impl IntVid : to_bytes::IterBytes {
     pure fn iter_bytes(&self, +lsb0: bool, f: to_bytes::Cb) {
-        (**self).iter_bytes(lsb0, f)
+        self.to_uint().iter_bytes(lsb0, f)
     }
 }
 
 impl FloatVid : to_bytes::IterBytes {
     pure fn iter_bytes(&self, +lsb0: bool, f: to_bytes::Cb) {
-        (**self).iter_bytes(lsb0, f)
+        self.to_uint().iter_bytes(lsb0, f)
     }
 }
 
-impl FnVid : to_bytes::IterBytes {
+impl RegionVid : to_bytes::IterBytes {
     pure fn iter_bytes(&self, +lsb0: bool, f: to_bytes::Cb) {
-        (**self).iter_bytes(lsb0, f)
+        self.to_uint().iter_bytes(lsb0, f)
     }
 }
 
@@ -3575,17 +3583,18 @@ fn type_err_to_str(cx: ctxt, err: &type_err) -> ~str {
         terr_self_substs => {
             ~"inconsistent self substitution" // XXX this is more of a bug
         }
-        terr_no_integral_type => {
-            ~"couldn't determine an appropriate integral type for integer \
-              literal"
-        }
         terr_integer_as_char => {
-            ~"integer literals can't be inferred to char type \
-              (try an explicit cast)"
+            fmt!("expected an integral type but found char")
         }
-        terr_no_floating_point_type => {
-            ~"couldn't determine an appropriate floating point type for \
-              floating point literal"
+        terr_int_mismatch(ref values) => {
+            fmt!("expected %s but found %s",
+                 values.expected.to_str(),
+                 values.found.to_str())
+        }
+        terr_float_mismatch(ref values) => {
+            fmt!("expected %s but found %s",
+                 values.expected.to_str(),
+                 values.found.to_str())
         }
     }
 }
@@ -4451,31 +4460,6 @@ impl vstore : cmp::Eq {
     pure fn ne(&self, other: &vstore) -> bool { !(*self).eq(other) }
 }
 
-impl TyVid : cmp::Eq {
-    pure fn eq(&self, other: &TyVid) -> bool { *(*self) == *(*other) }
-    pure fn ne(&self, other: &TyVid) -> bool { *(*self) != *(*other) }
-}
-
-impl IntVid : cmp::Eq {
-    pure fn eq(&self, other: &IntVid) -> bool { *(*self) == *(*other) }
-    pure fn ne(&self, other: &IntVid) -> bool { *(*self) != *(*other) }
-}
-
-impl FloatVid : cmp::Eq {
-    pure fn eq(&self, other: &FloatVid) -> bool { *(*self) == *(*other) }
-    pure fn ne(&self, other: &FloatVid) -> bool { *(*self) != *(*other) }
-}
-
-impl FnVid : cmp::Eq {
-    pure fn eq(&self, other: &FnVid) -> bool { *(*self) == *(*other) }
-    pure fn ne(&self, other: &FnVid) -> bool { *(*self) != *(*other) }
-}
-
-impl RegionVid : cmp::Eq {
-    pure fn eq(&self, other: &RegionVid) -> bool { *(*self) == *(*other) }
-    pure fn ne(&self, other: &RegionVid) -> bool { *(*self) != *(*other) }
-}
-
 impl Region : cmp::Eq {
     pure fn eq(&self, other: &Region) -> bool {
         match (*self) {
diff --git a/src/librustc/middle/typeck/infer/assignment.rs b/src/librustc/middle/typeck/infer/assignment.rs
index fef63cf9a42c..cd4514f6a2c5 100644
--- a/src/librustc/middle/typeck/infer/assignment.rs
+++ b/src/librustc/middle/typeck/infer/assignment.rs
@@ -103,8 +103,8 @@ impl Assign {
             }
 
             (ty::ty_infer(TyVar(a_id)), ty::ty_infer(TyVar(b_id))) => {
-                let nde_a = self.infcx.get(&self.infcx.ty_var_bindings, a_id);
-                let nde_b = self.infcx.get(&self.infcx.ty_var_bindings, b_id);
+                let nde_a = self.infcx.get(a_id);
+                let nde_b = self.infcx.get(b_id);
                 let a_bounds = nde_a.possible_types;
                 let b_bounds = nde_b.possible_types;
 
@@ -114,7 +114,7 @@ impl Assign {
             }
 
             (ty::ty_infer(TyVar(a_id)), _) => {
-                let nde_a = self.infcx.get(&self.infcx.ty_var_bindings, a_id);
+                let nde_a = self.infcx.get(a_id);
                 let a_bounds = nde_a.possible_types;
 
                 let a_bnd = option::or(a_bounds.ub, a_bounds.lb);
@@ -122,7 +122,7 @@ impl Assign {
             }
 
             (_, ty::ty_infer(TyVar(b_id))) => {
-                let nde_b = self.infcx.get(&self.infcx.ty_var_bindings, b_id);
+                let nde_b = self.infcx.get(b_id);
                 let b_bounds = nde_b.possible_types;
 
                 let b_bnd = option::or(b_bounds.lb, b_bounds.ub);
diff --git a/src/librustc/middle/typeck/infer/combine.rs b/src/librustc/middle/typeck/infer/combine.rs
index c5e99bc5c036..e9946ae7c13e 100644
--- a/src/librustc/middle/typeck/infer/combine.rs
+++ b/src/librustc/middle/typeck/infer/combine.rs
@@ -57,6 +57,7 @@
 use core::prelude::*;
 
 use middle::ty::{FloatVar, FnTyBase, FnMeta, FnSig, IntVar, TyVar};
+use middle::ty::{IntType, UintType};
 use middle::ty;
 use middle::typeck::infer::glb::Glb;
 use middle::typeck::infer::lub::Lub;
@@ -112,8 +113,8 @@ pub struct CombineFields {
 }
 
 fn expected_found<C:Combine,T>(
-    self: &C, +a: T, +b: T) -> ty::expected_found<T> {
-
+    self: &C, +a: T, +b: T) -> ty::expected_found<T>
+{
     if self.a_is_expected() {
         ty::expected_found {expected: move a, found: move b}
     } else {
@@ -392,7 +393,7 @@ fn super_tys<C:Combine>(
     self: &C, a: ty::t, b: ty::t) -> cres<ty::t>
 {
     let tcx = self.infcx().tcx;
-    match (/*bad*/copy ty::get(a).sty, /*bad*/copy ty::get(b).sty) {
+    return match (/*bad*/copy ty::get(a).sty, /*bad*/copy ty::get(b).sty) {
       // The "subtype" ought to be handling cases involving bot or var:
       (ty::ty_bot, _) |
       (_, ty::ty_bot) |
@@ -405,53 +406,46 @@ fn super_tys<C:Combine>(
                  b.inf_str(self.infcx())));
       }
 
-      // Relate integral variables to other types
-      (ty::ty_infer(IntVar(a_id)), ty::ty_infer(IntVar(b_id))) => {
-        if_ok!(self.infcx().simple_vars(&self.infcx().int_var_bindings,
-                                        ty::terr_no_integral_type,
-                                        a_id, b_id));
-        Ok(a)
-      }
-      (ty::ty_infer(IntVar(v_id)), ty::ty_int(v)) |
-      (ty::ty_int(v), ty::ty_infer(IntVar(v_id))) => {
-        if v == ast::ty_char {
-            Err(ty::terr_integer_as_char)
-        } else {
-            if_ok!(self.infcx().simple_var_t(&self.infcx().int_var_bindings,
-                                             ty::terr_no_integral_type,
-                                             v_id, IntType(v)));
-            Ok(ty::mk_mach_int(tcx, v))
+        // Relate integral variables to other types
+        (ty::ty_infer(IntVar(a_id)), ty::ty_infer(IntVar(b_id))) => {
+            if_ok!(self.infcx().simple_vars(self.a_is_expected(),
+                                            a_id, b_id));
+            Ok(a)
+        }
+        (ty::ty_infer(IntVar(v_id)), ty::ty_int(v)) => {
+            unify_integral_variable(self, self.a_is_expected(),
+                                    v_id, IntType(v))
+        }
+        (ty::ty_int(v), ty::ty_infer(IntVar(v_id))) => {
+            unify_integral_variable(self, !self.a_is_expected(),
+                                    v_id, IntType(v))
+        }
+        (ty::ty_infer(IntVar(v_id)), ty::ty_uint(v)) => {
+            unify_integral_variable(self, self.a_is_expected(),
+                                    v_id, UintType(v))
+        }
+        (ty::ty_uint(v), ty::ty_infer(IntVar(v_id))) => {
+            unify_integral_variable(self, !self.a_is_expected(),
+                                    v_id, UintType(v))
         }
-      }
-      (ty::ty_infer(IntVar(v_id)), ty::ty_uint(v)) |
-      (ty::ty_uint(v), ty::ty_infer(IntVar(v_id))) => {
-        if_ok!(self.infcx().simple_var_t(&self.infcx().int_var_bindings,
-                                         ty::terr_no_integral_type,
-                                         v_id, UintType(v)));
-        Ok(ty::mk_mach_uint(tcx, v))
-      }
 
-      // Relate floating-point variables to other types
-      (ty::ty_infer(FloatVar(a_id)), ty::ty_infer(FloatVar(b_id))) => {
-        if_ok!(self.infcx().simple_vars(&self.infcx().float_var_bindings,
-                                        ty::terr_no_floating_point_type,
-                                        a_id, b_id));
-        Ok(a)
-      }
-      (ty::ty_infer(FloatVar(v_id)), ty::ty_float(v)) |
-      (ty::ty_float(v), ty::ty_infer(FloatVar(v_id))) => {
-        if_ok!(self.infcx().simple_var_t(&self.infcx().float_var_bindings,
-                                         ty::terr_no_floating_point_type,
-                                         v_id, v));
-        Ok(ty::mk_mach_float(tcx, v))
-      }
+        // Relate floating-point variables to other types
+        (ty::ty_infer(FloatVar(a_id)), ty::ty_infer(FloatVar(b_id))) => {
+            if_ok!(self.infcx().simple_vars(self.a_is_expected(),
+                                            a_id, b_id));
+            Ok(a)
+        }
+        (ty::ty_infer(FloatVar(v_id)), ty::ty_float(v)) => {
+            unify_float_variable(self, self.a_is_expected(), v_id, v)
+        }
+        (ty::ty_float(v), ty::ty_infer(FloatVar(v_id))) => {
+            unify_float_variable(self, !self.a_is_expected(), v_id, v)
+        }
 
       (ty::ty_int(_), _) |
       (ty::ty_uint(_), _) |
       (ty::ty_float(_), _) => {
-        let as_ = /*bad*/copy ty::get(a).sty;
-        let bs = /*bad*/copy ty::get(b).sty;
-        if as_ == bs {
+        if ty::get(a).sty == ty::get(b).sty {
             Ok(a)
         } else {
             Err(ty::terr_sorts(expected_found(self, a, b)))
@@ -516,11 +510,9 @@ fn super_tys<C:Combine>(
       }
 
       (ty::ty_rptr(a_r, a_mt), ty::ty_rptr(b_r, b_mt)) => {
-        do self.contraregions(a_r, b_r).chain |r| {
-            do self.mts(a_mt, b_mt).chain |mt| {
-                Ok(ty::mk_rptr(tcx, r, mt))
-            }
-        }
+          let r = if_ok!(self.contraregions(a_r, b_r));
+          let mt = if_ok!(self.mts(a_mt, b_mt));
+          Ok(ty::mk_rptr(tcx, r, mt))
       }
 
       (ty::ty_evec(a_mt, vs_a), ty::ty_evec(b_mt, vs_b)) => {
@@ -565,5 +557,34 @@ fn super_tys<C:Combine>(
       }
 
       _ => Err(ty::terr_sorts(expected_found(self, a, b)))
+    };
+
+    fn unify_integral_variable<C:Combine>(
+        self: &C,
+        vid_is_expected: bool,
+        vid: ty::IntVid,
+        val: ty::IntVarValue) -> cres<ty::t>
+    {
+        let tcx = self.infcx().tcx;
+        if val == IntType(ast::ty_char) {
+            Err(ty::terr_integer_as_char)
+        } else {
+            if_ok!(self.infcx().simple_var_t(vid_is_expected, vid, val));
+            match val {
+                IntType(v) => Ok(ty::mk_mach_int(tcx, v)),
+                UintType(v) => Ok(ty::mk_mach_uint(tcx, v))
+            }
+        }
     }
-}
+
+    fn unify_float_variable<C:Combine>(
+        self: &C,
+        vid_is_expected: bool,
+        vid: ty::FloatVid,
+        val: ast::float_ty) -> cres<ty::t>
+    {
+        let tcx = self.infcx().tcx;
+        if_ok!(self.infcx().simple_var_t(vid_is_expected, vid, val));
+        Ok(ty::mk_mach_float(tcx, val))
+    }
+}
\ No newline at end of file
diff --git a/src/librustc/middle/typeck/infer/lattice.rs b/src/librustc/middle/typeck/infer/lattice.rs
index 54638819f7cc..6ae10b120fe7 100644
--- a/src/librustc/middle/typeck/infer/lattice.rs
+++ b/src/librustc/middle/typeck/infer/lattice.rs
@@ -89,9 +89,9 @@ impl FnMeta: LatticeValue {
 }
 
 impl CombineFields {
-    fn var_sub_var<V:Copy Eq Vid ToStr, T:Copy InferStr LatticeValue>(
+    fn var_sub_var<T:Copy InferStr LatticeValue,
+                   V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
         &self,
-        vb: &ValsAndBindings<V, Bounds<T>>,
         +a_id: V,
         +b_id: V) -> ures
     {
@@ -102,8 +102,8 @@ impl CombineFields {
          * top of infer.rs*/
 
         // Need to make sub_id a subtype of sup_id.
-        let node_a = self.infcx.get(vb, a_id);
-        let node_b = self.infcx.get(vb, b_id);
+        let node_a = self.infcx.get(a_id);
+        let node_b = self.infcx.get(b_id);
         let a_id = node_a.root;
         let b_id = node_b.root;
         let a_bounds = node_a.possible_types;
@@ -135,17 +135,17 @@ impl CombineFields {
         // A remains a subtype of B.  Actually, there are other options,
         // but that's the route we choose to take.
 
-        self.infcx.unify(vb, &node_a, &node_b, |new_root, new_rank| {
-            self.set_var_to_merged_bounds(vb, new_root,
+        self.infcx.unify(&node_a, &node_b, |new_root, new_rank| {
+            self.set_var_to_merged_bounds(new_root,
                                           &a_bounds, &b_bounds,
                                           new_rank)
         })
     }
 
     /// make variable a subtype of T
-    fn var_sub_t<V:Copy Eq Vid ToStr, T:Copy InferStr LatticeValue>(
+    fn var_sub_t<T:Copy InferStr LatticeValue,
+                 V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
         &self,
-        vb: &ValsAndBindings<V, Bounds<T>>,
         +a_id: V,
         +b: T) -> ures
     {
@@ -153,7 +153,7 @@ impl CombineFields {
          *
          * Make a variable (`a_id`) a subtype of the concrete type `b` */
 
-        let node_a = self.infcx.get(vb, a_id);
+        let node_a = self.infcx.get(a_id);
         let a_id = node_a.root;
         let a_bounds = &node_a.possible_types;
         let b_bounds = &{lb: None, ub: Some(b)};
@@ -164,12 +164,12 @@ impl CombineFields {
                b.inf_str(self.infcx));
 
         self.set_var_to_merged_bounds(
-            vb, a_id, a_bounds, b_bounds, node_a.rank)
+            a_id, a_bounds, b_bounds, node_a.rank)
     }
 
-    fn t_sub_var<V:Copy Eq Vid ToStr, T:Copy InferStr LatticeValue>(
+    fn t_sub_var<T:Copy InferStr LatticeValue,
+                 V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
         &self,
-        vb: &ValsAndBindings<V, Bounds<T>>,
         +a: T,
         +b_id: V) -> ures
     {
@@ -178,7 +178,7 @@ impl CombineFields {
          * Make a concrete type (`a`) a subtype of the variable `b_id` */
 
         let a_bounds = &{lb: Some(a), ub: None};
-        let node_b = self.infcx.get(vb, b_id);
+        let node_b = self.infcx.get(b_id);
         let b_id = node_b.root;
         let b_bounds = &node_b.possible_types;
 
@@ -188,7 +188,7 @@ impl CombineFields {
                b_bounds.inf_str(self.infcx));
 
         self.set_var_to_merged_bounds(
-            vb, b_id, a_bounds, b_bounds, node_b.rank)
+            b_id, a_bounds, b_bounds, node_b.rank)
     }
 
     fn merge_bnd<T:Copy InferStr LatticeValue>(
@@ -219,10 +219,9 @@ impl CombineFields {
         }
     }
 
-    fn set_var_to_merged_bounds<V:Copy Eq Vid ToStr,
-                                T:Copy InferStr LatticeValue>(
+    fn set_var_to_merged_bounds<T:Copy InferStr LatticeValue,
+                                V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
         &self,
-        vb: &ValsAndBindings<V, Bounds<T>>,
         +v_id: V,
         a: &Bounds<T>,
         b: &Bounds<T>,
@@ -278,7 +277,7 @@ impl CombineFields {
         // the new bounds must themselves
         // be relatable:
         let () = if_ok!(self.bnds(&bounds.lb, &bounds.ub));
-        self.infcx.set(vb, v_id, Root(bounds, rank));
+        self.infcx.set(v_id, Root(bounds, rank));
         uok()
     }
 
@@ -369,8 +368,7 @@ fn super_lattice_tys<L:LatticeDir TyLatticeDir Combine>(
         (_, ty::ty_bot) => { return self.ty_bot(a); }
 
         (ty::ty_infer(TyVar(a_id)), ty::ty_infer(TyVar(b_id))) => {
-            let r = if_ok!(lattice_vars(self, &self.infcx().ty_var_bindings,
-                                        a_id, b_id,
+            let r = if_ok!(lattice_vars(self, a_id, b_id,
                                         |x, y| self.tys(*x, *y)));
             return match r {
                 VarResult(v) => Ok(ty::mk_var(tcx, v)),
@@ -379,14 +377,12 @@ fn super_lattice_tys<L:LatticeDir TyLatticeDir Combine>(
         }
 
         (ty::ty_infer(TyVar(a_id)), _) => {
-            return lattice_var_and_t(self, &self.infcx().ty_var_bindings,
-                                     a_id, &b,
+            return lattice_var_and_t(self, a_id, &b,
                                      |x, y| self.tys(*x, *y));
         }
 
         (_, ty::ty_infer(TyVar(b_id))) => {
-            return lattice_var_and_t(self, &self.infcx().ty_var_bindings,
-                                     b_id, &a,
+            return lattice_var_and_t(self, b_id, &a,
                                      |x, y| self.tys(*x, *y));
         }
 
@@ -419,17 +415,16 @@ enum LatticeVarResult<V,T> {
  *   result is a variable.  This is indicated with a `VarResult`
  *   return. */
 fn lattice_vars<L:LatticeDir Combine,
-                V:Copy Eq Vid ToStr,
-                T:Copy InferStr LatticeValue>(
+                T:Copy InferStr LatticeValue,
+                V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
     self: &L,                           // defines whether we want LUB or GLB
-    vb: &ValsAndBindings<V, Bounds<T>>, // relevant variable bindings
     +a_vid: V,                          // first variable
     +b_vid: V,                          // second variable
     lattice_dir_op: LatticeDirOp<T>)    // LUB or GLB operation on types
     -> cres<LatticeVarResult<V,T>>
 {
-    let nde_a = self.infcx().get(vb, a_vid);
-    let nde_b = self.infcx().get(vb, b_vid);
+    let nde_a = self.infcx().get(a_vid);
+    let nde_b = self.infcx().get(b_vid);
     let a_vid = nde_a.root;
     let b_vid = nde_b.root;
     let a_bounds = &nde_a.possible_types;
@@ -461,22 +456,21 @@ 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 = self.combine_fields();
-    do cf.var_sub_var(vb, a_vid, b_vid).then {
+    do cf.var_sub_var(a_vid, b_vid).then {
         Ok(VarResult(a_vid))
     }
 }
 
 fn lattice_var_and_t<L:LatticeDir Combine,
-                     V:Copy Eq Vid ToStr,
-                     T:Copy InferStr LatticeValue>(
+                     T:Copy InferStr LatticeValue,
+                     V:Copy Eq ToStr Vid UnifyVid<Bounds<T>>>(
     self: &L,
-    vb: &ValsAndBindings<V, Bounds<T>>,
     +a_id: V,
     b: &T,
     lattice_dir_op: LatticeDirOp<T>)
     -> cres<T>
 {
-    let nde_a = self.infcx().get(vb, a_id);
+    let nde_a = self.infcx().get(a_id);
     let a_id = nde_a.root;
     let a_bounds = &nde_a.possible_types;
 
@@ -501,7 +495,7 @@ fn lattice_var_and_t<L:LatticeDir Combine,
             debug!("bnd=None");
             let a_bounds = self.with_bnd(a_bounds, *b);
             do self.combine_fields().bnds(&a_bounds.lb, &a_bounds.ub).then {
-                self.infcx().set(vb, a_id, Root(a_bounds, nde_a.rank));
+                self.infcx().set(a_id, Root(a_bounds, nde_a.rank));
                 Ok(*b)
             }
         }
diff --git a/src/librustc/middle/typeck/infer/mod.rs b/src/librustc/middle/typeck/infer/mod.rs
index ec5de2b4f261..b702448fbf47 100644
--- a/src/librustc/middle/typeck/infer/mod.rs
+++ b/src/librustc/middle/typeck/infer/mod.rs
@@ -251,6 +251,7 @@ use core::prelude::*;
 use middle::ty::{TyVid, IntVid, FloatVid, RegionVid, Vid};
 use middle::ty::{mk_fn, type_is_bot};
 use middle::ty::{ty_int, ty_uint, get, terr_fn, TyVar, IntVar, FloatVar};
+use middle::ty::IntVarValue;
 use middle::ty;
 use middle::typeck::check::regionmanip::{replace_bound_regions_in_fn_sig};
 use middle::typeck::infer::assignment::Assign;
@@ -351,12 +352,6 @@ type ures = cres<()>; // "unify result"
 type fres<T> = Result<T, fixup_err>; // "fixup result"
 type ares = cres<Option<@ty::AutoAdjustment>>; // "assignment result"
 
-#[deriving_eq]
-enum IntVarValue {
-    IntType(ast::int_ty),
-    UintType(ast::uint_ty),
-}
-
 struct InferCtxt {
     tcx: ty::ctxt,
 
@@ -364,22 +359,14 @@ struct InferCtxt {
     // types that might instantiate a general type variable have an
     // order, represented by its upper and lower bounds.
     ty_var_bindings: ValsAndBindings<ty::TyVid, Bounds<ty::t>>,
-
-    // Number of type variables created thus far.
     mut ty_var_counter: uint,
 
-    // The types that might instantiate an integral type variable are
-    // represented by an int_ty_set.
+    // Map from integral variable to the kind of integer it represents
     int_var_bindings: ValsAndBindings<ty::IntVid, Option<IntVarValue>>,
-
-    // Number of integral variables created thus far.
     mut int_var_counter: uint,
 
-    // The types that might instantiate a floating-point type variable are
-    // represented by an float_ty_set.
+    // Map from floating variable to the kind of float it represents
     float_var_bindings: ValsAndBindings<ty::FloatVid, Option<ast::float_ty>>,
-
-    // Number of floating-point variables created thus far.
     mut float_var_counter: uint,
 
     // For region variables.
@@ -582,6 +569,7 @@ fn rollback_to<V:Copy Vid, T:Copy>(
 struct Snapshot {
     ty_var_bindings_len: uint,
     int_var_bindings_len: uint,
+    float_var_bindings_len: uint,
     region_vars_snapshot: uint,
 }
 
@@ -607,6 +595,8 @@ impl @InferCtxt {
                 self.ty_var_bindings.bindings.len(),
             int_var_bindings_len:
                 self.int_var_bindings.bindings.len(),
+            float_var_bindings_len:
+                self.float_var_bindings.bindings.len(),
             region_vars_snapshot:
                 self.region_vars.start_snapshot(),
         }
@@ -616,9 +606,11 @@ impl @InferCtxt {
         debug!("rollback!");
         rollback_to(&self.ty_var_bindings, snapshot.ty_var_bindings_len);
 
-        // FIXME(#3211) -- int_var not transactional
+        // FIXME(#3211) -- int_var and float_var not transactional
         //rollback_to(&self.int_var_bindings,
         //            snapshot.int_var_bindings_len);
+        //rollback_to(&self.float_var_bindings,
+        //            snapshot.float_var_bindings_len);
 
         self.region_vars.rollback_to(snapshot.region_vars_snapshot);
     }
@@ -664,6 +656,16 @@ impl @InferCtxt {
     }
 }
 
+fn next_simple_var<V: Copy,T: Copy>(
+    +counter: &mut uint,
+    +bindings: &ValsAndBindings<V,Option<T>>) -> uint
+{
+    let id = *counter;
+    *counter += 1;
+    bindings.vals.insert(id, Root(None, 0));
+    return id;
+}
+
 impl @InferCtxt {
     fn next_ty_var_id() -> TyVid {
         let id = self.ty_var_counter;
@@ -682,11 +684,8 @@ impl @InferCtxt {
     }
 
     fn next_int_var_id() -> IntVid {
-        let id = self.int_var_counter;
-        self.int_var_counter += 1;
-
-        self.int_var_bindings.vals.insert(id, Root(None, 0));
-        return IntVid(id);
+        IntVid(next_simple_var(&mut self.int_var_counter,
+                               &self.int_var_bindings))
     }
 
     fn next_int_var() -> ty::t {
@@ -694,11 +693,8 @@ impl @InferCtxt {
     }
 
     fn next_float_var_id() -> FloatVid {
-        let id = self.float_var_counter;
-        self.float_var_counter += 1;
-
-        self.float_var_bindings.vals.insert(id, Root(None, 0));
-        return FloatVid(id);
+        FloatVid(next_simple_var(&mut self.float_var_counter,
+                                 &self.float_var_bindings))
     }
 
     fn next_float_var() -> ty::t {
diff --git a/src/librustc/middle/typeck/infer/resolve.rs b/src/librustc/middle/typeck/infer/resolve.rs
index 23be3b208271..01f4b86b4885 100644
--- a/src/librustc/middle/typeck/infer/resolve.rs
+++ b/src/librustc/middle/typeck/infer/resolve.rs
@@ -49,11 +49,10 @@
 use core::prelude::*;
 
 use middle::ty::{FloatVar, FloatVid, IntVar, IntVid, RegionVid, TyVar, TyVid};
-use middle::ty::{type_is_bot};
+use middle::ty::{type_is_bot, IntType, UintType};
 use middle::ty;
 use middle::typeck::infer::{cyclic_ty, fixup_err, fres, InferCtxt};
 use middle::typeck::infer::{region_var_bound_by_region_var, unresolved_ty};
-use middle::typeck::infer::{IntType, UintType};
 use middle::typeck::infer::to_str::InferStr;
 use middle::typeck::infer::unify::Root;
 use util::common::{indent, indenter};
@@ -219,7 +218,7 @@ impl ResolveState {
             // tend to carry more restrictions or higher
             // perf. penalties, so it pays to know more.
 
-            let nde = self.infcx.get(&self.infcx.ty_var_bindings, vid);
+            let nde = self.infcx.get(vid);
             let bounds = nde.possible_types;
 
             let t1 = match bounds {
@@ -243,7 +242,7 @@ impl ResolveState {
             return ty::mk_int_var(self.infcx.tcx, vid);
         }
 
-        let node = self.infcx.get(&self.infcx.int_var_bindings, vid);
+        let node = self.infcx.get(vid);
         match node.possible_types {
           Some(IntType(t)) => ty::mk_mach_int(self.infcx.tcx, t),
           Some(UintType(t)) => ty::mk_mach_uint(self.infcx.tcx, t),
@@ -251,9 +250,8 @@ impl ResolveState {
             if self.should(force_ivar) {
                 // As a last resort, default to int.
                 let ty = ty::mk_int(self.infcx.tcx);
-                self.infcx.set(
-                    &self.infcx.int_var_bindings, vid,
-                    Root(Some(IntType(ast::ty_i)), node.rank));
+                self.infcx.set(vid,
+                               Root(Some(IntType(ast::ty_i)), node.rank));
                 ty
             } else {
                 ty::mk_int_var(self.infcx.tcx, vid)
@@ -267,17 +265,14 @@ impl ResolveState {
             return ty::mk_float_var(self.infcx.tcx, vid);
         }
 
-        let node = self.infcx.get(&self.infcx.float_var_bindings, vid);
+        let node = self.infcx.get(vid);
         match node.possible_types {
           Some(t) => ty::mk_mach_float(self.infcx.tcx, t),
           None => {
             if self.should(force_fvar) {
                 // As a last resort, default to float.
                 let ty = ty::mk_float(self.infcx.tcx);
-                self.infcx.set(
-                    &self.infcx.float_var_bindings,
-                    vid,
-                    Root(Some(ast::ty_f), node.rank));
+                self.infcx.set(vid, Root(Some(ast::ty_f), 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 aa6721fb2298..4252580ac46c 100644
--- a/src/librustc/middle/typeck/infer/sub.rs
+++ b/src/librustc/middle/typeck/infer/sub.rs
@@ -102,38 +102,31 @@ impl Sub: Combine {
         debug!("%s.tys(%s, %s)", self.tag(),
                a.inf_str(self.infcx), b.inf_str(self.infcx));
         if a == b { return Ok(a); }
-        do indent {
-            match (ty::get(a).sty, ty::get(b).sty) {
-                (ty::ty_bot, _) => {
-                    Ok(a)
-                }
+        let _indenter = indenter();
+        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))) => {
-                    do self.var_sub_var(&self.infcx.ty_var_bindings,
-                                        a_id, b_id).then {
-                        Ok(a)
-                    }
-                }
-                (ty::ty_infer(TyVar(a_id)), _) => {
-                    do self.var_sub_t(&self.infcx.ty_var_bindings,
-                                      a_id, b).then {
-                        Ok(a)
-                    }
-                }
-                (_, ty::ty_infer(TyVar(b_id))) => {
-                    do self.t_sub_var(&self.infcx.ty_var_bindings,
-                                      a, b_id).then {
-                        Ok(a)
-                    }
-                }
+            (ty::ty_infer(TyVar(a_id)), ty::ty_infer(TyVar(b_id))) => {
+                if_ok!(self.var_sub_var(a_id, b_id));
+                Ok(a)
+            }
+            (ty::ty_infer(TyVar(a_id)), _) => {
+                if_ok!(self.var_sub_t(a_id, b));
+                Ok(a)
+            }
+            (_, ty::ty_infer(TyVar(b_id))) => {
+                if_ok!(self.t_sub_var(a, b_id));
+                Ok(a)
+            }
 
-                (_, ty::ty_bot) => {
-                    Err(ty::terr_sorts(expected_found(&self, a, b)))
-                }
+            (_, ty::ty_bot) => {
+                Err(ty::terr_sorts(expected_found(&self, a, b)))
+            }
 
-                _ => {
-                    super_tys(&self, a, b)
-                }
+            _ => {
+                super_tys(&self, a, b)
             }
         }
     }
diff --git a/src/librustc/middle/typeck/infer/to_str.rs b/src/librustc/middle/typeck/infer/to_str.rs
index 42f516fe6d88..a6d316db4287 100644
--- a/src/librustc/middle/typeck/infer/to_str.rs
+++ b/src/librustc/middle/typeck/infer/to_str.rs
@@ -10,10 +10,10 @@
 
 use core::prelude::*;
 
-use middle::ty::{FnMeta, FnTyBase, FnSig, FnVid, Vid};
+use middle::ty::{FnMeta, FnTyBase, FnSig, Vid};
+use middle::ty::{IntVarValue, IntType, UintType};
 use middle::ty;
 use middle::typeck::infer::{Bound, Bounds};
-use middle::typeck::infer::{IntVarValue, IntType, UintType};
 use middle::typeck::infer::InferCtxt;
 use middle::typeck::infer::unify::{Redirect, Root, VarValue};
 use util::ppaux::{mt_to_str, ty_to_str};
@@ -25,23 +25,23 @@ use core::uint;
 use core::str;
 
 pub trait InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str;
+    fn inf_str(&self, cx: &InferCtxt) -> ~str;
 }
 
 impl ty::t : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
-        ty_to_str(cx.tcx, self)
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
+        ty_to_str(cx.tcx, *self)
     }
 }
 
 impl FnMeta : InferStr {
-    fn inf_str(_cx: @InferCtxt) -> ~str {
-        fmt!("%?", self)
+    fn inf_str(&self, _cx: &InferCtxt) -> ~str {
+        fmt!("%?", *self)
     }
 }
 
 impl FnSig : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
         fmt!("(%s) -> %s",
              str::connect(self.inputs.map(|a| a.ty.inf_str(cx)), ", "),
              self.output.inf_str(cx))
@@ -49,26 +49,26 @@ impl FnSig : InferStr {
 }
 
 impl<M:InferStr> FnTyBase<M> : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
         fmt!("%s%s", self.meta.inf_str(cx), self.sig.inf_str(cx))
     }
 }
 
 impl ty::mt : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
-        mt_to_str(cx.tcx, self)
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
+        mt_to_str(cx.tcx, *self)
     }
 }
 
 impl ty::Region : InferStr {
-    fn inf_str(_cx: @InferCtxt) -> ~str {
-        fmt!("%?", self)
+    fn inf_str(&self, _cx: &InferCtxt) -> ~str {
+        fmt!("%?", *self)
     }
 }
 
 impl<V:InferStr> Bound<V> : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
-        match self {
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
+        match *self {
           Some(ref v) => v.inf_str(cx),
           None => ~"none"
         }
@@ -76,7 +76,7 @@ impl<V:InferStr> Bound<V> : InferStr {
 }
 
 impl<T:InferStr> Bounds<T> : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
         fmt!("{%s <: %s}",
              self.lb.inf_str(cx),
              self.ub.inf_str(cx))
@@ -84,8 +84,8 @@ impl<T:InferStr> Bounds<T> : InferStr {
 }
 
 impl<V:Vid ToStr, T:InferStr> VarValue<V, T> : InferStr {
-    fn inf_str(cx: @InferCtxt) -> ~str {
-        match self {
+    fn inf_str(&self, cx: &InferCtxt) -> ~str {
+        match *self {
           Redirect(ref vid) => fmt!("Redirect(%s)", vid.to_str()),
           Root(ref pt, rk) => fmt!("Root(%s, %s)", pt.inf_str(cx),
                                uint::to_str(rk, 10u))
@@ -94,17 +94,13 @@ impl<V:Vid ToStr, T:InferStr> VarValue<V, T> : InferStr {
 }
 
 impl IntVarValue : InferStr {
-    fn inf_str(_cx: @InferCtxt) -> ~str {
-        match self {
-            IntType(t) => ast_util::int_ty_to_str(t),
-            UintType(t) => ast_util::uint_ty_to_str(t)
-        }
+    fn inf_str(&self, _cx: &InferCtxt) -> ~str {
+        self.to_str()
     }
 }
 
 impl ast::float_ty : InferStr {
-    fn inf_str(_cx: @InferCtxt) -> ~str {
-        ast_util::float_ty_to_str(self)
+    fn inf_str(&self, _cx: &InferCtxt) -> ~str {
+        self.to_str()
     }
 }
-
diff --git a/src/librustc/middle/typeck/infer/unify.rs b/src/librustc/middle/typeck/infer/unify.rs
index 77bd46eea2df..6c831427b031 100644
--- a/src/librustc/middle/typeck/infer/unify.rs
+++ b/src/librustc/middle/typeck/infer/unify.rs
@@ -9,24 +9,24 @@
 // except according to those terms.
 
 use core::prelude::*;
+use core::result;
+use std::smallintmap::SmallIntMap;
 
-use middle::ty::Vid;
+use middle::ty::{Vid, expected_found, IntVarValue};
 use middle::ty;
 use middle::typeck::infer::{Bound, Bounds, cres, uok, ures};
 use middle::typeck::infer::combine::Combine;
 use middle::typeck::infer::InferCtxt;
 use middle::typeck::infer::to_str::InferStr;
+use syntax::ast;
 use util::common::{indent, indenter};
 
-use core::result;
-use std::smallintmap::SmallIntMap;
-
 enum VarValue<V, T> {
     Redirect(V),
     Root(T, uint),
 }
 
-struct ValsAndBindings<V:Copy, T:Copy> {
+struct ValsAndBindings<V, T> {
     vals: SmallIntMap<VarValue<V, T>>,
     mut bindings: ~[(V, VarValue<V, T>)],
 }
@@ -37,11 +37,15 @@ struct Node<V:Copy, T:Copy> {
     rank: uint,
 }
 
-impl @InferCtxt {
-    fn get<V:Copy Eq Vid, T:Copy>(
-        vb: &ValsAndBindings<V, T>,
-        vid: V)
-        -> Node<V, T>
+trait UnifyVid<T> {
+    static fn appropriate_vals_and_bindings(infcx: &v/InferCtxt)
+        -> &v/ValsAndBindings<self, T>;
+}
+
+impl InferCtxt {
+    fn get<T:Copy, V:Copy Eq Vid UnifyVid<T>>(
+        &self,
+        +vid: V) -> Node<V, T>
     {
         /*!
          *
@@ -50,6 +54,7 @@ impl @InferCtxt {
          * http://en.wikipedia.org/wiki/Disjoint-set_data_structure
          */
 
+        let vb = UnifyVid::appropriate_vals_and_bindings(self);
         let vid_u = vid.to_uint();
         match vb.vals.find(vid_u) {
           None => {
@@ -57,9 +62,9 @@ impl @InferCtxt {
           }
           Some(ref var_val) => {
             match (*var_val) {
-              Redirect(ref vid) => {
-                let node = self.get(vb, (*vid));
-                if node.root.ne(vid) {
+              Redirect(vid) => {
+                let node: Node<V,T> = self.get(vid);
+                if node.root != vid {
                     // Path compression
                     vb.vals.insert(vid.to_uint(), Redirect(node.root));
                 }
@@ -73,9 +78,9 @@ impl @InferCtxt {
         }
     }
 
-    fn set<V:Copy Vid ToStr, T:Copy InferStr>(
-        vb: &ValsAndBindings<V, T>,
-        vid: V,
+    fn set<T:Copy InferStr, V:Copy Vid ToStr UnifyVid<T>>(
+        &self,
+        +vid: V,
         +new_v: VarValue<V, T>)
     {
         /*!
@@ -83,6 +88,7 @@ impl @InferCtxt {
          * Sets the value for `vid` to `new_v`.  `vid` MUST be a root node!
          */
 
+        let vb = UnifyVid::appropriate_vals_and_bindings(self);
         let old_v = vb.vals.get(vid.to_uint());
         vb.bindings.push((vid, old_v));
         vb.vals.insert(vid.to_uint(), new_v);
@@ -91,8 +97,8 @@ impl @InferCtxt {
                vid.to_str(), old_v.inf_str(self), new_v.inf_str(self));
     }
 
-    fn unify<V:Copy Vid ToStr, T:Copy InferStr, R>(
-        vb: &ValsAndBindings<V, T>,
+    fn unify<T:Copy InferStr, V:Copy Vid ToStr UnifyVid<T>, R>(
+        &self,
         node_a: &Node<V, T>,
         node_b: &Node<V, T>,
         op: &fn(new_root: V, new_rank: uint) -> R
@@ -108,17 +114,17 @@ impl @InferCtxt {
         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(vb, node_b.root, Redirect(node_a.root));
+            self.set(node_b.root, Redirect(node_a.root));
             op(node_a.root, node_a.rank)
         } else if node_a.rank < node_b.rank {
             // b has greater rank, so a should redirect to b.
-            self.set(vb, node_a.root, Redirect(node_b.root));
+            self.set(node_a.root, Redirect(node_b.root));
             op(node_b.root, node_b.rank)
         } else {
             // If equal, redirect one to the other and increment the
             // other's rank.
             assert node_a.rank == node_b.rank;
-            self.set(vb, node_b.root, Redirect(node_a.root));
+            self.set(node_b.root, Redirect(node_a.root));
             op(node_a.root, node_a.rank + 1)
         }
     }
@@ -129,12 +135,30 @@ impl @InferCtxt {
 // Code to handle simple variables like ints, floats---anything that
 // doesn't have a subtyping relationship we need to worry about.
 
-impl @InferCtxt {
-    fn simple_vars<V:Copy Eq Vid ToStr, T:Copy Eq InferStr>(
-        vb: &ValsAndBindings<V, Option<T>>,
-        err: ty::type_err,
-        a_id: V,
-        b_id: V) -> ures
+trait SimplyUnifiable {
+    static fn to_type_err(expected_found<self>) -> ty::type_err;
+}
+
+fn mk_err<T: SimplyUnifiable>(+a_is_expected: bool,
+                              +a_t: T,
+                              +b_t: T) -> ures
+{
+    if a_is_expected {
+        Err(SimplyUnifiable::to_type_err(
+            ty::expected_found {expected: a_t, found: b_t}))
+    } else {
+        Err(SimplyUnifiable::to_type_err(
+            ty::expected_found {expected: b_t, found: a_t}))
+    }
+}
+
+impl InferCtxt {
+    fn simple_vars<T:Copy Eq InferStr SimplyUnifiable,
+                   V:Copy Eq Vid ToStr UnifyVid<Option<T>>>(
+        &self,
+        +a_is_expected: bool,
+        +a_id: V,
+        +b_id: V) -> ures
     {
         /*!
          *
@@ -143,8 +167,8 @@ impl @InferCtxt {
          * have already been associated with a value, then those two
          * values must be the same. */
 
-        let node_a = self.get(vb, a_id);
-        let node_b = self.get(vb, b_id);
+        let node_a = self.get(a_id);
+        let node_b = self.get(b_id);
         let a_id = node_a.root;
         let b_id = node_b.root;
 
@@ -155,22 +179,24 @@ impl @InferCtxt {
             (&None, &None) => None,
             (&Some(ref v), &None) | (&None, &Some(ref v)) => Some(*v),
             (&Some(ref v1), &Some(ref v2)) => {
-                if *v1 != *v2 { return Err(err); }
+                if *v1 != *v2 {
+                    return mk_err(a_is_expected, *v1, *v2);
+                }
                 Some(*v1)
             }
         };
 
-        self.unify(vb, &node_a, &node_b, |new_root, new_rank| {
-            self.set(vb, new_root, Root(combined, new_rank));
+        self.unify(&node_a, &node_b, |new_root, new_rank| {
+            self.set(new_root, Root(combined, new_rank));
         });
         return uok();
     }
 
-    fn simple_var_t<V:Copy Eq Vid ToStr, T:Copy Eq InferStr>(
-        vb: &ValsAndBindings<V, Option<T>>,
-        err: ty::type_err,
-        a_id: V,
-        b: T) -> ures
+    fn simple_var_t<T:Copy Eq InferStr SimplyUnifiable,
+                    V:Copy Eq Vid ToStr UnifyVid<Option<T>>>(
+        +a_is_expected: bool,
+        +a_id: V,
+        +b: T) -> ures
     {
         /*!
          *
@@ -179,19 +205,66 @@ impl @InferCtxt {
          * if `a_id` already has a value, it must be the same as
          * `b`. */
 
-        let node_a = self.get(vb, a_id);
+        let node_a = self.get(a_id);
         let a_id = node_a.root;
 
-        if node_a.possible_types.is_none() {
-            self.set(vb, a_id, Root(Some(b), node_a.rank));
-            return uok();
-        }
+        match node_a.possible_types {
+            None => {
+                self.set(a_id, Root(Some(b), node_a.rank));
+                return uok();
+            }
 
-        if node_a.possible_types == Some(b) {
-            return uok();
+            Some(ref a_t) => {
+                if *a_t == b {
+                    return uok();
+                } else {
+                    return mk_err(a_is_expected, *a_t, b);
+                }
+            }
         }
-
-        return Err(err);
     }
 }
 
+// ______________________________________________________________________
+
+impl ty::TyVid : UnifyVid<Bounds<ty::t>> {
+    static fn appropriate_vals_and_bindings(infcx: &v/InferCtxt)
+        -> &v/ValsAndBindings<ty::TyVid, Bounds<ty::t>>
+    {
+        return &infcx.ty_var_bindings;
+    }
+}
+
+impl ty::IntVid : UnifyVid<Option<IntVarValue>> {
+    static fn appropriate_vals_and_bindings(infcx: &v/InferCtxt)
+        -> &v/ValsAndBindings<ty::IntVid, Option<IntVarValue>>
+    {
+        return &infcx.int_var_bindings;
+    }
+}
+
+impl IntVarValue : SimplyUnifiable {
+    static fn to_type_err(err: expected_found<IntVarValue>)
+        -> ty::type_err
+    {
+        return ty::terr_int_mismatch(err);
+    }
+}
+
+impl ty::FloatVid : UnifyVid<Option<ast::float_ty>> {
+    static fn appropriate_vals_and_bindings(infcx: &v/InferCtxt)
+        -> &v/ValsAndBindings<ty::FloatVid, Option<ast::float_ty>>
+    {
+        return &infcx.float_var_bindings;
+    }
+}
+
+impl ast::float_ty : SimplyUnifiable {
+    static fn to_type_err(err: expected_found<ast::float_ty>)
+        -> ty::type_err
+    {
+        return ty::terr_float_mismatch(err);
+    }
+}
+
+