diff --git a/src/librustc/ty/fold.rs b/src/librustc/ty/fold.rs
index 6f0e8d4f026..5b9193ad74a 100644
--- a/src/librustc/ty/fold.rs
+++ b/src/librustc/ty/fold.rs
@@ -679,24 +679,31 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
 // vars. See comment on `shift_vars_through_binders` method in
 // `subst.rs` for more details.
 
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+enum Direction {
+    In,
+    Out,
+}
+
 struct Shifter<'a, 'gcx: 'a+'tcx, 'tcx: 'a> {
     tcx: TyCtxt<'a, 'gcx, 'tcx>,
-
     current_index: ty::DebruijnIndex,
     amount: u32,
+    direction: Direction,
 }
 
 impl Shifter<'a, 'gcx, 'tcx> {
-    pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32) -> Self {
+    pub fn new(tcx: TyCtxt<'a, 'gcx, 'tcx>, amount: u32, direction: Direction) -> Self {
         Shifter {
             tcx,
             current_index: ty::INNERMOST,
             amount,
+            direction,
         }
     }
 }
 
-impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
+impl TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
     fn tcx<'b>(&'b self) -> TyCtxt<'b, 'gcx, 'tcx> { self.tcx }
 
     fn fold_binder<T: TypeFoldable<'tcx>>(&mut self, t: &ty::Binder<T>) -> ty::Binder<T> {
@@ -712,7 +719,14 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
                 if self.amount == 0 || debruijn < self.current_index {
                     r
                 } else {
-                    let shifted = ty::ReLateBound(debruijn.shifted_in(self.amount), br);
+                    let debruijn = match self.direction {
+                        Direction::In => debruijn.shifted_in(self.amount),
+                        Direction::Out => {
+                            assert!(debruijn.as_u32() >= self.amount);
+                            debruijn.shifted_out(self.amount)
+                        }
+                    };
+                    let shifted = ty::ReLateBound(debruijn, br);
                     self.tcx.mk_region(shifted)
                 }
             }
@@ -726,8 +740,15 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Shifter<'a, 'gcx, 'tcx> {
                 if self.amount == 0 || debruijn < self.current_index {
                     ty
                 } else {
+                    let debruijn = match self.direction {
+                        Direction::In => debruijn.shifted_in(self.amount),
+                        Direction::Out => {
+                            assert!(debruijn.as_u32() >= self.amount);
+                            debruijn.shifted_out(self.amount)
+                        }
+                    };
                     self.tcx.mk_ty(
-                        ty::Bound(debruijn.shifted_in(self.amount), bound_ty)
+                        ty::Bound(debruijn, bound_ty)
                     )
                 }
             }
@@ -760,7 +781,18 @@ pub fn shift_vars<'a, 'gcx, 'tcx, T>(
     debug!("shift_vars(value={:?}, amount={})",
            value, amount);
 
-    value.fold_with(&mut Shifter::new(tcx, amount))
+    value.fold_with(&mut Shifter::new(tcx, amount, Direction::In))
+}
+
+pub fn shift_out_vars<'a, 'gcx, 'tcx, T>(
+    tcx: TyCtxt<'a, 'gcx, 'tcx>,
+    value: &T,
+    amount: u32
+) -> T where T: TypeFoldable<'tcx> {
+    debug!("shift_out_vars(value={:?}, amount={})",
+           value, amount);
+
+    value.fold_with(&mut Shifter::new(tcx, amount, Direction::Out))
 }
 
 /// An "escaping var" is a bound var whose binder is not part of `t`. A bound var can be a
diff --git a/src/librustc/ty/relate.rs b/src/librustc/ty/relate.rs
index 60ad7413cc7..1b64a686794 100644
--- a/src/librustc/ty/relate.rs
+++ b/src/librustc/ty/relate.rs
@@ -25,6 +25,7 @@ use std::rc::Rc;
 use std::iter;
 use rustc_target::spec::abi;
 use hir as ast;
+use traits;
 
 pub type RelateResult<'tcx, T> = Result<T, TypeError<'tcx>>;
 
@@ -723,6 +724,283 @@ impl<'tcx> Relate<'tcx> for Kind<'tcx> {
     }
 }
 
+impl<'tcx> Relate<'tcx> for ty::TraitPredicate<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &ty::TraitPredicate<'tcx>,
+        b: &ty::TraitPredicate<'tcx>
+    ) -> RelateResult<'tcx, ty::TraitPredicate<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        Ok(ty::TraitPredicate {
+            trait_ref: relation.relate(&a.trait_ref, &b.trait_ref)?,
+        })
+    }
+}
+
+impl<'tcx> Relate<'tcx> for ty::ProjectionPredicate<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &ty::ProjectionPredicate<'tcx>,
+        b: &ty::ProjectionPredicate<'tcx>,
+    ) -> RelateResult<'tcx, ty::ProjectionPredicate<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        Ok(ty::ProjectionPredicate {
+            projection_ty: relation.relate(&a.projection_ty, &b.projection_ty)?,
+            ty: relation.relate(&a.ty, &b.ty)?,
+        })
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::WhereClause<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::WhereClause<'tcx>,
+        b: &traits::WhereClause<'tcx>
+    ) -> RelateResult<'tcx, traits::WhereClause<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::WhereClause::*;
+        match (a, b) {
+            (Implemented(a_pred), Implemented(b_pred)) => {
+                Ok(Implemented(relation.relate(a_pred, b_pred)?))
+            }
+
+            (ProjectionEq(a_pred), ProjectionEq(b_pred)) => {
+                Ok(ProjectionEq(relation.relate(a_pred, b_pred)?))
+            }
+
+            (RegionOutlives(a_pred), RegionOutlives(b_pred)) => {
+                Ok(RegionOutlives(ty::OutlivesPredicate(
+                    relation.relate(&a_pred.0, &b_pred.0)?,
+                    relation.relate(&a_pred.1, &b_pred.1)?,
+                )))
+            }
+
+            (TypeOutlives(a_pred), TypeOutlives(b_pred)) => {
+                Ok(TypeOutlives(ty::OutlivesPredicate(
+                    relation.relate(&a_pred.0, &b_pred.0)?,
+                    relation.relate(&a_pred.1, &b_pred.1)?,
+                )))
+            }
+
+            _ =>  Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::WellFormed<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::WellFormed<'tcx>,
+        b: &traits::WellFormed<'tcx>
+    ) -> RelateResult<'tcx, traits::WellFormed<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::WellFormed::*;
+        match (a, b) {
+            (Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
+            (Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
+            _ =>  Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::FromEnv<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::FromEnv<'tcx>,
+        b: &traits::FromEnv<'tcx>
+    ) -> RelateResult<'tcx, traits::FromEnv<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::FromEnv::*;
+        match (a, b) {
+            (Trait(a_pred), Trait(b_pred)) => Ok(Trait(relation.relate(a_pred, b_pred)?)),
+            (Ty(a_ty), Ty(b_ty)) => Ok(Ty(relation.relate(a_ty, b_ty)?)),
+            _ =>  Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::DomainGoal<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::DomainGoal<'tcx>,
+        b: &traits::DomainGoal<'tcx>
+    ) -> RelateResult<'tcx, traits::DomainGoal<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::DomainGoal::*;
+        match (a, b) {
+            (Holds(a_wc), Holds(b_wc)) => Ok(Holds(relation.relate(a_wc, b_wc)?)),
+            (WellFormed(a_wf), WellFormed(b_wf)) => Ok(WellFormed(relation.relate(a_wf, b_wf)?)),
+            (FromEnv(a_fe), FromEnv(b_fe)) => Ok(FromEnv(relation.relate(a_fe, b_fe)?)),
+
+            (Normalize(a_pred), Normalize(b_pred)) => {
+                Ok(Normalize(relation.relate(a_pred, b_pred)?))
+            }
+
+            _ =>  Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::Goal<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::Goal<'tcx>,
+        b: &traits::Goal<'tcx>
+    ) -> RelateResult<'tcx, traits::Goal<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::GoalKind::*;
+        match (a, b) {
+            (Implies(a_clauses, a_goal), Implies(b_clauses, b_goal)) => {
+                let clauses = relation.relate(a_clauses, b_clauses)?;
+                let goal = relation.relate(a_goal, b_goal)?;
+                Ok(relation.tcx().mk_goal(Implies(clauses, goal)))
+            }
+
+            (And(a_left, a_right), And(b_left, b_right)) => {
+                let left = relation.relate(a_left, b_left)?;
+                let right = relation.relate(a_right, b_right)?;
+                Ok(relation.tcx().mk_goal(And(left, right)))
+            }
+
+            (Not(a_goal), Not(b_goal)) => {
+                let goal = relation.relate(a_goal, b_goal)?;
+                Ok(relation.tcx().mk_goal(Not(goal)))
+            }
+
+            (DomainGoal(a_goal), DomainGoal(b_goal)) => {
+                let goal = relation.relate(a_goal, b_goal)?;
+                Ok(relation.tcx().mk_goal(DomainGoal(goal)))
+            }
+
+            (Quantified(a_qkind, a_goal), Quantified(b_qkind, b_goal))
+                if a_qkind == b_qkind =>
+            {
+                let goal = relation.relate(a_goal, b_goal)?;
+                Ok(relation.tcx().mk_goal(Quantified(*a_qkind, goal)))
+            }
+
+            (CannotProve, CannotProve) => Ok(*a),
+
+            _ => Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::Goals<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::Goals<'tcx>,
+        b: &traits::Goals<'tcx>
+    ) -> RelateResult<'tcx, traits::Goals<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        if a.len() != b.len() {
+            return Err(TypeError::Mismatch);
+        }
+
+        let tcx = relation.tcx();
+        let goals = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
+        Ok(tcx.mk_goals(goals)?)
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::Clause<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::Clause<'tcx>,
+        b: &traits::Clause<'tcx>
+    ) -> RelateResult<'tcx, traits::Clause<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        use traits::Clause::*;
+        match (a, b) {
+            (Implies(a_clause), Implies(b_clause)) => {
+                let clause = relation.relate(a_clause, b_clause)?;
+                Ok(Implies(clause))
+            }
+
+            (ForAll(a_clause), ForAll(b_clause)) => {
+                let clause = relation.relate(a_clause, b_clause)?;
+                Ok(ForAll(clause))
+            }
+
+            _ => Err(TypeError::Mismatch),
+        }
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::Clauses<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::Clauses<'tcx>,
+        b: &traits::Clauses<'tcx>
+    ) -> RelateResult<'tcx, traits::Clauses<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        if a.len() != b.len() {
+            return Err(TypeError::Mismatch);
+        }
+
+        let tcx = relation.tcx();
+        let clauses = a.iter().zip(b.iter()).map(|(a, b)| relation.relate(a, b));
+        Ok(tcx.mk_clauses(clauses)?)
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::ProgramClause<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::ProgramClause<'tcx>,
+        b: &traits::ProgramClause<'tcx>
+    ) -> RelateResult<'tcx, traits::ProgramClause<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        Ok(traits::ProgramClause {
+            goal: relation.relate(&a.goal, &b.goal)?,
+            hypotheses: relation.relate(&a.hypotheses, &b.hypotheses)?,
+            category: traits::ProgramClauseCategory::Other,
+        })
+    }
+}
+
+impl<'tcx> Relate<'tcx> for traits::Environment<'tcx> {
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::Environment<'tcx>,
+        b: &traits::Environment<'tcx>
+    ) -> RelateResult<'tcx, traits::Environment<'tcx>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        Ok(traits::Environment {
+            clauses: relation.relate(&a.clauses, &b.clauses)?,
+        })
+    }
+}
+
+impl<'tcx, G> Relate<'tcx> for traits::InEnvironment<'tcx, G>
+    where G: Relate<'tcx>
+{
+    fn relate<'a, 'gcx, R>(
+        relation: &mut R,
+        a: &traits::InEnvironment<'tcx, G>,
+        b: &traits::InEnvironment<'tcx, G>
+    ) -> RelateResult<'tcx, traits::InEnvironment<'tcx, G>>
+        where R: TypeRelation<'a, 'gcx, 'tcx>, 'gcx: 'tcx, 'tcx: 'a
+    {
+        Ok(traits::InEnvironment {
+            environment: relation.relate(&a.environment, &b.environment)?,
+            goal: relation.relate(&a.goal, &b.goal)?,
+        })
+    }
+}
+
 ///////////////////////////////////////////////////////////////////////////
 // Error handling
 
diff --git a/src/librustc_traits/chalk_context/mod.rs b/src/librustc_traits/chalk_context/mod.rs
index e4d93374faa..bc3f2fd951b 100644
--- a/src/librustc_traits/chalk_context/mod.rs
+++ b/src/librustc_traits/chalk_context/mod.rs
@@ -9,14 +9,24 @@
 // except according to those terms.
 
 mod program_clauses;
+mod resolvent_ops;
 mod unify;
 
 use chalk_engine::fallible::{Fallible, NoSolution};
-use chalk_engine::{context, hh::HhGoal, DelayedLiteral, Literal, ExClause};
-use rustc::infer::canonical::{
-    Canonical, CanonicalVarValues, OriginalQueryValues, QueryResponse,
+use chalk_engine::{
+    context,
+    hh::HhGoal,
+    DelayedLiteral,
+    Literal,
+    ExClause
 };
 use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
+use rustc::infer::canonical::{
+    Canonical,
+    CanonicalVarValues,
+    OriginalQueryValues,
+    QueryResponse,
+};
 use rustc::traits::{
     DomainGoal,
     ExClauseFold,
@@ -28,9 +38,9 @@ use rustc::traits::{
     Environment,
     InEnvironment,
 };
+use rustc::ty::{self, TyCtxt};
 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
 use rustc::ty::subst::{Kind, UnpackedKind};
-use rustc::ty::{self, TyCtxt};
 use syntax_pos::DUMMY_SP;
 
 use std::fmt::{self, Debug};
@@ -201,7 +211,7 @@ impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
 
     fn is_trivial_substitution(
         u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
-        canonical_subst: &Canonical<'tcx, ConstrainedSubst<'tcx>>,
+        canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
     ) -> bool {
         let subst = &canonical_subst.value.subst;
         assert_eq!(u_canon.variables.len(), subst.var_values.len());
@@ -286,30 +296,6 @@ impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     }
 }
 
-impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
-    for ChalkInferenceContext<'cx, 'gcx, 'tcx>
-{
-    fn resolvent_clause(
-        &mut self,
-        _environment: &Environment<'tcx>,
-        _goal: &DomainGoal<'tcx>,
-        _subst: &CanonicalVarValues<'tcx>,
-        _clause: &Clause<'tcx>,
-    ) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
-        panic!()
-    }
-
-    fn apply_answer_subst(
-        &mut self,
-        _ex_clause: ChalkExClause<'tcx>,
-        _selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
-        _answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
-        _canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
-    ) -> Fallible<ChalkExClause<'tcx>> {
-        panic!()
-    }
-}
-
 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 {
diff --git a/src/librustc_traits/chalk_context/resolvent_ops.rs b/src/librustc_traits/chalk_context/resolvent_ops.rs
new file mode 100644
index 00000000000..df6458a766d
--- /dev/null
+++ b/src/librustc_traits/chalk_context/resolvent_ops.rs
@@ -0,0 +1,241 @@
+use chalk_engine::fallible::{Fallible, NoSolution};
+use chalk_engine::{
+    context,
+    Literal,
+    ExClause
+};
+use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
+use rustc::infer::canonical::{Canonical, CanonicalVarValues};
+use rustc::traits::{
+    DomainGoal,
+    Goal,
+    GoalKind,
+    Clause,
+    ProgramClause,
+    Environment,
+    InEnvironment,
+};
+use rustc::ty::{self, Ty};
+use rustc::ty::subst::Kind;
+use rustc::ty::relate::{Relate, RelateResult, TypeRelation};
+use syntax_pos::DUMMY_SP;
+
+use super::{ChalkInferenceContext, ChalkArenas, ChalkExClause, ConstrainedSubst};
+use super::unify::*;
+
+impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
+    for ChalkInferenceContext<'cx, 'gcx, 'tcx>
+{
+    fn resolvent_clause(
+        &mut self,
+        environment: &Environment<'tcx>,
+        goal: &DomainGoal<'tcx>,
+        subst: &CanonicalVarValues<'tcx>,
+        clause: &Clause<'tcx>,
+    ) -> Fallible<Canonical<'gcx, ChalkExClause<'gcx>>> {
+        use chalk_engine::context::UnificationOps;
+
+        self.infcx.probe(|_| {
+            let ProgramClause {
+                goal: consequence,
+                hypotheses,
+                ..
+            } = match clause {
+                Clause::Implies(program_clause) => *program_clause,
+                Clause::ForAll(program_clause) => self.infcx.replace_bound_vars_with_fresh_vars(
+                    DUMMY_SP,
+                    LateBoundRegionConversionTime::HigherRankedType,
+                    program_clause
+                ).0,
+            };
+
+            let result = unify(self.infcx, *environment, goal, &consequence)
+                .map_err(|_| NoSolution)?;
+
+            let mut ex_clause = ExClause {
+                subst: subst.clone(),
+                delayed_literals: vec![],
+                constraints: vec![],
+                subgoals: vec![],
+            };
+
+            self.into_ex_clause(result, &mut ex_clause);
+
+            ex_clause.subgoals.extend(
+                hypotheses.iter().map(|g| match g {
+                    GoalKind::Not(g) => Literal::Negative(environment.with(*g)),
+                    g => Literal::Positive(environment.with(*g)),
+                })
+            );
+
+            let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
+            Ok(canonical_ex_clause)
+        })
+    }
+
+    fn apply_answer_subst(
+        &mut self,
+        ex_clause: ChalkExClause<'tcx>,
+        selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
+        answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
+        canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
+    ) -> Fallible<ChalkExClause<'tcx>> {
+        let (answer_subst, _) = self.infcx.instantiate_canonical_with_fresh_inference_vars(
+            DUMMY_SP,
+            canonical_answer_subst
+        );
+
+        let mut substitutor = AnswerSubstitutor {
+            infcx: self.infcx,
+            environment: selected_goal.environment,
+            answer_subst: answer_subst.subst,
+            binder_index: ty::INNERMOST,
+            ex_clause,
+        };
+
+        substitutor.relate(&answer_table_goal.value, &selected_goal)
+            .map_err(|_| NoSolution)?;
+
+        let mut ex_clause = substitutor.ex_clause;
+        ex_clause.constraints.extend(answer_subst.constraints);
+        Ok(ex_clause)
+    }
+}
+
+struct AnswerSubstitutor<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
+    infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
+    environment: Environment<'tcx>,
+    answer_subst: CanonicalVarValues<'tcx>,
+    binder_index: ty::DebruijnIndex,
+    ex_clause: ChalkExClause<'tcx>,
+}
+
+impl AnswerSubstitutor<'cx, 'gcx, 'tcx> {
+    fn unify_free_answer_var(
+        &mut self,
+        answer_var: ty::BoundVar,
+        pending: Kind<'tcx>
+    ) -> RelateResult<'tcx, ()> {
+        let answer_param = &self.answer_subst.var_values[answer_var];
+        let pending = &ty::fold::shift_out_vars(
+            self.infcx.tcx,
+            &pending,
+            self.binder_index.as_u32()
+        );
+
+        super::into_ex_clause(
+            unify(self.infcx, self.environment, answer_param, pending)?,
+            &mut self.ex_clause
+        );
+
+        Ok(())
+    }
+}
+
+impl TypeRelation<'cx, 'gcx, 'tcx> for AnswerSubstitutor<'cx, 'gcx, 'tcx> {
+    fn tcx(&self) -> ty::TyCtxt<'cx, 'gcx, 'tcx> {
+        self.infcx.tcx
+    }
+
+    fn tag(&self) -> &'static str {
+        "chalk_context::answer_substitutor"
+    }
+
+    fn a_is_expected(&self) -> bool {
+        true
+    }
+
+    fn relate_with_variance<T: Relate<'tcx>>(
+        &mut self,
+        _variance: ty::Variance,
+        a: &T,
+        b: &T,
+    ) -> RelateResult<'tcx, T> {
+        // We don't care about variance.
+        self.relate(a, b)
+    }
+
+    fn binders<T: Relate<'tcx>>(
+        &mut self,
+        a: &ty::Binder<T>,
+        b: &ty::Binder<T>,
+    ) -> RelateResult<'tcx, ty::Binder<T>> {
+        self.binder_index.shift_in(1);
+        let result = self.relate(a.skip_binder(), b.skip_binder())?;
+        self.binder_index.shift_out(1);
+        Ok(ty::Binder::bind(result))
+    }
+
+    fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+        let b = self.infcx.shallow_resolve(b);
+
+        if let &ty::Bound(debruijn, bound_ty) = &a.sty {
+            // Free bound var
+            if debruijn == self.binder_index {
+                self.unify_free_answer_var(bound_ty.var, b.into())?;
+                return Ok(b);
+            }
+        }
+
+        match (&a.sty, &b.sty) {
+            (&ty::Bound(a_debruijn, a_bound), &ty::Bound(b_debruijn, b_bound)) => {
+                assert_eq!(a_debruijn, b_debruijn);
+                assert_eq!(a_bound.var, b_bound.var);
+                Ok(a)
+            }
+
+            // Those should have been canonicalized away.
+            (ty::Placeholder(..), _) => {
+                bug!("unexpected placeholder ty in `AnswerSubstitutor`: {:?} ", a);
+            }
+
+            // Everything else should just be a perfect match as well,
+            // and we forbid inference variables.
+            _ => match ty::relate::super_relate_tys(self, a, b) {
+                Ok(ty) => Ok(ty),
+                Err(err) => bug!("type mismatch in `AnswerSubstitutor`: {}", err),
+            }
+        }
+    }
+
+    fn regions(
+        &mut self,
+        a: ty::Region<'tcx>,
+        b: ty::Region<'tcx>,
+    ) -> RelateResult<'tcx, ty::Region<'tcx>> {
+        let b = match b {
+            &ty::ReVar(vid) => self.infcx
+                .borrow_region_constraints()
+                .opportunistic_resolve_var(self.infcx.tcx, vid),
+
+            other => other,
+        };
+
+        if let &ty::ReLateBound(debruijn, bound) = a {
+            // Free bound region
+            if debruijn == self.binder_index {
+                self.unify_free_answer_var(bound.assert_bound_var(), b.into())?;
+                return Ok(b);
+            }
+        }
+
+        match (a, b) {
+            (&ty::ReLateBound(a_debruijn, a_bound), &ty::ReLateBound(b_debruijn, b_bound)) => {
+                assert_eq!(a_debruijn, b_debruijn);
+                assert_eq!(a_bound.assert_bound_var(), b_bound.assert_bound_var());
+            }
+
+            (ty::ReStatic, ty::ReStatic) |
+            (ty::ReErased, ty::ReErased) |
+            (ty::ReEmpty, ty::ReEmpty) => (),
+
+            (&ty::ReFree(a_free), &ty::ReFree(b_free)) => {
+                assert_eq!(a_free, b_free);
+            }
+
+            _ => bug!("unexpected regions in `AnswerSubstitutor`: {:?}, {:?}", a, b),
+        }
+
+        Ok(a)
+    }
+}