Rollup merge of #56214 - scalexm:unification, r=nikomatsakis

Implement chalk unification routines

`ResolventOps` and `AggregateOps` are mostly straightforwardly translated from chalk. I had caught a few bugs already in my `chalk` branch and backported fixes to this branch, but there may be other ones left. EDIT: I hope there are none left now :)

Fixes #54935.

7 files changed, 985 insertions, 151 deletions

diff --git a/src/librustc/infer/nll_relate/mod.rs b/src/librustc/infer/nll_relate/mod.rs
index 9bdbf77fee0..972ba16f7e2 100644
--- a/src/librustc/infer/nll_relate/mod.rs
+++ b/src/librustc/infer/nll_relate/mod.rs
@@ -11,30 +11,41 @@
 //! This code is kind of an alternate way of doing subtyping,
 //! supertyping, and type equating, distinct from the `combine.rs`
 //! code but very similar in its effect and design. Eventually the two
-//! ought to be merged. This code is intended for use in NLL.
+//! ought to be merged. This code is intended for use in NLL and chalk.
 //!
 //! Here are the key differences:
 //!
-//! - This code generally assumes that there are no unbound type
-//!   inferences variables, because at NLL
-//!   time types are fully inferred up-to regions.
-//!   - Actually, to support user-given type annotations like
-//!     `Vec<_>`, we do have some measure of support for type
-//!     inference variables, but we impose some simplifying
-//!     assumptions on them that would not be suitable for the infer
-//!     code more generally. This could be fixed.
+//! - This code may choose to bypass some checks (e.g. the occurs check)
+//!   in the case where we know that there are no unbound type inference
+//!   variables. This is the case for NLL, because at NLL time types are fully
+//!   inferred up-to regions.
 //! - This code uses "universes" to handle higher-ranked regions and
 //!   not the leak-check. This is "more correct" than what rustc does
 //!   and we are generally migrating in this direction, but NLL had to
 //!   get there first.
+//!
+//! Also, this code assumes that there are no bound types at all, not even
+//! free ones. This is ok because:
+//! - we are not relating anything quantified over some type variable
+//! - we will have instantiated all the bound type vars already (the one
+//!   thing we relate in chalk are basically domain goals and their
+//!   constituents)
 
 use crate::infer::InferCtxt;
 use crate::ty::fold::{TypeFoldable, TypeVisitor};
 use crate::ty::relate::{self, Relate, RelateResult, TypeRelation};
 use crate::ty::subst::Kind;
 use crate::ty::{self, Ty, TyCtxt};
+use crate::ty::error::TypeError;
+use crate::traits::DomainGoal;
 use rustc_data_structures::fx::FxHashMap;
 
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+pub enum NormalizationStrategy {
+    Lazy,
+    Eager,
+}
+
 pub struct TypeRelating<'me, 'gcx: 'tcx, 'tcx: 'me, D>
 where
     D: TypeRelatingDelegate<'tcx>,
@@ -75,6 +86,10 @@ pub trait TypeRelatingDelegate<'tcx> {
     /// delegate.
     fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>);
 
+    /// Push a domain goal that will need to be proved for the two types to
+    /// be related. Used for lazy normalization.
+    fn push_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>);
+
     /// Creates a new universe index. Used when instantiating placeholders.
     fn create_next_universe(&mut self) -> ty::UniverseIndex;
 
@@ -105,6 +120,13 @@ pub trait TypeRelatingDelegate<'tcx> {
     /// relate `Foo<'?0>` with `Foo<'a>` (and probably add an outlives
     /// relation stating that `'?0: 'a`).
     fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx>;
+
+    /// Define the normalization strategy to use, eager or lazy.
+    fn normalization() -> NormalizationStrategy;
+
+    /// Enable some optimizations if we do not expect inference variables
+    /// in the RHS of the relation.
+    fn forbid_inference_vars() -> bool;
 }
 
 #[derive(Clone, Debug)]
@@ -242,15 +264,79 @@ where
         self.delegate.push_outlives(sup, sub);
     }
 
-    /// When we encounter a canonical variable `var` in the output,
-    /// equate it with `kind`. If the variable has been previously
-    /// equated, then equate it again.
-    fn relate_var(&mut self, var_ty: Ty<'tcx>, value_ty: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
-        debug!("equate_var(var_ty={:?}, value_ty={:?})", var_ty, value_ty);
+    /// Relate a projection type and some value type lazily. This will always
+    /// succeed, but we push an additional `ProjectionEq` goal depending
+    /// on the value type:
+    /// - if the value type is any type `T` which is not a projection, we push
+    ///   `ProjectionEq(projection = T)`.
+    /// - if the value type is another projection `other_projection`, we create
+    ///   a new inference variable `?U` and push the two goals
+    ///   `ProjectionEq(projection = ?U)`, `ProjectionEq(other_projection = ?U)`.
+    fn relate_projection_ty(
+        &mut self,
+        projection_ty: ty::ProjectionTy<'tcx>,
+        value_ty: ty::Ty<'tcx>
+    ) -> Ty<'tcx> {
+        use crate::infer::type_variable::TypeVariableOrigin;
+        use crate::traits::WhereClause;
+        use syntax_pos::DUMMY_SP;
+
+        match value_ty.sty {
+            ty::Projection(other_projection_ty) => {
+                let var = self.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
+                self.relate_projection_ty(projection_ty, var);
+                self.relate_projection_ty(other_projection_ty, var);
+                var
+            }
+
+            _ => {
+                let projection = ty::ProjectionPredicate {
+                    projection_ty,
+                    ty: value_ty,
+                };
+                self.delegate.push_domain_goal(
+                    DomainGoal::Holds(WhereClause::ProjectionEq(projection))
+                );
+                value_ty
+            }
+        }
+    }
+
+    /// Relate a type inference variable with a value type.
+    fn relate_ty_var(
+        &mut self,
+        vid: ty::TyVid,
+        value_ty: Ty<'tcx>
+    ) -> RelateResult<'tcx, Ty<'tcx>> {
+        debug!("relate_ty_var(vid={:?}, value_ty={:?})", vid, value_ty);
+
+        match value_ty.sty {
+            ty::Infer(ty::TyVar(value_vid)) => {
+                // Two type variables: just equate them.
+                self.infcx.type_variables.borrow_mut().equate(vid, value_vid);
+                return Ok(value_ty);
+            }
+
+            ty::Projection(projection_ty)
+                if D::normalization() == NormalizationStrategy::Lazy =>
+            {
+                return Ok(self.relate_projection_ty(projection_ty, self.infcx.tcx.mk_var(vid)));
+            }
+
+            _ => (),
+        }
+
+        let generalized_ty = self.generalize_value(value_ty, vid)?;
+        debug!("relate_ty_var: generalized_ty = {:?}", generalized_ty);
+
+        if D::forbid_inference_vars() {
+            // In NLL, we don't have type inference variables
+            // floating around, so we can do this rather imprecise
+            // variant of the occurs-check.
+            assert!(!generalized_ty.has_infer_types());
+        }
 
-        let generalized_ty = self.generalize_value(value_ty);
-        self.infcx
-            .force_instantiate_unchecked(var_ty, generalized_ty);
+        self.infcx.type_variables.borrow_mut().instantiate(vid, generalized_ty);
 
         // The generalized values we extract from `canonical_var_values` have
         // been fully instantiated and hence the set of scopes we have
@@ -264,22 +350,27 @@ where
         // Restore the old scopes now.
         self.a_scopes = old_a_scopes;
 
-        debug!("equate_var: complete, result = {:?}", result);
+        debug!("relate_ty_var: complete, result = {:?}", result);
         result
     }
 
-    fn generalize_value<T: Relate<'tcx>>(&mut self, value: T) -> T {
-        TypeGeneralizer {
-            tcx: self.infcx.tcx,
+    fn generalize_value<T: Relate<'tcx>>(
+        &mut self,
+        value: T,
+        for_vid: ty::TyVid
+    ) -> RelateResult<'tcx, T> {
+        let universe = self.infcx.probe_ty_var(for_vid).unwrap_err();
+
+        let mut generalizer = TypeGeneralizer {
+            infcx: self.infcx,
             delegate: &mut self.delegate,
             first_free_index: ty::INNERMOST,
             ambient_variance: self.ambient_variance,
+            for_vid_sub_root: self.infcx.type_variables.borrow_mut().sub_root_var(for_vid),
+            universe,
+        };
 
-            // These always correspond to an `_` or `'_` written by
-            // user, and those are always in the root universe.
-            universe: ty::UniverseIndex::ROOT,
-        }.relate(&value, &value)
-            .unwrap()
+        generalizer.relate(&value, &value)
     }
 }
 
@@ -327,11 +418,35 @@ where
         Ok(r)
     }
 
-    fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+    fn tys(&mut self, a: Ty<'tcx>, mut b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
         let a = self.infcx.shallow_resolve(a);
-        match a.sty {
-            ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_)) => {
-                self.relate_var(a.into(), b.into())
+
+        if !D::forbid_inference_vars() {
+            b = self.infcx.shallow_resolve(b);
+        }
+
+        match (&a.sty, &b.sty) {
+            (_, &ty::Infer(ty::TyVar(vid))) => {
+                if D::forbid_inference_vars() {
+                    // Forbid inference variables in the RHS.
+                    bug!("unexpected inference var {:?}", b)
+                } else {
+                    self.relate_ty_var(vid, a)
+                }
+            }
+
+            (&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var(vid, b),
+
+            (&ty::Projection(projection_ty), _)
+                if D::normalization() == NormalizationStrategy::Lazy =>
+            {
+                Ok(self.relate_projection_ty(projection_ty, b))
+            }
+
+            (_, &ty::Projection(projection_ty))
+                if D::normalization() == NormalizationStrategy::Lazy =>
+            {
+                Ok(self.relate_projection_ty(projection_ty, a))
             }
 
             _ => {
@@ -340,7 +455,8 @@ where
                     a, b, self.ambient_variance
                 );
 
-                relate::super_relate_tys(self, a, b)
+                // Will also handle unification of `IntVar` and `FloatVar`.
+                self.infcx.super_combine_tys(self, a, b)
             }
         }
     }
@@ -551,7 +667,7 @@ struct TypeGeneralizer<'me, 'gcx: 'tcx, 'tcx: 'me, D>
 where
     D: TypeRelatingDelegate<'tcx> + 'me,
 {
-    tcx: TyCtxt<'me, 'gcx, 'tcx>,
+    infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
 
     delegate: &'me mut D,
 
@@ -561,6 +677,14 @@ where
 
     first_free_index: ty::DebruijnIndex,
 
+    /// The vid of the type variable that is in the process of being
+    /// instantiated. If we find this within the value we are folding,
+    /// that means we would have created a cyclic value.
+    for_vid_sub_root: ty::TyVid,
+
+    /// The universe of the type variable that is in the process of being
+    /// instantiated. If we find anything that this universe cannot name,
+    /// we reject the relation.
     universe: ty::UniverseIndex,
 }
 
@@ -569,7 +693,7 @@ where
     D: TypeRelatingDelegate<'tcx>,
 {
     fn tcx(&self) -> TyCtxt<'me, 'gcx, 'tcx> {
-        self.tcx
+        self.infcx.tcx
     }
 
     fn tag(&self) -> &'static str {
@@ -609,17 +733,84 @@ where
     }
 
     fn tys(&mut self, a: Ty<'tcx>, _: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+        use crate::infer::type_variable::TypeVariableValue;
+
         debug!("TypeGeneralizer::tys(a={:?})", a,);
 
         match a.sty {
-            ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_)) => {
+            ty::Infer(ty::TyVar(_)) | ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_))
+                if D::forbid_inference_vars() =>
+            {
                 bug!(
                     "unexpected inference variable encountered in NLL generalization: {:?}",
                     a
                 );
             }
 
-            _ => relate::super_relate_tys(self, a, a),
+            ty::Infer(ty::TyVar(vid)) => {
+                let mut variables = self.infcx.type_variables.borrow_mut();
+                let vid = variables.root_var(vid);
+                let sub_vid = variables.sub_root_var(vid);
+                if sub_vid == self.for_vid_sub_root {
+                    // If sub-roots are equal, then `for_vid` and
+                    // `vid` are related via subtyping.
+                    debug!("TypeGeneralizer::tys: occurs check failed");
+                    return Err(TypeError::Mismatch);
+                } else {
+                    match variables.probe(vid) {
+                        TypeVariableValue::Known { value: u } => {
+                            drop(variables);
+                            self.relate(&u, &u)
+                        }
+                        TypeVariableValue::Unknown { universe: _universe } => {
+                            if self.ambient_variance == ty::Bivariant {
+                                // FIXME: we may need a WF predicate (related to #54105).
+                            }
+
+                            let origin = *variables.var_origin(vid);
+
+                            // Replacing with a new variable in the universe `self.universe`,
+                            // it will be unified later with the original type variable in
+                            // the universe `_universe`.
+                            let new_var_id = variables.new_var(self.universe, false, origin);
+
+                            let u = self.tcx().mk_var(new_var_id);
+                            debug!(
+                                "generalize: replacing original vid={:?} with new={:?}",
+                                vid,
+                                u
+                            );
+                            return Ok(u);
+                        }
+                    }
+                }
+            }
+
+            ty::Infer(ty::IntVar(_)) |
+            ty::Infer(ty::FloatVar(_)) => {
+                // No matter what mode we are in,
+                // integer/floating-point types must be equal to be
+                // relatable.
+                Ok(a)
+            }
+
+            ty::Placeholder(placeholder) => {
+                if self.universe.cannot_name(placeholder.universe) {
+                    debug!(
+                        "TypeGeneralizer::tys: root universe {:?} cannot name\
+                        placeholder in universe {:?}",
+                        self.universe,
+                        placeholder.universe
+                    );
+                    Err(TypeError::Mismatch)
+                } else {
+                    Ok(a)
+                }
+            }
+
+            _ => {
+                relate::super_relate_tys(self, a, a)
+            }
         }
     }
 
@@ -673,64 +864,3 @@ where
         Ok(ty::Binder::bind(result))
     }
 }
-
-impl InferCtxt<'_, '_, 'tcx> {
-    /// A hacky sort of method used by the NLL type-relating code:
-    ///
-    /// - `var` must be some unbound type variable.
-    /// - `value` must be a suitable type to use as its value.
-    ///
-    /// `var` will then be equated with `value`. Note that this
-    /// sidesteps a number of important checks, such as the "occurs
-    /// check" that prevents cyclic types, so it is important not to
-    /// use this method during regular type-check.
-    fn force_instantiate_unchecked(&self, var: Ty<'tcx>, value: Ty<'tcx>) {
-        match (&var.sty, &value.sty) {
-            (&ty::Infer(ty::TyVar(vid)), _) => {
-                let mut type_variables = self.type_variables.borrow_mut();
-
-                // In NLL, we don't have type inference variables
-                // floating around, so we can do this rather imprecise
-                // variant of the occurs-check.
-                assert!(!value.has_infer_types());
-
-                type_variables.instantiate(vid, value);
-            }
-
-            (&ty::Infer(ty::IntVar(vid)), &ty::Int(value)) => {
-                let mut int_unification_table = self.int_unification_table.borrow_mut();
-                int_unification_table
-                    .unify_var_value(vid, Some(ty::IntVarValue::IntType(value)))
-                    .unwrap_or_else(|_| {
-                        bug!("failed to unify int var `{:?}` with `{:?}`", vid, value);
-                    });
-            }
-
-            (&ty::Infer(ty::IntVar(vid)), &ty::Uint(value)) => {
-                let mut int_unification_table = self.int_unification_table.borrow_mut();
-                int_unification_table
-                    .unify_var_value(vid, Some(ty::IntVarValue::UintType(value)))
-                    .unwrap_or_else(|_| {
-                        bug!("failed to unify int var `{:?}` with `{:?}`", vid, value);
-                    });
-            }
-
-            (&ty::Infer(ty::FloatVar(vid)), &ty::Float(value)) => {
-                let mut float_unification_table = self.float_unification_table.borrow_mut();
-                float_unification_table
-                    .unify_var_value(vid, Some(ty::FloatVarValue(value)))
-                    .unwrap_or_else(|_| {
-                        bug!("failed to unify float var `{:?}` with `{:?}`", vid, value)
-                    });
-            }
-
-            _ => {
-                bug!(
-                    "force_instantiate_unchecked invoked with bad combination: var={:?} value={:?}",
-                    var,
-                    value,
-                );
-            }
-        }
-    }
-}
diff --git a/src/librustc/ty/fold.rs b/src/librustc/ty/fold.rs
index 1bc7d648792..20f64597b78 100644
--- a/src/librustc/ty/fold.rs
+++ b/src/librustc/ty/fold.rs
@@ -680,24 +680,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> {
@@ -713,7 +720,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)
                 }
             }
@@ -727,8 +741,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)
                     )
                 }
             }
@@ -761,7 +782,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 082c1bd5fea..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>>;
 
@@ -371,6 +372,10 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
             bug!("var types encountered in super_relate_tys")
         }
 
+        (ty::Bound(..), _) | (_, ty::Bound(..)) => {
+            bug!("bound types encountered in super_relate_tys")
+        }
+
         (&ty::Error, _) | (_, &ty::Error) =>
         {
             Ok(tcx.types.err)
@@ -394,6 +399,10 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
             Ok(a)
         }
 
+        (ty::Placeholder(p1), ty::Placeholder(p2)) if p1 == p2 => {
+            Ok(a)
+        }
+
         (&ty::Adt(a_def, a_substs), &ty::Adt(b_def, b_substs))
             if a_def == b_def =>
         {
@@ -556,8 +565,13 @@ pub fn super_relate_tys<'a, 'gcx, 'tcx, R>(relation: &mut R,
             Ok(tcx.mk_fn_ptr(fty))
         }
 
-        (&ty::Projection(ref a_data), &ty::Projection(ref b_data)) =>
-        {
+        (ty::UnnormalizedProjection(a_data), ty::UnnormalizedProjection(b_data)) => {
+            let projection_ty = relation.relate(a_data, b_data)?;
+            Ok(tcx.mk_ty(ty::UnnormalizedProjection(projection_ty)))
+        }
+
+        // these two are already handled downstream in case of lazy normalization
+        (ty::Projection(a_data), ty::Projection(b_data)) => {
             let projection_ty = relation.relate(a_data, b_data)?;
             Ok(tcx.mk_projection(projection_ty.item_def_id, projection_ty.substs))
         }
@@ -710,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_mir/borrow_check/nll/type_check/relate_tys.rs b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
index cf4f9130807..225e2841fb0 100644
--- a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
+++ b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
@@ -10,10 +10,11 @@
 
 use borrow_check::nll::constraints::OutlivesConstraint;
 use borrow_check::nll::type_check::{BorrowCheckContext, Locations};
-use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate};
+use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate, NormalizationStrategy};
 use rustc::infer::{InferCtxt, NLLRegionVariableOrigin};
 use rustc::mir::ConstraintCategory;
 use rustc::traits::query::Fallible;
+use rustc::traits::DomainGoal;
 use rustc::ty::relate::TypeRelation;
 use rustc::ty::{self, Ty};
 
@@ -38,7 +39,7 @@ pub(super) fn relate_types<'tcx>(
     TypeRelating::new(
         infcx,
         NllTypeRelatingDelegate::new(infcx, borrowck_context, locations, category),
-        v,
+        v
     ).relate(&a, &b)?;
     Ok(())
 }
@@ -115,4 +116,16 @@ impl TypeRelatingDelegate<'tcx> for NllTypeRelatingDelegate<'_, '_, '_, 'tcx> {
                 });
         }
     }
+
+    fn push_domain_goal(&mut self, _: DomainGoal<'tcx>) {
+        bug!("should never be invoked with eager normalization")
+    }
+
+    fn normalization() -> NormalizationStrategy {
+        NormalizationStrategy::Eager
+    }
+
+    fn forbid_inference_vars() -> bool {
+        true
+    }
 }
diff --git a/src/librustc_traits/chalk_context/mod.rs b/src/librustc_traits/chalk_context/mod.rs
index 25a6af284b5..58a8d2abd99 100644
--- a/src/librustc_traits/chalk_context/mod.rs
+++ b/src/librustc_traits/chalk_context/mod.rs
@@ -9,13 +9,25 @@
 // except according to those terms.
 
 mod program_clauses;
-
-use chalk_engine::fallible::Fallible as ChalkEngineFallible;
-use chalk_engine::{context, hh::HhGoal, DelayedLiteral, Literal, ExClause};
+mod resolvent_ops;
+mod unify;
+
+use chalk_engine::fallible::{Fallible, NoSolution};
+use chalk_engine::{
+    context,
+    hh::HhGoal,
+    DelayedLiteral,
+    Literal,
+    ExClause
+};
+use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
 use rustc::infer::canonical::{
-    Canonical, CanonicalVarValues, OriginalQueryValues, QueryRegionConstraint, QueryResponse,
+    Canonical,
+    CanonicalVarValues,
+    OriginalQueryValues,
+    QueryResponse,
+    Certainty,
 };
-use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
 use rustc::traits::{
     DomainGoal,
     ExClauseFold,
@@ -27,14 +39,15 @@ 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};
 use std::marker::PhantomData;
 
-use syntax_pos::DUMMY_SP;
+use self::unify::*;
 
 #[derive(Copy, Clone, Debug)]
 crate struct ChalkArenas<'gcx> {
@@ -55,10 +68,12 @@ crate struct ChalkInferenceContext<'cx, 'gcx: 'tcx, 'tcx: 'cx> {
 #[derive(Copy, Clone, Debug)]
 crate struct UniverseMap;
 
+crate type RegionConstraint<'tcx> = ty::OutlivesPredicate<Kind<'tcx>, ty::Region<'tcx>>;
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 crate struct ConstrainedSubst<'tcx> {
     subst: CanonicalVarValues<'tcx>,
-    constraints: Vec<QueryRegionConstraint<'tcx>>,
+    constraints: Vec<RegionConstraint<'tcx>>,
 }
 
 BraceStructTypeFoldableImpl! {
@@ -86,7 +101,7 @@ impl context::Context for ChalkArenas<'tcx> {
 
     type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
 
-    type RegionConstraint = QueryRegionConstraint<'tcx>;
+    type RegionConstraint = RegionConstraint<'tcx>;
 
     type Substitution = CanonicalVarValues<'tcx>;
 
@@ -104,7 +119,7 @@ impl context::Context for ChalkArenas<'tcx> {
 
     type ProgramClauses = Vec<Clause<'tcx>>;
 
-    type UnificationResult = InferOk<'tcx, ()>;
+    type UnificationResult = UnificationResult<'tcx>;
 
     fn goal_in_environment(
         env: &Environment<'tcx>,
@@ -118,9 +133,34 @@ impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
     fn make_solution(
         &self,
         _root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
-        _simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
+        mut simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
     ) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
-        unimplemented!()
+        use chalk_engine::SimplifiedAnswer;
+
+        if simplified_answers.peek_answer().is_none() {
+            return None;
+        }
+
+        let SimplifiedAnswer { subst, ambiguous } = simplified_answers
+            .next_answer()
+            .unwrap();
+
+        let ambiguous = simplified_answers.peek_answer().is_some() || ambiguous;
+
+        Some(subst.unchecked_map(|subst| {
+            QueryResponse {
+                var_values: subst.subst,
+                region_constraints: subst.constraints
+                    .into_iter()
+                    .map(|c| ty::Binder::bind(c))
+                    .collect(),
+                certainty: match ambiguous {
+                    true => Certainty::Ambiguous,
+                    false => Certainty::Proven,
+                },
+                value: (),
+            }
+        }))
     }
 }
 
@@ -197,7 +237,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());
@@ -282,30 +322,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>,
-    ) -> chalk_engine::fallible::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>>,
-    ) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
-        panic!()
-    }
-}
-
 impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     for ChalkInferenceContext<'cx, 'gcx, 'tcx>
 {
@@ -376,7 +392,7 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
     fn canonicalize_constrained_subst(
         &mut self,
         subst: CanonicalVarValues<'tcx>,
-        constraints: Vec<QueryRegionConstraint<'tcx>>,
+        constraints: Vec<RegionConstraint<'tcx>>,
     ) -> Canonical<'gcx, ConstrainedSubst<'gcx>> {
         self.infcx.canonicalize_response(&ConstrainedSubst { subst, constraints })
     }
@@ -400,11 +416,13 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
 
     fn unify_parameters(
         &mut self,
-        _environment: &Environment<'tcx>,
-        _a: &Kind<'tcx>,
-        _b: &Kind<'tcx>,
-    ) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
-        panic!()
+        environment: &Environment<'tcx>,
+        a: &Kind<'tcx>,
+        b: &Kind<'tcx>,
+    ) -> Fallible<UnificationResult<'tcx>> {
+        self.infcx.commit_if_ok(|_| {
+            unify(self.infcx, *environment, a, b).map_err(|_| NoSolution)
+        })
     }
 
     fn sink_answer_subset(
@@ -421,11 +439,22 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         panic!("lift")
     }
 
-    fn into_ex_clause(&mut self, _result: InferOk<'tcx, ()>, _ex_clause: &mut ChalkExClause<'tcx>) {
-        panic!("TBD")
+    fn into_ex_clause(
+        &mut self,
+        result: UnificationResult<'tcx>,
+        ex_clause: &mut ChalkExClause<'tcx>
+    ) {
+        into_ex_clause(result, ex_clause);
     }
 }
 
+crate fn into_ex_clause(result: UnificationResult<'tcx>, ex_clause: &mut ChalkExClause<'tcx>) {
+    ex_clause.subgoals.extend(
+        result.goals.into_iter().map(Literal::Positive)
+    );
+    ex_clause.constraints.extend(result.constraints);
+}
+
 type ChalkHhGoal<'tcx> = HhGoal<ChalkArenas<'tcx>>;
 
 type ChalkExClause<'tcx> = ExClause<ChalkArenas<'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)
+    }
+}
diff --git a/src/librustc_traits/chalk_context/unify.rs b/src/librustc_traits/chalk_context/unify.rs
new file mode 100644
index 00000000000..3a9c3918d13
--- /dev/null
+++ b/src/librustc_traits/chalk_context/unify.rs
@@ -0,0 +1,98 @@
+use rustc::infer::nll_relate::{TypeRelating, TypeRelatingDelegate, NormalizationStrategy};
+use rustc::infer::{InferCtxt, RegionVariableOrigin};
+use rustc::traits::{DomainGoal, Goal, Environment, InEnvironment};
+use rustc::ty::relate::{Relate, TypeRelation, RelateResult};
+use rustc::ty;
+use syntax_pos::DUMMY_SP;
+
+crate struct UnificationResult<'tcx> {
+    crate goals: Vec<InEnvironment<'tcx, Goal<'tcx>>>,
+    crate constraints: Vec<super::RegionConstraint<'tcx>>,
+}
+
+crate fn unify<'me, 'gcx, 'tcx, T: Relate<'tcx>>(
+    infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
+    environment: Environment<'tcx>,
+    a: &T,
+    b: &T
+) -> RelateResult<'tcx, UnificationResult<'tcx>> {
+    let mut delegate = ChalkTypeRelatingDelegate::new(
+        infcx,
+        environment
+    );
+
+    TypeRelating::new(
+        infcx,
+        &mut delegate,
+        ty::Variance::Invariant
+    ).relate(a, b)?;
+
+    Ok(UnificationResult {
+        goals: delegate.goals,
+        constraints: delegate.constraints,
+    })
+}
+
+struct ChalkTypeRelatingDelegate<'me, 'gcx: 'tcx, 'tcx: 'me> {
+    infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
+    environment: Environment<'tcx>,
+    goals: Vec<InEnvironment<'tcx, Goal<'tcx>>>,
+    constraints: Vec<super::RegionConstraint<'tcx>>,
+}
+
+impl ChalkTypeRelatingDelegate<'me, 'gcx, 'tcx> {
+    fn new(
+        infcx: &'me InferCtxt<'me, 'gcx, 'tcx>,
+        environment: Environment<'tcx>,
+    ) -> Self {
+        Self {
+            infcx,
+            environment,
+            goals: Vec::new(),
+            constraints: Vec::new(),
+        }
+    }
+}
+
+impl TypeRelatingDelegate<'tcx> for &mut ChalkTypeRelatingDelegate<'_, '_, 'tcx> {
+    fn create_next_universe(&mut self) -> ty::UniverseIndex {
+        self.infcx.create_next_universe()
+    }
+
+    fn next_existential_region_var(&mut self) -> ty::Region<'tcx> {
+        self.infcx.next_region_var(RegionVariableOrigin::MiscVariable(DUMMY_SP))
+    }
+
+    fn next_placeholder_region(
+        &mut self,
+        placeholder: ty::PlaceholderRegion
+    ) -> ty::Region<'tcx> {
+        self.infcx.tcx.mk_region(ty::RePlaceholder(placeholder))
+    }
+
+    fn generalize_existential(&mut self, universe: ty::UniverseIndex) -> ty::Region<'tcx> {
+        self.infcx.next_region_var_in_universe(
+            RegionVariableOrigin::MiscVariable(DUMMY_SP),
+            universe
+        )
+    }
+
+    fn push_outlives(&mut self, sup: ty::Region<'tcx>, sub: ty::Region<'tcx>) {
+        self.constraints.push(ty::OutlivesPredicate(sup.into(), sub));
+    }
+
+    fn push_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>) {
+        let goal = self.environment.with(
+            self.infcx.tcx.mk_goal(domain_goal.into_goal())
+        );
+        self.goals.push(goal);
+    }
+
+    fn normalization() -> NormalizationStrategy {
+        NormalizationStrategy::Lazy
+    }
+
+    fn forbid_inference_vars() -> bool {
+        false
+    }
+}