diff --git a/src/rustc/metadata/tydecode.rs b/src/rustc/metadata/tydecode.rs
index 920a4d71a46..b527b5d1f43 100644
--- a/src/rustc/metadata/tydecode.rs
+++ b/src/rustc/metadata/tydecode.rs
@@ -265,7 +265,9 @@ fn parse_ty(st: @pstate, conv: conv_did) -> ty::t {
         st.pos = st.pos + 1u;
         ret ty::mk_res(st.tcx, def, inner, params);
       }
-      'X' { ret ty::mk_var(st.tcx, parse_int(st)); }
+      'X' {
+        ret ty::mk_var(st.tcx, ty::ty_vid(parse_int(st) as uint));
+      }
       'Y' { ret ty::mk_type(st.tcx); }
       'C' {
         let ck = alt check next(st) {
diff --git a/src/rustc/metadata/tyencode.rs b/src/rustc/metadata/tyencode.rs
index 6e1e8b15f56..c5f23f37b86 100644
--- a/src/rustc/metadata/tyencode.rs
+++ b/src/rustc/metadata/tyencode.rs
@@ -5,6 +5,7 @@ import std::map::hashmap;
 import syntax::ast::*;
 import driver::session::session;
 import middle::ty;
+import middle::ty::vid;
 import syntax::print::pprust::*;
 import middle::trans::reachable;
 
@@ -99,23 +100,46 @@ fn enc_mt(w: io::writer, cx: @ctxt, mt: ty::mt) {
     }
     enc_ty(w, cx, mt.ty);
 }
+fn enc_bound_region(w: io::writer, br: ty::bound_region) {
+    alt br {
+      ty::br_self { w.write_char('s') }
+      ty::br_anon { w.write_char('a') }
+      ty::br_param(id, s) {
+        w.write_char('[');
+        w.write_uint(id);
+        w.write_char('|');
+        w.write_str(s);
+        w.write_char(']')
+      }
+    }
+}
 fn enc_region(w: io::writer, r: ty::region) {
     alt r {
-        ty::re_block(nid) {
-            w.write_char('b'); w.write_int(nid); w.write_char('|');
-        }
-        ty::re_self {
-            w.write_char('s');
-        }
-        ty::re_inferred {
-            w.write_char('i');
-        }
-        ty::re_param(id) {
-            w.write_char('p'); w.write_uint(id); w.write_char('|');
-        }
-        ty::re_var(id) {
-            w.write_char('v'); w.write_uint(id); w.write_char('|');
-        }
+      ty::re_bound(br) {
+        w.write_char('b');
+        enc_bound_region(w, br);
+      }
+      ty::re_free(id, br) {
+        w.write_char('f');
+        w.write_char('[');
+        w.write_int(id);
+        w.write_char('|');
+        enc_bound_region(w, br);
+        w.write_char(']');
+      }
+      ty::re_scope(nid) {
+        w.write_char('s');
+        w.write_int(nid);
+        w.write_char('|');
+      }
+      ty::re_default {
+        w.write_char('i');
+      }
+      ty::re_var(id) {
+        w.write_char('v');
+        w.write_uint(id.to_uint());
+        w.write_char('|');
+      }
     }
 }
 fn enc_sty(w: io::writer, cx: @ctxt, st: ty::sty) {
@@ -199,7 +223,10 @@ fn enc_sty(w: io::writer, cx: @ctxt, st: ty::sty) {
         for t: ty::t in tps { enc_ty(w, cx, t); }
         w.write_char(']');
       }
-      ty::ty_var(id) { w.write_char('X'); w.write_str(int::str(id)); }
+      ty::ty_var(id) {
+        w.write_char('X');
+        w.write_uint(id.to_uint());
+      }
       ty::ty_param(id, did) {
         w.write_char('p');
         w.write_str(cx.ds(did));
diff --git a/src/rustc/middle/infer.rs b/src/rustc/middle/infer.rs
index 157141235b3..035da0d477b 100644
--- a/src/rustc/middle/infer.rs
+++ b/src/rustc/middle/infer.rs
@@ -2,11 +2,13 @@ import std::smallintmap;
 import std::smallintmap::smallintmap;
 import std::smallintmap::map;
 import middle::ty;
+import middle::ty::{ty_vid, region_vid, vid};
 import syntax::ast;
 import syntax::ast::{ret_style};
 import util::ppaux::{ty_to_str, mt_to_str};
 import result::{result, extensions, ok, err, map, map2, iter2};
 import ty::type_is_bot;
+import driver::session::session;
 
 export infer_ctxt;
 export new_infer_ctxt;
@@ -16,29 +18,46 @@ export resolve_type_structure;
 export fixup_vars;
 export resolve_var;
 export compare_tys;
+export fixup_err, fixup_err_to_str;
 
 type bound<T:copy> = option<T>;
 
 type bounds<T:copy> = {lb: bound<T>, ub: bound<T>};
 
-enum var_value<T:copy> {
-    redirect(uint),
+enum var_value<V:copy, T:copy> {
+    redirect(V),
     bounded(bounds<T>)
 }
 
-type vals_and_bindings<T:copy> = {
-    vals: smallintmap<var_value<T>>,
-    mut bindings: [(uint, var_value<T>)]
+type vals_and_bindings<V:copy, T:copy> = {
+    vals: smallintmap<var_value<V, T>>,
+    mut bindings: [(V, var_value<V, T>)]
 };
 
 enum infer_ctxt = @{
     tcx: ty::ctxt,
-    vb: vals_and_bindings<ty::t>,
-    rb: vals_and_bindings<ty::region>,
+    vb: vals_and_bindings<ty::ty_vid, ty::t>,
+    rb: vals_and_bindings<ty::region_vid, ty::region>,
 };
 
+enum fixup_err {
+    unresolved_ty(ty_vid),
+    cyclic_ty(ty_vid),
+    unresolved_region(region_vid),
+    cyclic_region(region_vid)
+}
+
+fn fixup_err_to_str(f: fixup_err) -> str {
+    alt f {
+      unresolved_ty(_) { "unconstrained type" }
+      cyclic_ty(_) { "cyclic type of infinite size" }
+      unresolved_region(_) { "unconstrained region" }
+      cyclic_region(_) { "cyclic region" }
+    }
+}
+
 type ures = result::result<(), ty::type_err>;
-type fres<T> = result::result<T,int>;
+type fres<T> = result::result<T, fixup_err>;
 
 fn new_infer_ctxt(tcx: ty::ctxt) -> infer_ctxt {
     infer_ctxt(@{tcx: tcx,
@@ -74,12 +93,12 @@ fn resolve_type_structure(cx: infer_ctxt, a: ty::t) -> fres<ty::t> {
     cx.resolve_ty(a)
 }
 
-fn resolve_var(cx: infer_ctxt, vid: int) -> fres<ty::t> {
-    cx.fixup_vars(ty::mk_var(cx.tcx, vid))
+fn resolve_var(cx: infer_ctxt, vid: ty_vid) -> fres<ty::t> {
+    cx.fixup_ty(ty::mk_var(cx.tcx, vid))
 }
 
 fn fixup_vars(cx: infer_ctxt, a: ty::t) -> fres<ty::t> {
-    cx.fixup_vars(a)
+    cx.fixup_ty(a)
 }
 
 impl methods for ures {
@@ -120,7 +139,7 @@ impl<V:copy to_str> of to_str for bound<V> {
     }
 }
 
-impl<V:copy to_str> of to_str for bounds<V> {
+impl<T:copy to_str> of to_str for bounds<T> {
     fn to_str(cx: infer_ctxt) -> str {
         #fmt["{%s <: %s}",
              self.lb.to_str(cx),
@@ -128,15 +147,49 @@ impl<V:copy to_str> of to_str for bounds<V> {
     }
 }
 
-impl<V:copy to_str> of to_str for var_value<V> {
+impl<V:copy vid, T:copy to_str> of to_str for var_value<V,T> {
     fn to_str(cx: infer_ctxt) -> str {
         alt self {
-          redirect(id) { #fmt("redirect(%u)", id) }
+          redirect(vid) { #fmt("redirect(%s)", vid.to_str()) }
           bounded(bnds) { #fmt("bounded(%s)", bnds.to_str(cx)) }
         }
     }
 }
 
+iface st {
+    fn st(infcx: infer_ctxt, b: self) -> ures;
+    fn lub(infcx: infer_ctxt, b: self) -> cres<self>;
+    fn glb(infcx: infer_ctxt, b: self) -> cres<self>;
+}
+
+impl of st for ty::t {
+    fn st(infcx: infer_ctxt, b: ty::t) -> ures {
+        infcx.tys(self, b)
+    }
+
+    fn lub(infcx: infer_ctxt, b: ty::t) -> cres<ty::t> {
+        lub(infcx).c_tys(self, b)
+    }
+
+    fn glb(infcx: infer_ctxt, b: ty::t) -> cres<ty::t> {
+        glb(infcx).c_tys(self, b)
+    }
+}
+
+impl of st for ty::region {
+    fn st(infcx: infer_ctxt, b: ty::region) -> ures {
+        infcx.regions(self, b)
+    }
+
+    fn lub(infcx: infer_ctxt, b: ty::region) -> cres<ty::region> {
+        lub(infcx).c_regions(self, b)
+    }
+
+    fn glb(infcx: infer_ctxt, b: ty::region) -> cres<ty::region> {
+        glb(infcx).c_regions(self, b)
+    }
+}
+
 // Most of these methods, like tys() and so forth, take two parameters
 // a and b and they are tasked with "ensuring that a is a subtype of
 // b".  They return success or failure.  They make changes in-place to
@@ -157,31 +210,20 @@ impl unify_methods for infer_ctxt {
         err(e)
     }
 
-    fn set<T:copy to_str>(
-        vb: vals_and_bindings<T>, vid: uint,
-        +new_v: var_value<T>) {
+    fn set<V:copy vid, T:copy to_str>(
+        vb: vals_and_bindings<V, T>, vid: V,
+        +new_v: var_value<V, T>) {
 
-        let old_v = vb.vals.get(vid);
+        let old_v = vb.vals.get(vid.to_uint());
         vec::push(vb.bindings, (vid, old_v));
-        vb.vals.insert(vid, new_v);
+        vb.vals.insert(vid.to_uint(), new_v);
 
-        #debug["Updating variable <%u> from %s to %s",
-               vid, old_v.to_str(self), new_v.to_str(self)];
+        #debug["Updating variable %s from %s to %s",
+               vid.to_str(), old_v.to_str(self), new_v.to_str(self)];
     }
 
-    fn set_ty(vid: uint, +new_v: var_value<ty::t>) {
-        let old_v = self.vb.vals.get(vid);
+    fn set_ty(vid: ty_vid, +new_v: var_value<ty_vid, ty::t>) {
         self.set(self.vb, vid, new_v);
-
-        #debug["Updating variable <T%u> from %s to %s",
-               vid, old_v.to_str(self), new_v.to_str(self)];
-    }
-
-    fn rollback_to<T:copy>(vb: vals_and_bindings<T>, len: uint) {
-        while vb.bindings.len() != len {
-            let (vid, old_v) = vec::pop(vb.bindings);
-            vb.vals.insert(vid, old_v);
-        }
     }
 
     fn commit<T:copy,E:copy>(f: fn() -> result<T,E>) -> result<T,E> {
@@ -203,10 +245,12 @@ impl unify_methods for infer_ctxt {
 
     fn try<T:copy,E:copy>(f: fn() -> result<T,E>) -> result<T,E> {
 
-        fn rollback_to<T:copy>(vb: vals_and_bindings<T>, len: uint) {
+        fn rollback_to<V:copy vid, T:copy>(
+            vb: vals_and_bindings<V, T>, len: uint) {
+
             while vb.bindings.len() != len {
                 let (vid, old_v) = vec::pop(vb.bindings);
-                vb.vals.insert(vid, old_v);
+                vb.vals.insert(vid.to_uint(), old_v);
             }
         }
 
@@ -225,19 +269,20 @@ impl unify_methods for infer_ctxt {
         ret r;
     }
 
-    fn get<T:copy>(vb: vals_and_bindings<T>, vid: uint)
-        -> {root: uint, bounds:bounds<T>} {
+    fn get<V:copy vid, T:copy>(
+        vb: vals_and_bindings<V, T>, vid: V)
+        -> {root: V, bounds:bounds<T>} {
 
-        alt vb.vals.find(vid) {
+        alt vb.vals.find(vid.to_uint()) {
           none {
             let bnds = {lb: none, ub: none};
-            vb.vals.insert(vid, bounded(bnds));
+            vb.vals.insert(vid.to_uint(), bounded(bnds));
             {root: vid, bounds: bnds}
           }
           some(redirect(vid)) {
             let {root, bounds} = self.get(vb, vid);
             if root != vid {
-                vb.vals.insert(vid, redirect(root));
+                vb.vals.insert(vid.to_uint(), redirect(root));
             }
             {root: root, bounds: bounds}
           }
@@ -247,11 +292,15 @@ impl unify_methods for infer_ctxt {
         }
     }
 
-    fn get_var(vid: uint) -> {root: uint, bounds:bounds<ty::t>} {
+    fn get_var(vid: ty_vid)
+        -> {root: ty_vid, bounds:bounds<ty::t>} {
+
         ret self.get(self.vb, vid);
     }
 
-    fn get_region(rid: uint) -> {root: uint, bounds:bounds<ty::region>} {
+    fn get_region(rid: region_vid)
+        -> {root: region_vid, bounds:bounds<ty::region>} {
+
         ret self.get(self.rb, rid);
     }
 
@@ -304,8 +353,9 @@ impl unify_methods for infer_ctxt {
     //    a.lb <: c.lb
     //    b.lb <: c.lb
     // If this cannot be achieved, the result is failure.
-    fn set_ty_var_to_merged_bounds(
-        v_id: uint, a: bounds<ty::t>, b: bounds<ty::t>) -> ures {
+    fn set_var_to_merged_bounds<V:copy vid, T:copy to_str st>(
+        vb: vals_and_bindings<V, T>,
+        v_id: V, a: bounds<T>, b: bounds<T>) -> ures {
 
         // Think of the two diamonds, we want to find the
         // intersection.  There are basically four possibilities (you
@@ -322,8 +372,8 @@ impl unify_methods for infer_ctxt {
         //       A     \ / A
         //              B
 
-        #debug["merge(<T%u>,%s,%s)",
-               v_id,
+        #debug["merge(%s,%s,%s)",
+               v_id.to_str(),
                a.to_str(self),
                b.to_str(self)];
 
@@ -335,33 +385,33 @@ impl unify_methods for infer_ctxt {
         // when necessary.
         self.bnds(a.lb, b.ub).then {||
         self.bnds(b.lb, a.ub).then {||
-        self.merge_bnds(
-            a, b,
-            {|a_ty, b_ty| lub(self).c_tys(a_ty, b_ty) },
-            {|a_ty, b_ty| glb(self).c_tys(a_ty, b_ty) }).chain {|bnds|
-
-            #debug["merge(<T%u>): bnds=%s",
-                   v_id,
+        self.merge_bnd(a.ub, b.ub, {|x, y| x.glb(self, y)}).chain {|ub|
+        self.merge_bnd(a.lb, b.lb, {|x, y| x.lub(self, y)}).chain {|lb|
+            let bnds = {lb: lb, ub: ub};
+            #debug["merge(%s): bnds=%s",
+                   v_id.to_str(),
                    bnds.to_str(self)];
 
             // the new bounds must themselves
             // be relatable:
             self.bnds(bnds.lb, bnds.ub).then {||
-            self.set_ty(v_id, bounded(bnds));
+            self.set(vb, v_id, bounded(bnds));
             self.uok()
             }
-        }}}
+        }}}}
     }
 
-    // TODO: Generalize to regions.
-    fn vars(a_id: uint, b_id: uint) -> ures {
-        // Need to make sub_id a subtype of sup_id.
-        let {root: a_id, bounds: a_bounds} = self.get(self.vb, a_id);
-        let {root: b_id, bounds: b_bounds} = self.get(self.vb, b_id);
+    fn vars<V:copy vid, T:copy to_str st>(
+        vb: vals_and_bindings<V, T>,
+        a_id: V, b_id: V) -> ures {
 
-        #debug["vars(<T%u>=%s <: <T%u>=%s)",
-               a_id, a_bounds.to_str(self),
-               b_id, b_bounds.to_str(self)];
+        // Need to make sub_id a subtype of sup_id.
+        let {root: a_id, bounds: a_bounds} = self.get(vb, a_id);
+        let {root: b_id, bounds: b_bounds} = self.get(vb, b_id);
+
+        #debug["vars(%s=%s <: %s=%s)",
+               a_id.to_str(), a_bounds.to_str(self),
+               b_id.to_str(), b_bounds.to_str(self)];
 
         if a_id == b_id { ret self.uok(); }
 
@@ -369,7 +419,7 @@ impl unify_methods for infer_ctxt {
         // see if we can make those types subtypes.
         alt (a_bounds.ub, b_bounds.lb) {
           (some(a_ub), some(b_lb)) {
-            let r = self.try {|| self.tys(a_ub, b_lb) };
+            let r = self.try {|| a_ub.st(self, b_lb) };
             alt r {
               ok(()) { ret result::ok(()); }
               err(_) { /*fallthrough */ }
@@ -380,38 +430,81 @@ impl unify_methods for infer_ctxt {
 
         // For max perf, we should consider the rank here.  But for now,
         // we always make b redirect to a.
-        self.set_ty(b_id, redirect(a_id));
+        self.set(vb, b_id, redirect(a_id));
 
         // 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.
-        self.set_ty_var_to_merged_bounds(a_id, a_bounds, b_bounds).then {||
+        self.set_var_to_merged_bounds(vb, a_id, a_bounds, b_bounds).then {||
             self.uok()
         }
     }
 
-    fn varty(a_id: uint, b: ty::t) -> ures {
-        let {root: a_id, bounds: a_bounds} = self.get(self.vb, a_id);
-        #debug["varty(<T%u>=%s <: %s)",
-               a_id, a_bounds.to_str(self),
+    fn vart<V: copy vid, T: copy to_str st>(
+        vb: vals_and_bindings<V, T>,
+        a_id: V, b: T) -> ures {
+
+        let {root: a_id, bounds: a_bounds} = self.get(vb, a_id);
+        #debug["vart(%s=%s <: %s)",
+               a_id.to_str(), a_bounds.to_str(self),
                b.to_str(self)];
         let b_bounds = {lb: none, ub: some(b)};
-        self.set_ty_var_to_merged_bounds(a_id, a_bounds, b_bounds)
+        self.set_var_to_merged_bounds(vb, a_id, a_bounds, b_bounds)
     }
 
-    fn tyvar(a: ty::t, b_id: uint) -> ures {
+    fn tvar<V: copy vid, T: copy to_str st>(
+        vb: vals_and_bindings<V, T>,
+        a: T, b_id: V) -> ures {
+
         let a_bounds = {lb: some(a), ub: none};
-        let {root: b_id, bounds: b_bounds} = self.get(self.vb, b_id);
-        #debug["tyvar(%s <: <T%u>=%s)",
+        let {root: b_id, bounds: b_bounds} = self.get(vb, b_id);
+        #debug["tvar(%s <: %s=%s)",
                a.to_str(self),
-               b_id, b_bounds.to_str(self)];
-        self.set_ty_var_to_merged_bounds(b_id, a_bounds, b_bounds)
+               b_id.to_str(), b_bounds.to_str(self)];
+        self.set_var_to_merged_bounds(vb, b_id, a_bounds, b_bounds)
     }
 
     fn regions(a: ty::region, b: ty::region) -> ures {
-        alt combine_or_unify_regions(self.tcx, a, b, false) {
-            ok(_)   { self.uok()   }
-            err(e)  { self.uerr(e) }
+        alt (a, b) { // XXX
+          (ty::re_var(a_id), ty::re_var(b_id)) {
+            self.vars(self.rb, a_id, b_id)
+          }
+          (ty::re_var(a_id), _) {
+            self.vart(self.rb, a_id, b)
+          }
+          (_, ty::re_var(b_id)) {
+            self.tvar(self.rb, a, b_id)
+          }
+
+          (ty::re_free(a_id, _), ty::re_scope(b_id)) |
+          (ty::re_scope(a_id), ty::re_free(b_id, _)) |
+          (ty::re_scope(a_id), ty::re_scope(b_id)) {
+            let rm = self.tcx.region_map;
+            alt region::nearest_common_ancestor(rm, a_id, b_id) {
+              some(r_id) if r_id == a_id { self.uok() }
+              _ { err(ty::terr_regions_differ(false, b, a)) }
+            }
+          }
+
+          // For these types, we cannot define any additional relationship:
+          (ty::re_free(_, _), ty::re_free(_, _)) |
+          (ty::re_bound(_), ty::re_bound(_)) |
+          (ty::re_bound(_), ty::re_free(_, _)) |
+          (ty::re_bound(_), ty::re_scope(_)) |
+          (ty::re_free(_, _), ty::re_bound(_)) |
+          (ty::re_scope(_), ty::re_bound(_)) {
+            if a == b {
+                self.uok()
+            } else {
+                err(ty::terr_regions_differ(false, b, a))
+            }
+          }
+
+          (ty::re_default, _) |
+          (_, ty::re_default) {
+            // actually a compiler bug, I think.
+            err(ty::terr_regions_differ(false, b, a))
+          }
         }
     }
 
@@ -557,11 +650,10 @@ impl unify_methods for infer_ctxt {
         ret self.uok();
     }
 
-    // TODO: Generalize this.
-    fn bnds(a: bound<ty::t>, b: bound<ty::t>) -> ures {
-        #debug("bnds(%s <: %s)",
-               a.to_str(self),
-               b.to_str(self));
+    fn bnds<T:copy to_str st>(
+        a: bound<T>, b: bound<T>) -> ures {
+
+        #debug("bnds(%s <: %s)", a.to_str(self), b.to_str(self));
 
         alt (a, b) {
           (none, none) |
@@ -570,7 +662,7 @@ impl unify_methods for infer_ctxt {
             self.uok()
           }
           (some(t_a), some(t_b)) {
-            self.tys(t_a, t_b)
+            t_a.st(self, t_b)
           }
         }
     }
@@ -605,13 +697,13 @@ impl unify_methods for infer_ctxt {
           (ty::ty_bot, _) { self.uok() }
 
           (ty::ty_var(a_id), ty::ty_var(b_id)) {
-            self.vars(a_id as uint, b_id as uint)
+            self.vars(self.vb, a_id, b_id)
           }
           (ty::ty_var(a_id), _) {
-            self.varty(a_id as uint, b)
+            self.vart(self.vb, a_id, b)
           }
           (_, ty::ty_var(b_id)) {
-            self.tyvar(a, b_id as uint)
+            self.tvar(self.vb, a, b_id)
           }
 
           (ty::ty_nil, _) |
@@ -700,19 +792,19 @@ impl resolve_methods for infer_ctxt {
         ok(t)
     }
 
-    fn rerr<T>(v: int) -> fres<T> {
+    fn rerr<T>(v: fixup_err) -> fres<T> {
         #debug["Resolve error: %?", v];
         err(v)
     }
 
-    fn resolve_var<T:copy to_str>(
-        vb: vals_and_bindings<T>, bot_guard: fn(T)->bool,
-        vid: int, unbound: fn() -> fres<T>) -> fres<T> {
+    fn resolve_var<V: copy vid, T:copy to_str>(
+        vb: vals_and_bindings<V, T>, bot_guard: fn(T)->bool,
+        vid: V, unbound: fn() -> fres<T>) -> fres<T> {
 
-        let {root:_, bounds} = self.get(vb, vid as uint);
+        let {root:_, bounds} = self.get(vb, vid);
 
-        #debug["resolve_var(%d) bounds=%s",
-               vid, bounds.to_str(self)];
+        #debug["resolve_var(%s) bounds=%s",
+               vid.to_str(), bounds.to_str(self)];
 
         // Nonobvious: prefer the most specific type
         // (i.e., the lower bound) to the more general
@@ -728,7 +820,7 @@ impl resolve_methods for infer_ctxt {
         }
     }
 
-    fn resolve_ty_var(vid: int) -> fres<ty::t> {
+    fn resolve_ty_var(vid: ty_vid) -> fres<ty::t> {
         ret self.resolve_var(
             self.vb,
             {|t| type_is_bot(t) },
@@ -736,19 +828,19 @@ impl resolve_methods for infer_ctxt {
             {|| ok(ty::mk_bot(self.tcx)) });
     }
 
-    fn resolve_region_var(rid: int) -> fres<ty::region> {
+    fn resolve_region_var(rid: region_vid) -> fres<ty::region> {
         ret self.resolve_var(
             self.rb,
             {|_t| false },
             rid,
-            {|| err(rid) });
+            {|| err(unresolved_region(rid)) });
     }
 
     fn resolve_ty(typ: ty::t) -> fres<ty::t> {
         alt ty::get(typ).struct {
           ty::ty_var(vid) { self.resolve_ty_var(vid) }
           ty::ty_rptr(ty::re_var(rid), base_ty) {
-            alt self.resolve_region_var(rid as int) {
+            alt self.resolve_region_var(rid) {
               err(terr)  { err(terr) }
               ok(region) {
                 self.rok(ty::mk_rptr(self.tcx, region, base_ty))
@@ -759,95 +851,76 @@ impl resolve_methods for infer_ctxt {
         }
     }
 
-    fn subst_vars(unresolved: @mut option<int>,
-                  vars_seen: std::list::list<int>,
-                  vid: int) -> ty::t {
-        // Should really return a fixup_result instead of a t, but fold_ty
-        // doesn't allow returning anything but a t.
-        alt self.resolve_ty_var(vid) {
-          err(vid) {
-            *unresolved = some(vid);
-            ret ty::mk_var(self.tcx, vid);
+    fn fixup_region(r: ty::region,
+                    &r_seen: [region_vid],
+                    err: @mut option<fixup_err>) -> ty::region {
+        alt r {
+          ty::re_var(rid) if vec::contains(r_seen, rid) {
+            *err = some(cyclic_region(rid)); r
           }
-          ok(rt) {
-            let mut give_up = false;
-            std::list::iter(vars_seen) {|v|
-                if v == vid {
-                    *unresolved = some(-1); // hack: communicate inf ty
-                    give_up = true;
-                }
-            }
 
-            // Return the type unchanged, so we can error out
-            // downstream
-            if give_up { ret rt; }
-            ret ty::fold_ty(self.tcx,
-                            ty::fm_var(
-                                self.subst_vars(
-                                    unresolved,
-                                    std::list::cons(vid, @vars_seen),
-                                    _)),
-                            rt);
-          }
-        }
-    }
-
-    fn fixup_vars(typ: ty::t) -> fres<ty::t> {
-        let unresolved = @mut none::<int>;
-        let rty =
-            ty::fold_ty(self.tcx,
-                        ty::fm_var(
-                            self.subst_vars(
-                                unresolved,
-                                std::list::nil,
-                                _)),
-                        typ);
-
-        let ur = *unresolved;
-        alt ur {
-          none { ret self.rok(rty); }
-          some(var_id) { ret self.rerr(var_id); }
-        }
-    }
-
-    fn subst_regions(unresolved: @mut option<int>,
-                     regions_seen: std::list::list<int>,
-                     rid: int) -> ty::region {
-        // Should really return a fixup_result instead of a t, but fold_ty
-        // doesn't allow returning anything but a t.
-        alt self.resolve_region_var(rid) {
-          err(rid) {
-            *unresolved = some(rid);
-            ret ty::re_var(rid as uint);
-          }
-          ok(rr) {
-            let mut give_up = false;
-            std::list::iter(regions_seen) {|r|
-                if r == rid {
-                    *unresolved = some(-1); // hack: communicate inf region
-                    give_up = true;
-                }
-            }
-            ret rr;
-          }
-        }
-    }
-
-    fn fixup_regions(typ: ty::t) -> fres<ty::t> {
-        let unresolved = @mut none::<int>;
-        let rty = ty::fold_ty(self.tcx, ty::fm_rptr({ |region, _under_rptr|
-            alt region {
-              ty::re_var(rid) {
-                self.subst_regions(unresolved, std::list::nil, rid as int)
+          ty::re_var(rid) {
+            alt self.resolve_region_var(rid) {
+              result::ok(r1) {
+                vec::push(r_seen, rid);
+                let r2 = self.fixup_region(r1, r_seen, err);
+                vec::pop(r_seen);
+                ret r2;
               }
-              _ { region }
+              result::err(e) { *err = some(e); r }
             }
-        }, false), typ);
+          }
 
-        let ur = *unresolved;
-        alt ur {
+          _ { r }
+        }
+    }
+
+    fn fixup_ty1(ty: ty::t,
+                 &ty_seen: [ty_vid],
+                 &r_seen: [region_vid],
+                 err: @mut option<fixup_err>) -> ty::t {
+        let tb = ty::get(ty);
+        if !tb.has_vars { ret ty; }
+        alt tb.struct {
+          ty::ty_var(vid) if vec::contains(ty_seen, vid) {
+            *err = some(cyclic_ty(vid)); ty
+          }
+
+          ty::ty_var(vid) {
+            alt self.resolve_ty_var(vid) {
+              result::err(e) { *err = some(e); ty }
+              result::ok(ty1) {
+                vec::push(ty_seen, vid);
+                let ty2 = self.fixup_ty1(ty1, ty_seen, r_seen, err);
+                vec::pop(ty_seen);
+                ret ty2;
+              }
+            }
+          }
+
+          ty::ty_rptr(r, {ty: base_ty, mutbl: m}) {
+            let base_ty1 = self.fixup_ty1(base_ty, ty_seen, r_seen, err);
+            let r1 = self.fixup_region(r, r_seen, err);
+            ret ty::mk_rptr(self.tcx, r1, {ty: base_ty1, mutbl: m});
+          }
+
+          sty {
+            ty::fold_sty_to_ty(self.tcx, sty) {|t|
+                self.fixup_ty1(t, ty_seen, r_seen, err)
+            }
+          }
+        }
+    }
+
+    fn fixup_ty(typ: ty::t) -> fres<ty::t> {
+        #debug["fixup_ty(%s)", ty_to_str(self.tcx, typ)];
+        let mut ty_seen = [];
+        let mut r_seen = [];
+        let unresolved = @mut none;
+        let rty = self.fixup_ty1(typ, ty_seen, r_seen, unresolved);
+        alt *unresolved {
           none { ret self.rok(rty); }
-          some(var_id) { ret self.rerr(var_id); }
+          some(e) { ret self.rerr(e); }
         }
     }
 }
@@ -868,6 +941,10 @@ impl resolve_methods for infer_ctxt {
 // instance as the first parameter.  This would be better implemented
 // using traits.
 //
+// The `c_X()` top-level items work for *both LUB and GLB*: any
+// operation which varies between LUB and GLB will be dynamically
+// dispatched using a `self.c_Y()` operation.
+//
 // In principle, the subtyping relation computed above could be built
 // on the combine framework---this would result in less code but would
 // be less efficient.  There is a significant performance gain from
@@ -884,42 +961,55 @@ iface combine {
     fn bnd<V:copy>(b: bounds<V>) -> option<V>;
     fn with_bnd<V:copy>(b: bounds<V>, v: V) -> bounds<V>;
     fn c_bot(b: ty::t) -> cres<ty::t>;
-    fn c_regions(a: ty::region, b: ty::region) -> cres<ty::region>;
     fn c_mts(a: ty::mt, b: ty::mt) -> cres<ty::mt>;
     fn c_contratys(t1: ty::t, t2: ty::t) -> cres<ty::t>;
     fn c_tys(t1: ty::t, t2: ty::t) -> cres<ty::t>;
     fn c_protos(p1: ast::proto, p2: ast::proto) -> cres<ast::proto>;
     fn c_ret_styles(r1: ret_style, r2: ret_style) -> cres<ret_style>;
+
+    // Combining regions (along with some specific cases that are
+    // different for LUB/GLB):
+    fn c_regions(
+        a: ty::region, b: ty::region) -> cres<ty::region>;
+    fn c_regions_scope_scope(
+        a: ty::region, a_id: ast::node_id,
+        b: ty::region, b_id: ast::node_id) -> cres<ty::region>;
+    fn c_regions_free_scope(
+        a: ty::region, a_id: ast::node_id, a_br: ty::bound_region,
+        b: ty::region, b_id: ast::node_id) -> cres<ty::region>;
 }
 
 enum lub = infer_ctxt;
 enum glb = infer_ctxt;
 
-fn c_ty_vars<C:combine>(self: C, a_id: uint, b_id: uint) -> cres<ty::t> {
+fn c_vars<V:copy vid, C:combine, T:copy to_str st>(
+    self: C, vb: vals_and_bindings<V, T>,
+    a_t: T, a_vid: V, b_vid: V,
+    c_ts: fn(T, T) -> cres<T>) -> cres<T> {
+
+    // The comments in this function are written for LUB and types,
+    // but they apply equally well to GLB and regions if you inverse
+    // upper/lower/sub/super/etc.
+
     // Need to find a type that is a supertype of both a and b:
-    let {root: a_id, bounds: a_bounds} = self.infcx().get_var(a_id);
-    let {root: b_id, bounds: b_bounds} = self.infcx().get_var(b_id);
+    let {root: a_vid, bounds: a_bounds} = self.infcx().get(vb, a_vid);
+    let {root: b_vid, bounds: b_bounds} = self.infcx().get(vb, b_vid);
 
-    #debug["%s.c_ty_vars(<T%u>=%s <: <T%u>=%s)",
+    #debug["%s.c_vars(%s=%s <: %s=%s)",
            self.tag(),
-           a_id, a_bounds.to_str(self.infcx()),
-           b_id, b_bounds.to_str(self.infcx())];
+           a_vid.to_str(), a_bounds.to_str(self.infcx()),
+           b_vid.to_str(), b_bounds.to_str(self.infcx())];
 
-    let tcx = self.infcx().tcx;
-
-    if a_id == b_id {
-        ret ok(ty::mk_var(tcx, a_id as int));
+    if a_vid == b_vid {
+        ret ok(a_t);
     }
 
-    // The comments in this function are written for LUB, but they
-    // apply equally well to GLB if you inverse upper/lower/sub/super/etc.
-
     // If both A and B have an UB type, then we can just compute the
     // LUB of those types:
     let a_bnd = self.bnd(a_bounds), b_bnd = self.bnd(b_bounds);
     alt (a_bnd, b_bnd) {
       (some(a_ty), some(b_ty)) {
-        alt self.infcx().try {|| self.c_tys(a_ty, b_ty) } {
+        alt self.infcx().try {|| c_ts(a_ty, b_ty) } {
             ok(t) { ret ok(t); }
             err(_) { /*fallthrough */ }
         }
@@ -929,33 +1019,37 @@ fn c_ty_vars<C:combine>(self: C, a_id: uint, b_id: uint) -> cres<ty::t> {
 
     // Otherwise, we need to merge A and B into one variable.  We can
     // then use either variable as an upper bound:
-    self.infcx().vars(a_id, b_id).then {||
-        ok(ty::mk_var(tcx, a_id as int))
+    self.infcx().vars(vb, a_vid, b_vid).then {||
+        ok(a_t)
     }
 }
 
-fn c_ty_var_ty<C:combine>(self: C, a_id: uint, b: ty::t) -> cres<ty::t> {
-    let {root: a_id, bounds: a_bounds} = self.infcx().get_var(a_id);
+fn c_var_t<V:copy vid, C:combine, T:copy to_str st>(
+    self: C, vb: vals_and_bindings<V, T>,
+    a_vid: V, b: T,
+    c_ts: fn(T, T) -> cres<T>) -> cres<T> {
+
+    let {root: a_id, bounds: a_bounds} = self.infcx().get(vb, a_vid);
 
     // 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["%s.c_ty_var_ty(<T%u>=%s <: %s)",
+    #debug["%s.c_var_ty(%s=%s <: %s)",
            self.tag(),
-           a_id, a_bounds.to_str(self.infcx()),
+           a_id.to_str(), a_bounds.to_str(self.infcx()),
            b.to_str(self.infcx())];
 
     alt self.bnd(a_bounds) {
-      some(a_ty) {
+      some(a_bnd) {
         // If a has an upper bound, return it.
-        ret self.c_tys(a_ty, b);
+        ret c_ts(a_bnd, b);
       }
       none {
         // If a does not have an upper bound, make b the upper bound of a
         // and then return b.
         let a_bounds = self.with_bnd(a_bounds, b);
         self.infcx().bnds(a_bounds.lb, a_bounds.ub).then {||
-            self.infcx().set_ty(a_id, bounded(a_bounds));
+            self.infcx().set(vb, a_id, bounded(a_bounds));
             ok(b)
         }
       }
@@ -1070,15 +1164,21 @@ fn c_tys<C:combine>(
       (_, ty::ty_bot) { self.c_bot(b) }
 
       (ty::ty_var(a_id), ty::ty_var(b_id)) {
-        c_ty_vars(self, a_id as uint, b_id as uint)
+        c_vars(self, self.infcx().vb,
+               a, a_id, b_id,
+               {|x, y| self.c_tys(x, y) })
       }
 
       // Note that the LUB/GLB operations are commutative:
-      (ty::ty_var(a_id), _) {
-        c_ty_var_ty(self, a_id as uint, b)
+      (ty::ty_var(v_id), _) {
+        c_var_t(self, self.infcx().vb,
+                v_id, b,
+                {|x, y| self.c_tys(x, y) })
       }
-      (_, ty::ty_var(b_id)) {
-        c_ty_var_ty(self, b_id as uint, a)
+      (_, ty::ty_var(v_id)) {
+        c_var_t(self, self.infcx().vb,
+                v_id, a,
+                {|x, y| self.c_tys(x, y) })
       }
 
       (ty::ty_nil, _) |
@@ -1192,43 +1292,61 @@ fn c_tys<C:combine>(
     }
 }
 
-fn combine_or_unify_regions(tcx: ty::ctxt,
-                            a: ty::region,
-                            b: ty::region,
-                            contravariant_combine: bool) -> cres<ty::region> {
+fn c_regions<C:combine>(
+    self: C, a: ty::region, b: ty::region) -> cres<ty::region> {
+
+    #debug["%s.c_regions(%?, %?)",
+           self.tag(),
+           a.to_str(self.infcx()),
+           b.to_str(self.infcx())];
+
     alt (a, b) {
-      (ty::re_var(_), _) | (_, ty::re_var(_)) {
-        ok(a)   // FIXME: We need region variables!
+      (ty::re_var(a_id), ty::re_var(b_id)) {
+        c_vars(self, self.infcx().rb,
+               a, a_id, b_id,
+               {|x, y| self.c_regions(x, y) })
       }
-      (ty::re_inferred, _) | (_, ty::re_inferred) {
-        fail "tried to combine or unify inferred regions"
+
+      (ty::re_var(v_id), r) |
+      (r, ty::re_var(v_id)) {
+        c_var_t(self, self.infcx().rb,
+                v_id, r,
+                {|x, y| self.c_regions(x, y) })
       }
-      (ty::re_param(_), ty::re_param(_)) |
-      (ty::re_self, ty::re_self) {
+
+      (f @ ty::re_free(f_id, f_br), s @ ty::re_scope(s_id)) |
+      (s @ ty::re_scope(s_id), f @ ty::re_free(f_id, f_br)) {
+        self.c_regions_free_scope(f, f_id, f_br, s, s_id)
+      }
+
+      (ty::re_scope(a_id), ty::re_scope(b_id)) {
+        self.c_regions_scope_scope(a, a_id, b, b_id)
+      }
+
+      // For these types, we cannot define any additional relationship:
+      (ty::re_free(_, _), ty::re_free(_, _)) |
+      (ty::re_bound(_), ty::re_bound(_)) |
+      (ty::re_bound(_), ty::re_free(_, _)) |
+      (ty::re_bound(_), ty::re_scope(_)) |
+      (ty::re_free(_, _), ty::re_bound(_)) |
+      (ty::re_scope(_), ty::re_bound(_)) {
         if a == b {
+            #debug["... yes, %s == %s.",
+                   a.to_str(self.infcx()),
+                   b.to_str(self.infcx())];
             ok(a)
         } else {
-            err(ty::terr_regions_differ(false, a, b))
+            #debug["... no, %s != %s.",
+                   a.to_str(self.infcx()),
+                   b.to_str(self.infcx())];
+            err(ty::terr_regions_differ(false, b, a))
         }
       }
-      (ty::re_param(_), ty::re_block(_)) |
-      (ty::re_self, ty::re_block(_)) {
-        ok(a)
-      }
-      (ty::re_block(_), ty::re_param(_)) |
-      (ty::re_block(_), ty::re_self) {
-        err(ty::terr_regions_differ(false, a, b))
-      }
-      (ty::re_block(block_a), ty::re_block(block_b)) {
-        // The region corresponding to an outer block is a subtype of the
-        // region corresponding to an inner block.
-        let rm = tcx.region_map;
-        let nca_opt = region::nearest_common_ancestor(rm, block_a, block_b);
-        alt nca_opt {
-            some(nca) if nca == block_b { ok(a) }
-            some(nca) if contravariant_combine { ok(ty::re_block(nca)) }
-            _ { err(ty::terr_regions_differ(false, a, b)) }
-        }
+
+      (ty::re_default, _) |
+      (_, ty::re_default) {
+        // actually a compiler bug, I think.
+        err(ty::terr_regions_differ(false, b, a))
       }
     }
 }
@@ -1319,7 +1437,29 @@ impl of combine for lub {
     }
 
     fn c_regions(a: ty::region, b: ty::region) -> cres<ty::region> {
-        ret combine_or_unify_regions(self.tcx, a, b, true);
+        ret c_regions(self, a, b);
+    }
+
+    fn c_regions_free_scope(
+        a: ty::region, _a_id: ast::node_id, _a_br: ty::bound_region,
+        _b: ty::region, _b_id: ast::node_id) -> cres<ty::region> {
+
+        // for LUB, the scope is within the function and the free
+        // region is always a parameter to the method.
+        ret ok(a); // NDM--not so for nested functions
+    }
+
+    fn c_regions_scope_scope(a: ty::region, a_id: ast::node_id,
+                             b: ty::region, b_id: ast::node_id)
+        -> cres<ty::region> {
+
+        // The region corresponding to an outer block is a subtype of the
+        // region corresponding to an inner block.
+        let rm = self.infcx().tcx.region_map;
+        alt region::nearest_common_ancestor(rm, a_id, b_id) {
+          some(r_id) { ok(ty::re_scope(r_id)) }
+          _ { err(ty::terr_regions_differ(false, b, a)) }
+        }
     }
 }
 
@@ -1427,6 +1567,31 @@ impl of combine for glb {
     }
 
     fn c_regions(a: ty::region, b: ty::region) -> cres<ty::region> {
-        ret combine_or_unify_regions(self.tcx, a, b, false);
+        ret c_regions(self, a, b);
+    }
+
+    fn c_regions_free_scope(
+        _a: ty::region, _a_id: ast::node_id, _a_br: ty::bound_region,
+        b: ty::region, _b_id: ast::node_id) -> cres<ty::region> {
+
+        // for GLB, the scope is within the function and the free
+        // region is always a parameter to the method.  So the GLB
+        // must be the scope.
+        ret ok(b); // NDM--not so for nested functions
+    }
+
+    fn c_regions_scope_scope(a: ty::region, a_id: ast::node_id,
+                             b: ty::region, b_id: ast::node_id)
+        -> cres<ty::region> {
+
+        // We want to generate a region that is contained by both of
+        // these: so, if one of these scopes is a subscope of the
+        // other, return it.  Otherwise fail.
+        let rm = self.infcx().tcx.region_map;
+        alt region::nearest_common_ancestor(rm, a_id, b_id) {
+          some(r_id) if a_id == r_id { ok(b) }
+          some(r_id) if b_id == r_id { ok(a) }
+          _ { err(ty::terr_regions_differ(false, b, a)) }
+        }
     }
 }
diff --git a/src/rustc/middle/region.rs b/src/rustc/middle/region.rs
index 7afe2c26624..1e002e9c1d0 100644
--- a/src/rustc/middle/region.rs
+++ b/src/rustc/middle/region.rs
@@ -1,11 +1,141 @@
 /*
- * Region resolution. This pass runs before typechecking and resolves region
- * names to the appropriate block.
- */
+
+Region resolution. This pass runs before typechecking and resolves region
+names to the appropriate block.
+
+This seems to be as good a place as any to explain in detail how
+region naming, representation, and type check works.
+
+### Naming and so forth
+
+We really want regions to be very lightweight to use. Therefore,
+unlike other named things, the scopes for regions are not explicitly
+declared: instead, they are implicitly defined.  Functions declare new
+scopes: if the function is not a bare function, then as always it
+inherits the names in scope from the outer scope.  Within a function
+declaration, new names implicitly declare new region variables.  Outside
+of function declarations, new names are illegal.  To make this more
+concrete, here is an example:
+
+    fn foo(s: &a.S, t: &b.T) {
+        let s1: &a.S = s; // a refers to the same a as in the decl
+        let t1: &c.T = t; // illegal: cannot introduce new name here
+    }
+
+The code in this file is what actually handles resolving these names.
+It creates a couple of maps that map from the AST node representing a
+region ptr type to the resolved form of its region parameter.  If new
+names are introduced where they shouldn't be, then an error is
+reported.
+
+If regions are not given an explicit name, then the behavior depends
+a bit on the context.  Within a function declaration, all unnamed regions
+are mapped to a single, anonymous parameter.  That is, a function like:
+
+    fn foo(s: &S) -> &S { s }
+
+is equivalent to a declaration like:
+
+    fn foo(s: &a.S) -> &a.S { s }
+
+Within a function body or other non-binding context, an unnamed region
+reference is mapped to a fresh region variable whose value can be
+inferred as normal.
+
+The resolved form of regions is `ty::region`.  Before I can explain
+why this type is setup the way it is, I have to digress a little bit
+into some ill-explained type theory.
+
+### Universal Quantification
+
+Regions are more complex than type parameters because, unlike type
+parameters, they can be universally quantified within a type.  To put
+it another way, you cannot (at least at the time of this writing) have
+a variable `x` of type `fn<T>(T) -> T`.  You can have an *item* of
+type `fn<T>(T) - T`, but whenever it is referenced within a method,
+that type parameter `T` is replaced with a concrete type *variable*
+`$T`.  To make this more concrete, imagine this code:
+
+    fn identity<T>(x: T) -> T { x }
+    let f = identity; // f has type fn($T) -> $T
+    f(3u); // $T is bound to uint
+    f(3);  // Type error
+
+You can see here that a type error will result because the type of `f`
+(as opposed to the type of `identity`) is not universally quantified
+over `$T`.  That's fancy math speak for saying that the type variable
+`$T` refers to a specific type that may not yet be known, unlike the
+type parameter `T` which refers to some type which will never be
+known.
+
+Anyway, regions work differently.  If you have an item of type
+`fn(&a.T) -> &a.T` and you reference it, its type remains the same:
+only when the function *is called* is `&a` instantiated with a
+concrete region variable.  This means you could call it twice and give
+different values for `&a` each time.
+
+This more general form is possible for regions because they do not
+impact code generation.  We do not need to monomorphize functions
+differently just because they contain region pointers.  In fact, we
+don't really do *anything* differently.
+
+### Representing regions; or, why do I care about all that?
+
+The point of this discussion is that the representation of regions
+must distinguish between a *bound* reference to a region and a *free*
+reference.  A bound reference is one which will be replaced with a
+fresh type variable when the function is called, like the type
+parameter `T` in `identity`.  They can only appear within function
+types.  A free reference is a region that may not yet be concretely
+known, like the variable `$T`.
+
+To see why we must distinguish them carefully, consider this program:
+
+    fn item1(s: &a.S) {
+        let choose = fn@(s1: &a.S) -> &a.S {
+            if some_cond { s } else { s1 }
+        };
+    }
+
+Here, the variable `s1: &a.S` that appears within the `fn@` is a free
+reference to `a`.  That is, when you call `choose()`, you don't
+replace `&a` with a fresh region variable, but rather you expect `s1`
+to be in the same region as the parameter `s`.
+
+But in this program, this is not the case at all:
+
+    fn item2() {
+        let identity = fn@(s1: &a.S) -> &a.S { s1 };
+    }
+
+To distinguish between these two cases, `ty::region` contains two
+variants: `re_bound` and `re_free`.  In `item1()`, the outer reference
+to `&a` would be `re_bound(rid_param("a", 0u))`, and the inner reference
+would be `re_free(rid_param("a", 0u))`.  In `item2()`, the inner reference
+would be `re_bound(rid_param("a", 0u))`.
+
+#### Impliciations for typeck
+
+In typeck, whenever we call a function, we must go over and replace
+all references to `re_bound()` regions within its parameters with
+fresh type variables (we do not, however, replace bound regions within
+nested function types, as those nested functions have not yet been
+called).
+
+Also, when we typecheck the *body* of an item, we must replace all
+`re_bound` references with `re_free` references.  This means that the
+region in the type of the argument `s` in `item1()` *within `item1()`*
+is not `re_bound(re_param("a", 0u))` but rather `re_free(re_param("a",
+0u))`.  This is because, for any particular *invocation of `item1()`*,
+`&a` will be bound to some specific region, and hence it is no longer
+bound.
+
+*/
 
 import driver::session::session;
 import middle::ty;
 import syntax::{ast, visit};
+import syntax::codemap::span;
 import util::common::new_def_hash;
 
 import std::list;
@@ -23,10 +153,9 @@ enum parent {
 }
 
 /* Records the parameter ID of a region name. */
-type binding = {
-    name: str,
-    id: uint
-};
+type binding = {node_id: ast::node_id,
+                name: str,
+                br: ty::bound_region};
 
 type region_map = {
     /* Mapping from a block/function expression to its parent. */
@@ -44,11 +173,105 @@ type region_map = {
     rvalue_to_block: hashmap<ast::node_id,ast::node_id>
 };
 
+type region_scope = @{
+    node_id: ast::node_id,
+    kind: region_scope_kind
+};
+
+enum region_scope_kind {
+    rsk_root,
+    rsk_body(region_scope),
+    rsk_self(region_scope),
+    rsk_binding(region_scope, @mut [binding])
+}
+
+fn root_scope(node_id: ast::node_id) -> region_scope {
+    @{node_id: node_id, kind: rsk_root}
+}
+
+impl methods for region_scope {
+    fn body_subscope(node_id: ast::node_id) -> region_scope {
+        @{node_id: node_id, kind: rsk_body(self)}
+    }
+
+    fn binding_subscope(node_id: ast::node_id) -> region_scope {
+        @{node_id: node_id, kind: rsk_binding(self, @mut [])}
+    }
+
+    fn self_subscope(node_id: ast::node_id) -> region_scope {
+        @{node_id: node_id, kind: rsk_self(self)}
+    }
+
+    fn find(nm: str) -> option<binding> {
+        alt self.kind {
+          rsk_root { none }
+          rsk_body(parent) { parent.find(nm) }
+          rsk_self(parent) { parent.find(nm) }
+          rsk_binding(parent, bs) {
+            alt (*bs).find({|b| b.name == nm }) {
+              none { parent.find(nm) }
+              some(b) { some(b) }
+            }
+          }
+        }
+    }
+
+    // fn resolve_anon() -> option<ty::region> {
+    //     alt self.kind {
+    //       rsk_root { none }
+    //       rsk_body(_) { none }
+    //       rsk_self(_) { none }
+    //       rsk_binding(_, _) { ty::re_bound(ty::br_anon) }
+    //     }
+    // }
+
+    fn resolve_self_helper(bound: bool) -> option<ty::region> {
+        alt self.kind {
+          rsk_root { none }
+          rsk_self(_) if bound { some(ty::re_bound(ty::br_self)) }
+          rsk_self(_) { some(ty::re_free(self.node_id, ty::br_self)) }
+          rsk_binding(p, _) { p.resolve_self_helper(bound) }
+          rsk_body(p) { p.resolve_self_helper(false) }
+        }
+    }
+
+    fn resolve_self() -> option<ty::region> {
+        self.resolve_self_helper(true)
+    }
+
+    fn resolve_ident(nm: str) -> option<ty::region> {
+        alt self.find(nm) {
+          some(b) if b.node_id == self.node_id {
+            some(ty::re_bound(b.br))
+          }
+
+          some(b) {
+            some(ty::re_free(b.node_id, b.br))
+          }
+
+          none {
+            alt self.kind {
+              rsk_self(_) | rsk_root | rsk_body(_) { none }
+              rsk_binding(_, bs) {
+                let idx = (*bs).len();
+                let br = ty::br_param(idx, nm);
+                vec::push(*bs, {node_id: self.node_id,
+                                name: nm,
+                                br: br});
+                some(ty::re_bound(br))
+              }
+            }
+          }
+        }
+    }
+}
+
 type ctxt = {
     sess: session,
     def_map: resolve::def_map,
     region_map: @region_map,
-    mut bindings: @list<binding>,
+
+    scope: region_scope,
 
     /*
      * A list of local IDs that will be parented to the next block we
@@ -63,9 +286,6 @@ type ctxt = {
     /* True if we're within the pattern part of an alt, false otherwise. */
     in_alt: bool,
 
-    /* True if we're within a typeclass implementation, false otherwise. */
-    in_typeclass: bool,
-
     /* The next parameter ID. */
     mut next_param_id: uint
 };
@@ -108,16 +328,28 @@ fn nearest_common_ancestor(region_map: @region_map, scope_a: ast::node_id,
     let b_ancestors = ancestors_of(region_map, scope_b);
     let mut a_index = vec::len(a_ancestors) - 1u;
     let mut b_index = vec::len(b_ancestors) - 1u;
-    while a_ancestors[a_index] == b_ancestors[b_index] {
+
+    // Here, [ab]_ancestors is a vector going from narrow to broad.
+    // The end of each vector will be the item where the scope is
+    // defined; if there are any common ancestors, then the tails of
+    // the vector will be the same.  So basically we want to walk
+    // backwards from the tail of each vector and find the first point
+    // where they diverge.  If one vector is a suffix of the other,
+    // then the corresponding scope is a superscope of the other.
+
+    loop {
+        if a_ancestors[a_index] != b_ancestors[b_index] {
+            if a_index == a_ancestors.len() {
+                ret none;
+            } else {
+                ret some(a_ancestors[a_index + 1u]);
+            }
+        }
+        if a_index == 0u { ret some(scope_a); }
+        if b_index == 0u { ret some(scope_b); }
         a_index -= 1u;
         b_index -= 1u;
     }
-
-    if a_index == vec::len(a_ancestors) {
-        ret none;
-    }
-
-    ret some(a_ancestors[a_index + 1u]);
 }
 
 fn get_inferred_region(cx: ctxt, sp: syntax::codemap::span) -> ty::region {
@@ -127,14 +359,51 @@ fn get_inferred_region(cx: ctxt, sp: syntax::codemap::span) -> ty::region {
     // TODO: What do we do if we're in an alt?
 
     ret alt cx.parent {
-        pa_fn_item(_) | pa_nested_fn(_) {
-            let id = cx.next_param_id;
-            cx.next_param_id += 1u;
-            ty::re_param(id)
+      pa_fn_item(_) | pa_nested_fn(_) { ty::re_bound(ty::br_anon) }
+      pa_block(block_id) { ty::re_scope(block_id) }
+      pa_item(_) { ty::re_bound(ty::br_anon) }
+      pa_crate { cx.sess.span_bug(sp, "inferred region at crate level?!"); }
+    }
+}
+
+fn resolve_region_binding(cx: ctxt, span: span, region: ast::region) {
+
+    let id = region.id;
+    let rm = cx.region_map;
+    alt region.node {
+      ast::re_inferred {
+        // option::may(cx.scope.resolve_anon()) {|r|
+        //     rm.ast_type_to_region.insert(id, r);
+        // }
+      }
+
+      ast::re_named(ident) {
+        alt cx.scope.resolve_ident(ident) {
+          some(r) {
+            rm.ast_type_to_region.insert(id, r);
+          }
+
+          none {
+            cx.sess.span_err(
+                span,
+                #fmt["the region `%s` is not declared", ident]);
+          }
         }
-        pa_block(block_id) { ty::re_block(block_id) }
-        pa_item(_) { ty::re_param(0u) }
-        pa_crate { cx.sess.span_bug(sp, "inferred region at crate level?!"); }
+      }
+
+      ast::re_self {
+        alt cx.scope.resolve_self() {
+          some(r) {
+            rm.ast_type_to_region.insert(id, r);
+          }
+
+          none {
+            cx.sess.span_err(
+                span,
+                "the `self` region is not allowed here");
+          }
+        }
+      }
     }
 }
 
@@ -143,65 +412,10 @@ fn resolve_ty(ty: @ast::ty, cx: ctxt, visitor: visit::vt<ctxt>) {
     cx.region_map.ast_type_to_inferred_region.insert(ty.id, inferred_region);
 
     alt ty.node {
-        ast::ty_rptr({id: region_id, node: node}, _) {
-            alt node {
-                ast::re_inferred { /* no-op */ }
-                ast::re_self {
-                    if cx.in_typeclass {
-                        let r = ty::re_self;
-                        let rm = cx.region_map;
-                        rm.ast_type_to_region.insert(region_id, r);
-                    } else {
-                        cx.sess.span_err(ty.span,
-                                         "the `self` region is not allowed \
-                                          here");
-                    }
-                }
-                ast::re_named(ident) {
-                    // If at item scope, introduce or reuse a binding. If at
-                    // block scope, require that the binding be introduced.
-                    let bindings = cx.bindings;
-                    let mut region;
-                    alt list::find(*bindings, {|b| ident == b.name}) {
-                        some(binding) { region = ty::re_param(binding.id); }
-                        none {
-                            let id = cx.next_param_id;
-                            let binding = {name: ident, id: id};
-                            cx.next_param_id += 1u;
-
-                            cx.bindings = @list::cons(binding, cx.bindings);
-                            region = ty::re_param(id);
-
-                            alt cx.parent {
-                                pa_fn_item(fn_id) | pa_nested_fn(fn_id) {
-                                    /* ok */
-                                }
-                                pa_item(_) {
-                                    cx.sess.span_err(ty.span,
-                                                     "named region not " +
-                                                     "allowed in this " +
-                                                     "context");
-                                }
-                                pa_block(_) {
-                                    cx.sess.span_err(ty.span,
-                                                     "unknown region `" +
-                                                     ident + "`");
-                                }
-                                pa_crate {
-                                    cx.sess.span_bug(ty.span, "named " +
-                                                     "region at crate " +
-                                                     "level?!");
-                                }
-                            }
-                        }
-                    }
-
-                    let ast_type_to_region = cx.region_map.ast_type_to_region;
-                    ast_type_to_region.insert(region_id, region);
-                }
-            }
-        }
-        _ { /* nothing to do */ }
+      ast::ty_rptr(r, _) {
+        resolve_region_binding(cx, ty.span, r);
+      }
+      _ { /* nothing to do */ }
     }
 
     visit::visit_ty(ty, cx, visitor);
@@ -230,6 +444,7 @@ fn resolve_block(blk: ast::blk, cx: ctxt, visitor: visit::vt<ctxt>) {
 
     // Descend.
     let new_cx: ctxt = {parent: pa_block(blk.node.id),
+                        scope: cx.scope.body_subscope(blk.node.id),
                         mut queued_locals: [],
                         in_alt: false with cx};
     visit::visit_block(blk, new_cx, visitor);
@@ -282,6 +497,7 @@ fn resolve_expr(expr: @ast::expr, cx: ctxt, visitor: visit::vt<ctxt>) {
         ast::expr_fn(_, _, _, _) | ast::expr_fn_block(_, _) {
             record_parent(cx, expr.id);
             let new_cx = {parent: pa_nested_fn(expr.id),
+                          scope: cx.scope.binding_subscope(expr.id),
                           in_alt: false with cx};
             visit::visit_expr(expr, new_cx, visitor);
         }
@@ -312,27 +528,26 @@ fn resolve_local(local: @ast::local, cx: ctxt, visitor: visit::vt<ctxt>) {
 
 fn resolve_item(item: @ast::item, cx: ctxt, visitor: visit::vt<ctxt>) {
     // Items create a new outer block scope as far as we're concerned.
-    let mut parent;
-    let mut in_typeclass;
-    alt item.node {
-        ast::item_fn(_, _, _) | ast::item_enum(_, _) {
-            parent = pa_fn_item(item.id);
-            in_typeclass = false;
-        }
-        ast::item_impl(_, _, _, _) {
-            parent = pa_item(item.id);
-            in_typeclass = true;
-        }
-        _ {
-            parent = pa_item(item.id);
-            in_typeclass = false;
+    let {parent, scope} = {
+        alt item.node {
+          ast::item_fn(_, _, _) | ast::item_enum(_, _) {
+            {parent: pa_fn_item(item.id),
+             scope: cx.scope.binding_subscope(item.id)}
+          }
+          ast::item_impl(_, _, _, _) | ast::item_class(_, _, _) {
+            {parent: pa_item(item.id),
+             scope: cx.scope.self_subscope(item.id)}
+          }
+          _ {
+            {parent: pa_item(item.id),
+             scope: root_scope(item.id)}
+          }
         }
     };
 
-    let new_cx: ctxt = {bindings: @list::nil,
-                        parent: parent,
+    let new_cx: ctxt = {parent: parent,
+                        scope: scope,
                         in_alt: false,
-                        in_typeclass: in_typeclass,
                         mut next_param_id: 0u
                         with cx};
 
@@ -349,11 +564,10 @@ fn resolve_crate(sess: session, def_map: resolve::def_map, crate: @ast::crate)
                                   ast_type_to_inferred_region:
                                     map::int_hash(),
                                   rvalue_to_block: map::int_hash()},
-                    mut bindings: @list::nil,
+                    scope: root_scope(0),
                     mut queued_locals: [],
                     parent: pa_crate,
                     in_alt: false,
-                    in_typeclass: false,
                     mut next_param_id: 0u};
     let visitor = visit::mk_vt(@{
         visit_block: resolve_block,
diff --git a/src/rustc/middle/regionck.rs b/src/rustc/middle/regionck.rs
index a969785cd2e..611f010ae10 100644
--- a/src/rustc/middle/regionck.rs
+++ b/src/rustc/middle/regionck.rs
@@ -26,38 +26,38 @@ fn check_expr(expr: @ast::expr, cx: ctxt, visitor: visit::vt<ctxt>) {
     if ty::type_has_rptrs(t) {
         ty::walk_ty(t) { |t|
             alt ty::get(t).struct {
-                ty::ty_rptr(region, _) {
-                    alt region {
-                        ty::re_self | ty::re_inferred | ty::re_param(_) {
-                            /* ok */
-                        }
-                        ty::re_block(rbi) {
-                            let referent_block_id = rbi;
-                            let enclosing_block_id = alt cx.enclosing_block {
-                                none {
-                                    cx.tcx.sess.span_bug(expr.span,
-                                                         "block region " +
-                                                         "type outside a " +
-                                                         "block?!");
-                                }
-                                some(eb) { eb }
-                            };
+              ty::ty_rptr(region, _) {
+                alt region {
+                  ty::re_bound(_) | ty::re_free(_, _) {
+                    /* ok */
+                  }
+                  ty::re_scope(rbi) {
+                    let referent_block_id = rbi;
+                    let enclosing_block_id = alt cx.enclosing_block {
+                      none {
+                        cx.tcx.sess.span_bug(expr.span,
+                                             "block region " +
+                                             "type outside a " +
+                                             "block?!");
+                      }
+                      some(eb) { eb }
+                    };
 
-                            if !region::scope_contains(cx.tcx.region_map,
-                                                       referent_block_id,
-                                                       enclosing_block_id) {
+                    if !region::scope_contains(cx.tcx.region_map,
+                                               referent_block_id,
+                                               enclosing_block_id) {
 
-                                cx.tcx.sess.span_err(expr.span, "reference " +
-                                                     "escapes its block");
-                            }
-                        }
-                        ty::re_var(_) {
-                            cx.tcx.sess.span_bug(expr.span,
-                                                 "unresolved region");
-                        }
+                        cx.tcx.sess.span_err(expr.span, "reference " +
+                                             "escapes its block");
                     }
+                  }
+                  ty::re_default | ty::re_var(_) {
+                    cx.tcx.sess.span_bug(expr.span,
+                                         "unresolved region");
+                  }
                 }
-                _ { /* no-op */ }
+              }
+              _ { /* no-op */ }
             }
         }
     }
diff --git a/src/rustc/middle/trans/shape.rs b/src/rustc/middle/trans/shape.rs
index 03277667ada..49efb8a00cc 100644
--- a/src/rustc/middle/trans/shape.rs
+++ b/src/rustc/middle/trans/shape.rs
@@ -641,7 +641,7 @@ fn simplify_type(tcx: ty::ctxt, typ: ty::t) -> ty::t {
           _ { typ }
         }
     }
-    ty::fold_ty(tcx, ty::fm_general(bind simplifier(tcx, _)), typ)
+    ty::fold_ty(tcx, typ) {|t| simplifier(tcx, t) }
 }
 
 // Given a tag type `ty`, returns the offset of the payload.
diff --git a/src/rustc/middle/ty.rs b/src/rustc/middle/ty.rs
index 8ab1330fad9..89c34064f6d 100644
--- a/src/rustc/middle/ty.rs
+++ b/src/rustc/middle/ty.rs
@@ -15,6 +15,8 @@ import util::ppaux::ty_to_str;
 import util::ppaux::ty_constr_to_str;
 import syntax::print::pprust::*;
 
+export ty_vid, region_vid, vid;
+export br_hashmap;
 export is_instantiable;
 export node_id_to_type;
 export node_id_to_type_params;
@@ -33,12 +35,11 @@ export expr_ty;
 export expr_ty_params_and_ty;
 export expr_is_lval;
 export field_ty;
-export fold_ty;
+export fold_ty, fold_sty_to_ty, fold_region, fold_ty_var;
 export field;
 export field_idx;
 export get_field;
 export get_fields;
-export fm_var, fm_general, fm_rptr;
 export get_element_type;
 export is_binopable;
 export is_pred_ty;
@@ -93,7 +94,7 @@ export ty_uint, mk_uint, mk_mach_uint;
 export ty_uniq, mk_uniq, mk_imm_uniq, type_is_unique_box;
 export ty_var, mk_var;
 export ty_self, mk_self;
-export region, re_block, re_param, re_var;
+export region, bound_region;
 export get, type_has_params, type_has_vars, type_has_rptrs, type_id;
 export ty_var_id;
 export ty_to_def_id;
@@ -127,7 +128,6 @@ export resolved_mode;
 export arg_mode;
 export unify_mode;
 export set_default_mode;
-export unify;
 export variant_info;
 export walk_ty, maybe_walk_ty;
 export occurs_check;
@@ -261,20 +261,25 @@ type fn_ty = {proto: ast::proto,
               ret_style: ret_style,
               constraints: [@constr]};
 
+// See discussion at head of region.rs
 enum region {
-    // The region of a block.
-    re_block(node_id),
-    // The self region. Only valid inside classes and typeclass
-    // implementations.
-    re_self,
-    // The inferred region, which also corresponds to &self in typedefs.
-    re_inferred,
+    re_bound(bound_region),
+    re_free(node_id, bound_region),
+    re_scope(node_id),
+    re_var(region_vid),
+    re_default
+}
 
-    // A region parameter.
-    re_param(uint),
+enum bound_region {
+    // The `self` region for a given class/impl/iface.  The defining item may
+    // appear in another crate.
+    br_self,
 
-    // A region variable.
-    re_var(uint)
+    // The anonymous region parameter for a given function.
+    br_anon,
+
+    // A named region parameter.
+    br_param(uint, str)
 }
 
 // NB: If you change this, you'll probably want to change the corresponding
@@ -300,7 +305,7 @@ enum sty {
     ty_res(def_id, t, [t]),
     ty_tup([t]),
 
-    ty_var(int), // type variable during typechecking
+    ty_var(ty_vid), // type variable during typechecking
     ty_param(uint, def_id), // type parameter
     ty_self([t]), // interface method self type
 
@@ -344,6 +349,24 @@ enum param_bound {
     bound_iface(t),
 }
 
+enum ty_vid = uint;
+enum region_vid = uint;
+
+iface vid {
+    fn to_uint() -> uint;
+    fn to_str() -> str;
+}
+
+impl of vid for ty_vid {
+    fn to_uint() -> uint { *self }
+    fn to_str() -> str { #fmt["<V%u>", self.to_uint()] }
+}
+
+impl of vid for region_vid {
+    fn to_uint() -> uint { *self }
+    fn to_str() -> str { #fmt["<R%u>", self.to_uint()] }
+}
+
 fn param_bounds_to_kind(bounds: param_bounds) -> kind {
     let mut kind = kind_noncopyable;
     for bound in *bounds {
@@ -443,7 +466,11 @@ fn mk_t_with_id(cx: ctxt, st: sty, o_def_id: option<ast::def_id>) -> t {
       ty_box(m) | ty_uniq(m) | ty_vec(m) | ty_ptr(m) {
         derive_flags(has_params, has_vars, has_rptrs, m.ty);
       }
-      ty_rptr(_, m) {
+      ty_rptr(r, m) {
+        alt r {
+          ty::re_var(_) { has_vars = true; }
+          _ { }
+        }
         has_rptrs = true;
         derive_flags(has_params, has_vars, has_rptrs, m.ty);
       }
@@ -555,7 +582,7 @@ fn mk_res(cx: ctxt, did: ast::def_id, inner: t, tps: [t]) -> t {
     mk_t(cx, ty_res(did, inner, tps))
 }
 
-fn mk_var(cx: ctxt, v: int) -> t { mk_t(cx, ty_var(v)) }
+fn mk_var(cx: ctxt, v: ty_vid) -> t { mk_t(cx, ty_var(v)) }
 
 fn mk_self(cx: ctxt, tps: [t]) -> t { mk_t(cx, ty_self(tps)) }
 
@@ -622,146 +649,124 @@ fn maybe_walk_ty(ty: t, f: fn(t) -> bool) {
     }
 }
 
-enum fold_mode {
-    fm_var(fn@(int) -> t),
-    fm_param(fn@(uint, def_id) -> t),
-    fm_rptr(fn@(region, bool /* under & */) -> region,
-            bool /* descend into outermost fn */),
-    fm_general(fn@(t) -> t),
+fn fold_sty_to_ty(tcx: ty::ctxt, sty: sty, foldop: fn(t) -> t) -> t {
+    mk_t(tcx, fold_sty(sty, foldop))
 }
 
-fn fold_ty(cx: ctxt, fld: fold_mode, ty_0: t) -> t {
-    fn do_fold(cx: ctxt, fld: fold_mode, ty_0: t, under_rptr: bool) -> t {
-        let mut ty = ty_0;
+fn fold_sty(sty: sty, fldop: fn(t) -> t) -> sty {
+    alt sty {
+      ty_box(tm) {
+        ty_box({ty: fldop(tm.ty), mutbl: tm.mutbl})
+      }
+      ty_uniq(tm) {
+        ty_uniq({ty: fldop(tm.ty), mutbl: tm.mutbl})
+      }
+      ty_ptr(tm) {
+        ty_ptr({ty: fldop(tm.ty), mutbl: tm.mutbl})
+      }
+      ty_vec(tm) {
+        ty_vec({ty: fldop(tm.ty), mutbl: tm.mutbl})
+      }
+      ty_enum(tid, subtys) {
+        ty_enum(tid, vec::map(subtys) {|t| fldop(t) })
+      }
+      ty_iface(did, subtys) {
+        ty_iface(did, vec::map(subtys) {|t| fldop(t) })
+      }
+      ty_self(subtys) {
+        ty_self(vec::map(subtys) {|t| fldop(t) })
+      }
+      ty_rec(fields) {
+        let new_fields = vec::map(fields) {|fl|
+            let new_ty = fldop(fl.mt.ty);
+            let new_mt = {ty: new_ty, mutbl: fl.mt.mutbl};
+            {ident: fl.ident, mt: new_mt}
+        };
+        ty_rec(new_fields)
+      }
+      ty_tup(ts) {
+        let new_ts = vec::map(ts) {|tt| fldop(tt) };
+        ty_tup(new_ts)
+      }
+      ty_fn(f) {
+        let new_args = vec::map(f.inputs) {|a|
+            let new_ty = fldop(a.ty);
+            {mode: a.mode, ty: new_ty}
+        };
+        let new_output = fldop(f.output);
+        ty_fn({inputs: new_args, output: new_output with f})
+      }
+      ty_res(did, subty, tps) {
+        let new_tps = vec::map(tps) {|ty| fldop(ty) };
+        ty_res(did, fldop(subty), new_tps)
+      }
+      ty_rptr(r, tm) {
+        ty_rptr(r, {ty: fldop(tm.ty), mutbl: tm.mutbl})
+      }
+      ty_constr(subty, cs) {
+        ty_constr(fldop(subty), cs)
+      }
+      ty_class(did, tps) {
+        let new_tps = vec::map(tps) {|ty| fldop(ty) };
+        ty_class(did, new_tps)
+      }
+      ty_nil | ty_bot | ty_bool | ty_int(_) | ty_uint(_) | ty_float(_) |
+      ty_str | ty_type | ty_opaque_closure_ptr(_) |
+      ty_opaque_box | ty_var(_) | ty_param(_, _) {
+        sty
+      }
+    }
+}
 
-        let tb = get(ty);
-        alt fld {
-          fm_var(_) { if !tb.has_vars { ret ty; } }
-          fm_param(_) { if !tb.has_params { ret ty; } }
-          fm_rptr(_,_) { if !tb.has_rptrs { ret ty; } }
-          fm_general(_) {/* no fast path */ }
-        }
+// Folds types from the bottom up.
+fn fold_ty(cx: ctxt, t0: t, fldop: fn(t) -> t) -> t {
+    let sty = fold_sty(get(t0).struct) {|t| fold_ty(cx, t, fldop) };
+    fldop(mk_t(cx, sty))
+}
 
+fn fold_ty_var(cx: ctxt, t0: t, fldop: fn(ty_vid) -> t) -> t {
+    let tb = get(t0);
+    if !tb.has_vars { ret t0; }
+    alt tb.struct {
+      ty_var(id) { fldop(id) }
+      sty { fold_sty_to_ty(cx, sty) {|t| fold_ty_var(cx, t, fldop) } }
+    }
+}
+
+fn fold_region(cx: ctxt, t0: t, fldop: fn(region, bool) -> region) -> t {
+    fn do_fold(cx: ctxt, t0: t, under_r: bool,
+               fldop: fn(region, bool) -> region) -> t {
+        let tb = get(t0);
+        if !tb.has_rptrs { ret t0; }
         alt tb.struct {
-          ty_nil | ty_bot | ty_bool | ty_int(_) | ty_uint(_) | ty_float(_) |
-          ty_str | ty_type | ty_opaque_closure_ptr(_) |
-          ty_opaque_box {}
-          ty_box(tm) {
-            ty = mk_box(cx, {ty: do_fold(cx, fld, tm.ty, under_rptr),
-                             mutbl: tm.mutbl});
+          ty_rptr(r, {ty: t1, mutbl: m}) {
+            let m_r = fldop(r, under_r);
+            let m_t1 = do_fold(cx, t1, true, fldop);
+            ty::mk_rptr(cx, m_r, {ty: m_t1, mutbl: m})
           }
-          ty_uniq(tm) {
-            ty = mk_uniq(cx, {ty: do_fold(cx, fld, tm.ty, under_rptr),
-                              mutbl: tm.mutbl});
+          ty_fn(_) {
+            // do not recurse into functions, which introduce fresh bindings
+            t0
           }
-          ty_ptr(tm) {
-            ty = mk_ptr(cx, {ty: do_fold(cx, fld, tm.ty, under_rptr),
-                             mutbl: tm.mutbl});
-          }
-          ty_vec(tm) {
-            ty = mk_vec(cx, {ty: do_fold(cx, fld, tm.ty, under_rptr),
-                             mutbl: tm.mutbl});
-          }
-          ty_enum(tid, subtys) {
-            ty = mk_enum(cx, tid,
-                         vec::map(subtys, {|t|
-                            do_fold(cx, fld, t, under_rptr)
-                         }));
-          }
-          ty_iface(did, subtys) {
-            ty = mk_iface(cx, did,
-                          vec::map(subtys, {|t|
-                              do_fold(cx, fld, t, under_rptr)
-                          }));
-          }
-          ty_self(subtys) {
-            ty = mk_self(cx, vec::map(subtys, {|t|
-                                do_fold(cx, fld, t, under_rptr)
-                             }));
-          }
-          ty_rec(fields) {
-            let mut new_fields: [field] = [];
-            for fl: field in fields {
-                let new_ty = do_fold(cx, fld, fl.mt.ty, under_rptr);
-                let new_mt = {ty: new_ty, mutbl: fl.mt.mutbl};
-                new_fields += [{ident: fl.ident, mt: new_mt}];
+          sty {
+            fold_sty_to_ty(cx, sty) {|t|
+                do_fold(cx, t, under_r, fldop)
             }
-            ty = mk_rec(cx, new_fields);
           }
-          ty_tup(ts) {
-            let mut new_ts = [];
-            for tt in ts { new_ts += [do_fold(cx, fld, tt, under_rptr)]; }
-            ty = mk_tup(cx, new_ts);
-          }
-          ty_fn(f) {
-            let mut new_fld;
-            alt fld {
-              fm_rptr(_, false) {
-                // Don't recurse into functions, because regions are
-                // universally quantified, well, universally, at function
-                // boundaries.
-                ret ty;
-              }
-              fm_rptr(f, true) {
-                new_fld = fm_rptr(f, false);
-              }
-              _ { new_fld = fld; }
-            }
-
-            let mut new_args: [arg] = [];
-            for a: arg in f.inputs {
-                let new_ty = do_fold(cx, new_fld, a.ty, under_rptr);
-                new_args += [{mode: a.mode, ty: new_ty}];
-            }
-            let new_output = do_fold(cx, new_fld, f.output, under_rptr);
-            ty = mk_fn(cx, {inputs: new_args, output: new_output with f});
-          }
-          ty_res(did, subty, tps) {
-            let mut new_tps = [];
-            for tp: t in tps {
-                new_tps += [do_fold(cx, fld, tp, under_rptr)];
-            }
-            ty = mk_res(cx, did, do_fold(cx, fld, subty, under_rptr),
-                        new_tps);
-          }
-          ty_var(id) {
-            alt fld { fm_var(folder) { ty = folder(id); } _ {/* no-op */ } }
-          }
-          ty_param(id, did) {
-            alt fld { fm_param(folder) { ty = folder(id, did); } _ {} }
-          }
-          ty_rptr(r, tm) {
-            let region = alt fld {
-                fm_rptr(folder, _) { folder(r, under_rptr) }
-                _ { r }
-            };
-            ty = mk_rptr(cx, region,
-                         {ty: do_fold(cx, fld, tm.ty, true),
-                          mutbl: tm.mutbl});
-          }
-          ty_constr(subty, cs) {
-              ty = mk_constr(cx, do_fold(cx, fld, subty, under_rptr), cs);
-          }
-          ty_class(did, ts) {
-              ty = mk_class(cx, did, vec::map(ts, {|t|
-                              do_fold(cx, fld, t, under_rptr)}));
-          }
-          _ {
-              cx.sess.bug("unsupported sort of type in fold_ty");
-          }
-        }
-        alt tb.o_def_id {
-          some(did) { ty = mk_t_with_id(cx, get(ty).struct, some(did)); }
-          _ {}
-        }
-
-        // If this is a general type fold, then we need to run it now.
-        alt fld { fm_general(folder) { ret folder(ty); } _ { ret ty; } }
+      }
     }
 
-    ret do_fold(cx, fld, ty_0, false);
+    do_fold(cx, t0, false, fldop)
 }
 
+fn substitute_type_params(cx: ctxt, substs: [ty::t], typ: t) -> t {
+    let tb = get(typ);
+    alt tb.struct {
+      ty_param(idx, _) { substs[idx] }
+      _ if !tb.has_params { typ }
+      s { mk_t(cx, fold_sty(s) {|t| substitute_type_params(cx, substs, t)}) }
+    }
+}
 
 // Type utilities
 
@@ -1392,7 +1397,7 @@ fn type_param(ty: t) -> option<uint> {
 
 // Returns a vec of all the type variables
 // occurring in t. It may contain duplicates.
-fn vars_in_type(ty: t) -> [int] {
+fn vars_in_type(ty: t) -> [ty_vid] {
     let mut rslt = [];
     walk_ty(ty) {|ty|
         alt get(ty).struct { ty_var(v) { rslt += [v]; } _ { } }
@@ -1421,6 +1426,19 @@ fn type_autoderef(cx: ctxt, t: t) -> t {
     ret t1;
 }
 
+fn hash_bound_region(br: bound_region) -> uint {
+    alt br { // no idea if this is any good
+      br_self { 0u }
+      br_anon { 1u }
+      br_param(id, _) { id }
+    }
+}
+
+fn br_hashmap<V:copy>() -> hashmap<bound_region, V> {
+    map::hashmap(hash_bound_region,
+                 {|&&a: bound_region, &&b: bound_region| a == b })
+}
+
 // Type hashing.
 fn hash_type_structure(st: sty) -> uint {
     fn hash_uint(id: uint, n: uint) -> uint { (id << 2u) + n }
@@ -1448,12 +1466,13 @@ fn hash_type_structure(st: sty) -> uint {
         h
     }
     fn hash_region(r: region) -> uint {
-        alt r {
-          re_block(_)   { 0u }
-          re_self       { 1u }
-          re_inferred   { 2u }
-          re_param(_)   { 3u }
-          re_var(_)     { 4u }
+        alt r { // no idea if this is any good
+          re_bound(br) { (hash_bound_region(br)) << 2u | 0u }
+          re_free(id, br) { ((id as uint) << 4u) |
+                               (hash_bound_region(br)) << 2u | 1u }
+          re_scope(id)  { ((id as uint) << 2u) | 2u }
+          re_var(id)    { (id.to_uint() << 2u) | 3u }
+          re_default    { 4u }
         }
     }
     alt st {
@@ -1492,7 +1511,7 @@ fn hash_type_structure(st: sty) -> uint {
         for a in f.inputs { h = hash_subty(h, a.ty); }
         hash_subty(h, f.output)
       }
-      ty_var(v) { hash_uint(30u, v as uint) }
+      ty_var(v) { hash_uint(30u, v.to_uint()) }
       ty_param(pid, did) { hash_def(hash_uint(31u, pid), did) }
       ty_self(ts) {
         let mut h = 28u;
@@ -1638,7 +1657,7 @@ fn is_pred_ty(fty: t) -> bool {
     is_fn_ty(fty) && type_is_bool(ty_fn_ret(fty))
 }
 
-fn ty_var_id(typ: t) -> int {
+fn ty_var_id(typ: t) -> ty_vid {
     alt get(typ).struct {
       ty_var(vid) { ret vid; }
       _ { #error("ty_var_id called on non-var ty"); fail; }
@@ -1727,7 +1746,7 @@ fn sort_methods(meths: [method]) -> [method] {
     ret std::sort::merge_sort(bind method_lteq(_, _), meths);
 }
 
-fn occurs_check(tcx: ctxt, sp: span, vid: int, rt: t) {
+fn occurs_check(tcx: ctxt, sp: span, vid: ty_vid, rt: t) {
     // Fast path
     if !type_has_vars(rt) { ret; }
 
@@ -1816,115 +1835,6 @@ fn set_default_mode(cx: ctxt, m: ast::mode, m_def: ast::rmode) {
     }
 }
 
-// Type unification via Robinson's algorithm (Robinson 1965). Implemented as
-// described in Hoder and Voronkov:
-//
-//     http://www.cs.man.ac.uk/~hoderk/ubench/unification_full.pdf
-mod unify {
-    import result::{result, ok, err, chain, map, map2};
-
-    export mk_region_bindings;
-    export region_bindings;
-    export precise, in_region_bindings;
-
-    type ures<T> = result<T,type_err>;
-
-    type region_bindings =
-        {sets: ufind::ufind, regions: smallintmap::smallintmap<region>};
-
-    enum unify_style {
-        precise,
-        in_region_bindings(@region_bindings)
-    }
-    type uctxt = {st: unify_style, tcx: ctxt};
-
-    fn mk_region_bindings() -> @region_bindings {
-        ret @{sets: ufind::make(), regions: smallintmap::mk::<region>()};
-    }
-
-    // Unifies two region sets.
-    //
-    // FIXME: This is a straight copy of the code above. We should use
-    //        polymorphism to make this better.
-    fn union_region_sets<T:copy>(
-        cx: @uctxt, set_a: uint, set_b: uint,
-        nxt: fn() -> ures<T>) -> ures<T> {
-
-        let rb = alt cx.st {
-            in_region_bindings(rb) { rb }
-            precise {
-                cx.tcx.sess.bug("attempted to unify two region sets without \
-                                 a set of region bindings present");
-            }
-        };
-        ufind::grow(rb.sets, uint::max(set_a, set_b) + 1u);
-        let root_a = ufind::find(rb.sets, set_a);
-        let root_b = ufind::find(rb.sets, set_b);
-
-        let replace_region = (
-            fn@(rb: @region_bindings, r: region) {
-                ufind::union(rb.sets, set_a, set_b);
-                let root_c: uint = ufind::find(rb.sets, set_a);
-                smallintmap::insert(rb.regions, root_c, r);
-            }
-        );
-
-        alt smallintmap::find(rb.regions, root_a) {
-          none {
-            alt smallintmap::find(rb.regions, root_b) {
-              none { ufind::union(rb.sets, set_a, set_b); ret nxt(); }
-              some(r_b) { replace_region(rb, r_b); ret nxt(); }
-            }
-          }
-          some(r_a) {
-            alt smallintmap::find(rb.regions, root_b) {
-              none { replace_region(rb, r_a); ret nxt(); }
-              some(r_b) {
-                ret unify_regions(cx, r_a, r_b) {|r_c|
-                    replace_region(rb, r_c);
-                    nxt()
-                };
-              }
-            }
-          }
-        }
-    }
-
-    fn record_region_binding<T:copy>(
-        cx: @uctxt, key: uint,
-        r: region,
-        nxt: fn(region) -> ures<T>) -> ures<T> {
-
-        let rb = alt cx.st {
-            in_region_bindings(rb) { rb }
-            precise { fail; }
-        };
-
-        ufind::grow(rb.sets, key + 1u);
-        let root = ufind::find(rb.sets, key);
-        let mut result_region = r;
-        alt smallintmap::find(rb.regions, root) {
-          some(old_region) {
-            alt unify_regions(cx, old_region, r, {|v| ok(v)}) {
-              ok(unified_region) { result_region = unified_region; }
-              err(e) { ret err(e); }
-            }
-          }
-          none {/* fall through */ }
-        }
-        smallintmap::insert(rb.regions, root, result_region);
-
-        // FIXME: This should be re_var instead.
-        ret nxt(re_param(key));
-    }
-
-    fn unify_regions<T:copy>(
-            _cx: @uctxt, _e_region: region, _a_region: region,
-            _nxt: fn(region) -> ures<T>) -> ures<T> {
-        fail;   // unused
-    }
-}
-
 fn type_err_to_str(cx: ctxt, err: type_err) -> str {
     alt err {
       terr_mismatch { ret "types differ"; }
@@ -1995,14 +1905,6 @@ fn type_err_to_str(cx: ctxt, err: type_err) -> str {
     }
 }
 
-// Replaces type parameters in the given type using the given list of
-// substitions.
-fn substitute_type_params(cx: ctxt, substs: [ty::t], typ: t) -> t {
-    if !type_has_params(typ) { ret typ; }
-    // Precondition? idx < vec::len(substs)
-    fold_ty(cx, fm_param({|idx, _id| substs[idx]}), typ)
-}
-
 fn def_has_ty_params(def: ast::def) -> bool {
     alt def {
       ast::def_fn(_, _) | ast::def_variant(_, _) | ast::def_class(_)
diff --git a/src/rustc/middle/typeck.rs b/src/rustc/middle/typeck.rs
index feb70cff859..9fcef505586 100644
--- a/src/rustc/middle/typeck.rs
+++ b/src/rustc/middle/typeck.rs
@@ -11,6 +11,7 @@ import pat_util::*;
 import middle::ty;
 import middle::ty::{arg, field, node_type_table, mk_nil,
                     ty_param_bounds_and_ty, lookup_public_fields};
+import middle::ty::{ty_vid, region_vid, vid};
 import util::ppaux::ty_to_str;
 import std::smallintmap;
 import std::smallintmap::map;
@@ -49,13 +50,7 @@ type vtable_map = hashmap<ast::node_id, vtable_res>;
 
 type ty_table = hashmap<ast::def_id, ty::t>;
 
-// Used for typechecking the methods of an impl
-// first field is the self type, second is the ID for the "self" object
-// that's currently in scope
-enum self_info { self_impl(ty::t, ast::node_id) }
-
-type crate_ctxt = {mut self_infos: [self_info],
-                   impl_map: resolve::impl_map,
+type crate_ctxt = {impl_map: resolve::impl_map,
                    method_map: method_map,
                    vtable_map: vtable_map,
                    // Not at all sure it's right to put these here
@@ -73,15 +68,16 @@ type fn_ctxt =
     // var_bindings, locals and next_var_id are shared
     // with any nested functions that capture the environment
     // (and with any functions whose environment is being captured).
-    {ret_ty: ty::t,
+    {self_ty: option<ty::t>,
+     ret_ty: ty::t,
      // Used by loop bodies that return from the outer function
      indirect_ret_ty: option<ty::t>,
      purity: ast::purity,
      proto: ast::proto,
      infcx: infer::infer_ctxt,
-     locals: hashmap<ast::node_id, int>,
-     next_var_id: @mut int,
-     next_region_var_id: @mut int,
+     locals: hashmap<ast::node_id, ty_vid>,
+     next_var_id: @mut uint,
+     next_region_var_id: @mut uint,
 
      // While type checking a function, the intermediate types for the
      // expressions, blocks, and so forth contained within the function are
@@ -114,21 +110,14 @@ type fn_ctxt =
 // Determines whether the given node ID is a use of the def of
 // the self ID for the current method, if there is one
 fn self_ref(fcx: @fn_ctxt, id: ast::node_id) -> bool {
-    let node_def = alt fcx.ccx.tcx.def_map.find(id) {
-            none { ret false; }
-            some(d) { d } };
-    alt get_self_info(fcx.ccx) {
-       some(self_impl(_, slf_def)) {
-           alt node_def {
-                   ast::def_self(slf_actual) { slf_def == slf_actual }
-                   _ { false }
-           }
-       }
-       none { false }
+    // check what def `id` was resolved to (if anything)
+    alt fcx.ccx.tcx.def_map.find(id) {
+      some(ast::def_self(_)) { true }
+      _ { false }
     }
 }
 
-fn lookup_local(fcx: @fn_ctxt, sp: span, id: ast::node_id) -> int {
+fn lookup_local(fcx: @fn_ctxt, sp: span, id: ast::node_id) -> ty_vid {
     alt fcx.locals.find(id) {
       some(x) { x }
       _ {
@@ -163,12 +152,12 @@ fn ty_param_bounds_and_ty_for_def(fcx: @fn_ctxt, sp: span, defn: ast::def) ->
         ret {bounds: @[], ty: typ};
       }
       ast::def_self(_) {
-        alt get_self_info(fcx.ccx) {
-          some(self_impl(impl_t,_)) {
-            ret {bounds: @[], ty: impl_t};
+        alt fcx.self_ty {
+          some(self_ty) {
+            ret {bounds: @[], ty: self_ty};
           }
           none {
-              fcx.ccx.tcx.sess.span_bug(sp, "def_self with no self_info");
+              fcx.ccx.tcx.sess.span_bug(sp, "def_self with no self_ty");
           }
         }
       }
@@ -369,14 +358,16 @@ fn ast_ty_to_ty(tcx: ty::ctxt, mode: mode, &&ast_ty: @ast::ty) -> ty::t {
             ty::mk_ptr(tcx, ast_mt_to_mt(tcx, mode, mt))
           }
           ast::ty_rptr(region, mt) {
-            let region = alt region.node {
-                ast::re_inferred { ty::re_inferred }
-                ast::re_self { ty::re_self }
-                ast::re_named(_) {
-                    tcx.region_map.ast_type_to_region.get(region.id)
-                }
+            let r = alt region.node {
+              ast::re_inferred {
+                // this must be replaced later by a fixup_regions() pass
+                ty::re_default
+              }
+              ast::re_self | ast::re_named(_) {
+                tcx.region_map.ast_type_to_region.get(region.id)
+              }
             };
-            ty::mk_rptr(tcx, region, ast_mt_to_mt(tcx, mode, mt))
+            ty::mk_rptr(tcx, r, ast_mt_to_mt(tcx, mode, mt))
           }
           ast::ty_tup(fields) {
             let flds = vec::map(fields, bind do_ast_ty_to_ty(tcx, mode, _));
@@ -554,32 +545,75 @@ fn ty_of_native_item(tcx: ty::ctxt, mode: mode, it: @ast::native_item)
 
 type next_region_param_id = { mut id: uint };
 
-fn fixup_regions(tcx: ty::ctxt, next_region_param_id: next_region_param_id,
-                 ty: ty::t) -> ty::t {
-    let cur_region_param = @mut next_region_param_id.id;
-    ret ty::fold_ty(tcx, ty::fm_rptr({|region, under_rptr|
-        alt region {
-            ty::re_inferred {
-                if !under_rptr {
-                    *cur_region_param = next_region_param_id.id;
-                    next_region_param_id.id += 1u;
-                }
-                ty::re_param(*cur_region_param)
+// fn replace_inferred(tcx: ty::ctxt, ty: ty::t,
+//                     rop: fn() -> ty::region) -> ty::t {
+//     let tb = ty::get(ty);
+//     if !tb.has_rptrs { ret ty; }
+//     alt tb.struct {
+//       // Replace re_inferred that are nested underneath
+//       // a top-level region ptr with the region ptr itself.
+//       ty::ty_rptr(ty::re_inferred, ty1) {
+//         let r = rop();
+//         ty::mk_rptr(r, replace_inferred(tcx, ty1) {|| r })
+//       }
+//       ty::ty_rptr(r, ty1) {
+//         ty::mk_rptr(r, replace_inferred(tcx, ty1) {|| r })
+//       }
+//
+//       // Do not replace inferred ptrs that appear within fn(...) types, as
+//       // those are bound by the function.
+//       ty::ty_fn(f) {
+//         ty
+//       }
+//
+//       // Otherwise just map.
+//       sty {
+//         ty::fold_sty_to_ty(tcx, sty) {|t|
+//           replace_inferred(tcx, with_r, t) }
+//       }
+//     }
+// }
+
+fn replace_default_region(tcx: ty::ctxt,
+                          with_region: ty::region,
+                          ty: ty::t) -> ty::t {
+    let mut last_region = with_region;
+    ret ty::fold_region(tcx, ty) {|region, under_rptr|
+        if !under_rptr {
+            last_region = alt region {
+              ty::re_default { with_region }
+              _ { region }
             }
-            _ { region }
         }
-    }, false), ty);
+        last_region
+   };
+}
+
+fn default_region_to_bound_anon(tcx: ty::ctxt, ty: ty::t) -> ty::t {
+    replace_default_region(tcx, ty::re_bound(ty::br_anon), ty)
+}
+
+fn default_region_to_bound_self(tcx: ty::ctxt, ty: ty::t) -> ty::t {
+    replace_default_region(tcx, ty::re_bound(ty::br_self), ty)
 }
 
 fn fixup_regions_to_block(tcx: ty::ctxt, ty: ty::t, ast_ty: @ast::ty)
         -> ty::t {
     let region = tcx.region_map.ast_type_to_inferred_region.get(ast_ty.id);
-    ret ty::fold_ty(tcx, ty::fm_rptr({|this_region, _under_rptr|
-        alt this_region {
-            ty::re_inferred { region }
-            _ { this_region }
+    replace_default_region(tcx, region, ty)
+}
+
+fn replace_bound_regions_with_free_regions(
+    tcx: ty::ctxt,
+    id: ast::node_id,
+    ty: ty::t) -> ty::t {
+
+    ty::fold_region(tcx, ty) {|region, _under_rptr|
+        alt region {
+          ty::re_bound(br) { ty::re_free(id, br) }
+          _ { region }
         }
-    }, false), ty);
+    }
 }
 
 fn ty_of_arg(tcx: ty::ctxt, mode: mode, a: ast::arg) -> ty::arg {
@@ -614,38 +648,16 @@ fn ty_of_fn_decl(tcx: ty::ctxt,
                  mode: mode,
                  proto: ast::proto,
                  decl: ast::fn_decl) -> ty::fn_ty {
-    let mut has_regions: bool = false;
-    let mut max_region_param: @mut uint = @mut 0u;
-
-    let mut input_tys = vec::map(decl.inputs) {|a|
+    let input_tys = vec::map(decl.inputs) {|a|
         let arg_ty = ty_of_arg(tcx, mode, a);
-
-        if ty::type_has_rptrs(arg_ty.ty) {
-            has_regions = true;
-            let _ = ty::fold_ty(tcx, ty::fm_rptr({|r, _under_rptr|
-                alt r {
-                    ty::re_param(n) {
-                        *max_region_param = uint::max(n, *max_region_param);
-                    }
-                    _ { /* no-op */ }
-                };
-                r
-            }, false), arg_ty.ty);
-        }
-
-        arg_ty
+        {ty: default_region_to_bound_anon(tcx, arg_ty.ty)
+         with arg_ty}
     };
 
-    let mut output_ty = ast_ty_to_ty(tcx, mode, decl.output);
-
-    if has_regions {
-        let next_region_param_id = { mut id: *max_region_param };
-        input_tys = vec::map(input_tys, {|input_ty|
-            {ty: fixup_regions(tcx, next_region_param_id, input_ty.ty)
-             with input_ty}
-        });
-        output_ty = fixup_regions(tcx, next_region_param_id, output_ty);
-    }
+    let output_ty = {
+        let t = ast_ty_to_ty(tcx, mode, decl.output);
+        default_region_to_bound_anon(tcx, t)
+    };
 
     let out_constrs = vec::map(decl.constraints) {|constr|
         ty::ast_constr_to_constr(tcx, constr)
@@ -745,6 +757,7 @@ fn ast_ty_to_ty_crate_infer(ccx: @crate_ctxt, &&ast_ty: @ast::ty) ->
 
 // Functions that write types into the node type table
 fn write_ty_to_tcx(tcx: ty::ctxt, node_id: ast::node_id, ty: ty::t) {
+    #debug["write_ty_to_tcx(%d, %s)", node_id, ty_to_str(tcx, ty)];
     smallintmap::insert(*tcx.node_types, node_id as uint, ty);
 }
 fn write_substs_to_tcx(tcx: ty::ctxt, node_id: ast::node_id,
@@ -763,6 +776,9 @@ fn write_ty_substs_to_tcx(tcx: ty::ctxt, node_id: ast::node_id, ty: ty::t,
 impl methods for @fn_ctxt {
     fn tcx() -> ty::ctxt { self.ccx.tcx }
     fn tag() -> str { #fmt["%x", ptr::addr_of(*self) as uint] }
+    fn ty_to_str(t: ty::t) -> str {
+        ty_to_str(self.ccx.tcx, resolve_type_vars_if_possible(self, t))
+    }
     fn write_ty(node_id: ast::node_id, ty: ty::t) {
         #debug["write_ty(%d, %s) in fcx %s",
                node_id, ty_to_str(self.tcx(), ty), self.tag()];
@@ -888,7 +904,7 @@ enum self_subst { self_param(ty::t, @fn_ctxt, span), self_full(ty::t, uint) }
 fn fixup_self_in_method_ty(cx: ty::ctxt, mty: ty::t, m_substs: [ty::t],
                            self: self_subst) -> ty::t {
     if ty::type_has_vars(mty) {
-        ty::fold_ty(cx, ty::fm_general(fn@(t: ty::t) -> ty::t {
+        ty::fold_ty(cx, mty) {|t|
             alt ty::get(t).struct {
               ty::ty_self(tps) {
                 if vec::len(tps) > 0u {
@@ -931,20 +947,32 @@ fn fixup_self_in_method_ty(cx: ty::ctxt, mty: ty::t, m_substs: [ty::t],
               }
               _ { t }
             }
-        }), mty)
+        }
     } else { mty }
 }
 
-// Mangles an iface method ty to instantiate its `self` region.
-fn fixup_self_region_in_method_ty(fcx: @fn_ctxt, mty: ty::t,
-                                  self_expr: @ast::expr) -> ty::t {
-    let self_region = region_of(fcx, self_expr);
-    ty::fold_ty(fcx.ccx.tcx, ty::fm_rptr({|r, _under_rptr|
+// Replaces all occurrences of the `self` region with `with_region`.  Note
+// that we descend into `fn()` types here, because `fn()` does not bind the
+// `self` region.
+fn replace_self_region(tcx: ty::ctxt, with_region: ty::region,
+                       ty: ty::t) -> ty::t {
+
+   ty::fold_region(tcx, ty) {|r, _under_rptr|
+       alt r {
+           ty::re_bound(re_self) { with_region }
+           _ { r }
+       }
+   }
+}
+
+fn instantiate_bound_regions(tcx: ty::ctxt, region: ty::region, &&ty: ty::t)
+        -> ty::t {
+    ty::fold_region(tcx, ty) {|r, _under_rptr|
         alt r {
-            ty::re_self { self_region }
-            _ { r }
+          ty::re_bound(_) { region }
+          _ { r }
         }
-    }, false), mty)
+    }
 }
 
 // Item collection - a pair of bootstrap passes:
@@ -972,12 +1000,13 @@ mod collect {
                 // should be called to resolve named types.
                 let mut args: [arg] = [];
                 for va: ast::variant_arg in variant.node.args {
-                    let mut arg_ty = ast_ty_to_ty(tcx, m_collect, va.ty);
-                    if ty::type_has_rptrs(arg_ty) {
-                        let next_region_param_id = { mut id: 0u };
-                        arg_ty = fixup_regions(tcx, next_region_param_id,
-                                               arg_ty);
-                    }
+                    let arg_ty = {
+                        // NDM We need BOUNDS here.  It should be that this
+                        // yields a type like "foo &anon".  Basically every
+                        // nominal type is going to require a region bound.
+                        let arg_ty = ast_ty_to_ty(tcx, m_collect, va.ty);
+                        default_region_to_bound_anon(tcx, arg_ty)
+                    };
 
                     args += [{mode: ast::expl(ast::by_copy), ty: arg_ty}];
                 }
@@ -1312,7 +1341,7 @@ mod demand {
        ty_param_substs_and_ty {
 
         let mut ty_param_substs: [mut ty::t] = [mut];
-        let mut ty_param_subst_var_ids: [int] = [];
+        let mut ty_param_subst_var_ids: [ty_vid] = [];
         for ty_param_subst: ty::t in ty_param_substs_0 {
             // Generate a type variable and unify it with the type parameter
             // substitution. We will then pull out these type variables.
@@ -1323,10 +1352,10 @@ mod demand {
         }
 
         fn mk_result(fcx: @fn_ctxt, result_ty: ty::t,
-                     ty_param_subst_var_ids: [int]) ->
+                     ty_param_subst_var_ids: [ty_vid]) ->
            ty_param_substs_and_ty {
             let mut result_ty_param_substs: [ty::t] = [];
-            for var_id: int in ty_param_subst_var_ids {
+            for var_id in ty_param_subst_var_ids {
                 let tp_subst = ty::mk_var(fcx.ccx.tcx, var_id);
                 result_ty_param_substs += [tp_subst];
             }
@@ -1339,17 +1368,15 @@ mod demand {
             ret mk_result(fcx, expected, ty_param_subst_var_ids);
           }
           result::err(err) {
-            let e_err = resolve_type_vars_if_possible(fcx, expected);
-            let a_err = resolve_type_vars_if_possible(fcx, actual);
             fcx.ccx.tcx.sess.span_err(sp,
                                       "mismatched types: expected `" +
-                                          ty_to_str(fcx.ccx.tcx, e_err) +
-                                          "` but found `" +
-                                          ty_to_str(fcx.ccx.tcx, a_err) +
-                                          "` (" +
-                                          ty::type_err_to_str(fcx.ccx.tcx,
-                                                              err) +
-                                          ")");
+                                      fcx.ty_to_str(expected) +
+                                      "` but found `" +
+                                      fcx.ty_to_str(actual) +
+                                      "` (" +
+                                      ty::type_err_to_str(
+                                          fcx.ccx.tcx, err) +
+                                      ")");
             ret mk_result(fcx, expected, ty_param_subst_var_ids);
           }
         }
@@ -1403,16 +1430,13 @@ mod writeback {
         if !ty::type_has_vars(typ) { ret some(typ); }
         alt infer::fixup_vars(fcx.infcx, typ) {
           result::ok(new_type) { ret some(new_type); }
-          result::err(-1) {
-            fcx.ccx.tcx.sess.span_err(
-                sp,
-                "can not instantiate infinite type");
-            ret none;
-          }
-          result::err(vid) {
+          result::err(e) {
             if !fcx.ccx.tcx.sess.has_errors() {
-                fcx.ccx.tcx.sess.span_err(sp, "cannot determine a type \
-                                               for this expression");
+                fcx.ccx.tcx.sess.span_err(
+                    sp,
+                    #fmt["cannot determine a type \
+                          for this expression: %s",
+                         infer::fixup_err_to_str(e)])
             }
             ret none;
           }
@@ -1421,13 +1445,16 @@ mod writeback {
     fn resolve_type_vars_for_node(wbcx: wb_ctxt, sp: span, id: ast::node_id)
         -> option<ty::t> {
         let fcx = wbcx.fcx, tcx = fcx.ccx.tcx;
-        alt resolve_type_vars_in_type(fcx, sp, fcx.node_ty(id)) {
+        let n_ty = fcx.node_ty(id);
+        alt resolve_type_vars_in_type(fcx, sp, n_ty) {
           none {
             wbcx.success = false;
             ret none;
           }
 
           some(t) {
+            #debug["resolve_type_vars_for_node(id=%d, n_ty=%s, t=%s)",
+                   id, ty_to_str(tcx, n_ty), ty_to_str(tcx, t)];
             write_ty_to_tcx(tcx, id, t);
             alt fcx.opt_node_ty_substs(id) {
               some(substs) {
@@ -1514,9 +1541,9 @@ mod writeback {
         resolve_type_vars_for_node(wbcx, p.span, p.id);
         #debug["Type for pattern binding %s (id %d) resolved to %s",
                pat_to_str(p), p.id,
-               ty_to_str(wbcx.fcx.ccx.tcx,
-                         ty::node_id_to_type(wbcx.fcx.ccx.tcx,
-                                             p.id))];
+               wbcx.fcx.ty_to_str(
+                   ty::node_id_to_type(wbcx.fcx.ccx.tcx,
+                                       p.id))];
         visit::visit_pat(p, wbcx, v);
     }
     fn visit_local(l: @ast::local, wbcx: wb_ctxt, v: wb_vt) {
@@ -1526,19 +1553,15 @@ mod writeback {
           result::ok(lty) {
             #debug["Type for local %s (id %d) resolved to %s",
                    pat_to_str(l.node.pat), l.node.id,
-                   ty_to_str(wbcx.fcx.ccx.tcx, lty)];
+                   wbcx.fcx.ty_to_str(lty)];
             write_ty_to_tcx(wbcx.fcx.ccx.tcx, l.node.id, lty);
           }
-          result::err(-1) {
+          result::err(e) {
             wbcx.fcx.ccx.tcx.sess.span_err(
                 l.span,
-                "this local variable has a type of infinite size");
-            wbcx.success = false;
-          }
-          result::err(_) {
-            wbcx.fcx.ccx.tcx.sess.span_err(l.span,
-                                           "cannot determine a type \
-                                                for this local variable");
+                #fmt["cannot determine a type \
+                      for this local variable: %s",
+                     infer::fixup_err_to_str(e)]);
             wbcx.success = false;
           }
         }
@@ -1629,8 +1652,8 @@ fn check_intrinsic_type(tcx: ty::ctxt, it: @ast::native_item) {
 // for them before typechecking the function.
 type gather_result =
     {infcx: infer::infer_ctxt,
-     locals: hashmap<ast::node_id, int>,
-     next_var_id: @mut int};
+     locals: hashmap<ast::node_id, ty_vid>,
+     next_var_id: @mut uint};
 
 // Used only as a helper for check_fn.
 fn gather_locals(ccx: @crate_ctxt,
@@ -1641,8 +1664,8 @@ fn gather_locals(ccx: @crate_ctxt,
     let {infcx, locals, nvi} = alt old_fcx {
       none {
         {infcx: infer::new_infer_ctxt(ccx.tcx),
-         locals: int_hash::<int>(),
-         nvi: @mut 0}
+         locals: int_hash(),
+         nvi: @mut 0u}
       }
       some(fcx) {
         {infcx: fcx.infcx,
@@ -1652,10 +1675,12 @@ fn gather_locals(ccx: @crate_ctxt,
     };
     let tcx = ccx.tcx;
 
-    let next_var_id = fn@() -> int { let rv = *nvi; *nvi += 1; ret rv; };
+    let next_var_id = fn@() -> uint {
+        let rv = *nvi; *nvi += 1u; ret rv;
+    };
 
     let assign = fn@(nid: ast::node_id, ty_opt: option<ty::t>) {
-        let var_id = next_var_id();
+        let var_id = ty_vid(next_var_id());
         locals.insert(nid, var_id);
         alt ty_opt {
           none {/* nothing to do */ }
@@ -1668,8 +1693,8 @@ fn gather_locals(ccx: @crate_ctxt,
     // Add formal parameters.
     vec::iter2(arg_tys, decl.inputs) {|arg_ty, input|
         assign(input.id, some(arg_ty));
-        #debug["Argument %s is assigned to <T%d>",
-               input.ident, locals.get(input.id)];
+        #debug["Argument %s is assigned to %s",
+               input.ident, locals.get(input.id).to_str()];
     }
 
     // Add explicitly-declared locals.
@@ -1684,8 +1709,9 @@ fn gather_locals(ccx: @crate_ctxt,
         }
 
         assign(local.node.id, local_ty_opt);
-        #debug["Local variable %s is assigned to <T%d>",
-               pat_to_str(local.node.pat), locals.get(local.node.id)];
+        #debug["Local variable %s is assigned to %s",
+               pat_to_str(local.node.pat),
+               locals.get(local.node.id).to_str()];
         visit::visit_local(local, e, v);
     };
 
@@ -1695,8 +1721,9 @@ fn gather_locals(ccx: @crate_ctxt,
           ast::pat_ident(path, _)
           if !pat_util::pat_is_variant(ccx.tcx.def_map, p) {
             assign(p.id, none);
-            #debug["Pattern binding %s is assigned to <T%d>",
-                   path.node.idents[0], locals.get(p.id)];
+            #debug["Pattern binding %s is assigned to %s",
+                   path.node.idents[0],
+                   locals.get(p.id).to_str()];
           }
           _ {}
         }
@@ -1754,7 +1781,7 @@ fn count_region_params(ty: ty::t) -> uint {
     let count = @mut 0u;
     ty::walk_ty(ty) {|ty|
         alt ty::get(ty).struct {
-            ty::ty_rptr(ty::re_param(param_id), _) {
+            ty::ty_rptr(ty::re_bound(ty::br_param(param_id, _)), _) {
                 if param_id > *count {
                     *count = param_id;
                 }
@@ -1765,49 +1792,57 @@ fn count_region_params(ty: ty::t) -> uint {
     ret *count;
 }
 
-// Replaces self, caller, or inferred regions in the given type with the given
-// region.
-fn instantiate_self_regions(tcx: ty::ctxt, region: ty::region, &&ty: ty::t)
-        -> ty::t {
-    if ty::type_has_rptrs(ty) {
-        ty::fold_ty(tcx, ty::fm_rptr({|r, _under_rptr|
-            alt r {
-                ty::re_inferred | ty::re_self | ty::re_param(_) { region }
-                _ { r }
-            }
-        }, false), ty)
-    } else {
-        ty
-    }
-}
-
-type region_env = smallintmap::smallintmap<int>;
+type region_env = hashmap<ty::bound_region, region_vid>;
 
 fn region_env() -> @region_env {
-    ret @smallintmap::mk::<int>();
+    ret @ty::br_hashmap();
 }
 
 // Replaces all region parameters in the given type with region variables.
-// This is used when typechecking function calls, bind expressions, and method
-// calls.
-fn universally_quantify_regions(fcx: @fn_ctxt, ty: ty::t) -> ty::t {
-    if ty::type_has_rptrs(ty) {
-        let renv = region_env();
-        ty::fold_ty(fcx.ccx.tcx, ty::fm_rptr({|r, _under_rptr|
-            alt r {
-                ty::re_param(param_id) {
-                    alt smallintmap::find(*renv, param_id) {
-                        some(var_id) { ty::re_var(var_id as uint) }
-                        none {
-                            let var_id = next_region_var_id(fcx);
-                            smallintmap::insert(*renv, param_id, var_id);
-                            ty::re_var(var_id as uint)
-                        }
-                    }
-                }
-                _ { r }
+// Does not descend into fn types.  This is used when deciding whether an impl
+// applies at a given call site.  See also universally_quantify_before_call().
+fn universally_quantify_regions(fcx: @fn_ctxt, renv: @region_env,
+                                ty: ty::t) -> ty::t {
+    ty::fold_region(fcx.ccx.tcx, ty) {|r, _under_rptr|
+        alt r {
+          ty::re_bound(br) {
+            alt (*renv).find(br) {
+              some(var_id) { ty::re_var(var_id) }
+              none {
+                let var_id = next_region_var_id(fcx);
+                (*renv).insert(br, var_id);
+                ty::re_var(var_id)
+              }
             }
-        }, true), ty)
+          }
+          _ { r }
+        }
+    }
+}
+
+// Expects a function type.  Replaces all region parameters in the arguments
+// and return type with fresh region variables. This is used when typechecking
+// function calls, bind expressions, and method calls.
+fn universally_quantify_before_call(
+    fcx: @fn_ctxt, renv: @region_env, ty: ty::t) -> ty::t {
+    if ty::type_has_rptrs(ty) {
+        // This is subtle: we expect `ty` to be a function type, but
+        // fold_region() will not descend into function types.  As it happens
+        // we only want to descend 1 level, so we just bypass fold_region for
+        // the outer type and apply it to all of the types contained with
+        // `ty`.
+        alt ty::get(ty).struct {
+          sty @ ty::ty_fn(_) {
+            ty::fold_sty_to_ty(fcx.ccx.tcx, sty) {|t|
+                universally_quantify_regions(fcx, renv, t)
+            }
+          }
+          _ {
+            // if not a function type, we're gonna' report an error
+            // at some point, since the user is trying to call this thing
+            ty
+          }
+        }
     } else {
         ty
     }
@@ -1832,10 +1867,10 @@ fn check_pat_variant(pcx: pat_ctxt, pat: @ast::pat, path: @ast::path,
         // Get the number of arguments in this enum variant.
         let arg_types = variant_arg_types(pcx.fcx.ccx, pat.span,
                                           v_def_ids.var, expected_tps);
-        let arg_types = vec::map(arg_types,
-                             bind instantiate_self_regions(pcx.fcx.ccx.tcx,
-                                                           pcx.pat_region,
-                                                           _));
+        let arg_types = vec::map(arg_types) {|t|
+            // NDM---is this reasonable?
+            instantiate_bound_regions(pcx.fcx.ccx.tcx, pcx.pat_region, t)
+        };
         let subpats_len = subpats.len(), arg_len = arg_types.len();
         if arg_len > 0u {
             // N-ary variant.
@@ -1932,7 +1967,7 @@ fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
             tcx.sess.span_fatal
                 (pat.span,
                 #fmt["mismatched types: expected `%s` but found record",
-                                ty_to_str(tcx, expected)]);
+                     fcx.ty_to_str(expected)]);
           }
         };
         let f_count = vec::len(fields);
@@ -1969,7 +2004,7 @@ fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
             tcx.sess.span_fatal
                 (pat.span,
                  #fmt["mismatched types: expected `%s`, found tuple",
-                        ty_to_str(tcx, expected)]);
+                      fcx.ty_to_str(expected)]);
           }
         };
         let e_count = vec::len(elts);
@@ -1994,10 +2029,11 @@ fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
             fcx.write_ty(pat.id, expected);
           }
           _ {
-            tcx.sess.span_fatal(pat.span,
-                                        "mismatched types: expected `" +
-                                            ty_to_str(tcx, expected) +
-                                            "` found box");
+            tcx.sess.span_fatal(
+                pat.span,
+                "mismatched types: expected `" +
+                pcx.fcx.ty_to_str(expected) +
+                "` found box");
           }
         }
       }
@@ -2008,10 +2044,11 @@ fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
             fcx.write_ty(pat.id, expected);
           }
           _ {
-            tcx.sess.span_fatal(pat.span,
-                                        "mismatched types: expected `" +
-                                            ty_to_str(tcx, expected) +
-                                            "` found uniq");
+            tcx.sess.span_fatal(
+                pat.span,
+                "mismatched types: expected `" +
+                pcx.fcx.ty_to_str(expected) +
+                "` found uniq");
           }
         }
       }
@@ -2146,7 +2183,8 @@ fn lookup_method(fcx: @fn_ctxt, expr: @ast::expr, node_id: ast::node_id,
         }
         if ty::type_has_rptrs(ty::ty_fn_ret(fty)) {
             let fty = fcx.node_ty(node_id);
-            let fty = fixup_self_region_in_method_ty(fcx, fty, expr);
+            let self_region = region_of(fcx, expr);
+            let fty = replace_self_region(fcx.ccx.tcx, self_region, fty);
             fcx.write_ty(node_id, fty);
         }
         some(origin)
@@ -2213,9 +2251,7 @@ fn lookup_method_inner(fcx: @fn_ctxt, expr: @ast::expr,
     let tcx = fcx.ccx.tcx;
 
     #debug["lookup_method_inner: expr=%s name=%s ty=%s",
-           expr_to_str(expr),
-           name,
-           ty_to_str(fcx.ccx.tcx, ty)];
+           expr_to_str(expr), name, fcx.ty_to_str(ty)];
 
     // First, see whether this is an interface-bounded parameter
     alt ty::get(ty).struct {
@@ -2297,14 +2333,17 @@ fn lookup_method_inner(fcx: @fn_ctxt, expr: @ast::expr,
                     };
 
                     // Here "self" refers to the callee side...
-                    let next_rid = count_region_params(self_ty);
-                    self_ty = instantiate_self_regions(fcx.ccx.tcx,
-                                                       ty::re_param(next_rid),
-                                                       self_ty);
-                    self_ty = universally_quantify_regions(fcx, self_ty);
+                    //let next_rid = count_region_params(self_ty);
+                    //self_ty = instantiate_bound_regions(
+                    //    fcx.ccx.tcx,
+                    //    ty::re_bound(ty::br_param(next_rid)),
+                    //    self_ty);
+                    self_ty = universally_quantify_regions(
+                        fcx, region_env(), self_ty);
 
                     // ... and "ty" refers to the caller side.
-                    let ty = universally_quantify_regions(fcx, ty);
+                    let ty = universally_quantify_regions(
+                        fcx, region_env(), ty);
 
                     alt unify::unify(fcx, self_ty, ty) {
                       result::ok(_) {
@@ -2365,7 +2404,7 @@ fn region_of(fcx: @fn_ctxt, expr: @ast::expr) -> ty::region {
                 ast::def_upvar(local_id, _, _) {
                     let local_blocks = fcx.ccx.tcx.region_map.local_blocks;
                     let local_block_id = local_blocks.get(local_id);
-                    ret ty::re_block(local_block_id);
+                    ret ty::re_scope(local_block_id);
                 }
                 _ {
                     fcx.ccx.tcx.sess.span_unimpl(expr.span,
@@ -2394,7 +2433,7 @@ fn region_of(fcx: @fn_ctxt, expr: @ast::expr) -> ty::region {
         }
         _ {
             let blk_id = fcx.ccx.tcx.region_map.rvalue_to_block.get(expr.id);
-            ret ty::re_block(blk_id);
+            ret ty::re_scope(blk_id);
         }
     }
 }
@@ -2412,8 +2451,7 @@ fn check_expr_fn_with_unifier(fcx: @fn_ctxt,
                         ty_of_fn_decl(tcx, m_check_tyvar(fcx), proto, decl));
 
     #debug("check_expr_fn_with_unifier %s fty=%s",
-           expr_to_str(expr),
-           ty_to_str(tcx, fty));
+           expr_to_str(expr), fcx.ty_to_str(fty));
 
     fcx.write_ty(expr.id, fty);
 
@@ -2426,15 +2464,16 @@ fn check_expr_fn_with_unifier(fcx: @fn_ctxt,
     let ret_ty = ty::ty_fn_ret(fty);
     let arg_tys = vec::map(ty::ty_fn_args(fty)) {|a| a.ty };
 
-    check_fn(fcx.ccx, proto, decl, body,
-             ret_ty, arg_tys, is_loop_body, some(fcx));
+    check_fn(fcx.ccx, proto, decl, body, expr.id,
+             ret_ty, arg_tys, is_loop_body, some(fcx),
+             fcx.self_ty);
 }
 
 fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
                            expected: ty::t) -> bool {
 
-    #debug("typechecking expr %s",
-           syntax::print::pprust::expr_to_str(expr));
+    #debug("typechecking expr %d (%s)",
+           expr.id, syntax::print::pprust::expr_to_str(expr));
 
     // A generic function to factor out common logic from call and bind
     // expressions.
@@ -2442,7 +2481,9 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
         fcx: @fn_ctxt, sp: span, fty: ty::t,
         args: [option<@ast::expr>]) -> {fty: ty::t, bot: bool} {
 
-        let fty = universally_quantify_regions(fcx, fty);
+        let fty = universally_quantify_before_call(fcx, region_env(), fty);
+        #debug["check_call_or_bind: after universal quant., fty=%s",
+               fcx.ty_to_str(fty)];
         let sty = structure_of(fcx, sp, fty);
         // Grab the argument types
         let mut arg_tys = alt sty {
@@ -2451,7 +2492,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
             fcx.ccx.tcx.sess.span_fatal(sp, "mismatched types: \
                                              expected function or native \
                                              function but found "
-                                        + ty_to_str(fcx.ccx.tcx, fty))
+                                        + fcx.ty_to_str(fty))
           }
         };
 
@@ -2527,7 +2568,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
 
     // A generic function for checking call expressions
     fn check_call(fcx: @fn_ctxt, sp: span, f: @ast::expr, args: [@ast::expr])
-            -> bool {
+        -> {fty: ty::t, bot: bool} {
         let mut args_opt_0: [option<@ast::expr>] = [];
         for arg: @ast::expr in args {
             args_opt_0 += [some::<@ast::expr>(arg)];
@@ -2536,30 +2577,29 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
         let bot = check_expr(fcx, f);
 
         // Call the generic checker.
-        ret {
-            let fn_ty = fcx.expr_ty(f);
-            check_call_or_bind(fcx, sp, fn_ty, args_opt_0).bot | bot
-        };
+        let fn_ty = fcx.expr_ty(f);
+        let {fty, bot: bot1} = check_call_or_bind(fcx, sp, fn_ty, args_opt_0);
+        ret {fty: fty, bot: bot | bot1};
     }
 
     // A generic function for doing all of the checking for call expressions
     fn check_call_full(fcx: @fn_ctxt, sp: span, id: ast::node_id,
                        f: @ast::expr, args: [@ast::expr]) -> bool {
-        let mut bot = check_call(fcx, sp, f, args);
+        let {fty, bot} = check_call(fcx, sp, f, args);
+
         /* need to restrict oper to being an explicit expr_path if we're
         inside a pure function */
         require_pure_call(fcx.ccx, fcx.purity, f, sp);
 
         // Pull the return type out of the type of the function.
-        let fty = fcx.expr_ty(f);
-        let mut rt_1 = alt structure_of(fcx, sp, fty) {
+        let {rt, bot} = alt structure_of(fcx, sp, fty) {
           ty::ty_fn(f) {
-            bot |= f.ret_style == ast::noreturn;
-            f.output
+            {rt: f.output,
+             bot: bot | (f.ret_style == ast::noreturn)}
           }
           _ { fcx.ccx.tcx.sess.span_fatal(sp, "calling non-function"); }
         };
-        fcx.write_ty(id, rt_1);
+        fcx.write_ty(id, rt);
         ret bot;
     }
 
@@ -2709,7 +2749,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
         tcx.sess.span_err(
             ex.span, "binary operation " + ast_util::binop_to_str(op) +
             " cannot be applied to type `" +
-            ty_to_str(tcx, lhs_resolved_t) +
+            fcx.ty_to_str(lhs_resolved_t) +
             "`");
         (lhs_resolved_t, false)
     }
@@ -2720,7 +2760,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
           _ {
             fcx.ccx.tcx.sess.span_err(
                 ex.span, #fmt["cannot apply unary operator `%s` to type `%s`",
-                              op_str, ty_to_str(fcx.ccx.tcx, rhs_t)]);
+                              op_str, fcx.ty_to_str(rhs_t)]);
             rhs_t
           }
         }
@@ -2957,9 +2997,9 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
             let pcx = {
                 fcx: fcx,
                 map: pat_util::pat_id_map(tcx.def_map, arm.pats[0]),
-                alt_region: ty::re_block(parent_block),
-                block_region: ty::re_block(arm.body.node.id),
-                pat_region: ty::re_block(parent_block)
+                alt_region: ty::re_scope(parent_block),
+                block_region: ty::re_scope(arm.body.node.id),
+                pat_region: ty::re_scope(parent_block)
             };
 
             for p: @ast::pat in arm.pats {
@@ -3037,9 +3077,9 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
         // Call the generic checker.
         bot = check_expr(fcx, f);
 
-        let ccob_bot = {
+        let {fty, bot: ccob_bot} = {
             let fn_ty = fcx.expr_ty(f);
-            check_call_or_bind(fcx, expr.span, fn_ty, args).bot
+            check_call_or_bind(fcx, expr.span, fn_ty, args)
         };
         bot |= ccob_bot;
 
@@ -3047,7 +3087,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
 
         // Pull the argument and return types out.
         let mut proto, arg_tys, rt, cf, constrs;
-        alt structure_of(fcx, expr.span, fcx.expr_ty(f)) {
+        alt structure_of(fcx, expr.span, fty) {
           // FIXME:
           // probably need to munge the constrs to drop constraints
           // for any bound args
@@ -3352,28 +3392,28 @@ fn require_integral(fcx: @fn_ctxt, sp: span, t: ty::t) {
     if !type_is_integral(fcx, sp, t) {
         fcx.ccx.tcx.sess.span_err(sp, "mismatched types: expected \
                                        `integer` but found `"
-                                  + ty_to_str(fcx.ccx.tcx, t) + "`");
+                                  + fcx.ty_to_str(t) + "`");
     }
 }
 
-fn next_ty_var_id(fcx: @fn_ctxt) -> int {
+fn next_ty_var_id(fcx: @fn_ctxt) -> ty_vid {
     let id = *fcx.next_var_id;
-    *fcx.next_var_id += 1;
-    ret id;
+    *fcx.next_var_id += 1u;
+    ret ty_vid(id);
 }
 
 fn next_ty_var(fcx: @fn_ctxt) -> ty::t {
     ret ty::mk_var(fcx.ccx.tcx, next_ty_var_id(fcx));
 }
 
-fn next_region_var_id(fcx: @fn_ctxt) -> int {
+fn next_region_var_id(fcx: @fn_ctxt) -> region_vid {
     let id = *fcx.next_region_var_id;
-    *fcx.next_region_var_id += 1;
-    ret id;
+    *fcx.next_region_var_id += 1u;
+    ret region_vid(id);
 }
 
 fn next_region_var(fcx: @fn_ctxt) -> ty::region {
-    ret ty::re_var(next_region_var_id(fcx) as uint);
+    ret ty::re_var(next_region_var_id(fcx));
 }
 
 fn bind_params(fcx: @fn_ctxt, tp: ty::t, count: uint)
@@ -3382,10 +3422,6 @@ fn bind_params(fcx: @fn_ctxt, tp: ty::t, count: uint)
     {vars: vars, ty: ty::substitute_type_params(fcx.ccx.tcx, vars, tp)}
 }
 
-fn get_self_info(ccx: @crate_ctxt) -> option<self_info> {
-    ret vec::last_opt(ccx.self_infos);
-}
-
 fn check_decl_initializer(fcx: @fn_ctxt, nid: ast::node_id,
                           init: ast::initializer) -> bool {
     let lty = ty::mk_var(fcx.ccx.tcx, lookup_local(fcx, init.expr.span, nid));
@@ -3405,7 +3441,7 @@ fn check_decl_local(fcx: @fn_ctxt, local: @ast::local) -> bool {
     }
 
     let block_id = fcx.ccx.tcx.region_map.rvalue_to_block.get(local.node.id);
-    let region = ty::re_block(block_id);
+    let region = ty::re_scope(block_id);
     let pcx = {
         fcx: fcx,
         map: pat_util::pat_id_map(fcx.ccx.tcx.def_map, local.node.pat),
@@ -3498,14 +3534,15 @@ fn check_const(ccx: @crate_ctxt, _sp: span, e: @ast::expr, id: ast::node_id) {
     // and statement context for checking the initializer expression.
     let rty = ty::node_id_to_type(ccx.tcx, id);
     let fcx: @fn_ctxt =
-        @{ret_ty: rty,
+        @{self_ty: none,
+          ret_ty: rty,
           indirect_ret_ty: none,
           purity: ast::pure_fn,
           proto: ast::proto_box,
           infcx: infer::new_infer_ctxt(ccx.tcx),
-          locals: int_hash::<int>(),
-          next_var_id: @mut 0,
-          next_region_var_id: @mut 0,
+          locals: int_hash(),
+          next_var_id: @mut 0u,
+          next_region_var_id: @mut 0u,
           node_types: smallintmap::mk(),
           node_type_substs: map::int_hash(),
           ccx: ccx};
@@ -3534,14 +3571,15 @@ fn check_enum_variants(ccx: @crate_ctxt, sp: span, vs: [ast::variant],
     // and statement context for checking the initializer expression.
     let rty = ty::node_id_to_type(ccx.tcx, id);
     let fcx: @fn_ctxt =
-        @{ret_ty: rty,
+        @{self_ty: none,
+          ret_ty: rty,
           indirect_ret_ty: none,
           purity: ast::pure_fn,
           proto: ast::proto_box,
           infcx: infer::new_infer_ctxt(ccx.tcx),
-          locals: int_hash::<int>(),
-          next_var_id: @mut 0,
-          next_region_var_id: @mut 0,
+          locals: int_hash(),
+          next_var_id: @mut 0u,
+          next_region_var_id: @mut 0u,
           node_types: smallintmap::mk(),
           node_type_substs: map::int_hash(),
           ccx: ccx};
@@ -3709,22 +3747,41 @@ fn check_constraints(fcx: @fn_ctxt, cs: [@ast::constr], args: [ast::arg]) {
 fn check_bare_fn(ccx: @crate_ctxt,
                  decl: ast::fn_decl,
                  body: ast::blk,
-                 id: ast::node_id) {
+                 id: ast::node_id,
+                 self_ty: option<ty::t>) {
     let fty = ty::node_id_to_type(ccx.tcx, id);
     let ret_ty = ty::ty_fn_ret(fty);
     let arg_tys = vec::map(ty::ty_fn_args(fty)) {|a| a.ty };
-    check_fn(ccx, ast::proto_bare, decl, body,
-             ret_ty, arg_tys, false, none);
+    check_fn(ccx, ast::proto_bare, decl, body, id,
+             ret_ty, arg_tys, false, none, self_ty);
 }
 
 fn check_fn(ccx: @crate_ctxt,
             proto: ast::proto,
             decl: ast::fn_decl,
             body: ast::blk,
+            fid: ast::node_id,
             ret_ty: ty::t,
             arg_tys: [ty::t],
             indirect_ret: bool,
-            old_fcx: option<@fn_ctxt>) {
+            old_fcx: option<@fn_ctxt>,
+            self_ty: option<ty::t>) {
+
+    // See big comment in region.rs.
+    let arg_tys = arg_tys.map {|arg_ty|
+        replace_bound_regions_with_free_regions(ccx.tcx, fid, arg_ty)
+    };
+    let ret_ty =
+        replace_bound_regions_with_free_regions(ccx.tcx, fid, ret_ty);
+    let self_ty = option::map(self_ty) {|st|
+        replace_bound_regions_with_free_regions(ccx.tcx, fid, st)
+    };
+
+    #debug["check_fn(arg_tys=%?, ret_ty=%?, self_ty=%?)",
+           arg_tys.map {|a| ty_to_str(ccx.tcx, a) },
+           ty_to_str(ccx.tcx, ret_ty),
+           option::map(self_ty) {|st| ty_to_str(ccx.tcx, st) }];
+
     // If old_fcx is some(...), this is a block fn { |x| ... }.
     // In that case, the purity is inherited from the context.
     let {purity, node_types, node_type_substs} = alt old_fcx {
@@ -3750,14 +3807,15 @@ fn check_fn(ccx: @crate_ctxt,
         }
     } else { none };
     let fcx: @fn_ctxt =
-        @{ret_ty: ret_ty,
+        @{self_ty: self_ty,
+          ret_ty: ret_ty,
           indirect_ret_ty: indirect_ret_ty,
           purity: purity,
           proto: proto,
           infcx: gather_result.infcx,
           locals: gather_result.locals,
           next_var_id: gather_result.next_var_id,
-          next_region_var_id: @mut 0,
+          next_region_var_id: @mut 0u,
           node_types: node_types,
           node_type_substs: node_type_substs,
           ccx: ccx};
@@ -3791,8 +3849,8 @@ fn check_fn(ccx: @crate_ctxt,
     }
 }
 
-fn check_method(ccx: @crate_ctxt, method: @ast::method) {
-    check_bare_fn(ccx, method.decl, method.body, method.id);
+fn check_method(ccx: @crate_ctxt, method: @ast::method, self_ty: ty::t) {
+    check_bare_fn(ccx, method.decl, method.body, method.id, some(self_ty));
 }
 
 fn class_types(ccx: @crate_ctxt, members: [@ast::class_member]) -> class_map {
@@ -3816,9 +3874,7 @@ fn check_class_member(ccx: @crate_ctxt, class_t: ty::t,
     alt cm.node {
       ast::instance_var(_,t,_,_,_) { }
       ast::class_method(m) {
-          ccx.self_infos += [self_impl(class_t, m.self_id)];
-          check_method(ccx, m);
-          vec::pop(ccx.self_infos);
+          check_method(ccx, m, class_t);
       }
     }
 }
@@ -3828,20 +3884,18 @@ fn check_item(ccx: @crate_ctxt, it: @ast::item) {
       ast::item_const(_, e) { check_const(ccx, it.span, e, it.id); }
       ast::item_enum(vs, _) { check_enum_variants(ccx, it.span, vs, it.id); }
       ast::item_fn(decl, tps, body) {
-        check_bare_fn(ccx, decl, body, it.id);
+        check_bare_fn(ccx, decl, body, it.id, none);
       }
       ast::item_res(decl, tps, body, dtor_id, _) {
         check_instantiable(ccx.tcx, it.span, it.id);
-        check_bare_fn(ccx, decl, body, dtor_id);
+        check_bare_fn(ccx, decl, body, dtor_id, none);
       }
       ast::item_impl(tps, _, ty, ms) {
-        let mut self_ty = ast_ty_to_ty(ccx.tcx, m_check, ty);
-        let self_region = ty::re_self;
-        self_ty = instantiate_self_regions(ccx.tcx, self_region, self_ty);
+        let self_ty = ast_ty_to_ty(ccx.tcx, m_check, ty);
+        let self_region = ty::re_free(it.id, ty::br_self);
+        let self_ty = replace_self_region(ccx.tcx, self_region, self_ty);
         for m in ms {
-             ccx.self_infos += [self_impl(self_ty, m.id)];
-             check_method(ccx, m);
-             vec::pop(ccx.self_infos);
+            check_method(ccx, m, self_ty);
         }
       }
       ast::item_class(tps, members, ctor) {
@@ -3852,11 +3906,11 @@ fn check_item(ccx: @crate_ctxt, it: @ast::item) {
           // FIXME
           let class_ccx = @{enclosing_class_id:cid,
                             enclosing_class:members_info with *ccx};
-          class_ccx.self_infos += [self_impl(class_t, ctor.node.self_id)];
           // typecheck the ctor
           check_bare_fn(class_ccx, ctor.node.dec,
-                        ctor.node.body, ctor.node.id);
-          vec::pop(class_ccx.self_infos);
+                        ctor.node.body, ctor.node.id,
+                        some(class_t));
+
           // typecheck the members
           for m in members { check_class_member(class_ccx, class_t, m); }
       }
@@ -4057,13 +4111,12 @@ mod vtable {
         let tcx = fcx.ccx.tcx;
         alt infer::fixup_vars(fcx.infcx, ty) {
           result::ok(new_type) { new_type }
-          result::err(-1) {
-            tcx.sess.span_fatal(sp, "bounded type parameter with \
-                                     cyclic type");
-          }
-          result::err(vid) {
-            tcx.sess.span_fatal(sp, "could not determine a type for a \
-                                     bounded type parameter");
+          result::err(e) {
+            tcx.sess.span_fatal(
+                sp,
+                #fmt["cannot determine a type \
+                      for this bounded type parameter: %s",
+                     infer::fixup_err_to_str(e)])
           }
         }
     }
@@ -4153,8 +4206,7 @@ fn check_crate(tcx: ty::ctxt, impl_map: resolve::impl_map,
                crate: @ast::crate) -> (method_map, vtable_map) {
     collect::collect_item_types(tcx, crate);
 
-    let ccx = @{mut self_infos: [],
-                impl_map: impl_map,
+    let ccx = @{impl_map: impl_map,
                 method_map: std::map::int_hash(),
                 vtable_map: std::map::int_hash(),
                 enclosing_class_id: none,
diff --git a/src/rustc/util/ppaux.rs b/src/rustc/util/ppaux.rs
index 112308548de..2cb0fef1a90 100644
--- a/src/rustc/util/ppaux.rs
+++ b/src/rustc/util/ppaux.rs
@@ -10,21 +10,32 @@ import syntax::{ast, ast_util};
 import middle::ast_map;
 import driver::session::session;
 
+fn bound_region_to_str(_cx: ctxt, br: bound_region) -> str {
+    alt br {
+      br_anon          { "&" }
+      br_param(_, str) { #fmt["&%s.", str] }
+      br_self          { "&self." }
+    }
+}
+
 fn region_to_str(cx: ctxt, region: region) -> str {
     alt region {
-      re_block(node_id) {
+      re_scope(node_id) {
         alt cx.items.get(node_id) {
             ast_map::node_block(blk) {
-                #fmt("<block at %s>", codemap::span_to_str(blk.span,
+                #fmt("&<block at %s>.", codemap::span_to_str(blk.span,
                                                            cx.sess.codemap))
             }
             _ { cx.sess.bug("re_block refers to non-block") }
         }
       }
-      re_self       { "self" }
-      re_inferred   { "" }
-      re_param(id)  { #fmt("<P%u>", id) }    // TODO: do better than this
-      re_var(id)    { #fmt("<R%u>", id) }    // TODO: do better than this
+
+      re_bound(br) { bound_region_to_str(cx, br) }
+      re_free(id, br) { #fmt["{%d} %s", id, bound_region_to_str(cx, br)] }
+
+      // These two should not be seen by end-users (very often, anyhow):
+      re_var(id)    { #fmt("&%s.", id.to_str()) }
+      re_default    { "&(default)." }
     }
 }
 
@@ -122,7 +133,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> str {
       ty_box(tm) { "@" + mt_to_str(cx, tm) }
       ty_uniq(tm) { "~" + mt_to_str(cx, tm) }
       ty_ptr(tm) { "*" + mt_to_str(cx, tm) }
-      ty_rptr(r, tm) { "&" + region_to_str(cx, r) + "." + mt_to_str(cx, tm) }
+      ty_rptr(r, tm) { region_to_str(cx, r) + mt_to_str(cx, tm) }
       ty_vec(tm) { "[" + mt_to_str(cx, tm) + "]" }
       ty_type { "type" }
       ty_rec(elems) {
@@ -139,7 +150,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> str {
         fn_to_str(cx, f.proto, none, f.inputs, f.output, f.ret_style,
                   f.constraints)
       }
-      ty_var(v) { "<T" + int::str(v) + ">" }
+      ty_var(v) { v.to_str() }
       ty_param(id, _) {
         "'" + str::from_bytes([('a' as u8) + (id as u8)])
       }
diff --git a/src/test/compile-fail/occurs-check.rs b/src/test/compile-fail/occurs-check.rs
index 4c4cacb36e7..a802967bc7a 100644
--- a/src/test/compile-fail/occurs-check.rs
+++ b/src/test/compile-fail/occurs-check.rs
@@ -1,4 +1,4 @@
 fn main() {
-    let f; //! ERROR this local variable has a type of infinite size
+    let f; //! ERROR cyclic type of infinite size
     f = @f;
 }
diff --git a/src/test/run-pass/region-param.rs b/src/test/run-pass/region-param.rs
new file mode 100644
index 00000000000..9e483f063a2
--- /dev/null
+++ b/src/test/run-pass/region-param.rs
@@ -0,0 +1,15 @@
+fn region_identity(x: &r.uint) -> &r.uint { x }
+
+fn apply<T>(t: T, f: fn(T) -> T) -> T { f(t) }
+
+fn parameterized(x: &uint) -> uint {
+    let z = apply(x) {|y|
+        region_identity(y)
+    };
+    *z
+}
+
+fn main() {
+    let x = 3u;
+    assert parameterized(&x) == 3u;
+}
\ No newline at end of file
diff --git a/src/test/run-pass/regions-self-impls.rs b/src/test/run-pass/regions-self-impls.rs
index 4e0cd5b1aee..a587c19f38f 100644
--- a/src/test/run-pass/regions-self-impls.rs
+++ b/src/test/run-pass/regions-self-impls.rs
@@ -1,3 +1,6 @@
+// xfail-test
+// ^ handling of self is currently broken
+
 type clam = { chowder: &int };
 
 impl clam for clam {