From c5754f3971b4bb6ea1c9527863189792ab5ee336 Mon Sep 17 00:00:00 2001
From: Niko Matsakis <niko@alum.mit.edu>
Date: Fri, 12 Sep 2014 10:53:35 -0400
Subject: [PATCH] Guts of the new trait matching algorithm, not yet in use

---
 src/librustc/lib.rs                           |    1 +
 src/librustc/middle/lang_items.rs             |   11 +
 src/librustc/middle/subst.rs                  |   28 +-
 src/librustc/middle/traits/doc.rs             |  268 +++++
 src/librustc/middle/traits/fulfill.rs         |  250 ++++
 src/librustc/middle/traits/mod.rs             |  438 +++++++
 src/librustc/middle/traits/select.rs          | 1024 +++++++++++++++++
 src/librustc/middle/traits/util.rs            |  356 ++++++
 src/librustc/middle/ty.rs                     |  116 +-
 src/librustc/middle/ty_fold.rs                |   95 +-
 .../middle/typeck/infer/error_reporting.rs    |    7 +-
 src/librustc/middle/typeck/infer/mod.rs       |  161 ++-
 src/librustc/middle/typeck/infer/resolve.rs   |   27 +-
 src/librustc/middle/typeck/infer/skolemize.rs |  157 +++
 src/librustc/middle/typeck/infer/unify.rs     |   23 +
 15 files changed, 2856 insertions(+), 106 deletions(-)
 create mode 100644 src/librustc/middle/traits/doc.rs
 create mode 100644 src/librustc/middle/traits/fulfill.rs
 create mode 100644 src/librustc/middle/traits/mod.rs
 create mode 100644 src/librustc/middle/traits/select.rs
 create mode 100644 src/librustc/middle/traits/util.rs
 create mode 100644 src/librustc/middle/typeck/infer/skolemize.rs

diff --git a/src/librustc/lib.rs b/src/librustc/lib.rs
index fd643a70c7b..af3d19c4d2d 100644
--- a/src/librustc/lib.rs
+++ b/src/librustc/lib.rs
@@ -108,6 +108,7 @@ pub mod middle {
     pub mod save;
     pub mod stability;
     pub mod subst;
+    pub mod traits;
     pub mod trans;
     pub mod ty;
     pub mod ty_fold;
diff --git a/src/librustc/middle/lang_items.rs b/src/librustc/middle/lang_items.rs
index 24782240f06..1ea0681085b 100644
--- a/src/librustc/middle/lang_items.rs
+++ b/src/librustc/middle/lang_items.rs
@@ -85,6 +85,17 @@ impl LanguageItems {
         }
     }
 
+    pub fn from_builtin_kind(&self, bound: ty::BuiltinBound)
+                             -> Result<ast::DefId, String>
+    {
+        match bound {
+            ty::BoundSend => self.require(SendTraitLangItem),
+            ty::BoundSized => self.require(SizedTraitLangItem),
+            ty::BoundCopy => self.require(CopyTraitLangItem),
+            ty::BoundSync => self.require(SyncTraitLangItem),
+        }
+    }
+
     pub fn to_builtin_kind(&self, id: ast::DefId) -> Option<ty::BuiltinBound> {
         if Some(id) == self.send_trait() {
             Some(ty::BoundSend)
diff --git a/src/librustc/middle/subst.rs b/src/librustc/middle/subst.rs
index c1c23dff984..23f53d9b4ab 100644
--- a/src/librustc/middle/subst.rs
+++ b/src/librustc/middle/subst.rs
@@ -333,6 +333,16 @@ impl<T> VecPerParamSpace<T> {
         }
     }
 
+    fn new_internal(content: Vec<T>, type_limit: uint, self_limit: uint)
+                    -> VecPerParamSpace<T>
+    {
+        VecPerParamSpace {
+            type_limit: type_limit,
+            self_limit: self_limit,
+            content: content,
+        }
+    }
+
     pub fn sort(t: Vec<T>, space: |&T| -> ParamSpace) -> VecPerParamSpace<T> {
         let mut result = VecPerParamSpace::empty();
         for t in t.move_iter() {
@@ -448,13 +458,17 @@ impl<T> VecPerParamSpace<T> {
     }
 
     pub fn map<U>(&self, pred: |&T| -> U) -> VecPerParamSpace<U> {
-        // FIXME (#15418): this could avoid allocating the intermediate
-        // Vec's, but note that the values of type_limit and self_limit
-        // also need to be kept in sync during construction.
-        VecPerParamSpace::new(
-            self.get_slice(TypeSpace).iter().map(|p| pred(p)).collect(),
-            self.get_slice(SelfSpace).iter().map(|p| pred(p)).collect(),
-            self.get_slice(FnSpace).iter().map(|p| pred(p)).collect())
+        let result = self.iter().map(pred).collect();
+        VecPerParamSpace::new_internal(result,
+                                       self.type_limit,
+                                       self.self_limit)
+    }
+
+    pub fn map_move<U>(self, pred: |T| -> U) -> VecPerParamSpace<U> {
+        let (t, s, f) = self.split();
+        VecPerParamSpace::new(t.move_iter().map(|p| pred(p)).collect(),
+                              s.move_iter().map(|p| pred(p)).collect(),
+                              f.move_iter().map(|p| pred(p)).collect())
     }
 
     pub fn map_rev<U>(&self, pred: |&T| -> U) -> VecPerParamSpace<U> {
diff --git a/src/librustc/middle/traits/doc.rs b/src/librustc/middle/traits/doc.rs
new file mode 100644
index 00000000000..98db2263874
--- /dev/null
+++ b/src/librustc/middle/traits/doc.rs
@@ -0,0 +1,268 @@
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+/*!
+
+# TRAIT RESOLUTION
+
+This document describes the general process and points out some non-obvious
+things.
+
+## Major concepts
+
+Trait resolution is the process of pairing up an impl with each
+reference to a trait. So, for example, if there is a generic function like:
+
+    fn clone_slice<T:Clone>(x: &[T]) -> Vec<T> { ... }
+
+and then a call to that function:
+
+    let v: Vec<int> = clone_slice([1, 2, 3].as_slice())
+
+it is the job of trait resolution to figure out (in which case)
+whether there exists an impl of `int : Clone`
+
+Note that in some cases, like generic functions, we may not be able to
+find a specific impl, but we can figure out that the caller must
+provide an impl. To see what I mean, consider the body of `clone_slice`:
+
+    fn clone_slice<T:Clone>(x: &[T]) -> Vec<T> {
+        let mut v = Vec::new();
+        for e in x.iter() {
+            v.push((*e).clone()); // (*)
+        }
+    }
+
+The line marked `(*)` is only legal if `T` (the type of `*e`)
+implements the `Clone` trait. Naturally, since we don't know what `T`
+is, we can't find the specific impl; but based on the bound `T:Clone`,
+we can say that there exists an impl which the caller must provide.
+
+We use the term *obligation* to refer to a trait reference in need of
+an impl.
+
+## Overview
+
+Trait resolution consists of three major parts:
+
+- SELECTION: Deciding how to resolve a specific obligation. For
+  example, selection might decide that a specific obligation can be
+  resolved by employing an impl which matches the self type, or by
+  using a parameter bound. In the case of an impl, Selecting one
+  obligation can create *nested obligations* because of where clauses
+  on the impl itself.
+
+- FULFILLMENT: The fulfillment code is what tracks that obligations
+  are completely fulfilled. Basically it is a worklist of obligations
+  to be selected: once selection is successful, the obligation is
+  removed from the worklist and any nested obligations are enqueued.
+
+- COHERENCE: The coherence checks are intended to ensure that there
+  are never overlapping impls, where two impls could be used with
+  equal precedence.
+
+## Selection
+
+Selection is the process of deciding whether an obligation can be
+resolved and, if so, how it is to be resolved (via impl, where clause, etc).
+The main interface is the `select()` function, which takes an obligation
+and returns a `SelectionResult`. There are three possible outcomes:
+
+- `Ok(Some(selection))` -- yes, the obligation can be resolved, and
+  `selection` indicates how. If the impl was resolved via an impl,
+  then `selection` may also indicate nested obligations that are required
+  by the impl.
+
+- `Ok(None)` -- we are not yet sure whether the obligation can be
+  resolved or not. This happens most commonly when the obligation
+  contains unbound type variables.
+
+- `Err(err)` -- the obligation definitely cannot be resolved due to a
+  type error, or because there are no impls that could possibly apply,
+  etc.
+
+The basic algorithm for selection is broken into two big phases:
+candidate assembly and confirmation.
+
+### Candidate assembly
+
+Searches for impls/where-clauses/etc that might
+possibly be used to satisfy the obligation. Each of those is called
+a candidate. To avoid ambiguity, we want to find exactly one
+candidate that is definitively applicable. In some cases, we may not
+know whether an impl/where-clause applies or not -- this occurs when
+the obligation contains unbound inference variables.
+
+One important point is that candidate assembly considers *only the
+input types* of the obligation when deciding whether an impl applies
+or not. Consider the following example:
+
+    trait Convert<T> { // T is output, Self is input
+        fn convert(&self) -> T;
+    }
+
+    impl Convert<uint> for int { ... }
+
+Now assume we have an obligation `int : Convert<char>`. During
+candidate assembly, the impl above would be considered a definitively
+applicable candidate, because it has the same self type (`int`). The
+fact that the output type parameter `T` is `uint` on the impl and
+`char` in the obligation is not considered.
+
+#### Skolemization
+
+We (at least currently) wish to guarantee "crate concatenability" --
+which basically means that you could take two crates, concatenate
+them textually, and the combined crate would continue to compile. The
+only real way that this relates to trait matching is with
+inference. We have to be careful not to influence unbound type
+variables during the selection process, basically.
+
+Here is an example:
+
+    trait Foo { fn method() { ... }}
+    impl Foo for int { ... }
+
+    fn something() {
+        let mut x = None; // `x` has type `Option<?>`
+        loop {
+            match x {
+                Some(ref y) => { // `y` has type ?
+                    y.method();  // (*)
+                    ...
+        }}}
+    }
+
+The question is, can we resolve the call to `y.method()`? We don't yet
+know what type `y` has. However, there is only one impl in scope, and
+it is for `int`, so perhaps we could deduce that `y` *must* have type
+`int` (and hence the type of `x` is `Option<int>`)? This is actually
+sound reasoning: `int` is the only type in scope that could possibly
+make this program type check. However, this deduction is a bit
+"unstable", though, because if we concatenated with another crate that
+defined a newtype and implemented `Foo` for this newtype, then the
+inference would fail, because there would be two potential impls, not
+one.
+
+It is unclear how important this property is. It might be nice to drop it.
+But for the time being we maintain it.
+
+The way we do this is by *skolemizing* the obligation self type during
+the selection process -- skolemizing means, basically, replacing all
+unbound type variables with a new "skolemized" type. Each skolemized
+type is basically considered "as if" it were some fresh type that is
+distinct from all other types. The skolemization process also replaces
+lifetimes with `'static`, see the section on lifetimes below for an
+explanation.
+
+In the example above, this means that when matching `y.method()` we
+would convert the type of `y` from a type variable `?` to a skolemized
+type `X`. Then, since `X` cannot unify with `int`, the match would
+fail.  Special code exists to check that the match failed because a
+skolemized type could not be unified with another kind of type -- this is
+not considered a definitive failure, but rather an ambiguous result,
+since if the type variable were later to be unified with int, then this
+obligation could be resolved then.
+
+*Note:* Currently, method matching does not use the trait resolution
+code, so if you in fact type in the example above, it may
+compile. Hopefully this will be fixed in later patches.
+
+#### Matching
+
+The subroutines that decide whether a particular impl/where-clause/etc
+applies to a particular obligation. At the moment, this amounts to
+unifying the self types, but in the future we may also recursively
+consider some of the nested obligations, in the case of an impl.
+
+#### Lifetimes and selection
+
+Because of how that lifetime inference works, it is not possible to
+give back immediate feedback as to whether a unification or subtype
+relationship between lifetimes holds or not. Therefore, lifetime
+matching is *not* considered during selection. This is achieved by
+having the skolemization process just replace *ALL* lifetimes with
+`'static`. Later, during confirmation, the non-skolemized self-type
+will be unified with the type from the impl (or whatever). This may
+yield lifetime constraints that will later be found to be in error (in
+contrast, the non-lifetime-constraints have already been checked
+during selection and can never cause an error, though naturally they
+may lead to other errors downstream).
+
+#### Where clauses
+
+Besides an impl, the other major way to resolve an obligation is via a
+where clause. The selection process is always given a *parameter
+environment* which contains a list of where clauses, which are
+basically obligations that can assume are satisfiable. We will iterate
+over that list and check whether our current obligation can be found
+in that list, and if so it is considered satisfied. More precisely, we
+want to check whether there is a where-clause obligation that is for
+the same trait (or some subtrait) and for which the self types match,
+using the definition of *matching* given above.
+
+Consider this simple example:
+
+     trait A1 { ... }
+     trait A2 : A1 { ... }
+
+     trait B { ... }
+
+     fn foo<X:A2+B> { ... }
+
+Clearly we can use methods offered by `A1`, `A2`, or `B` within the
+body of `foo`. In each case, that will incur an obligation like `X :
+A1` or `X : A2`. The parameter environment will contain two
+where-clauses, `X : A2` and `X : B`. For each obligation, then, we
+search this list of where-clauses.  To resolve an obligation `X:A1`,
+we would note that `X:A2` implies that `X:A1`.
+
+### Confirmation
+
+Confirmation unifies the output type parameters of the trait with the
+values found in the obligation, possibly yielding a type error.  If we
+return to our example of the `Convert` trait from the previous
+section, confirmation is where an error would be reported, because the
+impl specified that `T` would be `uint`, but the obligation reported
+`char`. Hence the result of selection would be an error.
+
+### Selection during translation
+
+During type checking, we do not store the results of trait selection.
+We simply wish to verify that trait selection will succeed. Then
+later, at trans time, when we have all concrete types available, we
+can repeat the trait selection.  In this case, we do not consider any
+where-clauses to be in scope. We know that therefore each resolution
+will resolve to a particular impl.
+
+One interesting twist has to do with nested obligations. In general, in trans,
+we only need to do a "shallow" selection for an obligation. That is, we wish to
+identify which impl applies, but we do not (yet) need to decide how to select
+any nested obligations. Nonetheless, we *do* currently do a complete resolution,
+and that is because it can sometimes inform the results of type inference. That is,
+we do not have the full substitutions in terms of the type varibales of the impl available
+to us, so we must run trait selection to figure everything out.
+
+Here is an example:
+
+    trait Foo { ... }
+    impl<U,T:Bar<U>> Foo for Vec<T> { ... }
+
+    impl Bar<uint> for int { ... }
+
+After one shallow round of selection for an obligation like `Vec<int>
+: Foo`, we would know which impl we want, and we would know that
+`T=int`, but we do not know the type of `U`.  We must select the
+nested obligation `int : Bar<U>` to find out that `U=uint`.
+
+It would be good to only do *just as much* nested resolution as
+necessary. Currently, though, we just do a full resolution.
+
+*/
diff --git a/src/librustc/middle/traits/fulfill.rs b/src/librustc/middle/traits/fulfill.rs
new file mode 100644
index 00000000000..78d105c251e
--- /dev/null
+++ b/src/librustc/middle/traits/fulfill.rs
@@ -0,0 +1,250 @@
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+use middle::ty;
+use middle::typeck::infer::{InferCtxt, skolemize};
+use util::nodemap::DefIdMap;
+use util::ppaux::Repr;
+
+use super::Ambiguity;
+use super::Obligation;
+use super::FulfillmentError;
+use super::SelectionError;
+use super::select::SelectionContext;
+use super::Unimplemented;
+
+/**
+ * The fulfillment context is used to drive trait resolution.  It
+ * consists of a list of obligations that must be (eventually)
+ * satisfied. The job is to track which are satisfied, which yielded
+ * errors, and which are still pending. At any point, users can call
+ * `select_where_possible`, and the fulfilment context will try to do
+ * selection, retaining only those obligations that remain
+ * ambiguous. This may be helpful in pushing type inference
+ * along. Once all type inference constraints have been generated, the
+ * method `select_all_or_error` can be used to report any remaining
+ * ambiguous cases as errors.
+ */
+pub struct FulfillmentContext {
+    // A list of all obligations that have been registered with this
+    // fulfillment context.
+    trait_obligations: Vec<Obligation>,
+
+    // For semi-hacky reasons (see FIXME below) we keep the builtin
+    // trait obligations segregated.
+    builtin_obligations: Vec<Obligation>,
+}
+
+impl FulfillmentContext {
+    pub fn new() -> FulfillmentContext {
+        FulfillmentContext {
+            trait_obligations: Vec::new(),
+            builtin_obligations: Vec::new()
+        }
+    }
+
+    pub fn register_obligation(&mut self,
+                               tcx: &ty::ctxt,
+                               obligation: Obligation)
+    {
+        debug!("register_obligation({})", obligation.repr(tcx));
+        match tcx.lang_items.to_builtin_kind(obligation.trait_ref.def_id) {
+            Some(_) => {
+                self.builtin_obligations.push(obligation);
+            }
+            None => {
+                self.trait_obligations.push(obligation);
+            }
+        }
+    }
+
+    pub fn select_all_or_error(&mut self,
+                               infcx: &InferCtxt,
+                               param_env: &ty::ParameterEnvironment,
+                               unboxed_closures: &DefIdMap<ty::UnboxedClosure>)
+                               -> Result<(),Vec<FulfillmentError>>
+    {
+        try!(self.select_where_possible(infcx, param_env,
+                                        unboxed_closures));
+
+        // Anything left is ambiguous.
+        let errors: Vec<FulfillmentError> =
+            self.trait_obligations
+            .iter()
+            .map(|o| FulfillmentError::new((*o).clone(), Ambiguity))
+            .collect();
+
+        if errors.is_empty() {
+            Ok(())
+        } else {
+            Err(errors)
+        }
+    }
+
+    pub fn select_where_possible(&mut self,
+                                 infcx: &InferCtxt,
+                                 param_env: &ty::ParameterEnvironment,
+                                 unboxed_closures: &DefIdMap<ty::UnboxedClosure>)
+                                 -> Result<(),Vec<FulfillmentError>>
+    {
+        let tcx = infcx.tcx;
+        let selcx = SelectionContext::new(infcx, param_env,
+                                          unboxed_closures);
+
+        debug!("select_where_possible({} obligations) start",
+               self.trait_obligations.len());
+
+        let mut errors = Vec::new();
+
+        loop {
+            let count = self.trait_obligations.len();
+
+            debug!("select_where_possible({} obligations) iteration",
+                   count);
+
+            let mut selections = Vec::new();
+
+            // First pass: walk each obligation, retaining
+            // only those that we cannot yet process.
+            self.trait_obligations.retain(|obligation| {
+                match selcx.select(obligation) {
+                    Ok(None) => {
+                        true
+                    }
+                    Ok(Some(s)) => {
+                        selections.push(s);
+                        false
+                    }
+                    Err(selection_err) => {
+                        debug!("obligation: {} error: {}",
+                               obligation.repr(tcx),
+                               selection_err.repr(tcx));
+
+                        errors.push(FulfillmentError::new(
+                            (*obligation).clone(),
+                            SelectionError(selection_err)));
+                        false
+                    }
+                }
+            });
+
+            if self.trait_obligations.len() == count {
+                // Nothing changed.
+                break;
+            }
+
+            // Now go through all the successful ones,
+            // registering any nested obligations for the future.
+            for selection in selections.move_iter() {
+                selection.map_move_nested(
+                    |o| self.register_obligation(tcx, o));
+            }
+        }
+
+        debug!("select_where_possible({} obligations, {} errors) done",
+               self.trait_obligations.len(),
+               errors.len());
+
+        if errors.len() == 0 {
+            Ok(())
+        } else {
+            Err(errors)
+        }
+    }
+
+    pub fn check_builtin_bound_obligations(
+        &self,
+        infcx: &InferCtxt)
+        -> Result<(),Vec<FulfillmentError>>
+    {
+        let tcx = infcx.tcx;
+        let mut errors = Vec::new();
+        debug!("check_builtin_bound_obligations");
+        for obligation in self.builtin_obligations.iter() {
+            debug!("obligation={}", obligation.repr(tcx));
+
+            let def_id = obligation.trait_ref.def_id;
+            let bound = match tcx.lang_items.to_builtin_kind(def_id) {
+                Some(bound) => { bound }
+                None => { continue; }
+            };
+
+            let unskol_self_ty = obligation.self_ty();
+
+            // Skolemize the self-type so that it no longer contains
+            // inference variables. Note that this also replaces
+            // regions with 'static. You might think that this is not
+            // ok, because checking whether something is `Send`
+            // implies checking whether it is 'static: that's true,
+            // but in fact the region bound is fed into region
+            // inference separately and enforced there (and that has
+            // even already been done before this code executes,
+            // generally speaking).
+            let self_ty = skolemize(infcx, unskol_self_ty);
+
+            debug!("bound={} self_ty={}", bound, self_ty.repr(tcx));
+            if ty::type_is_error(self_ty) {
+                // Indicates an error that was/will-be
+                // reported elsewhere.
+                continue;
+            }
+
+            // Determine if builtin bound is met.
+            let tc = ty::type_contents(tcx, self_ty);
+            debug!("tc={}", tc);
+            let met = match bound {
+                ty::BoundSend   => tc.is_sendable(tcx),
+                ty::BoundSized  => tc.is_sized(tcx),
+                ty::BoundCopy   => tc.is_copy(tcx),
+                ty::BoundSync   => tc.is_sync(tcx),
+            };
+
+            if met {
+                continue;
+            }
+
+            // FIXME -- This is kind of a hack: it requently happens
+            // that some earlier error prevents types from being fully
+            // inferred, and then we get a bunch of uninteresting
+            // errors saying something like "<generic #0> doesn't
+            // implement Sized".  It may even be true that we could
+            // just skip over all checks where the self-ty is an
+            // inference variable, but I was afraid that there might
+            // be an inference variable created, registered as an
+            // obligation, and then never forced by writeback, and
+            // hence by skipping here we'd be ignoring the fact that
+            // we don't KNOW the type works out. Though even that
+            // would probably be harmless, given that we're only
+            // talking about builtin traits, which are known to be
+            // inhabited. But in any case I just threw in this check
+            // for has_errors() to be sure that compilation isn't
+            // happening anyway. In that case, why inundate the user.
+            if ty::type_needs_infer(self_ty) &&
+                tcx.sess.has_errors()
+            {
+                debug!("skipping printout because self_ty={}",
+                       self_ty.repr(tcx));
+                continue;
+            }
+
+            errors.push(
+                FulfillmentError::new(
+                    (*obligation).clone(),
+                    SelectionError(Unimplemented)));
+        }
+
+        if errors.is_empty() {
+            Ok(())
+        } else {
+            Err(errors)
+        }
+    }
+}
+
diff --git a/src/librustc/middle/traits/mod.rs b/src/librustc/middle/traits/mod.rs
new file mode 100644
index 00000000000..62b3c982ccd
--- /dev/null
+++ b/src/librustc/middle/traits/mod.rs
@@ -0,0 +1,438 @@
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+/*!
+ * Trait Resolution. See doc.rs.
+ */
+
+use middle::subst;
+use middle::ty;
+use middle::typeck::infer::InferCtxt;
+use std::rc::Rc;
+use syntax::ast;
+use syntax::codemap::{Span, DUMMY_SP};
+use util::nodemap::DefIdMap;
+
+pub use self::fulfill::FulfillmentContext;
+pub use self::select::SelectionContext;
+pub use self::util::supertraits;
+pub use self::util::transitive_bounds;
+pub use self::util::Supertraits;
+pub use self::util::search_trait_and_supertraits_from_bound;
+
+mod coherence;
+mod fulfill;
+mod select;
+mod util;
+
+/**
+ * An `Obligation` represents some trait reference (e.g. `int:Eq`) for
+ * which the vtable must be found.  The process of finding a vtable is
+ * called "resolving" the `Obligation`. This process consists of
+ * either identifying an `impl` (e.g., `impl Eq for int`) that
+ * provides the required vtable, or else finding a bound that is in
+ * scope. The eventual result is usually a `Selection` (defined below).
+ */
+#[deriving(Clone)]
+pub struct Obligation {
+    pub cause: ObligationCause,
+    pub recursion_depth: uint,
+    pub trait_ref: Rc<ty::TraitRef>,
+}
+
+/**
+ * Why did we incur this obligation? Used for error reporting.
+ */
+#[deriving(Clone)]
+pub struct ObligationCause {
+    pub span: Span,
+    pub code: ObligationCauseCode
+}
+
+#[deriving(Clone)]
+pub enum ObligationCauseCode {
+    /// Not well classified or should be obvious from span.
+    MiscObligation,
+
+    /// In an impl of trait X for type Y, type Y must
+    /// also implement all supertraits of X.
+    ItemObligation(ast::DefId),
+
+    /// Obligation incurred due to an object cast.
+    ObjectCastObligation(/* Object type */ ty::t),
+
+    /// Various cases where expressions must be sized/copy/etc:
+    AssignmentLhsSized,        // L = X implies that L is Sized
+    StructInitializerSized,    // S { ... } must be Sized
+    VariableType(ast::NodeId), // Type of each variable must be Sized
+    RepeatVec,                 // [T,..n] --> T must be Copy
+}
+
+pub static DUMMY_CAUSE: ObligationCause =
+    ObligationCause { span: DUMMY_SP,
+                      code: MiscObligation };
+
+pub type Obligations = subst::VecPerParamSpace<Obligation>;
+
+pub type Selection = Vtable<Obligation>;
+
+#[deriving(Clone,Show)]
+pub enum SelectionError {
+    Unimplemented,
+    Overflow,
+    OutputTypeParameterMismatch(Rc<ty::TraitRef>, ty::type_err)
+}
+
+pub struct FulfillmentError {
+    pub obligation: Obligation,
+    pub code: FulfillmentErrorCode
+}
+
+#[deriving(Clone)]
+pub enum FulfillmentErrorCode {
+    SelectionError(SelectionError),
+    Ambiguity,
+}
+
+/**
+ * When performing resolution, it is typically the case that there
+ * can be one of three outcomes:
+ *
+ * - `Ok(Some(r))`: success occurred with result `r`
+ * - `Ok(None)`: could not definitely determine anything, usually due
+ *   to inconclusive type inference.
+ * - `Err(e)`: error `e` occurred
+ */
+pub type SelectionResult<T> = Result<Option<T>,SelectionError>;
+
+#[deriving(PartialEq,Eq,Show)]
+pub enum EvaluationResult {
+    EvaluatedToMatch,
+    EvaluatedToAmbiguity,
+    EvaluatedToUnmatch
+}
+
+/**
+ * Given the successful resolution of an obligation, the `Vtable`
+ * indicates where the vtable comes from. Note that while we call this
+ * a "vtable", it does not necessarily indicate dynamic dispatch at
+ * runtime. `Vtable` instances just tell the compiler where to find
+ * methods, but in generic code those methods are typically statically
+ * dispatched -- only when an object is constructed is a `Vtable`
+ * instance reified into an actual vtable.
+ *
+ * For example, the vtable may be tied to a specific impl (case A),
+ * or it may be relative to some bound that is in scope (case B).
+ *
+ *
+ * ```
+ * impl<T:Clone> Clone<T> for Option<T> { ... } // Impl_1
+ * impl<T:Clone> Clone<T> for Box<T> { ... }    // Impl_2
+ * impl Clone for int { ... }             // Impl_3
+ *
+ * fn foo<T:Clone>(concrete: Option<Box<int>>,
+ *                 param: T,
+ *                 mixed: Option<T>) {
+ *
+ *    // Case A: Vtable points at a specific impl. Only possible when
+ *    // type is concretely known. If the impl itself has bounded
+ *    // type parameters, Vtable will carry resolutions for those as well:
+ *    concrete.clone(); // Vtable(Impl_1, [Vtable(Impl_2, [Vtable(Impl_3)])])
+ *
+ *    // Case B: Vtable must be provided by caller. This applies when
+ *    // type is a type parameter.
+ *    param.clone();    // VtableParam(Oblig_1)
+ *
+ *    // Case C: A mix of cases A and B.
+ *    mixed.clone();    // Vtable(Impl_1, [VtableParam(Oblig_1)])
+ * }
+ * ```
+ *
+ * ### The type parameter `N`
+ *
+ * See explanation on `VtableImpl`.
+ */
+#[deriving(Show,Clone)]
+pub enum Vtable<N> {
+    /// Vtable identifying a particular impl.
+    VtableImpl(VtableImpl<N>),
+
+    /// Vtable automatically generated for an unboxed closure. The def
+    /// ID is the ID of the closure expression. This is a `VtableImpl`
+    /// in spirit, but the impl is generated by the compiler and does
+    /// not appear in the source.
+    VtableUnboxedClosure(ast::DefId),
+
+    /// Successful resolution to an obligation provided by the caller
+    /// for some type parameter.
+    VtableParam(VtableParam),
+
+    /// Successful resolution for a builtin trait.
+    VtableBuiltin,
+}
+
+/**
+ * Identifies a particular impl in the source, along with a set of
+ * substitutions from the impl's type/lifetime parameters. The
+ * `nested` vector corresponds to the nested obligations attached to
+ * the impl's type parameters.
+ *
+ * The type parameter `N` indicates the type used for "nested
+ * obligations" that are required by the impl. During type check, this
+ * is `Obligation`, as one might expect. During trans, however, this
+ * is `()`, because trans only requires a shallow resolution of an
+ * impl, and nested obligations are satisfied later.
+ */
+#[deriving(Clone)]
+pub struct VtableImpl<N> {
+    pub impl_def_id: ast::DefId,
+    pub substs: subst::Substs,
+    pub nested: subst::VecPerParamSpace<N>
+}
+
+/**
+ * A vtable provided as a parameter by the caller. For example, in a
+ * function like `fn foo<T:Eq>(...)`, if the `eq()` method is invoked
+ * on an instance of `T`, the vtable would be of type `VtableParam`.
+ */
+#[deriving(Clone)]
+pub struct VtableParam {
+    // In the above example, this would `Eq`
+    pub bound: Rc<ty::TraitRef>,
+}
+
+pub fn try_select_obligation(infcx: &InferCtxt,
+                             param_env: &ty::ParameterEnvironment,
+                             unboxed_closures: &DefIdMap<ty::UnboxedClosure>,
+                             obligation: &Obligation)
+                             -> SelectionResult<Selection>
+{
+    /*!
+     * Attempts to select the impl/bound/etc for the obligation
+     * given. Returns `None` if we are unable to resolve, either
+     * because of ambiguity or due to insufficient inference.  Note
+     * that selection is a shallow process and hence the result may
+     * contain nested obligations that must be resolved. The caller is
+     * responsible for ensuring that those get resolved. (But see
+     * `try_select_obligation_deep` below.)
+     */
+
+    let selcx = select::SelectionContext::new(infcx, param_env, unboxed_closures);
+    selcx.select(obligation)
+}
+
+pub fn evaluate_obligation(infcx: &InferCtxt,
+                           param_env: &ty::ParameterEnvironment,
+                           obligation: &Obligation,
+                           unboxed_closures: &DefIdMap<ty::UnboxedClosure>)
+                           -> EvaluationResult
+{
+    /*!
+     * Attempts to resolve the obligation given. Returns `None` if
+     * we are unable to resolve, either because of ambiguity or
+     * due to insufficient inference.
+     */
+
+    let selcx = select::SelectionContext::new(infcx, param_env,
+                                              unboxed_closures);
+    selcx.evaluate_obligation(obligation)
+}
+
+pub fn evaluate_impl(infcx: &InferCtxt,
+                     param_env: &ty::ParameterEnvironment,
+                     unboxed_closures: &DefIdMap<ty::UnboxedClosure>,
+                     cause: ObligationCause,
+                     impl_def_id: ast::DefId,
+                     self_ty: ty::t)
+                     -> EvaluationResult
+{
+    /*!
+     * Tests whether the impl `impl_def_id` can be applied to the self
+     * type `self_ty`. This is similar to "selection", but simpler:
+     *
+     * - It does not take a full trait-ref as input, so it skips over
+     *   the "confirmation" step which would reconcile output type
+     *   parameters.
+     * - It returns an `EvaluationResult`, which is a tri-value return
+     *   (yes/no/unknown).
+     */
+
+    let selcx = select::SelectionContext::new(infcx, param_env, unboxed_closures);
+    selcx.evaluate_impl(impl_def_id, cause, self_ty)
+}
+
+pub fn select_inherent_impl(infcx: &InferCtxt,
+                            param_env: &ty::ParameterEnvironment,
+                            unboxed_closures: &DefIdMap<ty::UnboxedClosure>,
+                            cause: ObligationCause,
+                            impl_def_id: ast::DefId,
+                            self_ty: ty::t)
+                            -> SelectionResult<VtableImpl<Obligation>>
+{
+    /*!
+     * Matches the self type of the inherent impl `impl_def_id`
+     * against `self_ty` and returns the resulting resolution.  This
+     * routine may modify the surrounding type context (for example,
+     * it may unify variables).
+     */
+
+    // This routine is only suitable for inherent impls. This is
+    // because it does not attempt to unify the output type parameters
+    // from the trait ref against the values from the obligation.
+    // (These things do not apply to inherent impls, for which there
+    // is no trait ref nor obligation.)
+    //
+    // Matching against non-inherent impls should be done with
+    // `try_resolve_obligation()`.
+    assert!(ty::impl_trait_ref(infcx.tcx, impl_def_id).is_none());
+
+    let selcx = select::SelectionContext::new(infcx, param_env,
+                                              unboxed_closures);
+    selcx.select_inherent_impl(impl_def_id, cause, self_ty)
+}
+
+pub fn is_orphan_impl(tcx: &ty::ctxt,
+                      impl_def_id: ast::DefId)
+                      -> bool
+{
+    /*!
+     * True if neither the trait nor self type is local. Note that
+     * `impl_def_id` must refer to an impl of a trait, not an inherent
+     * impl.
+     */
+
+    !coherence::impl_is_local(tcx, impl_def_id)
+}
+
+pub fn overlapping_impls(infcx: &InferCtxt,
+                         impl1_def_id: ast::DefId,
+                         impl2_def_id: ast::DefId)
+                         -> bool
+{
+    /*!
+     * True if there exist types that satisfy both of the two given impls.
+     */
+
+    coherence::impl_can_satisfy(infcx, impl1_def_id, impl2_def_id) &&
+    coherence::impl_can_satisfy(infcx, impl2_def_id, impl1_def_id)
+}
+
+pub fn obligations_for_generics(tcx: &ty::ctxt,
+                                cause: ObligationCause,
+                                generics: &ty::Generics,
+                                substs: &subst::Substs)
+                                -> subst::VecPerParamSpace<Obligation>
+{
+    /*!
+     * Given generics for an impl like:
+     *
+     *    impl<A:Foo, B:Bar+Qux> ...
+     *
+     * and a substs vector like `<A=A0, B=B0>`, yields a result like
+     *
+     *    [[Foo for A0, Bar for B0, Qux for B0], [], []]
+     */
+
+    util::obligations_for_generics(tcx, cause, 0, generics, substs)
+}
+
+pub fn obligation_for_builtin_bound(tcx: &ty::ctxt,
+                                    cause: ObligationCause,
+                                    source_ty: ty::t,
+                                    builtin_bound: ty::BuiltinBound)
+                                    -> Obligation
+{
+    util::obligation_for_builtin_bound(tcx, cause, builtin_bound, 0, source_ty)
+}
+
+impl Obligation {
+    pub fn new(cause: ObligationCause, trait_ref: Rc<ty::TraitRef>) -> Obligation {
+        Obligation { cause: cause,
+                     recursion_depth: 0,
+                     trait_ref: trait_ref }
+    }
+
+    pub fn misc(span: Span, trait_ref: Rc<ty::TraitRef>) -> Obligation {
+        Obligation::new(ObligationCause::misc(span), trait_ref)
+    }
+
+    pub fn self_ty(&self) -> ty::t {
+        self.trait_ref.self_ty()
+    }
+}
+
+impl ObligationCause {
+    pub fn new(span: Span, code: ObligationCauseCode) -> ObligationCause {
+        ObligationCause { span: span, code: code }
+    }
+
+    pub fn misc(span: Span) -> ObligationCause {
+        ObligationCause { span: span, code: MiscObligation }
+    }
+}
+
+impl<N> Vtable<N> {
+    pub fn map_nested<M>(&self, op: |&N| -> M) -> Vtable<M> {
+        match *self {
+            VtableImpl(ref i) => VtableImpl(i.map_nested(op)),
+            VtableUnboxedClosure(d) => VtableUnboxedClosure(d),
+            VtableParam(ref p) => VtableParam((*p).clone()),
+            VtableBuiltin => VtableBuiltin,
+        }
+    }
+
+    pub fn map_move_nested<M>(self, op: |N| -> M) -> Vtable<M> {
+        match self {
+            VtableImpl(i) => VtableImpl(i.map_move_nested(op)),
+            VtableUnboxedClosure(d) => VtableUnboxedClosure(d),
+            VtableParam(p) => VtableParam(p),
+            VtableBuiltin => VtableBuiltin,
+        }
+    }
+}
+
+impl<N> VtableImpl<N> {
+    pub fn map_nested<M>(&self,
+                         op: |&N| -> M)
+                         -> VtableImpl<M>
+    {
+        VtableImpl {
+            impl_def_id: self.impl_def_id,
+            substs: self.substs.clone(),
+            nested: self.nested.map(op)
+        }
+    }
+
+    pub fn map_move_nested<M>(self, op: |N| -> M) -> VtableImpl<M> {
+        let VtableImpl { impl_def_id, substs, nested } = self;
+        VtableImpl {
+            impl_def_id: impl_def_id,
+            substs: substs,
+            nested: nested.map_move(op)
+        }
+    }
+}
+
+impl EvaluationResult {
+    pub fn potentially_applicable(&self) -> bool {
+        match *self {
+            EvaluatedToMatch | EvaluatedToAmbiguity => true,
+            EvaluatedToUnmatch => false
+        }
+    }
+}
+
+impl FulfillmentError {
+    fn new(obligation: Obligation, code: FulfillmentErrorCode)
+           -> FulfillmentError
+    {
+        FulfillmentError { obligation: obligation, code: code }
+    }
+}
diff --git a/src/librustc/middle/traits/select.rs b/src/librustc/middle/traits/select.rs
new file mode 100644
index 00000000000..681e2650f39
--- /dev/null
+++ b/src/librustc/middle/traits/select.rs
@@ -0,0 +1,1024 @@
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+/*! See `doc.rs` for high-level documentation */
+
+use super::{Obligation, ObligationCause};
+use super::{EvaluationResult, EvaluatedToMatch,
+            EvaluatedToAmbiguity, EvaluatedToUnmatch};
+use super::{SelectionError, Unimplemented, Overflow,
+            OutputTypeParameterMismatch};
+use super::{Selection};
+use super::{SelectionResult};
+use super::{VtableBuiltin, VtableImpl, VtableParam, VtableUnboxedClosure};
+use super::{util};
+
+use middle::subst::{Subst, Substs, VecPerParamSpace};
+use middle::ty;
+use middle::typeck::check::regionmanip;
+use middle::typeck::infer;
+use middle::typeck::infer::InferCtxt;
+use std::rc::Rc;
+use syntax::ast;
+use util::nodemap::DefIdMap;
+use util::ppaux::Repr;
+
+pub struct SelectionContext<'cx, 'tcx:'cx> {
+    infcx: &'cx InferCtxt<'cx, 'tcx>,
+    param_env: &'cx ty::ParameterEnvironment,
+    unboxed_closures: &'cx DefIdMap<ty::UnboxedClosure>,
+}
+
+// pub struct SelectionCache {
+//     hashmap: RefCell<HashMap<CacheKey, Candidate>>,
+// }
+
+// #[deriving(Hash,Eq,PartialEq)]
+// struct CacheKey {
+//     trait_def_id: ast::DefId,
+//     skol_obligation_self_ty: ty::t,
+// }
+
+enum MatchResult<T> {
+    Matched(T),
+    AmbiguousMatch,
+    NoMatch
+}
+
+/**
+ * The selection process begins by considering all impls, where
+ * clauses, and so forth that might resolve an obligation.  Sometimes
+ * we'll be able to say definitively that (e.g.) an impl does not
+ * apply to the obligation: perhaps it is defined for `uint` but the
+ * obligation is for `int`. In that case, we drop the impl out of the
+ * list.  But the other cases are considered *candidates*.
+ *
+ * Candidates can either be definitive or ambiguous. An ambiguous
+ * candidate is one that might match or might not, depending on how
+ * type variables wind up being resolved. This only occurs during inference.
+ *
+ * For selection to suceed, there must be exactly one non-ambiguous
+ * candidate.  Usually, it is not possible to have more than one
+ * definitive candidate, due to the coherence rules. However, there is
+ * one case where it could occur: if there is a blanket impl for a
+ * trait (that is, an impl applied to all T), and a type parameter
+ * with a where clause. In that case, we can have a candidate from the
+ * where clause and a second candidate from the impl. This is not a
+ * problem because coherence guarantees us that the impl which would
+ * be used to satisfy the where clause is the same one that we see
+ * now. To resolve this issue, therefore, we ignore impls if we find a
+ * matching where clause. Part of the reason for this is that where
+ * clauses can give additional information (like, the types of output
+ * parameters) that would have to be inferred from the impl.
+ */
+#[deriving(Clone)]
+enum Candidate {
+    MatchedBuiltinCandidate,
+    AmbiguousBuiltinCandidate,
+    MatchedParamCandidate(VtableParam),
+    AmbiguousParamCandidate,
+    Impl(ImplCandidate),
+    MatchedUnboxedClosureCandidate(/* closure */ ast::DefId)
+}
+
+#[deriving(Clone)]
+enum ImplCandidate {
+    MatchedImplCandidate(ast::DefId),
+    AmbiguousImplCandidate(ast::DefId),
+}
+
+impl<'cx, 'tcx> SelectionContext<'cx, 'tcx> {
+    pub fn new(infcx: &'cx InferCtxt<'cx, 'tcx>,
+               param_env: &'cx ty::ParameterEnvironment,
+               unboxed_closures: &'cx DefIdMap<ty::UnboxedClosure>)
+               -> SelectionContext<'cx, 'tcx> {
+        SelectionContext { infcx: infcx, param_env: param_env,
+                           unboxed_closures: unboxed_closures }
+    }
+
+    pub fn tcx(&self) -> &'cx ty::ctxt<'tcx> {
+        self.infcx.tcx
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // Selection
+    //
+    // The selection phase tries to identify *how* an obligation will
+    // be resolved. For example, it will identify which impl or
+    // parameter bound is to be used. The process can be inconclusive
+    // if the self type in the obligation is not fully inferred. Selection
+    // can result in an error in one of two ways:
+    //
+    // 1. If no applicable impl or parameter bound can be found.
+    // 2. If the output type parameters in the obligation do not match
+    //    those specified by the impl/bound. For example, if the obligation
+    //    is `Vec<Foo>:Iterable<Bar>`, but the impl specifies
+    //    `impl<T> Iterable<T> for Vec<T>`, than an error would result.
+
+    pub fn select(&self, obligation: &Obligation) -> SelectionResult<Selection> {
+        /*!
+         * Evaluates whether the obligation can be satisfied. Returns
+         * an indication of whether the obligation can be satisfied
+         * and, if so, by what means. Never affects surrounding typing
+         * environment.
+         */
+
+        debug!("select({})", obligation.repr(self.tcx()));
+
+        match try!(self.candidate_from_obligation(obligation)) {
+            None => Ok(None),
+            Some(candidate) => self.confirm_candidate(obligation, candidate),
+        }
+    }
+
+    pub fn select_inherent_impl(&self,
+                                impl_def_id: ast::DefId,
+                                obligation_cause: ObligationCause,
+                                obligation_self_ty: ty::t)
+                                -> SelectionResult<VtableImpl<Obligation>>
+    {
+        debug!("select_inherent_impl(impl_def_id={}, obligation_self_ty={})",
+               impl_def_id.repr(self.tcx()),
+               obligation_self_ty.repr(self.tcx()));
+
+        match self.candidate_from_impl(impl_def_id,
+                                       obligation_cause,
+                                       obligation_self_ty) {
+            Some(MatchedImplCandidate(impl_def_id)) => {
+                let vtable_impl =
+                    try!(self.confirm_inherent_impl_candidate(
+                        impl_def_id,
+                        obligation_cause,
+                        obligation_self_ty,
+                        0));
+                Ok(Some(vtable_impl))
+            }
+            Some(AmbiguousImplCandidate(_)) => {
+                Ok(None)
+            }
+            None => {
+                Err(Unimplemented)
+            }
+        }
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // EVALUATION
+    //
+    // Tests whether an obligation can be selected or whether an impl can be
+    // applied to particular types. It skips the "confirmation" step and
+    // hence completely ignores output type parameters.
+
+    pub fn evaluate_obligation(&self,
+                               obligation: &Obligation)
+                               -> EvaluationResult
+    {
+        /*!
+         * Evaluates whether the obligation `obligation` can be
+         * satisfied (by any means).
+         */
+
+        debug!("evaluate_obligation({})",
+               obligation.repr(self.tcx()));
+
+        match self.candidate_from_obligation(obligation) {
+            Ok(Some(c)) => c.to_evaluation_result(),
+            Ok(None) => EvaluatedToAmbiguity,
+            Err(_) => EvaluatedToUnmatch,
+        }
+    }
+
+    pub fn evaluate_impl(&self,
+                         impl_def_id: ast::DefId,
+                         obligation_cause: ObligationCause,
+                         obligation_self_ty: ty::t)
+                         -> EvaluationResult
+    {
+        /*!
+         * Evaluates whether the impl with id `impl_def_id` could be
+         * applied to the self type `obligation_self_ty`. This can be
+         * used either for trait or inherent impls.
+         */
+
+        debug!("evaluate_impl(impl_def_id={}, obligation_self_ty={})",
+               impl_def_id.repr(self.tcx()),
+               obligation_self_ty.repr(self.tcx()));
+
+        match self.candidate_from_impl(impl_def_id,
+                                       obligation_cause,
+                                       obligation_self_ty) {
+            Some(c) => c.to_evaluation_result(),
+            None => EvaluatedToUnmatch,
+        }
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // CANDIDATE ASSEMBLY
+    //
+    // The selection process begins by examining all in-scope impls,
+    // caller obligations, and so forth and assembling a list of
+    // candidates. See `doc.rs` and the `Candidate` type for more details.
+
+    fn candidate_from_obligation(&self, obligation: &Obligation)
+                                 -> SelectionResult<Candidate>
+    {
+        debug!("candidate_from_obligation({}, self_ty={})",
+               obligation.repr(self.tcx()),
+               self.infcx.ty_to_string(obligation.self_ty()));
+
+        let skol_obligation_self_ty =
+            infer::skolemize(self.infcx, obligation.self_ty());
+
+        // First, check the cache.
+        match self.check_candidate_cache(obligation, skol_obligation_self_ty) {
+            Some(c) => {
+                return Ok(Some(c));
+            }
+            None => { }
+        }
+
+        let mut candidates =
+            try!(self.assemble_candidates(obligation,
+                                          skol_obligation_self_ty));
+
+        debug!("candidate_from_obligation: {} candidates for {}",
+               candidates.len(), obligation.repr(self.tcx()));
+
+        // Examine candidates to determine outcome. Ideally we will
+        // have exactly one candidate that is definitively applicable.
+
+        if candidates.len() == 0 {
+            // Annoying edge case: if there are no impls, then there
+            // is no way that this trait reference is implemented,
+            // *unless* it contains unbound variables. In that case,
+            // it is possible that one of those unbound variables will
+            // be bound to a new type from some other crate which will
+            // also contain impls.
+            let trait_ref = &*obligation.trait_ref;
+            return if !self.trait_ref_unconstrained(trait_ref) {
+                debug!("candidate_from_obligation({}) -> 0 matches, unimpl",
+                       obligation.repr(self.tcx()));
+                Err(Unimplemented)
+            } else {
+                debug!("candidate_from_obligation({}) -> 0 matches, ambig",
+                       obligation.repr(self.tcx()));
+                Ok(None)
+            };
+        }
+
+        if candidates.len() > 1 {
+            // Ambiguity. Possibly we should report back more
+            // information on the potential candidates so we can give
+            // a better error message.
+            debug!("candidate_from_obligation({}) -> multiple matches, ambig",
+                   obligation.repr(self.tcx()));
+
+            return Ok(None);
+        }
+
+        let candidate = candidates.pop().unwrap();
+        self.insert_candidate_cache(obligation, skol_obligation_self_ty,
+                                    candidate.clone());
+        Ok(Some(candidate))
+    }
+
+    fn check_candidate_cache(&self,
+                             _obligation: &Obligation,
+                             _skol_obligation_self_ty: ty::t)
+                             -> Option<Candidate>
+    {
+        // let cache_key = CacheKey::new(obligation.trait_ref.def_id,
+        //                               skol_obligation_self_ty);
+        // let hashmap = self.tcx().selection_cache.hashmap.borrow();
+        // hashmap.find(&cache_key).map(|c| (*c).clone())
+        None
+    }
+
+    fn insert_candidate_cache(&self,
+                              _obligation: &Obligation,
+                              _skol_obligation_self_ty: ty::t,
+                              _candidate: Candidate)
+    {
+        // FIXME -- Enable caching. I think the right place to put the cache
+        // is in the ParameterEnvironment, not the tcx, because otherwise
+        // when there are distinct where clauses in scope the cache can get
+        // confused.
+        //
+        //let cache_key = CacheKey::new(obligation.trait_ref.def_id,
+        //                              skol_obligation_self_ty);
+        //let mut hashmap = self.tcx().selection_cache.hashmap.borrow_mut();
+        //hashmap.insert(cache_key, candidate);
+    }
+
+    fn assemble_candidates(&self,
+                           obligation: &Obligation,
+                           skol_obligation_self_ty: ty::t)
+                           -> Result<Vec<Candidate>, SelectionError>
+    {
+        // Check for overflow.
+
+        let recursion_limit = self.infcx.tcx.sess.recursion_limit.get();
+        if obligation.recursion_depth >= recursion_limit {
+            debug!("{} --> overflow", obligation.repr(self.tcx()));
+            return Err(Overflow);
+        }
+
+        let mut candidates = Vec::new();
+
+        match self.tcx().lang_items.to_builtin_kind(obligation.trait_ref.def_id) {
+            Some(_) => {
+                // FIXME -- The treatment of builtin bounds is a bit
+                // hacky right now. Eventually, the idea is to move
+                // the logic for selection out of type_contents and
+                // into this module (And make it based on the generic
+                // mechanisms of OIBTT2).  However, I want to land
+                // some code today, so we're going to cut a few
+                // corners. What we do now is that the trait selection
+                // code always considers builtin obligations to
+                // match. The fulfillment code (which also has the job
+                // of tracking all the traits that must hold) will
+                // then just accumulate the various
+                // builtin-bound-related obligations that must be met.
+                // Later, at the end of typeck, after writeback etc,
+                // we will rewalk this list and extract all the
+                // builtin-bound-related obligations and test them
+                // again using type contents. Part of the motivation
+                // for this is that the type contents code requires
+                // that writeback has been completed in some cases.
+
+                candidates.push(AmbiguousBuiltinCandidate);
+            }
+
+            None => {
+                // Other bounds. Consider both in-scope bounds from fn decl
+                // and applicable impls.
+
+                try!(self.assemble_candidates_from_caller_bounds(
+                    obligation,
+                    skol_obligation_self_ty,
+                    &mut candidates));
+
+                try!(self.assemble_unboxed_candidates(
+                    obligation,
+                    skol_obligation_self_ty,
+                    &mut candidates));
+
+                // If there is a fn bound that applies, forego the
+                // impl search. It can only generate conflicts.
+
+                if candidates.len() == 0 {
+                    try!(self.assemble_candidates_from_impls(
+                        obligation,
+                        skol_obligation_self_ty,
+                        &mut candidates));
+                }
+            }
+        }
+
+        Ok(candidates)
+    }
+
+    fn assemble_candidates_from_caller_bounds(&self,
+                                              obligation: &Obligation,
+                                              skol_obligation_self_ty: ty::t,
+                                              candidates: &mut Vec<Candidate>)
+                                              -> Result<(),SelectionError>
+    {
+        /*!
+         * Given an obligation like `<SomeTrait for T>`, search the obligations
+         * that the caller supplied to find out whether it is listed among
+         * them.
+         *
+         * Never affects inference environment.
+v         */
+
+        debug!("assemble_candidates_from_caller_bounds({})",
+               obligation.repr(self.tcx()));
+
+        for caller_obligation in self.param_env.caller_obligations.iter() {
+            debug!("caller_obligation={}",
+                   caller_obligation.repr(self.tcx()));
+
+            // Skip over obligations that don't apply to
+            // `self_ty`.
+            let caller_bound = &caller_obligation.trait_ref;
+            let caller_self_ty = caller_bound.substs.self_ty().unwrap();
+            match self.match_self_types(obligation.cause,
+                                        caller_self_ty,
+                                        skol_obligation_self_ty) {
+                AmbiguousMatch => {
+                    debug!("-> AmbiguousParamCandidate");
+                    candidates.push(AmbiguousParamCandidate);
+                    return Ok(());
+                }
+                NoMatch => {
+                    continue;
+                }
+                Matched(()) => { }
+            }
+
+            // Search through the trait (and its supertraits) to
+            // see if it matches the def-id we are looking for.
+            let caller_bound = (*caller_bound).clone();
+            match util::search_trait_and_supertraits_from_bound(
+                self.infcx.tcx, caller_bound,
+                |d| d == obligation.trait_ref.def_id)
+            {
+                Some(vtable_param) => {
+                    // If so, we're done!
+                    debug!("-> MatchedParamCandidate({})", vtable_param);
+                    candidates.push(MatchedParamCandidate(vtable_param));
+                    return Ok(());
+                }
+
+                None => {
+                }
+            }
+        }
+
+        Ok(())
+    }
+
+    fn assemble_unboxed_candidates(&self,
+                                   obligation: &Obligation,
+                                   skol_obligation_self_ty: ty::t,
+                                   candidates: &mut Vec<Candidate>)
+                                   -> Result<(),SelectionError>
+    {
+        /*!
+         * Check for the artificial impl that the compiler will create
+         * for an obligation like `X : FnMut<..>` where `X` is an
+         * unboxed closure type.
+         */
+
+        let closure_def_id = match ty::get(skol_obligation_self_ty).sty {
+            ty::ty_unboxed_closure(id, _) => id,
+            _ => { return Ok(()); }
+        };
+
+        let tcx = self.tcx();
+        let fn_traits = [
+            (ty::FnUnboxedClosureKind, tcx.lang_items.fn_trait()),
+            (ty::FnMutUnboxedClosureKind, tcx.lang_items.fn_mut_trait()),
+            (ty::FnOnceUnboxedClosureKind, tcx.lang_items.fn_once_trait()),
+            ];
+        for tuple in fn_traits.iter() {
+            let kind = match tuple {
+                &(kind, Some(ref fn_trait))
+                    if *fn_trait == obligation.trait_ref.def_id =>
+                {
+                    kind
+                }
+                _ => continue,
+            };
+
+            // Check to see whether the argument and return types match.
+            let closure_kind = match self.unboxed_closures.find(&closure_def_id) {
+                Some(closure) => closure.kind,
+                None => {
+                    self.tcx().sess.span_bug(
+                        obligation.cause.span,
+                        format!("No entry for unboxed closure: {}",
+                                closure_def_id.repr(self.tcx())).as_slice());
+                }
+            };
+
+            if closure_kind != kind {
+                continue;
+            }
+
+            candidates.push(MatchedUnboxedClosureCandidate(closure_def_id));
+        }
+
+        Ok(())
+    }
+
+    fn assemble_candidates_from_impls(&self,
+                                      obligation: &Obligation,
+                                      skol_obligation_self_ty: ty::t,
+                                      candidates: &mut Vec<Candidate>)
+                                      -> Result<(), SelectionError>
+    {
+        /*!
+         * Search for impls that might apply to `obligation`.
+         */
+
+        let all_impls = self.all_impls(obligation.trait_ref.def_id);
+        for &impl_def_id in all_impls.iter() {
+            self.infcx.probe(|| {
+                match self.candidate_from_impl(impl_def_id,
+                                               obligation.cause,
+                                               skol_obligation_self_ty) {
+                    Some(c) => {
+                        candidates.push(Impl(c));
+                    }
+
+                    None => { }
+                }
+            });
+        }
+        Ok(())
+    }
+
+    fn candidate_from_impl(&self,
+                           impl_def_id: ast::DefId,
+                           obligation_cause: ObligationCause,
+                           skol_obligation_self_ty: ty::t)
+                           -> Option<ImplCandidate>
+    {
+        match self.match_impl_self_types(impl_def_id,
+                                         obligation_cause,
+                                         skol_obligation_self_ty) {
+            Matched(_) => {
+                Some(MatchedImplCandidate(impl_def_id))
+            }
+
+            AmbiguousMatch => {
+                Some(AmbiguousImplCandidate(impl_def_id))
+            }
+
+            NoMatch => {
+                None
+            }
+        }
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // CONFIRMATION
+    //
+    // Confirmation unifies the output type parameters of the trait
+    // with the values found in the obligation, possibly yielding a
+    // type error.  See `doc.rs` for more details.
+
+    fn confirm_candidate(&self,
+                         obligation: &Obligation,
+                         candidate: Candidate)
+                         -> SelectionResult<Selection>
+    {
+        debug!("confirm_candidate({}, {})",
+               obligation.repr(self.tcx()),
+               candidate.repr(self.tcx()));
+
+        match candidate {
+            AmbiguousBuiltinCandidate |
+            AmbiguousParamCandidate |
+            Impl(AmbiguousImplCandidate(_)) => {
+                Ok(None)
+            }
+
+            MatchedBuiltinCandidate => {
+                Ok(Some(VtableBuiltin))
+            }
+
+            MatchedParamCandidate(param) => {
+                Ok(Some(VtableParam(
+                    try!(self.confirm_param_candidate(obligation, param)))))
+            }
+
+            Impl(MatchedImplCandidate(impl_def_id)) => {
+                let vtable_impl = try!(self.confirm_impl_candidate(obligation,
+                                                                   impl_def_id));
+                Ok(Some(VtableImpl(vtable_impl)))
+            }
+
+            MatchedUnboxedClosureCandidate(closure_def_id) => {
+                try!(self.confirm_unboxed_closure_candidate(obligation, closure_def_id));
+                Ok(Some(VtableUnboxedClosure(closure_def_id)))
+            }
+        }
+    }
+
+    fn confirm_param_candidate(&self,
+                               obligation: &Obligation,
+                               param: VtableParam)
+                               -> Result<VtableParam,SelectionError>
+    {
+        debug!("confirm_param_candidate({},{})",
+               obligation.repr(self.tcx()),
+               param.repr(self.tcx()));
+
+        let () = try!(self.confirm(obligation.cause,
+                                   obligation.trait_ref.clone(),
+                                   param.bound.clone()));
+        Ok(param)
+    }
+
+    fn confirm_impl_candidate(&self,
+                              obligation: &Obligation,
+                              impl_def_id: ast::DefId)
+                              -> Result<VtableImpl<Obligation>,SelectionError>
+    {
+        debug!("confirm_impl_candidate({},{})",
+               obligation.repr(self.tcx()),
+               impl_def_id.repr(self.tcx()));
+
+        // For a non-inhernet impl, we begin the same way as an
+        // inherent impl, by matching the self-type and assembling
+        // list of nested obligations.
+        let vtable_impl =
+            try!(self.confirm_inherent_impl_candidate(
+                impl_def_id,
+                obligation.cause,
+                obligation.trait_ref.self_ty(),
+                obligation.recursion_depth));
+
+        // But then we must also match the output types.
+        let () = try!(self.confirm_impl_vtable(impl_def_id,
+                                               obligation.cause,
+                                               obligation.trait_ref.clone(),
+                                               &vtable_impl.substs));
+        Ok(vtable_impl)
+    }
+
+    fn confirm_inherent_impl_candidate(&self,
+                                       impl_def_id: ast::DefId,
+                                       obligation_cause: ObligationCause,
+                                       obligation_self_ty: ty::t,
+                                       obligation_recursion_depth: uint)
+                                       -> Result<VtableImpl<Obligation>,
+                                                 SelectionError>
+    {
+        let substs = match self.match_impl_self_types(impl_def_id,
+                                                      obligation_cause,
+                                                      obligation_self_ty) {
+            Matched(substs) => substs,
+            AmbiguousMatch | NoMatch => {
+                self.tcx().sess.bug(
+                    format!("Impl {} was matchable against {} but now is not",
+                            impl_def_id.repr(self.tcx()),
+                            obligation_self_ty.repr(self.tcx()))
+                        .as_slice());
+            }
+        };
+
+        let impl_obligations =
+            self.impl_obligations(obligation_cause,
+                                  obligation_recursion_depth,
+                                  impl_def_id,
+                                  &substs);
+        let vtable_impl = VtableImpl { impl_def_id: impl_def_id,
+                                       substs: substs,
+                                       nested: impl_obligations };
+
+        Ok(vtable_impl)
+    }
+
+    fn confirm_unboxed_closure_candidate(&self,
+                                         obligation: &Obligation,
+                                         closure_def_id: ast::DefId)
+                                         -> Result<(),SelectionError>
+    {
+        debug!("confirm_unboxed_closure_candidate({},{})",
+               obligation.repr(self.tcx()),
+               closure_def_id.repr(self.tcx()));
+
+        let closure_type = match self.unboxed_closures.find(&closure_def_id) {
+            Some(closure) => closure.closure_type.clone(),
+            None => {
+                self.tcx().sess.span_bug(
+                    obligation.cause.span,
+                    format!("No entry for unboxed closure: {}",
+                            closure_def_id.repr(self.tcx())).as_slice());
+            }
+        };
+
+        // FIXME(pcwalton): This is a bogus thing to do, but
+        // it'll do for now until we get the new trait-bound
+        // region skolemization working.
+        let (_, new_signature) =
+            regionmanip::replace_late_bound_regions_in_fn_sig(
+                self.tcx(),
+                &closure_type.sig,
+                |br| self.infcx.next_region_var(
+                         infer::LateBoundRegion(obligation.cause.span, br)));
+
+        let arguments_tuple = *new_signature.inputs.get(0);
+        let trait_ref = Rc::new(ty::TraitRef {
+            def_id: obligation.trait_ref.def_id,
+            substs: Substs::new_trait(
+                vec![arguments_tuple, new_signature.output],
+                vec![],
+                obligation.self_ty())
+        });
+
+        self.confirm(obligation.cause,
+                     obligation.trait_ref.clone(),
+                     trait_ref)
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // Matching
+    //
+    // Matching is a common path used for both evaluation and
+    // confirmation.  It basically unifies types that appear in impls
+    // and traits. This does affect the surrounding environment;
+    // therefore, when used during evaluation, match routines must be
+    // run inside of a `probe()` so that their side-effects are
+    // contained.
+
+    fn match_impl_self_types(&self,
+                             impl_def_id: ast::DefId,
+                             obligation_cause: ObligationCause,
+                             obligation_self_ty: ty::t)
+                             -> MatchResult<Substs>
+    {
+        /*!
+         * Determines whether the self type declared against
+         * `impl_def_id` matches `obligation_self_ty`. If successful,
+         * returns the substitutions used to make them match. See
+         * `match_impl()`.  For example, if `impl_def_id` is declared
+         * as:
+         *
+         *    impl<T:Copy> Foo for ~T { ... }
+         *
+         * and `obligation_self_ty` is `int`, we'd back an `Err(_)`
+         * result. But if `obligation_self_ty` were `~int`, we'd get
+         * back `Ok(T=int)`.
+         */
+
+        // Create fresh type variables for each type parameter declared
+        // on the impl etc.
+        let impl_substs = util::fresh_substs_for_impl(self.infcx,
+                                                      obligation_cause.span,
+                                                      impl_def_id);
+
+        // Find the self type for the impl.
+        let impl_self_ty = ty::lookup_item_type(self.tcx(), impl_def_id).ty;
+        let impl_self_ty = impl_self_ty.subst(self.tcx(), &impl_substs);
+
+        debug!("match_impl_self_types(obligation_self_ty={}, impl_self_ty={})",
+               obligation_self_ty.repr(self.tcx()),
+               impl_self_ty.repr(self.tcx()));
+
+        match self.match_self_types(obligation_cause,
+                                    impl_self_ty,
+                                    obligation_self_ty) {
+            Matched(()) => {
+                debug!("Matched impl_substs={}", impl_substs.repr(self.tcx()));
+                Matched(impl_substs)
+            }
+            AmbiguousMatch => {
+                debug!("AmbiguousMatch");
+                AmbiguousMatch
+            }
+            NoMatch => {
+                debug!("NoMatch");
+                NoMatch
+            }
+        }
+    }
+
+    fn match_self_types(&self,
+                        cause: ObligationCause,
+
+                        // The self type provided by the impl/caller-obligation:
+                        provided_self_ty: ty::t,
+
+                        // The self type the obligation is for:
+                        required_self_ty: ty::t)
+                        -> MatchResult<()>
+    {
+        // FIXME(#5781) -- equating the types is stronger than
+        // necessary. Should consider variance of trait w/r/t Self.
+
+        let origin = infer::RelateSelfType(cause.span);
+        match self.infcx.eq_types(false,
+                                  origin,
+                                  provided_self_ty,
+                                  required_self_ty) {
+            Ok(()) => Matched(()),
+            Err(ty::terr_sorts(ty::expected_found{expected: t1, found: t2})) => {
+                // This error occurs when there is an unresolved type
+                // variable in the `required_self_ty` that was forced
+                // to unify with a non-type-variable. That basically
+                // means we don't know enough to say with certainty
+                // whether there is a match or not -- it depends on
+                // how that type variable is ultimately resolved.
+                if ty::type_is_skolemized(t1) || ty::type_is_skolemized(t2) {
+                    AmbiguousMatch
+                } else {
+                    NoMatch
+                }
+            }
+            Err(_) => NoMatch,
+        }
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // Confirmation
+    //
+    // The final step of selection: once we know how an obligation is
+    // is resolved, we confirm that selection in order to have
+    // side-effects on the typing environment. This step also unifies
+    // the output type parameters from the obligation with those found
+    // on the impl/bound, which may yield type errors.
+
+    fn confirm_impl_vtable(&self,
+                           impl_def_id: ast::DefId,
+                           obligation_cause: ObligationCause,
+                           obligation_trait_ref: Rc<ty::TraitRef>,
+                           substs: &Substs)
+                           -> Result<(), SelectionError>
+    {
+        /*!
+         * Relates the output type parameters from an impl to the
+         * trait.  This may lead to type errors. The confirmation step
+         * is separated from the main match procedure because these
+         * type errors do not cause us to select another impl.
+         *
+         * As an example, consider matching the obligation
+         * `Iterator<char> for Elems<int>` using the following impl:
+         *
+         *    impl<T> Iterator<T> for Elems<T> { ... }
+         *
+         * The match phase will succeed with substitution `T=int`.
+         * The confirm step will then try to unify `int` and `char`
+         * and yield an error.
+         */
+
+        let impl_trait_ref = ty::impl_trait_ref(self.tcx(),
+                                                impl_def_id).unwrap();
+        let impl_trait_ref = impl_trait_ref.subst(self.tcx(),
+                                                  substs);
+        self.confirm(obligation_cause, obligation_trait_ref, impl_trait_ref)
+    }
+
+    fn confirm(&self,
+               obligation_cause: ObligationCause,
+               obligation_trait_ref: Rc<ty::TraitRef>,
+               expected_trait_ref: Rc<ty::TraitRef>)
+               -> Result<(), SelectionError>
+    {
+        /*!
+         * After we have determined which impl applies, and with what
+         * substitutions, there is one last step. We have to go back
+         * and relate the "output" type parameters from the obligation
+         * to the types that are specified in the impl.
+         *
+         * For example, imagine we have:
+         *
+         *     impl<T> Iterator<T> for Vec<T> { ... }
+         *
+         * and our obligation is `Iterator<Foo> for Vec<int>` (note
+         * the mismatch in the obligation types). Up until this step,
+         * no error would be reported: the self type is `Vec<int>`,
+         * and that matches `Vec<T>` with the substitution `T=int`.
+         * At this stage, we could then go and check that the type
+         * parameters to the `Iterator` trait match.
+         * (In terms of the parameters, the `expected_trait_ref`
+         * here would be `Iterator<int> for Vec<int>`, and the
+         * `obligation_trait_ref` would be `Iterator<Foo> for Vec<int>`.
+         *
+         * Note that this checking occurs *after* the impl has
+         * selected, because these output type parameters should not
+         * affect the selection of the impl. Therefore, if there is a
+         * mismatch, we report an error to the user.
+         */
+
+        let origin = infer::RelateOutputImplTypes(obligation_cause.span);
+
+        let obligation_trait_ref = obligation_trait_ref.clone();
+        match self.infcx.sub_trait_refs(false,
+                                        origin,
+                                        expected_trait_ref.clone(),
+                                        obligation_trait_ref) {
+            Ok(()) => Ok(()),
+            Err(e) => Err(OutputTypeParameterMismatch(expected_trait_ref, e))
+        }
+    }
+
+    ///////////////////////////////////////////////////////////////////////////
+    // Miscellany
+
+    fn all_impls(&self, trait_def_id: ast::DefId) -> Vec<ast::DefId> {
+        /*!
+         * Returns se tof all impls for a given trait.
+         */
+
+        ty::populate_implementations_for_trait_if_necessary(self.tcx(),
+                                                            trait_def_id);
+        match self.tcx().trait_impls.borrow().find(&trait_def_id) {
+            None => Vec::new(),
+            Some(impls) => impls.borrow().clone()
+        }
+    }
+
+    fn impl_obligations(&self,
+                        cause: ObligationCause,
+                        recursion_depth: uint,
+                        impl_def_id: ast::DefId,
+                        impl_substs: &Substs)
+                        -> VecPerParamSpace<Obligation>
+    {
+        let impl_generics = ty::lookup_item_type(self.tcx(),
+                                                 impl_def_id).generics;
+        util::obligations_for_generics(self.tcx(), cause, recursion_depth,
+                                       &impl_generics, impl_substs)
+    }
+
+    fn trait_ref_unconstrained(&self,
+                               trait_ref: &ty::TraitRef)
+                               -> bool
+    {
+        /*!
+         * True if the self type of the trait-ref contains
+         * unconstrained type variables.
+         */
+
+        let mut found_skol = false;
+
+        // Skolemization replaces all unconstrained type vars with
+        // a SkolemizedTy instance. Then we search to see if we
+        // found any.
+        let skol_ty = infer::skolemize(self.infcx, trait_ref.self_ty());
+        ty::walk_ty(skol_ty, |t| {
+            match ty::get(t).sty {
+                ty::ty_infer(ty::SkolemizedTy(_)) => { found_skol = true; }
+                _ => { }
+            }
+        });
+
+        found_skol
+    }
+}
+
+impl Candidate {
+    fn to_evaluation_result(&self) -> EvaluationResult {
+        match *self {
+            Impl(ref i) => i.to_evaluation_result(),
+
+            MatchedUnboxedClosureCandidate(..) |
+            MatchedBuiltinCandidate |
+            MatchedParamCandidate(..) => {
+                EvaluatedToMatch
+            }
+
+            AmbiguousBuiltinCandidate |
+            AmbiguousParamCandidate => {
+                EvaluatedToAmbiguity
+            }
+        }
+    }
+}
+
+impl ImplCandidate {
+    fn to_evaluation_result(&self) -> EvaluationResult {
+        match *self {
+            MatchedImplCandidate(..) => EvaluatedToMatch,
+            AmbiguousImplCandidate(..) => EvaluatedToAmbiguity
+        }
+    }
+}
+
+impl Repr for Candidate {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        match *self {
+            MatchedBuiltinCandidate => format!("MatchedBuiltinCandidate"),
+            AmbiguousBuiltinCandidate => format!("AmbiguousBuiltinCandidate"),
+            MatchedUnboxedClosureCandidate(c) => format!("MatchedUnboxedClosureCandidate({})", c),
+            MatchedParamCandidate(ref r) => format!("MatchedParamCandidate({})",
+                                                    r.repr(tcx)),
+            AmbiguousParamCandidate => format!("AmbiguousParamCandidate"),
+            Impl(ref i) => i.repr(tcx)
+        }
+    }
+}
+
+impl Repr for ImplCandidate {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        match *self {
+            MatchedImplCandidate(ref d) => format!("MatchedImplCandidate({})",
+                                                   d.repr(tcx)),
+            AmbiguousImplCandidate(ref d) => format!("AmbiguousImplCandidate({})",
+                                                     d.repr(tcx)),
+        }
+    }
+}
+
+
+// impl SelectionCache {
+//     pub fn new() -> SelectionCache {
+//         SelectionCache {
+//             hashmap: RefCell::new(HashMap::new())
+//         }
+//     }
+// }
+
+// impl CacheKey {
+//     pub fn new(trait_def_id: ast::DefId,
+//                skol_obligation_self_ty: ty::t)
+//                -> CacheKey
+//     {
+//         CacheKey {
+//             trait_def_id: trait_def_id,
+//             skol_obligation_self_ty: skol_obligation_self_ty
+//         }
+//     }
+// }
diff --git a/src/librustc/middle/traits/util.rs b/src/librustc/middle/traits/util.rs
new file mode 100644
index 00000000000..11b954f2ba6
--- /dev/null
+++ b/src/librustc/middle/traits/util.rs
@@ -0,0 +1,356 @@
+
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+use middle::subst;
+use middle::subst::{ParamSpace, Subst, Substs, VecPerParamSpace};
+use middle::typeck::infer::InferCtxt;
+use middle::ty;
+use std::fmt;
+use std::rc::Rc;
+use syntax::ast;
+use syntax::codemap::Span;
+use util::ppaux::Repr;
+
+use super::{Obligation, ObligationCause, VtableImpl, VtableParam};
+
+///////////////////////////////////////////////////////////////////////////
+// Supertrait iterator
+
+pub struct Supertraits<'cx, 'tcx:'cx> {
+    tcx: &'cx ty::ctxt<'tcx>,
+    stack: Vec<SupertraitEntry>,
+}
+
+struct SupertraitEntry {
+    position: uint,
+    supertraits: Vec<Rc<ty::TraitRef>>,
+}
+
+pub fn supertraits<'cx, 'tcx>(tcx: &'cx ty::ctxt<'tcx>,
+                              trait_ref: Rc<ty::TraitRef>)
+                              -> Supertraits<'cx, 'tcx>
+{
+    /*!
+     * Returns an iterator over the trait reference `T` and all of its
+     * supertrait references. May contain duplicates. In general
+     * the ordering is not defined.
+     *
+     * Example:
+     *
+     * ```
+     * trait Foo { ... }
+     * trait Bar : Foo { ... }
+     * trait Baz : Bar+Foo { ... }
+     * ```
+     *
+     * `supertraits(Baz)` yields `[Baz, Bar, Foo, Foo]` in some order.
+     */
+
+    transitive_bounds(tcx, [trait_ref])
+}
+
+pub fn transitive_bounds<'cx, 'tcx>(tcx: &'cx ty::ctxt<'tcx>,
+                                    bounds: &[Rc<ty::TraitRef>])
+                                    -> Supertraits<'cx, 'tcx>
+{
+    let bounds = Vec::from_fn(bounds.len(), |i| bounds[i].clone());
+    let entry = SupertraitEntry { position: 0, supertraits: bounds };
+    Supertraits { tcx: tcx, stack: vec![entry] }
+}
+
+impl<'cx, 'tcx> Supertraits<'cx, 'tcx> {
+    fn push(&mut self, trait_ref: &ty::TraitRef) {
+        let bounds = ty::bounds_for_trait_ref(self.tcx, trait_ref);
+        let entry = SupertraitEntry { position: 0,
+                                      supertraits: bounds.trait_bounds };
+        self.stack.push(entry);
+    }
+
+    pub fn indices(&self) -> Vec<uint> {
+        /*!
+         * Returns the path taken through the trait supertraits to
+         * reach the current point.
+         */
+
+        self.stack.iter().map(|e| e.position).collect()
+    }
+}
+
+impl<'cx, 'tcx> Iterator<Rc<ty::TraitRef>> for Supertraits<'cx, 'tcx> {
+    fn next(&mut self) -> Option<Rc<ty::TraitRef>> {
+        loop {
+            // Extract next item from top-most stack frame, if any.
+            let next_trait = match self.stack.mut_last() {
+                None => {
+                    // No more stack frames. Done.
+                    return None;
+                }
+                Some(entry) => {
+                    let p = entry.position;
+                    if p < entry.supertraits.len() {
+                        // Still more supertraits left in the top stack frame.
+                        entry.position += 1;
+
+                        let next_trait =
+                            (*entry.supertraits.get(p)).clone();
+                        Some(next_trait)
+                    } else {
+                        None
+                    }
+                }
+            };
+
+            match next_trait {
+                Some(next_trait) => {
+                    self.push(&*next_trait);
+                    return Some(next_trait);
+                }
+
+                None => {
+                    // Top stack frame is exhausted, pop it.
+                    self.stack.pop();
+                }
+            }
+        }
+    }
+}
+
+// determine the `self` type, using fresh variables for all variables
+// declared on the impl declaration e.g., `impl<A,B> for ~[(A,B)]`
+// would return ($0, $1) where $0 and $1 are freshly instantiated type
+// variables.
+pub fn fresh_substs_for_impl(infcx: &InferCtxt,
+                             span: Span,
+                             impl_def_id: ast::DefId)
+                             -> Substs
+{
+    let tcx = infcx.tcx;
+    let impl_generics = ty::lookup_item_type(tcx, impl_def_id).generics;
+    infcx.fresh_substs_for_generics(span, &impl_generics)
+}
+
+impl<N> fmt::Show for VtableImpl<N> {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "VtableImpl({})", self.impl_def_id)
+    }
+}
+
+impl fmt::Show for VtableParam {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        write!(f, "VtableParam(...)")
+    }
+}
+
+pub fn obligations_for_generics(tcx: &ty::ctxt,
+                                cause: ObligationCause,
+                                recursion_depth: uint,
+                                generics: &ty::Generics,
+                                substs: &Substs)
+                                -> VecPerParamSpace<Obligation>
+{
+    /*! See `super::obligations_for_generics` */
+
+    debug!("obligations_for_generics(generics={}, substs={})",
+           generics.repr(tcx), substs.repr(tcx));
+
+    let mut obligations = VecPerParamSpace::empty();
+
+    for def in generics.types.iter() {
+        push_obligations_for_param_bounds(tcx,
+                                          cause,
+                                          recursion_depth,
+                                          def.space,
+                                          def.index,
+                                          &def.bounds,
+                                          substs,
+                                          &mut obligations);
+    }
+
+    debug!("obligations() ==> {}", obligations.repr(tcx));
+
+    return obligations;
+}
+
+fn push_obligations_for_param_bounds(
+    tcx: &ty::ctxt,
+    cause: ObligationCause,
+    recursion_depth: uint,
+    space: subst::ParamSpace,
+    index: uint,
+    param_bounds: &ty::ParamBounds,
+    param_substs: &Substs,
+    obligations: &mut VecPerParamSpace<Obligation>)
+{
+    let param_ty = *param_substs.types.get(space, index);
+
+    for builtin_bound in param_bounds.builtin_bounds.iter() {
+        obligations.push(
+            space,
+            obligation_for_builtin_bound(tcx,
+                                         cause,
+                                         builtin_bound,
+                                         recursion_depth,
+                                         param_ty));
+    }
+
+    for bound_trait_ref in param_bounds.trait_bounds.iter() {
+        let bound_trait_ref = bound_trait_ref.subst(tcx, param_substs);
+        obligations.push(
+            space,
+            Obligation { cause: cause,
+                         recursion_depth: recursion_depth,
+                         trait_ref: bound_trait_ref });
+    }
+}
+
+pub fn obligation_for_builtin_bound(
+    tcx: &ty::ctxt,
+    cause: ObligationCause,
+    builtin_bound: ty::BuiltinBound,
+    recursion_depth: uint,
+    param_ty: ty::t)
+    -> Obligation
+{
+    match tcx.lang_items.from_builtin_kind(builtin_bound) {
+        Ok(def_id) => {
+            Obligation {
+                cause: cause,
+                recursion_depth: recursion_depth,
+                trait_ref: Rc::new(ty::TraitRef {
+                    def_id: def_id,
+                    substs: Substs::empty().with_self_ty(param_ty),
+                }),
+            }
+        }
+        Err(e) => {
+            tcx.sess.span_bug(cause.span, e.as_slice());
+        }
+    }
+}
+
+pub fn search_trait_and_supertraits_from_bound(tcx: &ty::ctxt,
+                                               caller_bound: Rc<ty::TraitRef>,
+                                               test: |ast::DefId| -> bool)
+                                               -> Option<VtableParam>
+{
+    /*!
+     * Starting from a caller obligation `caller_bound` (which has
+     * coordinates `space`/`i` in the list of caller obligations),
+     * search through the trait and supertraits to find one where
+     * `test(d)` is true, where `d` is the def-id of the
+     * trait/supertrait.  If any is found, return `Some(p)` where `p`
+     * is the path to that trait/supertrait. Else `None`.
+     */
+
+    for (bound_index, bound) in
+        transitive_bounds(tcx, &[caller_bound]).enumerate()
+    {
+        if test(bound.def_id) {
+            let vtable_param = VtableParam { bound: bound };
+            return Some(vtable_param);
+        }
+    }
+
+    return None;
+}
+
+impl Repr for super::Obligation {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        format!("Obligation(trait_ref={},depth={})",
+                self.trait_ref.repr(tcx),
+                self.recursion_depth)
+    }
+}
+
+impl<N:Repr> Repr for super::Vtable<N> {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        match *self {
+            super::VtableImpl(ref v) =>
+                v.repr(tcx),
+
+            super::VtableUnboxedClosure(ref d) =>
+                format!("VtableUnboxedClosure({})",
+                        d.repr(tcx)),
+
+            super::VtableParam(ref v) =>
+                format!("VtableParam({})", v.repr(tcx)),
+
+            super::VtableBuiltin =>
+                format!("Builtin"),
+        }
+    }
+}
+
+impl<N:Repr> Repr for super::VtableImpl<N> {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        format!("VtableImpl(impl_def_id={}, substs={}, nested={})",
+                self.impl_def_id.repr(tcx),
+                self.substs.repr(tcx),
+                self.nested.repr(tcx))
+    }
+}
+
+impl Repr for super::VtableParam {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        format!("VtableParam(bound={})",
+                self.bound.repr(tcx))
+    }
+}
+
+impl Repr for super::SelectionError {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        match *self {
+            super::Unimplemented =>
+                format!("Unimplemented"),
+
+            super::Overflow =>
+                format!("Overflow"),
+
+            super::OutputTypeParameterMismatch(ref t, ref e) =>
+                format!("OutputTypeParameterMismatch({}, {})",
+                        t.repr(tcx),
+                        e.repr(tcx)),
+        }
+    }
+}
+
+impl Repr for super::FulfillmentError {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        format!("FulfillmentError({},{})",
+                self.obligation.repr(tcx),
+                self.code.repr(tcx))
+    }
+}
+
+impl Repr for super::FulfillmentErrorCode {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        match *self {
+            super::SelectionError(ref o) => o.repr(tcx),
+            super::Ambiguity => format!("Ambiguity")
+        }
+    }
+}
+
+impl fmt::Show for super::FulfillmentErrorCode {
+    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
+        match *self {
+            super::SelectionError(ref e) => write!(f, "{}", e),
+            super::Ambiguity => write!(f, "Ambiguity")
+        }
+    }
+}
+
+impl Repr for ty::type_err {
+    fn repr(&self, tcx: &ty::ctxt) -> String {
+        ty::type_err_to_str(tcx, self)
+    }
+}
+
diff --git a/src/librustc/middle/ty.rs b/src/librustc/middle/ty.rs
index bf35e25635a..643c52e5d52 100644
--- a/src/librustc/middle/ty.rs
+++ b/src/librustc/middle/ty.rs
@@ -1089,7 +1089,13 @@ pub struct RegionVid {
 pub enum InferTy {
     TyVar(TyVid),
     IntVar(IntVid),
-    FloatVar(FloatVid)
+    FloatVar(FloatVid),
+    SkolemizedTy(uint),
+
+    // FIXME -- once integral fallback is impl'd, we should remove
+    // this type. It's only needed to prevent spurious errors for
+    // integers whose type winds up never being constrained.
+    SkolemizedIntTy(uint),
 }
 
 #[deriving(Clone, Encodable, Decodable, Eq, Hash, Show)]
@@ -1152,6 +1158,8 @@ impl fmt::Show for InferTy {
             TyVar(ref v) => v.fmt(f),
             IntVar(ref v) => v.fmt(f),
             FloatVar(ref v) => v.fmt(f),
+            SkolemizedTy(v) => write!(f, "SkolemizedTy({})", v),
+            SkolemizedIntTy(v) => write!(f, "SkolemizedIntTy({})", v),
         }
     }
 }
@@ -1207,6 +1215,12 @@ impl Generics {
     }
 }
 
+impl TraitRef {
+    pub fn self_ty(&self) -> ty::t {
+        self.substs.self_ty().unwrap()
+    }
+}
+
 /// When type checking, we use the `ParameterEnvironment` to track
 /// details about the type/lifetime parameters that are in scope.
 /// It primarily stores the bounds information.
@@ -1235,6 +1249,14 @@ pub struct ParameterEnvironment {
     /// may specify stronger requirements). This field indicates the
     /// region of the callee.
     pub implicit_region_bound: ty::Region,
+
+    /// Obligations that the caller must satisfy. This is basically
+    /// the set of bounds on the in-scope type parameters, translated
+    /// into Obligations.
+    ///
+    /// Note: This effectively *duplicates* the `bounds` array for
+    /// now.
+    pub caller_obligations: VecPerParamSpace<traits::Obligation>,
 }
 
 impl ParameterEnvironment {
@@ -1249,6 +1271,7 @@ impl ParameterEnvironment {
                                 let method_generics = &method_ty.generics;
                                 construct_parameter_environment(
                                     cx,
+                                    method.span,
                                     method_generics,
                                     method.pe_body().id)
                             }
@@ -1272,6 +1295,7 @@ impl ParameterEnvironment {
                                 let method_generics = &method_ty.generics;
                                 construct_parameter_environment(
                                     cx,
+                                    method.span,
                                     method_generics,
                                     method.pe_body().id)
                             }
@@ -1287,6 +1311,7 @@ impl ParameterEnvironment {
                         let fn_pty = ty::lookup_item_type(cx, fn_def_id);
 
                         construct_parameter_environment(cx,
+                                                        item.span,
                                                         &fn_pty.generics,
                                                         body.id)
                     }
@@ -1296,7 +1321,8 @@ impl ParameterEnvironment {
                     ast::ItemStatic(..) => {
                         let def_id = ast_util::local_def(id);
                         let pty = ty::lookup_item_type(cx, def_id);
-                        construct_parameter_environment(cx, &pty.generics, id)
+                        construct_parameter_environment(cx, item.span,
+                                                        &pty.generics, id)
                     }
                     _ => {
                         cx.sess.span_bug(item.span,
@@ -1328,7 +1354,14 @@ pub struct Polytype {
 
 /// As `Polytype` but for a trait ref.
 pub struct TraitDef {
+    /// Generic type definitions. Note that `Self` is listed in here
+    /// as having a single bound, the trait itself (e.g., in the trait
+    /// `Eq`, there is a single bound `Self : Eq`). This is so that
+    /// default methods get to assume that the `Self` parameters
+    /// implements the trait.
     pub generics: Generics,
+
+    /// The "supertrait" bounds.
     pub bounds: ParamBounds,
     pub trait_ref: Rc<ty::TraitRef>,
 }
@@ -1345,6 +1378,7 @@ pub type type_cache = RefCell<DefIdMap<Polytype>>;
 pub type node_type_table = RefCell<HashMap<uint,t>>;
 
 /// Records information about each unboxed closure.
+#[deriving(Clone)]
 pub struct UnboxedClosure {
     /// The type of the unboxed closure.
     pub closure_type: ClosureTy,
@@ -1352,7 +1386,7 @@ pub struct UnboxedClosure {
     pub kind: UnboxedClosureKind,
 }
 
-#[deriving(PartialEq, Eq)]
+#[deriving(Clone, PartialEq, Eq)]
 pub enum UnboxedClosureKind {
     FnUnboxedClosureKind,
     FnMutUnboxedClosureKind,
@@ -1523,7 +1557,7 @@ pub fn mk_t(cx: &ctxt, st: sty) -> t {
       &ty_enum(_, ref substs) | &ty_struct(_, ref substs) => {
           flags |= sflags(substs);
       }
-      &ty_trait(box ty::TyTrait { ref substs, ref bounds, .. }) => {
+      &ty_trait(box TyTrait { ref substs, ref bounds, .. }) => {
           flags |= sflags(substs);
           flags |= flags_for_bounds(bounds);
       }
@@ -2394,6 +2428,7 @@ pub fn type_contents(cx: &ctxt, ty: t) -> TypeContents {
             }
 
             // Scalar and unique types are sendable, and durable
+            ty_infer(ty::SkolemizedIntTy(_)) |
             ty_nil | ty_bot | ty_bool | ty_int(_) | ty_uint(_) | ty_float(_) |
             ty_bare_fn(_) | ty::ty_char => {
                 TC::None
@@ -2414,7 +2449,7 @@ pub fn type_contents(cx: &ctxt, ty: t) -> TypeContents {
                 }
             }
 
-            ty_trait(box ty::TyTrait { bounds, .. }) => {
+            ty_trait(box TyTrait { bounds, .. }) => {
                 object_contents(cx, bounds) | TC::ReachesFfiUnsafe | TC::Nonsized
             }
 
@@ -2926,6 +2961,14 @@ pub fn type_is_integral(ty: t) -> bool {
     }
 }
 
+pub fn type_is_skolemized(ty: t) -> bool {
+    match get(ty).sty {
+      ty_infer(SkolemizedTy(_)) => true,
+      ty_infer(SkolemizedIntTy(_)) => true,
+      _ => false
+    }
+}
+
 pub fn type_is_uint(ty: t) -> bool {
     match get(ty).sty {
       ty_infer(IntVar(_)) | ty_uint(ast::TyU) => true,
@@ -3760,6 +3803,8 @@ pub fn ty_sort_string(cx: &ctxt, t: t) -> String {
         ty_infer(TyVar(_)) => "inferred type".to_string(),
         ty_infer(IntVar(_)) => "integral variable".to_string(),
         ty_infer(FloatVar(_)) => "floating-point variable".to_string(),
+        ty_infer(SkolemizedTy(_)) => "skolemized type".to_string(),
+        ty_infer(SkolemizedIntTy(_)) => "skolemized integral type".to_string(),
         ty_param(ref p) => {
             if p.space == subst::SelfSpace {
                 "Self".to_string()
@@ -4683,7 +4728,7 @@ pub fn normalize_ty(cx: &ctxt, t: t) -> t {
     struct TypeNormalizer<'a, 'tcx: 'a>(&'a ctxt<'tcx>);
 
     impl<'a, 'tcx> TypeFolder<'tcx> for TypeNormalizer<'a, 'tcx> {
-        fn tcx<'a>(&'a self) -> &'a ctxt<'tcx> { let TypeNormalizer(c) = *self; c }
+        fn tcx(&self) -> &ctxt<'tcx> { let TypeNormalizer(c) = *self; c }
 
         fn fold_ty(&mut self, t: ty::t) -> ty::t {
             match self.tcx().normalized_cache.borrow().find_copy(&t) {
@@ -4783,42 +4828,11 @@ pub fn eval_repeat_count(tcx: &ctxt, count_expr: &ast::Expr) -> uint {
 pub fn each_bound_trait_and_supertraits(tcx: &ctxt,
                                         bounds: &[Rc<TraitRef>],
                                         f: |Rc<TraitRef>| -> bool)
-                                        -> bool {
-    for bound_trait_ref in bounds.iter() {
-        let mut supertrait_set = HashMap::new();
-        let mut trait_refs = Vec::new();
-        let mut i = 0;
-
-        // Seed the worklist with the trait from the bound
-        supertrait_set.insert(bound_trait_ref.def_id, ());
-        trait_refs.push(bound_trait_ref.clone());
-
-        // Add the given trait ty to the hash map
-        while i < trait_refs.len() {
-            debug!("each_bound_trait_and_supertraits(i={:?}, trait_ref={})",
-                   i, trait_refs.get(i).repr(tcx));
-
-            if !f(trait_refs.get(i).clone()) {
-                return false;
-            }
-
-            // Add supertraits to supertrait_set
-            let trait_ref = trait_refs.get(i).clone();
-            let trait_def = lookup_trait_def(tcx, trait_ref.def_id);
-            for supertrait_ref in trait_def.bounds.trait_bounds.iter() {
-                let supertrait_ref = supertrait_ref.subst(tcx, &trait_ref.substs);
-                debug!("each_bound_trait_and_supertraits(supertrait_ref={})",
-                       supertrait_ref.repr(tcx));
-
-                let d_id = supertrait_ref.def_id;
-                if !supertrait_set.contains_key(&d_id) {
-                    // FIXME(#5527) Could have same trait multiple times
-                    supertrait_set.insert(d_id, ());
-                    trait_refs.push(supertrait_ref.clone());
-                }
-            }
-
-            i += 1;
+                                        -> bool
+{
+    for bound_trait_ref in traits::transitive_bounds(tcx, bounds) {
+        if !f(bound_trait_ref) {
+            return false;
         }
     }
     return true;
@@ -5261,8 +5275,22 @@ impl Variance {
     }
 }
 
+pub fn empty_parameter_environment() -> ParameterEnvironment {
+    /*!
+     * Construct a parameter environment suitable for static contexts
+     * or other contexts where there are no free type/lifetime
+     * parameters in scope.
+     */
+
+    ty::ParameterEnvironment { free_substs: Substs::empty(),
+                               bounds: VecPerParamSpace::empty(),
+                               caller_obligations: VecPerParamSpace::empty(),
+                               implicit_region_bound: ty::ReEmpty }
+}
+
 pub fn construct_parameter_environment(
     tcx: &ctxt,
+    span: Span,
     generics: &ty::Generics,
     free_id: ast::NodeId)
     -> ParameterEnvironment
@@ -5321,10 +5349,14 @@ pub fn construct_parameter_environment(
            free_substs.repr(tcx),
            bounds.repr(tcx));
 
+    let obligations = traits::obligations_for_generics(tcx, traits::ObligationCause::misc(span),
+                                                       generics, &free_substs);
+
     return ty::ParameterEnvironment {
         free_substs: free_substs,
         bounds: bounds,
         implicit_region_bound: ty::ReScope(free_id),
+        caller_obligations: obligations,
     };
 
     fn push_region_params(regions: &mut VecPerParamSpace<ty::Region>,
diff --git a/src/librustc/middle/ty_fold.rs b/src/librustc/middle/ty_fold.rs
index bc53568694d..861afee0604 100644
--- a/src/librustc/middle/ty_fold.rs
+++ b/src/librustc/middle/ty_fold.rs
@@ -8,11 +8,38 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
-// Generalized type folding mechanism.
+/*!
+ * Generalized type folding mechanism. The setup is a bit convoluted
+ * but allows for convenient usage. Let T be an instance of some
+ * "foldable type" (one which implements `TypeFoldable`) and F be an
+ * instance of a "folder" (a type which implements `TypeFolder`). Then
+ * the setup is intended to be:
+ *
+ *     T.fold_with(F) --calls--> F.fold_T(T) --calls--> super_fold_T(F, T)
+ *
+ * This way, when you define a new folder F, you can override
+ * `fold_T()` to customize the behavior, and invoke `super_fold_T()`
+ * to get the original behavior. Meanwhile, to actually fold
+ * something, you can just write `T.fold_with(F)`, which is
+ * convenient. (Note that `fold_with` will also transparently handle
+ * things like a `Vec<T>` where T is foldable and so on.)
+ *
+ * In this ideal setup, the only function that actually *does*
+ * anything is `super_fold_T`, which traverses the type `T`. Moreover,
+ * `super_fold_T` should only ever call `T.fold_with()`.
+ *
+ * In some cases, we follow a degenerate pattern where we do not have
+ * a `fold_T` nor `super_fold_T` method. Instead, `T.fold_with`
+ * traverses the structure directly. This is suboptimal because the
+ * behavior cannot be overriden, but it's much less work to implement.
+ * If you ever *do* need an override that doesn't exist, it's not hard
+ * to convert the degenerate pattern into the proper thing.
+ */
 
 use middle::subst;
 use middle::subst::VecPerParamSpace;
 use middle::ty;
+use middle::traits;
 use middle::typeck;
 use std::rc::Rc;
 use syntax::ast;
@@ -97,6 +124,10 @@ pub trait TypeFolder<'tcx> {
     fn fold_item_substs(&mut self, i: ty::ItemSubsts) -> ty::ItemSubsts {
         super_fold_item_substs(self, i)
     }
+
+    fn fold_obligation(&mut self, o: &traits::Obligation) -> traits::Obligation {
+        super_fold_obligation(self, o)
+    }
 }
 
 ///////////////////////////////////////////////////////////////////////////
@@ -110,6 +141,12 @@ pub trait TypeFolder<'tcx> {
 // can easily refactor the folding into the TypeFolder trait as
 // needed.
 
+impl TypeFoldable for () {
+    fn fold_with<'tcx, F:TypeFolder<'tcx>>(&self, _: &mut F) -> () {
+        ()
+    }
+}
+
 impl<T:TypeFoldable> TypeFoldable for Option<T> {
     fn fold_with<'tcx, F: TypeFolder<'tcx>>(&self, folder: &mut F) -> Option<T> {
         self.as_ref().map(|t| t.fold_with(folder))
@@ -296,13 +333,54 @@ impl TypeFoldable for ty::UnsizeKind {
         match *self {
             ty::UnsizeLength(len) => ty::UnsizeLength(len),
             ty::UnsizeStruct(box ref k, n) => ty::UnsizeStruct(box k.fold_with(folder), n),
-            ty::UnsizeVtable(bounds, def_id, ref substs) => {
-                ty::UnsizeVtable(bounds.fold_with(folder), def_id, substs.fold_with(folder))
+            ty::UnsizeVtable(ty::TyTrait{bounds, def_id, substs: ref substs}, self_ty) => {
+                ty::UnsizeVtable(
+                    ty::TyTrait {
+                        bounds: bounds.fold_with(folder),
+                        def_id: def_id,
+                        substs: substs.fold_with(folder)
+                    },
+                    self_ty.fold_with(folder))
             }
         }
     }
 }
 
+impl TypeFoldable for traits::Obligation {
+    fn fold_with<'tcx, F:TypeFolder<'tcx>>(&self, folder: &mut F) -> traits::Obligation {
+        folder.fold_obligation(self)
+    }
+}
+
+impl<N:TypeFoldable> TypeFoldable for traits::VtableImpl<N> {
+    fn fold_with<'tcx, F:TypeFolder<'tcx>>(&self, folder: &mut F) -> traits::VtableImpl<N> {
+        traits::VtableImpl {
+            impl_def_id: self.impl_def_id,
+            substs: self.substs.fold_with(folder),
+            nested: self.nested.fold_with(folder),
+        }
+    }
+}
+
+impl<N:TypeFoldable> TypeFoldable for traits::Vtable<N> {
+    fn fold_with<'tcx, F:TypeFolder<'tcx>>(&self, folder: &mut F) -> traits::Vtable<N> {
+        match *self {
+            traits::VtableImpl(ref v) => traits::VtableImpl(v.fold_with(folder)),
+            traits::VtableUnboxedClosure(d) => traits::VtableUnboxedClosure(d),
+            traits::VtableParam(ref p) => traits::VtableParam(p.fold_with(folder)),
+            traits::VtableBuiltin => traits::VtableBuiltin,
+        }
+    }
+}
+
+impl TypeFoldable for traits::VtableParam {
+    fn fold_with<'tcx, F:TypeFolder<'tcx>>(&self, folder: &mut F) -> traits::VtableParam {
+        traits::VtableParam {
+            bound: self.bound.fold_with(folder),
+        }
+    }
+}
+
 ///////////////////////////////////////////////////////////////////////////
 // "super" routines: these are the default implementations for TypeFolder.
 //
@@ -482,6 +560,17 @@ pub fn super_fold_item_substs<'tcx, T: TypeFolder<'tcx>>(this: &mut T,
     }
 }
 
+pub fn super_fold_obligation<'tcx, T:TypeFolder<'tcx>>(this: &mut T,
+                                                       obligation: &traits::Obligation)
+                                                       -> traits::Obligation
+{
+    traits::Obligation {
+        cause: obligation.cause,
+        recursion_depth: obligation.recursion_depth,
+        trait_ref: obligation.trait_ref.fold_with(this),
+    }
+}
+
 ///////////////////////////////////////////////////////////////////////////
 // Some sample folders
 
diff --git a/src/librustc/middle/typeck/infer/error_reporting.rs b/src/librustc/middle/typeck/infer/error_reporting.rs
index b5b4cc80faa..4f663df5882 100644
--- a/src/librustc/middle/typeck/infer/error_reporting.rs
+++ b/src/librustc/middle/typeck/infer/error_reporting.rs
@@ -363,6 +363,7 @@ impl<'a, 'tcx> ErrorReporting for InferCtxt<'a, 'tcx> {
             infer::ExprAssignable(_) => "mismatched types",
             infer::RelateTraitRefs(_) => "mismatched traits",
             infer::RelateSelfType(_) => "mismatched types",
+            infer::RelateOutputImplTypes(_) => "mismatched types",
             infer::MatchExpressionArm(_, _) => "match arms have incompatible types",
             infer::IfExpression(_) => "if and else have incompatible types",
         };
@@ -1465,7 +1466,11 @@ impl<'a, 'tcx> ErrorReportingHelpers for InferCtxt<'a, 'tcx> {
                         format!("traits are compatible")
                     }
                     infer::RelateSelfType(_) => {
-                        format!("type matches impl")
+                        format!("self type matches impl self type")
+                    }
+                    infer::RelateOutputImplTypes(_) => {
+                        format!("trait type parameters matches those \
+                                 specified on the impl")
                     }
                     infer::MatchExpressionArm(_, _) => {
                         format!("match arms have compatible types")
diff --git a/src/librustc/middle/typeck/infer/mod.rs b/src/librustc/middle/typeck/infer/mod.rs
index f11584e9356..db90593b5b3 100644
--- a/src/librustc/middle/typeck/infer/mod.rs
+++ b/src/librustc/middle/typeck/infer/mod.rs
@@ -26,6 +26,7 @@ use middle::subst::Substs;
 use middle::ty::{TyVid, IntVid, FloatVid, RegionVid};
 use middle::ty;
 use middle::ty_fold;
+use middle::ty_fold::TypeFoldable;
 use middle::ty_fold::TypeFolder;
 use middle::typeck::check::regionmanip::replace_late_bound_regions_in_fn_sig;
 use middle::typeck::infer::coercion::Coerce;
@@ -57,6 +58,7 @@ pub mod lattice;
 pub mod lub;
 pub mod region_inference;
 pub mod resolve;
+mod skolemize;
 pub mod sub;
 pub mod test;
 pub mod type_variable;
@@ -114,9 +116,12 @@ pub enum TypeOrigin {
     // Relating trait refs when resolving vtables
     RelateTraitRefs(Span),
 
-    // Relating trait refs when resolving vtables
+    // Relating self types when resolving vtables
     RelateSelfType(Span),
 
+    // Relating trait type parameters to those found in impl etc
+    RelateOutputImplTypes(Span),
+
     // Computing common supertype in the arms of a match expression
     MatchExpressionArm(Span, Span),
 
@@ -262,6 +267,7 @@ pub enum RegionVariableOrigin {
     BoundRegionInCoherence(ast::Name),
 }
 
+#[deriving(Show)]
 pub enum fixup_err {
     unresolved_int_ty(IntVid),
     unresolved_float_ty(FloatVid),
@@ -336,17 +342,12 @@ pub fn mk_subty(cx: &InferCtxt,
                 origin: TypeOrigin,
                 a: ty::t,
                 b: ty::t)
-             -> ures {
+                -> ures
+{
     debug!("mk_subty({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
-    indent(|| {
-        cx.commit_if_ok(|| {
-            let trace = TypeTrace {
-                origin: origin,
-                values: Types(expected_found(a_is_expected, a, b))
-            };
-            cx.sub(a_is_expected, trace).tys(a, b)
-        })
-    }).to_ures()
+    cx.commit_if_ok(|| {
+        cx.sub_types(a_is_expected, origin, a, b)
+    })
 }
 
 pub fn can_mk_subty(cx: &InferCtxt, a: ty::t, b: ty::t) -> ures {
@@ -356,8 +357,8 @@ pub fn can_mk_subty(cx: &InferCtxt, a: ty::t, b: ty::t) -> ures {
             origin: Misc(codemap::DUMMY_SP),
             values: Types(expected_found(true, a, b))
         };
-        cx.sub(true, trace).tys(a, b)
-    }).to_ures()
+        cx.sub(true, trace).tys(a, b).to_ures()
+    })
 }
 
 pub fn can_mk_eqty(cx: &InferCtxt, a: ty::t, b: ty::t) -> ures {
@@ -393,6 +394,14 @@ pub fn verify_param_bound(cx: &InferCtxt,
 
     cx.region_vars.verify_param_bound(origin, param_ty, a, bs);
 }
+
+pub fn skolemize<T:TypeFoldable+Repr>(cx: &InferCtxt, a: T) -> T {
+    let mut skol = skolemize::TypeSkolemizer::new(cx);
+    let b = a.fold_with(&mut skol);
+    debug!("skol(a={}) -> {}", a.repr(cx.tcx), b.repr(cx.tcx));
+    b
+}
+
 pub fn mk_eqty(cx: &InferCtxt,
                a_is_expected: bool,
                origin: TypeOrigin,
@@ -401,14 +410,8 @@ pub fn mk_eqty(cx: &InferCtxt,
             -> ures
 {
     debug!("mk_eqty({} <: {})", a.repr(cx.tcx), b.repr(cx.tcx));
-    cx.commit_if_ok(|| {
-        let trace = TypeTrace {
-            origin: origin,
-            values: Types(expected_found(a_is_expected, a, b))
-        };
-        try!(cx.equate(a_is_expected, trace).tys(a, b));
-        Ok(())
-    })
+    cx.commit_if_ok(
+        || cx.eq_types(a_is_expected, origin, a, b))
 }
 
 pub fn mk_sub_trait_refs(cx: &InferCtxt,
@@ -416,25 +419,19 @@ pub fn mk_sub_trait_refs(cx: &InferCtxt,
                          origin: TypeOrigin,
                          a: Rc<ty::TraitRef>,
                          b: Rc<ty::TraitRef>)
-    -> ures
+                         -> ures
 {
     debug!("mk_sub_trait_refs({} <: {})",
            a.repr(cx.tcx), b.repr(cx.tcx));
-    indent(|| {
-        cx.commit_if_ok(|| {
-            let trace = TypeTrace {
-                origin: origin,
-                values: TraitRefs(expected_found(a_is_expected, a.clone(), b.clone()))
-            };
-            let suber = cx.sub(a_is_expected, trace);
-            suber.trait_refs(&*a, &*b)
-        })
-    }).to_ures()
+    cx.commit_if_ok(
+        || cx.sub_trait_refs(a_is_expected, origin, a.clone(), b.clone()))
 }
 
 fn expected_found<T>(a_is_expected: bool,
                      a: T,
-                     b: T) -> ty::expected_found<T> {
+                     b: T)
+                     -> ty::expected_found<T>
+{
     if a_is_expected {
         ty::expected_found {expected: a, found: b}
     } else {
@@ -629,7 +626,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
     }
 
     /// Execute `f` then unroll any bindings it creates
-    pub fn probe<T,E>(&self, f: || -> Result<T,E>) -> Result<T,E> {
+    pub fn probe<R>(&self, f: || -> R) -> R {
         debug!("probe()");
         let snapshot = self.start_snapshot();
         let r = f();
@@ -643,6 +640,54 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
     {
         self.region_vars.add_given(sub, sup);
     }
+
+    pub fn sub_types(&self,
+                     a_is_expected: bool,
+                     origin: TypeOrigin,
+                     a: ty::t,
+                     b: ty::t)
+                     -> ures
+    {
+        debug!("sub_types({} <: {})", a.repr(self.tcx), b.repr(self.tcx));
+        let trace = TypeTrace {
+            origin: origin,
+            values: Types(expected_found(a_is_expected, a, b))
+        };
+        self.sub(a_is_expected, trace).tys(a, b).to_ures()
+    }
+
+    pub fn eq_types(&self,
+                    a_is_expected: bool,
+                    origin: TypeOrigin,
+                    a: ty::t,
+                    b: ty::t)
+                    -> ures
+    {
+        let trace = TypeTrace {
+            origin: origin,
+            values: Types(expected_found(a_is_expected, a, b))
+        };
+        self.equate(a_is_expected, trace).tys(a, b).to_ures()
+    }
+
+    pub fn sub_trait_refs(&self,
+                          a_is_expected: bool,
+                          origin: TypeOrigin,
+                          a: Rc<ty::TraitRef>,
+                          b: Rc<ty::TraitRef>)
+                          -> ures
+    {
+        debug!("sub_trait_refs({} <: {})",
+               a.repr(self.tcx),
+               b.repr(self.tcx));
+        let trace = TypeTrace {
+            origin: origin,
+            values: TraitRefs(expected_found(a_is_expected,
+                                             a.clone(), b.clone()))
+        };
+        let suber = self.sub(a_is_expected, trace);
+        suber.trait_refs(&*a, &*b).to_ures()
+    }
 }
 
 impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
@@ -685,17 +730,40 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
             .collect()
     }
 
-    pub fn fresh_substs_for_type(&self,
-                                 span: Span,
-                                 generics: &ty::Generics)
-                                 -> subst::Substs
+    pub fn fresh_substs_for_generics(&self,
+                                     span: Span,
+                                     generics: &ty::Generics)
+                                     -> subst::Substs
     {
         /*!
          * Given a set of generics defined on a type or impl, returns
          * a substitution mapping each type/region parameter to a
          * fresh inference variable.
          */
-        assert!(generics.types.len(subst::SelfSpace) == 0);
+
+        let type_params =
+            generics.types.map(
+                |_| self.next_ty_var());
+        let region_params =
+            generics.regions.map(
+                |d| self.next_region_var(EarlyBoundRegion(span, d.name)));
+        subst::Substs::new(type_params, region_params)
+    }
+
+    pub fn fresh_substs_for_trait(&self,
+                                  span: Span,
+                                  generics: &ty::Generics,
+                                  self_ty: ty::t)
+                                  -> subst::Substs
+    {
+        /*!
+         * Given a set of generics defined on a trait, returns a
+         * substitution mapping each output type/region parameter to a
+         * fresh inference variable, and mapping the self type to
+         * `self_ty`.
+         */
+
+        assert!(generics.types.len(subst::SelfSpace) == 1);
         assert!(generics.types.len(subst::FnSpace) == 0);
         assert!(generics.regions.len(subst::SelfSpace) == 0);
         assert!(generics.regions.len(subst::FnSpace) == 0);
@@ -704,7 +772,7 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         let region_param_defs = generics.regions.get_slice(subst::TypeSpace);
         let regions = self.region_vars_for_defs(span, region_param_defs);
         let type_parameters = self.next_ty_vars(type_parameter_count);
-        subst::Substs::new_type(type_parameters, regions)
+        subst::Substs::new_trait(type_parameters, regions, self_ty)
     }
 
     pub fn fresh_bound_region(&self, binder_id: ast::NodeId) -> ty::Region {
@@ -731,6 +799,15 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         trait_ref_to_string(self.tcx, &t)
     }
 
+    pub fn contains_unbound_type_variables(&self, typ: ty::t) -> ty::t {
+        match resolve_type(self,
+                           None,
+                           typ, resolve_nested_tvar | resolve_ivar) {
+          Ok(new_type) => new_type,
+          Err(_) => typ
+        }
+    }
+
     pub fn resolve_type_vars_if_possible(&self, typ: ty::t) -> ty::t {
         match resolve_type(self,
                            None,
@@ -907,6 +984,7 @@ impl TypeOrigin {
             Misc(span) => span,
             RelateTraitRefs(span) => span,
             RelateSelfType(span) => span,
+            RelateOutputImplTypes(span) => span,
             MatchExpressionArm(match_span, _) => match_span,
             IfExpression(span) => span,
         }
@@ -929,6 +1007,9 @@ impl Repr for TypeOrigin {
             RelateSelfType(a) => {
                 format!("RelateSelfType({})", a.repr(tcx))
             }
+            RelateOutputImplTypes(a) => {
+                format!("RelateOutputImplTypes({})", a.repr(tcx))
+            }
             MatchExpressionArm(a, b) => {
                 format!("MatchExpressionArm({}, {})", a.repr(tcx), b.repr(tcx))
             }
diff --git a/src/librustc/middle/typeck/infer/resolve.rs b/src/librustc/middle/typeck/infer/resolve.rs
index 569206f6754..2c0b2dbe2ba 100644
--- a/src/librustc/middle/typeck/infer/resolve.rs
+++ b/src/librustc/middle/typeck/infer/resolve.rs
@@ -46,7 +46,6 @@
 // future).  If you want to resolve everything but one type, you are
 // probably better off writing `resolve_all - resolve_ivar`.
 
-
 use middle::ty::{FloatVar, FloatVid, IntVar, IntVid, RegionVid, TyVar, TyVid};
 use middle::ty::{IntType, UintType};
 use middle::ty;
@@ -54,7 +53,6 @@ use middle::ty_fold;
 use middle::typeck::infer::{fixup_err, fres, InferCtxt};
 use middle::typeck::infer::{unresolved_int_ty,unresolved_float_ty,unresolved_ty};
 use syntax::codemap::Span;
-use util::common::indent;
 use util::ppaux::{Repr, ty_to_string};
 
 pub static resolve_nested_tvar: uint = 0b0000000001;
@@ -94,7 +92,7 @@ pub fn resolver<'a, 'tcx>(infcx: &'a InferCtxt<'a, 'tcx>,
 }
 
 impl<'a, 'tcx> ty_fold::TypeFolder<'tcx> for ResolveState<'a, 'tcx> {
-    fn tcx<'a>(&'a self) -> &'a ty::ctxt<'tcx> {
+    fn tcx(&self) -> &ty::ctxt<'tcx> {
         self.infcx.tcx
     }
 
@@ -114,7 +112,8 @@ impl<'a, 'tcx> ResolveState<'a, 'tcx> {
 
     pub fn resolve_type_chk(&mut self,
                             typ: ty::t)
-                            -> fres<ty::t> {
+                            -> fres<ty::t>
+    {
         self.err = None;
 
         debug!("Resolving {} (modes={:x})",
@@ -126,14 +125,16 @@ impl<'a, 'tcx> ResolveState<'a, 'tcx> {
 
         let rty = self.resolve_type(typ);
         match self.err {
-          None => {
-            debug!("Resolved {} to {} (modes={:x})",
-                   ty_to_string(self.infcx.tcx, typ),
-                   ty_to_string(self.infcx.tcx, rty),
-                   self.modes);
-            return Ok(rty);
-          }
-          Some(e) => return Err(e)
+            None => {
+                debug!("Resolved {} to {} (modes={:x})",
+                       ty_to_string(self.infcx.tcx, typ),
+                       ty_to_string(self.infcx.tcx, rty),
+                       self.modes);
+                return Ok(rty);
+            }
+            Some(e) => {
+                return Err(e);
+            }
         }
     }
 
@@ -141,7 +142,7 @@ impl<'a, 'tcx> ResolveState<'a, 'tcx> {
                               orig: ty::Region)
                               -> fres<ty::Region> {
         self.err = None;
-        let resolved = indent(|| self.resolve_region(orig) );
+        let resolved = self.resolve_region(orig);
         match self.err {
           None => Ok(resolved),
           Some(e) => Err(e)
diff --git a/src/librustc/middle/typeck/infer/skolemize.rs b/src/librustc/middle/typeck/infer/skolemize.rs
new file mode 100644
index 00000000000..e1d48407f2e
--- /dev/null
+++ b/src/librustc/middle/typeck/infer/skolemize.rs
@@ -0,0 +1,157 @@
+// Copyright 2014 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+/*!
+ * Skolemization is the process of replacing unknown variables with
+ * fresh types. The idea is that the type, after skolemization,
+ * contains no inference variables but instead contains either a value
+ * for each variable (if the variable had already fresh "arbitrary"
+ * types wherever a variable would have been.
+ *
+ * Skolemization is used wherever we want to test what the type
+ * inferencer knows "so far". The primary place it is used right now
+ * is in the trait matching algorithm, which needs to be able to test
+ * whether an `impl` self type matches some other type X -- *without*
+ * affecting `X`. That means if that if the type `X` is in fact an
+ * unbound type variable, we want the match to be regarded as
+ * ambiguous, because depending on what type that type variable is
+ * ultimately assigned, the match may or may not succeed.
+ *
+ * Note that you should be careful not to allow the output of
+ * skolemization to leak to the user in error messages or in any other
+ * form. Skolemization is only really useful as an internal detail.
+ *
+ * __An important detail concerning regions.__ The skolemizer also
+ * replaces *all* regions with 'static. The reason behind this is
+ * that, in general, we do not take region relationships into account
+ * when making type-overloaded decisions. This is important because of
+ * the design of the region inferencer, which is not based on
+ * unification but rather on accumulating and then solving a set of
+ * constraints. In contrast, the type inferencer assigns a value to
+ * each type variable only once, and it does so as soon as it can, so
+ * it is reasonable to ask what the type inferencer knows "so far".
+ */
+
+use middle::ty;
+use middle::ty_fold;
+use middle::ty_fold::TypeFoldable;
+use middle::ty_fold::TypeFolder;
+
+use super::InferCtxt;
+use super::unify::InferCtxtMethodsForSimplyUnifiableTypes;
+use super::unify::SimplyUnifiable;
+use super::unify::UnifyKey;
+
+pub struct TypeSkolemizer<'a, 'tcx:'a> {
+    infcx: &'a InferCtxt<'a, 'tcx>,
+    skolemization_count: uint
+}
+
+impl<'a, 'tcx> TypeSkolemizer<'a, 'tcx> {
+    pub fn new<'tcx>(infcx: &'a InferCtxt<'a, 'tcx>) -> TypeSkolemizer<'a, 'tcx> {
+        TypeSkolemizer { infcx: infcx, skolemization_count: 0 }
+    }
+
+    fn probe_ty(&mut self, v: ty::TyVid) -> ty::t {
+        self.skolemize_if_none(self.infcx.type_variables.borrow().probe(v), ty::SkolemizedTy)
+    }
+
+    fn probe_unifiable<V:SimplyUnifiable,K:UnifyKey<Option<V>>>(&mut self, k: K) -> ty::t {
+        self.skolemize_if_none(self.infcx.probe_var(k), ty::SkolemizedIntTy)
+    }
+
+    fn skolemize_if_none(&mut self, o: Option<ty::t>,
+                         skolemizer: |uint| -> ty::InferTy)
+                         -> ty::t {
+        match o {
+            Some(t) => t.fold_with(self),
+            None => {
+                let index = self.skolemization_count;
+                self.skolemization_count += 1;
+                ty::mk_infer(self.tcx(), skolemizer(index))
+            }
+        }
+    }
+}
+
+impl<'a, 'tcx> TypeFolder<'tcx> for TypeSkolemizer<'a, 'tcx> {
+    fn tcx<'b>(&'b self) -> &'b ty::ctxt<'tcx> {
+        self.infcx.tcx
+    }
+
+    fn fold_region(&mut self, r: ty::Region) -> ty::Region {
+        match r {
+            ty::ReEarlyBound(..) |
+            ty::ReLateBound(..) => {
+                // leave bound regions alone
+                r
+            }
+
+            ty::ReStatic |
+            ty::ReFree(_) |
+            ty::ReScope(_) |
+            ty::ReInfer(_) |
+            ty::ReEmpty => {
+                // replace all free regions with 'static
+                ty::ReStatic
+            }
+        }
+    }
+
+    fn fold_ty(&mut self, t: ty::t) -> ty::t {
+        match ty::get(t).sty {
+            ty::ty_infer(ty::TyVar(v)) => {
+                self.probe_ty(v)
+            }
+
+            ty::ty_infer(ty::IntVar(v)) => {
+                self.probe_unifiable(v)
+            }
+
+            ty::ty_infer(ty::FloatVar(v)) => {
+                self.probe_unifiable(v)
+            }
+
+            ty::ty_infer(ty::SkolemizedTy(_)) |
+            ty::ty_infer(ty::SkolemizedIntTy(_)) => {
+                self.tcx().sess.bug("Cannot skolemize a skolemized type");
+            }
+
+            ty::ty_open(..) => {
+                self.tcx().sess.bug("Cannot skolemize an open existential type");
+            }
+
+            ty::ty_nil |
+            ty::ty_bot |
+            ty::ty_bool |
+            ty::ty_char |
+            ty::ty_int(..) |
+            ty::ty_uint(..) |
+            ty::ty_float(..) |
+            ty::ty_enum(..) |
+            ty::ty_box(..) |
+            ty::ty_uniq(..) |
+            ty::ty_str |
+            ty::ty_err |
+            ty::ty_vec(..) |
+            ty::ty_ptr(..) |
+            ty::ty_rptr(..) |
+            ty::ty_bare_fn(..) |
+            ty::ty_closure(..) |
+            ty::ty_trait(..) |
+            ty::ty_struct(..) |
+            ty::ty_unboxed_closure(..) |
+            ty::ty_tup(..) |
+            ty::ty_param(..) => {
+                ty_fold::super_fold_ty(self, t)
+            }
+        }
+    }
+}
diff --git a/src/librustc/middle/typeck/infer/unify.rs b/src/librustc/middle/typeck/infer/unify.rs
index 22d78340e96..301582d55d6 100644
--- a/src/librustc/middle/typeck/infer/unify.rs
+++ b/src/librustc/middle/typeck/infer/unify.rs
@@ -258,6 +258,7 @@ impl<K,V> sv::SnapshotVecDelegate<VarValue<K,V>,()> for Delegate {
  * relationship.
  */
 pub trait SimplyUnifiable : Clone + PartialEq + Repr {
+    fn to_type(&self) -> ty::t;
     fn to_type_err(expected_found<Self>) -> ty::type_err;
 }
 
@@ -286,6 +287,7 @@ pub trait InferCtxtMethodsForSimplyUnifiableTypes<V:SimplyUnifiable,
                     a_id: K,
                     b: V)
                     -> ures;
+    fn probe_var(&self, a_id: K) -> Option<ty::t>;
 }
 
 impl<'a,'tcx,V:SimplyUnifiable,K:UnifyKey<Option<V>>>
@@ -370,6 +372,16 @@ impl<'a,'tcx,V:SimplyUnifiable,K:UnifyKey<Option<V>>>
             }
         }
     }
+
+    fn probe_var(&self, a_id: K) -> Option<ty::t> {
+        let tcx = self.tcx;
+        let table = UnifyKey::unification_table(self);
+        let node_a = table.borrow_mut().get(tcx, a_id);
+        match node_a.value {
+            None => None,
+            Some(ref a_t) => Some(a_t.to_type())
+        }
+    }
 }
 
 ///////////////////////////////////////////////////////////////////////////
@@ -393,6 +405,13 @@ impl UnifyKey<Option<IntVarValue>> for ty::IntVid {
 }
 
 impl SimplyUnifiable for IntVarValue {
+    fn to_type(&self) -> ty::t {
+        match *self {
+            ty::IntType(i) => ty::mk_mach_int(i),
+            ty::UintType(i) => ty::mk_mach_uint(i),
+        }
+    }
+
     fn to_type_err(err: expected_found<IntVarValue>) -> ty::type_err {
         return ty::terr_int_mismatch(err);
     }
@@ -422,6 +441,10 @@ impl UnifyValue for Option<ast::FloatTy> {
 }
 
 impl SimplyUnifiable for ast::FloatTy {
+    fn to_type(&self) -> ty::t {
+        ty::mk_mach_float(*self)
+    }
+
     fn to_type_err(err: expected_found<ast::FloatTy>) -> ty::type_err {
         return ty::terr_float_mismatch(err);
     }