diff --git a/src/Cargo.lock b/src/Cargo.lock
index a4246b26c2268..0c08e35c18df3 100644
--- a/src/Cargo.lock
+++ b/src/Cargo.lock
@@ -2419,6 +2419,7 @@ dependencies = [
  "log 0.4.5 (registry+https://github.com/rust-lang/crates.io-index)",
  "rustc 0.0.0",
  "rustc_data_structures 0.0.0",
+ "rustc_target 0.0.0",
  "smallvec 0.6.5 (registry+https://github.com/rust-lang/crates.io-index)",
  "syntax 0.0.0",
  "syntax_pos 0.0.0",
diff --git a/src/librustc/infer/canonical/substitute.rs b/src/librustc/infer/canonical/substitute.rs
index b8c1ed236c0ba..70ce5d0d8dc0c 100644
--- a/src/librustc/infer/canonical/substitute.rs
+++ b/src/librustc/infer/canonical/substitute.rs
@@ -80,6 +80,6 @@ where
             }
         };
 
-        tcx.replace_escaping_bound_vars(value, fld_r, fld_t)
+        tcx.replace_escaping_bound_vars(value, fld_r, fld_t).0
     }
 }
diff --git a/src/librustc/infer/higher_ranked/mod.rs b/src/librustc/infer/higher_ranked/mod.rs
index 3e08a4e021aed..642382bcf0fa3 100644
--- a/src/librustc/infer/higher_ranked/mod.rs
+++ b/src/librustc/infer/higher_ranked/mod.rs
@@ -59,11 +59,11 @@ impl<'a, 'gcx, 'tcx> CombineFields<'a, 'gcx, 'tcx> {
             // with a fresh region variable. These region variables --
             // but no other pre-existing region variables -- can name
             // the placeholders.
-            let (a_prime, _) =
-                self.infcx.replace_late_bound_regions_with_fresh_var(
-                    span,
-                    HigherRankedType,
-                    a);
+            let (a_prime, _) = self.infcx.replace_bound_vars_with_fresh_vars(
+                span,
+                HigherRankedType,
+                a
+            );
 
             debug!("a_prime={:?}", a_prime);
             debug!("b_prime={:?}", b_prime);
diff --git a/src/librustc/infer/mod.rs b/src/librustc/infer/mod.rs
index f5513acecf9e7..4ddf47c88ddba 100644
--- a/src/librustc/infer/mod.rs
+++ b/src/librustc/infer/mod.rs
@@ -1328,18 +1328,18 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
         self.report_and_explain_type_error(trace, &err)
     }
 
-    pub fn replace_late_bound_regions_with_fresh_var<T>(
+    pub fn replace_bound_vars_with_fresh_vars<T>(
         &self,
         span: Span,
         lbrct: LateBoundRegionConversionTime,
-        value: &ty::Binder<T>,
+        value: &ty::Binder<T>
     ) -> (T, BTreeMap<ty::BoundRegion, ty::Region<'tcx>>)
     where
-        T: TypeFoldable<'tcx>,
+        T: TypeFoldable<'tcx>
     {
-        self.tcx.replace_late_bound_regions(value, |br| {
-            self.next_region_var(LateBoundRegion(span, br, lbrct))
-        })
+        let fld_r = |br| self.next_region_var(LateBoundRegion(span, br, lbrct));
+        let fld_t = |_| self.next_ty_var(TypeVariableOrigin::MiscVariable(span));
+        self.tcx.replace_bound_vars(value, fld_r, fld_t)
     }
 
     /// Given a higher-ranked projection predicate like:
diff --git a/src/librustc/traits/error_reporting.rs b/src/librustc/traits/error_reporting.rs
index fbada789956be..2761a954cea88 100644
--- a/src/librustc/traits/error_reporting.rs
+++ b/src/librustc/traits/error_reporting.rs
@@ -212,10 +212,11 @@ impl<'a, 'gcx, 'tcx> InferCtxt<'a, 'gcx, 'tcx> {
             // cause I have no idea for a good error message.
             if let ty::Predicate::Projection(ref data) = predicate {
                 let mut selcx = SelectionContext::new(self);
-                let (data, _) = self.replace_late_bound_regions_with_fresh_var(
+                let (data, _) = self.replace_bound_vars_with_fresh_vars(
                     obligation.cause.span,
                     infer::LateBoundRegionConversionTime::HigherRankedType,
-                    data);
+                    data
+                );
                 let mut obligations = vec![];
                 let normalized_ty = super::normalize_projection_type(
                     &mut selcx,
diff --git a/src/librustc/traits/structural_impls.rs b/src/librustc/traits/structural_impls.rs
index e83d085971caa..3e417f10c4494 100644
--- a/src/librustc/traits/structural_impls.rs
+++ b/src/librustc/traits/structural_impls.rs
@@ -14,9 +14,11 @@ use traits;
 use traits::project::Normalized;
 use ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
 use ty::{self, Lift, TyCtxt};
+use syntax::symbol::InternedString;
 
 use std::fmt;
 use std::rc::Rc;
+use std::collections::{BTreeSet, BTreeMap};
 
 // structural impls for the structs in traits
 
@@ -169,6 +171,290 @@ impl<'tcx> fmt::Debug for traits::MismatchedProjectionTypes<'tcx> {
     }
 }
 
+impl<'tcx> fmt::Display for traits::WhereClause<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::WhereClause::*;
+
+        // Bypass ppaux because it does not print out anonymous regions.
+        fn write_region_name<'tcx>(
+            r: ty::Region<'tcx>,
+            fmt: &mut fmt::Formatter<'_>
+        ) -> fmt::Result {
+            match r {
+                ty::ReLateBound(index, br) => match br {
+                    ty::BoundRegion::BrNamed(_, name) => write!(fmt, "{}", name),
+                    ty::BoundRegion::BrAnon(var) => {
+                        if *index == ty::INNERMOST {
+                            write!(fmt, "'^{}", var)
+                        } else {
+                            write!(fmt, "'^{}_{}", index.index(), var)
+                        }
+                    }
+                    _ => write!(fmt, "'_"),
+                }
+
+                _ => write!(fmt, "{}", r),
+            }
+        }
+
+        match self {
+            Implemented(trait_ref) => write!(fmt, "Implemented({})", trait_ref),
+            ProjectionEq(projection) => write!(fmt, "ProjectionEq({})", projection),
+            RegionOutlives(predicate) => {
+                write!(fmt, "RegionOutlives({}: ", predicate.0)?;
+                write_region_name(predicate.1, fmt)?;
+                write!(fmt, ")")
+            }
+            TypeOutlives(predicate) => {
+                write!(fmt, "TypeOutlives({}: ", predicate.0)?;
+                write_region_name(predicate.1, fmt)?;
+                write!(fmt, ")")
+            }
+        }
+    }
+}
+
+impl<'tcx> fmt::Display for traits::WellFormed<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::WellFormed::*;
+
+        match self {
+            Trait(trait_ref) => write!(fmt, "WellFormed({})", trait_ref),
+            Ty(ty) => write!(fmt, "WellFormed({})", ty),
+        }
+    }
+}
+
+impl<'tcx> fmt::Display for traits::FromEnv<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::FromEnv::*;
+
+        match self {
+            Trait(trait_ref) => write!(fmt, "FromEnv({})", trait_ref),
+            Ty(ty) => write!(fmt, "FromEnv({})", ty),
+        }
+    }
+}
+
+impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::DomainGoal::*;
+
+        match self {
+            Holds(wc) => write!(fmt, "{}", wc),
+            WellFormed(wf) => write!(fmt, "{}", wf),
+            FromEnv(from_env) => write!(fmt, "{}", from_env),
+            Normalize(projection) => write!(
+                fmt,
+                "Normalize({} -> {})",
+                projection.projection_ty,
+                projection.ty
+            ),
+        }
+    }
+}
+
+impl fmt::Display for traits::QuantifierKind {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::QuantifierKind::*;
+
+        match self {
+            Universal => write!(fmt, "forall"),
+            Existential => write!(fmt, "exists"),
+        }
+    }
+}
+
+/// Collect names for regions / types bound by a quantified goal / clause.
+/// This collector does not try to do anything clever like in ppaux, it's just used
+/// for debug output in tests anyway.
+struct BoundNamesCollector {
+    // Just sort by name because `BoundRegion::BrNamed` does not have a `BoundVar` index anyway.
+    regions: BTreeSet<InternedString>,
+
+    // Sort by `BoundVar` index, so usually this should be equivalent to the order given
+    // by the list of type parameters.
+    types: BTreeMap<u32, InternedString>,
+
+    binder_index: ty::DebruijnIndex,
+}
+
+impl BoundNamesCollector {
+    fn new() -> Self {
+        BoundNamesCollector {
+            regions: BTreeSet::new(),
+            types: BTreeMap::new(),
+            binder_index: ty::INNERMOST,
+        }
+    }
+
+    fn is_empty(&self) -> bool {
+        self.regions.is_empty() && self.types.is_empty()
+    }
+
+    fn write_names(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let mut start = true;
+        for r in &self.regions {
+            if !start {
+                write!(fmt, ", ")?;
+            }
+            start = false;
+            write!(fmt, "{}", r)?;
+        }
+        for (_, t) in &self.types {
+            if !start {
+                write!(fmt, ", ")?;
+            }
+            start = false;
+            write!(fmt, "{}", t)?;
+        }
+        Ok(())
+    }
+}
+
+impl<'tcx> TypeVisitor<'tcx> for BoundNamesCollector {
+    fn visit_binder<T: TypeFoldable<'tcx>>(&mut self, t: &ty::Binder<T>) -> bool {
+        self.binder_index.shift_in(1);
+        let result = t.super_visit_with(self);
+        self.binder_index.shift_out(1);
+        result
+    }
+
+    fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> bool {
+        use syntax::symbol::Symbol;
+
+        match t.sty {
+            ty::Bound(bound_ty) if bound_ty.index == self.binder_index => {
+                self.types.insert(
+                    bound_ty.var.as_u32(),
+                    match bound_ty.kind {
+                        ty::BoundTyKind::Param(name) => name,
+                        ty::BoundTyKind::Anon => Symbol::intern(
+                            &format!("^{}", bound_ty.var.as_u32())
+                        ).as_interned_str(),
+                    }
+                );
+            }
+
+            _ => (),
+        };
+
+        t.super_visit_with(self)
+    }
+
+    fn visit_region(&mut self, r: ty::Region<'tcx>) -> bool {
+        use syntax::symbol::Symbol;
+
+        match r {
+            ty::ReLateBound(index, br) if *index == self.binder_index => {
+                match br {
+                    ty::BoundRegion::BrNamed(_, name) => {
+                        self.regions.insert(*name);
+                    }
+
+                    ty::BoundRegion::BrAnon(var) => {
+                        self.regions.insert(Symbol::intern(
+                            &format!("'^{}", var)
+                        ).as_interned_str());
+                    }
+
+                    _ => (),
+                }
+            }
+
+            _ => (),
+        };
+
+        r.super_visit_with(self)
+    }
+}
+
+impl<'tcx> fmt::Display for traits::Goal<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::GoalKind::*;
+
+        match self {
+            Implies(hypotheses, goal) => {
+                write!(fmt, "if (")?;
+                for (index, hyp) in hypotheses.iter().enumerate() {
+                    if index > 0 {
+                        write!(fmt, ", ")?;
+                    }
+                    write!(fmt, "{}", hyp)?;
+                }
+                write!(fmt, ") {{ {} }}", goal)
+            }
+            And(goal1, goal2) => write!(fmt, "({} && {})", goal1, goal2),
+            Not(goal) => write!(fmt, "not {{ {} }}", goal),
+            DomainGoal(goal) => write!(fmt, "{}", goal),
+            Quantified(qkind, goal) => {
+                let mut collector = BoundNamesCollector::new();
+                goal.skip_binder().visit_with(&mut collector);
+
+                if !collector.is_empty() {
+                    write!(fmt, "{}<", qkind)?;
+                    collector.write_names(fmt)?;
+                    write!(fmt, "> {{ ")?;
+                }
+
+                write!(fmt, "{}", goal.skip_binder())?;
+
+                if !collector.is_empty() {
+                    write!(fmt, " }}")?;
+                }
+
+                Ok(())
+            }
+            CannotProve => write!(fmt, "CannotProve"),
+        }
+    }
+}
+
+impl<'tcx> fmt::Display for traits::ProgramClause<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let traits::ProgramClause { goal, hypotheses, .. } = self;
+        write!(fmt, "{}", goal)?;
+        if !hypotheses.is_empty() {
+            write!(fmt, " :- ")?;
+            for (index, condition) in hypotheses.iter().enumerate() {
+                if index > 0 {
+                    write!(fmt, ", ")?;
+                }
+                write!(fmt, "{}", condition)?;
+            }
+        }
+        write!(fmt, ".")
+    }
+}
+
+impl<'tcx> fmt::Display for traits::Clause<'tcx> {
+    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use traits::Clause::*;
+
+        match self {
+            Implies(clause) => write!(fmt, "{}", clause),
+            ForAll(clause) => {
+                let mut collector = BoundNamesCollector::new();
+                clause.skip_binder().visit_with(&mut collector);
+
+                if !collector.is_empty() {
+                    write!(fmt, "forall<")?;
+                    collector.write_names(fmt)?;
+                    write!(fmt, "> {{ ")?;
+                }
+
+                write!(fmt, "{}", clause.skip_binder())?;
+
+                if !collector.is_empty() {
+                    write!(fmt, " }}")?;
+                }
+
+                Ok(())
+            }
+        }
+    }
+}
+
 ///////////////////////////////////////////////////////////////////////////
 // Lift implementations
 
@@ -348,6 +634,91 @@ impl<'a, 'tcx> Lift<'tcx> for traits::Vtable<'a, ()> {
     }
 }
 
+EnumLiftImpl! {
+    impl<'a, 'tcx> Lift<'tcx> for traits::WhereClause<'a> {
+        type Lifted = traits::WhereClause<'tcx>;
+        (traits::WhereClause::Implemented)(trait_ref),
+        (traits::WhereClause::ProjectionEq)(projection),
+        (traits::WhereClause::TypeOutlives)(ty_outlives),
+        (traits::WhereClause::RegionOutlives)(region_outlives),
+    }
+}
+
+EnumLiftImpl! {
+    impl<'a, 'tcx> Lift<'tcx> for traits::WellFormed<'a> {
+        type Lifted = traits::WellFormed<'tcx>;
+        (traits::WellFormed::Trait)(trait_ref),
+        (traits::WellFormed::Ty)(ty),
+    }
+}
+
+EnumLiftImpl! {
+    impl<'a, 'tcx> Lift<'tcx> for traits::FromEnv<'a> {
+        type Lifted = traits::FromEnv<'tcx>;
+        (traits::FromEnv::Trait)(trait_ref),
+        (traits::FromEnv::Ty)(ty),
+    }
+}
+
+EnumLiftImpl! {
+    impl<'a, 'tcx> Lift<'tcx> for traits::DomainGoal<'a> {
+        type Lifted = traits::DomainGoal<'tcx>;
+        (traits::DomainGoal::Holds)(wc),
+        (traits::DomainGoal::WellFormed)(wf),
+        (traits::DomainGoal::FromEnv)(from_env),
+        (traits::DomainGoal::Normalize)(projection),
+    }
+}
+
+EnumLiftImpl! {
+    impl<'a, 'tcx> Lift<'tcx> for traits::GoalKind<'a> {
+        type Lifted = traits::GoalKind<'tcx>;
+        (traits::GoalKind::Implies)(hypotheses, goal),
+        (traits::GoalKind::And)(goal1, goal2),
+        (traits::GoalKind::Not)(goal),
+        (traits::GoalKind::DomainGoal)(domain_goal),
+        (traits::GoalKind::Quantified)(kind, goal),
+        (traits::GoalKind::CannotProve),
+    }
+}
+
+impl<'a, 'tcx> Lift<'tcx> for traits::Environment<'a> {
+    type Lifted = traits::Environment<'tcx>;
+    fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+        tcx.lift(&self.clauses).map(|clauses| {
+            traits::Environment {
+                clauses,
+            }
+        })
+    }
+}
+
+impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
+    type Lifted = traits::InEnvironment<'tcx, G::Lifted>;
+    fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+        tcx.lift(&self.environment).and_then(|environment| {
+            tcx.lift(&self.goal).map(|goal| {
+                traits::InEnvironment {
+                    environment,
+                    goal,
+                }
+            })
+        })
+    }
+}
+
+impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
+where
+    C: chalk_engine::context::Context + Clone,
+    C: traits::ExClauseLift<'tcx>,
+{
+    type Lifted = C::LiftedExClause;
+
+    fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+        <C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
+    }
+}
+
 ///////////////////////////////////////////////////////////////////////////
 // TypeFoldable implementations.
 
@@ -436,123 +807,6 @@ BraceStructTypeFoldableImpl! {
     } where T: TypeFoldable<'tcx>
 }
 
-impl<'tcx> fmt::Display for traits::WhereClause<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::WhereClause::*;
-
-        match self {
-            Implemented(trait_ref) => write!(fmt, "Implemented({})", trait_ref),
-            ProjectionEq(projection) => write!(fmt, "ProjectionEq({})", projection),
-            RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
-            TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
-        }
-    }
-}
-
-impl<'tcx> fmt::Display for traits::WellFormed<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::WellFormed::*;
-
-        match self {
-            Trait(trait_ref) => write!(fmt, "WellFormed({})", trait_ref),
-            Ty(ty) => write!(fmt, "WellFormed({})", ty),
-        }
-    }
-}
-
-impl<'tcx> fmt::Display for traits::FromEnv<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::FromEnv::*;
-
-        match self {
-            Trait(trait_ref) => write!(fmt, "FromEnv({})", trait_ref),
-            Ty(ty) => write!(fmt, "FromEnv({})", ty),
-        }
-    }
-}
-
-impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::DomainGoal::*;
-
-        match self {
-            Holds(wc) => write!(fmt, "{}", wc),
-            WellFormed(wf) => write!(fmt, "{}", wf),
-            FromEnv(from_env) => write!(fmt, "{}", from_env),
-            Normalize(projection) => write!(fmt, "Normalize({})", projection),
-        }
-    }
-}
-
-impl fmt::Display for traits::QuantifierKind {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::QuantifierKind::*;
-
-        match self {
-            Universal => write!(fmt, "forall"),
-            Existential => write!(fmt, "exists"),
-        }
-    }
-}
-
-impl<'tcx> fmt::Display for traits::Goal<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::GoalKind::*;
-
-        match self {
-            Implies(hypotheses, goal) => {
-                write!(fmt, "if (")?;
-                for (index, hyp) in hypotheses.iter().enumerate() {
-                    if index > 0 {
-                        write!(fmt, ", ")?;
-                    }
-                    write!(fmt, "{}", hyp)?;
-                }
-                write!(fmt, ") {{ {} }}", goal)
-            }
-            And(goal1, goal2) => write!(fmt, "({} && {})", goal1, goal2),
-            Not(goal) => write!(fmt, "not {{ {} }}", goal),
-            DomainGoal(goal) => write!(fmt, "{}", goal),
-            Quantified(qkind, goal) => {
-                // FIXME: appropriate binder names
-                write!(fmt, "{}<> {{ {} }}", qkind, goal.skip_binder())
-            }
-            CannotProve => write!(fmt, "CannotProve"),
-        }
-    }
-}
-
-impl<'tcx> fmt::Display for traits::ProgramClause<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        let traits::ProgramClause { goal, hypotheses, .. } = self;
-        write!(fmt, "{}", goal)?;
-        if !hypotheses.is_empty() {
-            write!(fmt, " :- ")?;
-            for (index, condition) in hypotheses.iter().enumerate() {
-                if index > 0 {
-                    write!(fmt, ", ")?;
-                }
-                write!(fmt, "{}", condition)?;
-            }
-        }
-        write!(fmt, ".")
-    }
-}
-
-impl<'tcx> fmt::Display for traits::Clause<'tcx> {
-    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
-        use traits::Clause::*;
-
-        match self {
-            Implies(clause) => write!(fmt, "{}", clause),
-            ForAll(clause) => {
-                // FIXME: appropriate binder names
-                write!(fmt, "forall<> {{ {} }}", clause.skip_binder())
-            }
-        }
-    }
-}
-
 EnumTypeFoldableImpl! {
     impl<'tcx> TypeFoldable<'tcx> for traits::WhereClause<'tcx> {
         (traits::WhereClause::Implemented)(trait_ref),
@@ -562,16 +816,6 @@ EnumTypeFoldableImpl! {
     }
 }
 
-EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::WhereClause<'a> {
-        type Lifted = traits::WhereClause<'tcx>;
-        (traits::WhereClause::Implemented)(trait_ref),
-        (traits::WhereClause::ProjectionEq)(projection),
-        (traits::WhereClause::TypeOutlives)(ty_outlives),
-        (traits::WhereClause::RegionOutlives)(region_outlives),
-    }
-}
-
 EnumTypeFoldableImpl! {
     impl<'tcx> TypeFoldable<'tcx> for traits::WellFormed<'tcx> {
         (traits::WellFormed::Trait)(trait_ref),
@@ -579,14 +823,6 @@ EnumTypeFoldableImpl! {
     }
 }
 
-EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::WellFormed<'a> {
-        type Lifted = traits::WellFormed<'tcx>;
-        (traits::WellFormed::Trait)(trait_ref),
-        (traits::WellFormed::Ty)(ty),
-    }
-}
-
 EnumTypeFoldableImpl! {
     impl<'tcx> TypeFoldable<'tcx> for traits::FromEnv<'tcx> {
         (traits::FromEnv::Trait)(trait_ref),
@@ -594,14 +830,6 @@ EnumTypeFoldableImpl! {
     }
 }
 
-EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::FromEnv<'a> {
-        type Lifted = traits::FromEnv<'tcx>;
-        (traits::FromEnv::Trait)(trait_ref),
-        (traits::FromEnv::Ty)(ty),
-    }
-}
-
 EnumTypeFoldableImpl! {
     impl<'tcx> TypeFoldable<'tcx> for traits::DomainGoal<'tcx> {
         (traits::DomainGoal::Holds)(wc),
@@ -611,16 +839,6 @@ EnumTypeFoldableImpl! {
     }
 }
 
-EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::DomainGoal<'a> {
-        type Lifted = traits::DomainGoal<'tcx>;
-        (traits::DomainGoal::Holds)(wc),
-        (traits::DomainGoal::WellFormed)(wf),
-        (traits::DomainGoal::FromEnv)(from_env),
-        (traits::DomainGoal::Normalize)(projection),
-    }
-}
-
 CloneTypeFoldableAndLiftImpls! {
     traits::QuantifierKind,
 }
@@ -636,18 +854,6 @@ EnumTypeFoldableImpl! {
     }
 }
 
-EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::GoalKind<'a> {
-        type Lifted = traits::GoalKind<'tcx>;
-        (traits::GoalKind::Implies)(hypotheses, goal),
-        (traits::GoalKind::And)(goal1, goal2),
-        (traits::GoalKind::Not)(goal),
-        (traits::GoalKind::DomainGoal)(domain_goal),
-        (traits::GoalKind::Quantified)(kind, goal),
-        (traits::GoalKind::CannotProve),
-    }
-}
-
 impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::List<traits::Goal<'tcx>> {
     fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
         let v = self.iter()
@@ -702,31 +908,6 @@ BraceStructTypeFoldableImpl! {
     } where G: TypeFoldable<'tcx>
 }
 
-impl<'a, 'tcx> Lift<'tcx> for traits::Environment<'a> {
-    type Lifted = traits::Environment<'tcx>;
-    fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
-        tcx.lift(&self.clauses).map(|clauses| {
-            traits::Environment {
-                clauses,
-            }
-        })
-    }
-}
-
-impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
-    type Lifted = traits::InEnvironment<'tcx, G::Lifted>;
-    fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
-        tcx.lift(&self.environment).and_then(|environment| {
-            tcx.lift(&self.goal).map(|goal| {
-                traits::InEnvironment {
-                    environment,
-                    goal,
-                }
-            })
-        })
-    }
-}
-
 impl<'tcx> TypeFoldable<'tcx> for traits::Clauses<'tcx> {
     fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
         let v = self.iter()
@@ -761,18 +942,6 @@ where
     }
 }
 
-impl<'tcx, C> Lift<'tcx> for chalk_engine::ExClause<C>
-where
-    C: chalk_engine::context::Context + Clone,
-    C: traits::ExClauseLift<'tcx>,
-{
-    type Lifted = C::LiftedExClause;
-
-    fn lift_to_tcx<'a, 'gcx>(&self, tcx: TyCtxt<'a, 'gcx, 'tcx>) -> Option<Self::Lifted> {
-        <C as traits::ExClauseLift>::lift_ex_clause_to_tcx(self, tcx)
-    }
-}
-
 EnumTypeFoldableImpl! {
     impl<'tcx, C> TypeFoldable<'tcx> for chalk_engine::DelayedLiteral<C> {
         (chalk_engine::DelayedLiteral::CannotProve)(a),
diff --git a/src/librustc/ty/fold.rs b/src/librustc/ty/fold.rs
index ffa4380a5d63c..a897afa0ca663 100644
--- a/src/librustc/ty/fold.rs
+++ b/src/librustc/ty/fold.rs
@@ -520,22 +520,14 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
     pub fn replace_late_bound_regions<T, F>(
         self,
         value: &Binder<T>,
-        mut fld_r: F
+        fld_r: F
     ) -> (T, BTreeMap<ty::BoundRegion, ty::Region<'tcx>>)
         where F: FnMut(ty::BoundRegion) -> ty::Region<'tcx>,
               T: TypeFoldable<'tcx>
     {
-        let mut map = BTreeMap::new();
-        let mut real_fldr = |br| {
-            *map.entry(br).or_insert_with(|| fld_r(br))
-        };
-
         // identity for bound types
-        let mut fld_t = |bound_ty| self.mk_ty(ty::Bound(bound_ty));
-
-        let mut replacer = BoundVarReplacer::new(self, &mut real_fldr, &mut fld_t);
-        let result = value.skip_binder().fold_with(&mut replacer);
-        (result, map)
+        let fld_t = |bound_ty| self.mk_ty(ty::Bound(bound_ty));
+        self.replace_escaping_bound_vars(value.skip_binder(), fld_r, fld_t)
     }
 
     /// Replace all escaping bound vars. The `fld_r` closure replaces escaping
@@ -545,17 +537,23 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
         value: &T,
         mut fld_r: F,
         mut fld_t: G
-    ) -> T
+    ) -> (T, BTreeMap<ty::BoundRegion, ty::Region<'tcx>>)
         where F: FnMut(ty::BoundRegion) -> ty::Region<'tcx>,
               G: FnMut(ty::BoundTy) -> ty::Ty<'tcx>,
               T: TypeFoldable<'tcx>
     {
+        let mut map = BTreeMap::new();
+
         if !value.has_escaping_bound_vars() {
-            value.clone()
+            (value.clone(), map)
         } else {
-            let mut replacer = BoundVarReplacer::new(self, &mut fld_r, &mut fld_t);
+            let mut real_fld_r = |br| {
+                *map.entry(br).or_insert_with(|| fld_r(br))
+            };
+
+            let mut replacer = BoundVarReplacer::new(self, &mut real_fld_r, &mut fld_t);
             let result = value.fold_with(&mut replacer);
-            result
+            (result, map)
         }
     }
 
@@ -567,7 +565,7 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
         value: &Binder<T>,
         fld_r: F,
         fld_t: G
-    ) -> T
+    ) -> (T, BTreeMap<ty::BoundRegion, ty::Region<'tcx>>)
         where F: FnMut(ty::BoundRegion) -> ty::Region<'tcx>,
               G: FnMut(ty::BoundTy) -> ty::Ty<'tcx>,
               T: TypeFoldable<'tcx>
diff --git a/src/librustc/ty/query/mod.rs b/src/librustc/ty/query/mod.rs
index ed7b2cffc46f6..c834166e67d88 100644
--- a/src/librustc/ty/query/mod.rs
+++ b/src/librustc/ty/query/mod.rs
@@ -687,7 +687,7 @@ define_queries! { <'tcx>
         ) -> Clauses<'tcx>,
 
         // Get the chalk-style environment of the given item.
-        [] fn environment: Environment(DefId) -> traits::Environment<'tcx>,
+        [] fn environment: Environment(DefId) -> ty::Binder<traits::Environment<'tcx>>,
     },
 
     Linking {
diff --git a/src/librustc/ty/subst.rs b/src/librustc/ty/subst.rs
index b28e7c9fb199b..b7f1731ba44e5 100644
--- a/src/librustc/ty/subst.rs
+++ b/src/librustc/ty/subst.rs
@@ -179,6 +179,34 @@ impl<'a, 'gcx, 'tcx> Substs<'tcx> {
         })
     }
 
+    /// Creates a `Substs` that maps each generic parameter to a higher-ranked
+    /// var bound at index `0`. For types, we use a `BoundVar` index equal to
+    /// the type parameter index. For regions, we use the `BoundRegion::BrNamed`
+    /// variant (which has a def-id).
+    pub fn bound_vars_for_item(
+        tcx: TyCtxt<'a, 'gcx, 'tcx>,
+        def_id: DefId
+    ) -> &'tcx Substs<'tcx> {
+        Substs::for_item(tcx, def_id, |param, _| {
+            match param.kind {
+                ty::GenericParamDefKind::Type { .. } => {
+                    tcx.mk_ty(ty::Bound(ty::BoundTy {
+                        index: ty::INNERMOST,
+                        var: ty::BoundVar::from(param.index),
+                        kind: ty::BoundTyKind::Param(param.name),
+                    })).into()
+                }
+
+                ty::GenericParamDefKind::Lifetime => {
+                    tcx.mk_region(ty::RegionKind::ReLateBound(
+                        ty::INNERMOST,
+                        ty::BoundRegion::BrNamed(param.def_id, param.name)
+                    )).into()
+                }
+            }
+        })
+    }
+
     /// Creates a `Substs` for generic parameter definitions,
     /// by calling closures to obtain each kind.
     /// The closures get to observe the `Substs` as they're
diff --git a/src/librustc/util/ppaux.rs b/src/librustc/util/ppaux.rs
index 5ec4f55b142eb..e44c0c05bb1a6 100644
--- a/src/librustc/util/ppaux.rs
+++ b/src/librustc/util/ppaux.rs
@@ -1114,9 +1114,9 @@ define_print! {
                     match bound_ty.kind {
                         ty::BoundTyKind::Anon => {
                             if bound_ty.index == ty::INNERMOST {
-                                write!(f, "?{}", bound_ty.var.index())
+                                write!(f, "^{}", bound_ty.var.index())
                             } else {
-                                write!(f, "?{}_{}", bound_ty.index.index(), bound_ty.var.index())
+                                write!(f, "^{}_{}", bound_ty.index.index(), bound_ty.var.index())
                             }
                         }
 
diff --git a/src/librustc_mir/borrow_check/nll/type_check/input_output.rs b/src/librustc_mir/borrow_check/nll/type_check/input_output.rs
index ab4ee3a4ad0e5..85ea39e538f78 100644
--- a/src/librustc_mir/borrow_check/nll/type_check/input_output.rs
+++ b/src/librustc_mir/borrow_check/nll/type_check/input_output.rs
@@ -62,7 +62,7 @@ impl<'a, 'gcx, 'tcx> TypeChecker<'a, 'gcx, 'tcx> {
                     // "inside" the closure.
                     Some(
                         self.infcx
-                            .replace_late_bound_regions_with_fresh_var(
+                            .replace_bound_vars_with_fresh_vars(
                                 mir.span,
                                 LateBoundRegionConversionTime::FnCall,
                                 &poly_sig,
diff --git a/src/librustc_mir/borrow_check/nll/type_check/mod.rs b/src/librustc_mir/borrow_check/nll/type_check/mod.rs
index c8d2bcd8b9315..2193dba9fcac8 100644
--- a/src/librustc_mir/borrow_check/nll/type_check/mod.rs
+++ b/src/librustc_mir/borrow_check/nll/type_check/mod.rs
@@ -1406,7 +1406,7 @@ impl<'a, 'gcx, 'tcx> TypeChecker<'a, 'gcx, 'tcx> {
                         return;
                     }
                 };
-                let (sig, map) = self.infcx.replace_late_bound_regions_with_fresh_var(
+                let (sig, map) = self.infcx.replace_bound_vars_with_fresh_vars(
                     term.source_info.span,
                     LateBoundRegionConversionTime::FnCall,
                     &sig,
diff --git a/src/librustc_traits/Cargo.toml b/src/librustc_traits/Cargo.toml
index 16f0f11757a12..f057cbb50334e 100644
--- a/src/librustc_traits/Cargo.toml
+++ b/src/librustc_traits/Cargo.toml
@@ -14,6 +14,7 @@ graphviz = { path = "../libgraphviz" }
 log = { version = "0.4" }
 rustc = { path = "../librustc" }
 rustc_data_structures = { path = "../librustc_data_structures" }
+rustc_target = { path = "../librustc_target" }
 syntax = { path = "../libsyntax" }
 syntax_pos = { path = "../libsyntax_pos" }
 chalk-engine = { version = "0.8.0", default-features=false }
diff --git a/src/librustc_traits/chalk_context.rs b/src/librustc_traits/chalk_context/mod.rs
similarity index 63%
rename from src/librustc_traits/chalk_context.rs
rename to src/librustc_traits/chalk_context/mod.rs
index bf252053199f8..0fd9f607a5462 100644
--- a/src/librustc_traits/chalk_context.rs
+++ b/src/librustc_traits/chalk_context/mod.rs
@@ -8,6 +8,8 @@
 // option. This file may not be copied, modified, or distributed
 // except according to those terms.
 
+mod program_clauses;
+
 use chalk_engine::fallible::Fallible as ChalkEngineFallible;
 use chalk_engine::{context, hh::HhGoal, DelayedLiteral, ExClause};
 use rustc::infer::canonical::{
@@ -15,15 +17,12 @@ use rustc::infer::canonical::{
 };
 use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
 use rustc::traits::{
-    WellFormed,
-    FromEnv,
     DomainGoal,
     ExClauseFold,
     ExClauseLift,
     Goal,
     GoalKind,
     Clause,
-    ProgramClauseCategory,
     QuantifierKind,
     Environment,
     InEnvironment,
@@ -31,7 +30,6 @@ use rustc::traits::{
 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
 use rustc::ty::subst::Kind;
 use rustc::ty::{self, TyCtxt};
-use rustc::hir::def_id::DefId;
 
 use std::fmt::{self, Debug};
 use std::marker::PhantomData;
@@ -335,228 +333,7 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         environment: &Environment<'tcx>,
         goal: &DomainGoal<'tcx>,
     ) -> Vec<Clause<'tcx>> {
-        use rustc::traits::WhereClause::*;
-
-        fn assemble_clauses_from_impls<'tcx>(
-            tcx: ty::TyCtxt<'_, '_, 'tcx>,
-            trait_def_id: DefId,
-            clauses: &mut Vec<Clause<'tcx>>
-        ) {
-            tcx.for_each_impl(trait_def_id, |impl_def_id| {
-                clauses.extend(
-                    tcx.program_clauses_for(impl_def_id)
-                        .into_iter()
-                        .cloned()
-                );
-            });
-        }
-
-        fn assemble_clauses_from_assoc_ty_values<'tcx>(
-            tcx: ty::TyCtxt<'_, '_, 'tcx>,
-            trait_def_id: DefId,
-            clauses: &mut Vec<Clause<'tcx>>
-        ) {
-            tcx.for_each_impl(trait_def_id, |impl_def_id| {
-                for def_id in tcx.associated_item_def_ids(impl_def_id).iter() {
-                    clauses.extend(
-                        tcx.program_clauses_for(*def_id)
-                            .into_iter()
-                            .cloned()
-                    );
-                }
-            });
-        }
-
-        let mut clauses = match goal {
-            DomainGoal::Holds(Implemented(trait_predicate)) => {
-                // These come from:
-                // * implementations of the trait itself (rule `Implemented-From-Impl`)
-                // * the trait decl (rule `Implemented-From-Env`)
-
-                let mut clauses = vec![];
-                assemble_clauses_from_impls(
-                    self.infcx.tcx,
-                    trait_predicate.def_id(),
-                    &mut clauses
-                );
-
-                // FIXME: we need to add special rules for builtin impls:
-                // * `Copy` / `Clone`
-                // * `Sized`
-                // * `Unsize`
-                // * `Generator`
-                // * `FnOnce` / `FnMut` / `Fn`
-                // * trait objects
-                // * auto traits
-
-                // Rule `Implemented-From-Env` will be computed from the environment.
-                clauses
-            }
-
-            DomainGoal::Holds(ProjectionEq(projection_predicate)) => {
-                // These come from:
-                // * the assoc type definition (rule `ProjectionEq-Placeholder`)
-                // * normalization of the assoc ty values (rule `ProjectionEq-Normalize`)
-                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
-                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
-
-                let clauses = self.infcx.tcx.program_clauses_for(
-                    projection_predicate.projection_ty.item_def_id
-                ).into_iter()
-
-                    // only select `ProjectionEq-Placeholder` and `ProjectionEq-Normalize`
-                    .filter(|clause| clause.category() == ProgramClauseCategory::Other)
-
-                    .cloned()
-                    .collect::<Vec<_>>();
-
-                // Rules `Implied-Bound-From-Trait` and `Implied-Bound-From-Type` will be computed
-                // from the environment.
-                clauses
-            }
-
-            DomainGoal::Holds(RegionOutlives(..)) => {
-                // These come from:
-                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
-                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
-
-                // All of these rules are computed in the environment.
-                vec![]
-            }
-
-            DomainGoal::Holds(TypeOutlives(..)) => {
-                // These come from:
-                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
-                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
-
-                // All of these rules are computed in the environment.
-                vec![]
-            }
-
-            DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => {
-                // These come from -- the trait decl (rule `WellFormed-TraitRef`).
-                self.infcx.tcx.program_clauses_for(trait_predicate.def_id())
-                    .into_iter()
-
-                    // only select `WellFormed-TraitRef`
-                    .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
-
-                    .cloned()
-                    .collect()
-            }
-
-            DomainGoal::WellFormed(WellFormed::Ty(ty)) => {
-                // These come from:
-                // * the associated type definition if `ty` refers to an unnormalized
-                //   associated type (rule `WellFormed-AssocTy`)
-                // * custom rules for built-in types
-                // * the type definition otherwise (rule `WellFormed-Type`)
-                let clauses = match ty.sty {
-                    ty::Projection(data) => {
-                        self.infcx.tcx.program_clauses_for(data.item_def_id)
-                    }
-
-                    // These types are always WF (recall that we do not check
-                    // for parameters to be WF)
-                    ty::Bool |
-                    ty::Char |
-                    ty::Int(..) |
-                    ty::Uint(..) |
-                    ty::Float(..) |
-                    ty::Str |
-                    ty::RawPtr(..) |
-                    ty::FnPtr(..) |
-                    ty::Param(..) |
-                    ty::Never => {
-                        ty::List::empty()
-                    }
-
-                    // WF if inner type is `Sized`
-                    ty::Slice(..) |
-                    ty::Array(..) => {
-                        ty::List::empty()
-                    }
-
-                    ty::Tuple(..) => {
-                        ty::List::empty()
-                    }
-
-                    // WF if `sub_ty` outlives `region`
-                    ty::Ref(..) => {
-                        ty::List::empty()
-                    }
-
-                    ty::Dynamic(..) => {
-                        // FIXME: no rules yet for trait objects
-                        ty::List::empty()
-                    }
-
-                    ty::Adt(def, ..) => {
-                        self.infcx.tcx.program_clauses_for(def.did)
-                    }
-
-                    ty::Foreign(def_id) |
-                    ty::FnDef(def_id, ..) |
-                    ty::Closure(def_id, ..) |
-                    ty::Generator(def_id, ..) |
-                    ty::Opaque(def_id, ..) => {
-                        self.infcx.tcx.program_clauses_for(def_id)
-                    }
-
-                    ty::GeneratorWitness(..) |
-                    ty::UnnormalizedProjection(..) |
-                    ty::Infer(..) |
-                    ty::Bound(..) |
-                    ty::Error => {
-                        bug!("unexpected type {:?}", ty)
-                    }
-                };
-
-                clauses.into_iter()
-                    .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
-                    .cloned()
-                    .collect()
-            }
-
-            DomainGoal::FromEnv(FromEnv::Trait(..)) => {
-                // These come from:
-                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
-                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
-                // * implied bounds from assoc type defs (rules `Implied-Trait-From-AssocTy`,
-                //   `Implied-Bound-From-AssocTy` and `Implied-WC-From-AssocTy`)
-
-                // All of these rules are computed in the environment.
-                vec![]
-            }
-
-            DomainGoal::FromEnv(FromEnv::Ty(..)) => {
-                // There are no `FromEnv::Ty(..) :- ...` rules (this predicate only
-                // comes from the environment).
-                vec![]
-            }
-
-            DomainGoal::Normalize(projection_predicate) => {
-                // These come from -- assoc ty values (rule `Normalize-From-Impl`).
-                let mut clauses = vec![];
-
-                assemble_clauses_from_assoc_ty_values(
-                    self.infcx.tcx,
-                    projection_predicate.projection_ty.trait_ref(self.infcx.tcx).def_id,
-                    &mut clauses
-                );
-
-                clauses
-            }
-        };
-
-        let environment = self.infcx.tcx.lift_to_global(environment)
-            .expect("environment is not global");
-        clauses.extend(
-            self.infcx.tcx.program_clauses_for_env(environment)
-                .into_iter()
-                .cloned()
-        );
-        clauses
+        self.program_clauses_impl(environment, goal)
     }
 
     fn instantiate_binders_universally(
@@ -570,12 +347,11 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         &mut self,
         arg: &ty::Binder<Goal<'tcx>>,
     ) -> Goal<'tcx> {
-        let (value, _map) = self.infcx.replace_late_bound_regions_with_fresh_var(
+        self.infcx.replace_bound_vars_with_fresh_vars(
             DUMMY_SP,
             LateBoundRegionConversionTime::HigherRankedType,
-            arg,
-        );
-        value
+            arg
+        ).0
     }
 
     fn debug_ex_clause(&mut self, value: &'v ChalkExClause<'tcx>) -> Box<dyn Debug + 'v> {
diff --git a/src/librustc_traits/chalk_context/program_clauses.rs b/src/librustc_traits/chalk_context/program_clauses.rs
new file mode 100644
index 0000000000000..31f97b72e1927
--- /dev/null
+++ b/src/librustc_traits/chalk_context/program_clauses.rs
@@ -0,0 +1,476 @@
+// Copyright 2018 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 rustc::traits::{
+    WellFormed,
+    FromEnv,
+    DomainGoal,
+    GoalKind,
+    Clause,
+    Clauses,
+    ProgramClause,
+    ProgramClauseCategory,
+    Environment,
+};
+use rustc::ty;
+use rustc::hir;
+use rustc::hir::def_id::DefId;
+use rustc_target::spec::abi;
+use super::ChalkInferenceContext;
+use crate::lowering::Lower;
+use std::iter;
+
+fn assemble_clauses_from_impls<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    trait_def_id: DefId,
+    clauses: &mut Vec<Clause<'tcx>>
+) {
+    tcx.for_each_impl(trait_def_id, |impl_def_id| {
+        clauses.extend(
+            tcx.program_clauses_for(impl_def_id)
+                .into_iter()
+                .cloned()
+        );
+    });
+}
+
+fn assemble_clauses_from_assoc_ty_values<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    trait_def_id: DefId,
+    clauses: &mut Vec<Clause<'tcx>>
+) {
+    tcx.for_each_impl(trait_def_id, |impl_def_id| {
+        for def_id in tcx.associated_item_def_ids(impl_def_id).iter() {
+            clauses.extend(
+                tcx.program_clauses_for(*def_id)
+                    .into_iter()
+                    .cloned()
+            );
+        }
+    });
+}
+
+fn program_clauses_for_raw_ptr<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+    let ty = ty::Bound(
+        ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(0))
+    );
+    let ty = tcx.mk_ty(ty);
+
+    let ptr_ty = tcx.mk_ptr(ty::TypeAndMut {
+        ty,
+        mutbl: hir::Mutability::MutImmutable,
+    });
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(ptr_ty)),
+        hypotheses: ty::List::empty(),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall<T> { WellFormed(*const T). }`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+fn program_clauses_for_fn_ptr<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    arity_and_output: usize,
+    variadic: bool,
+    unsafety: hir::Unsafety,
+    abi: abi::Abi
+) -> Clauses<'tcx> {
+    let inputs_and_output = tcx.mk_type_list(
+        (0..arity_and_output).into_iter()
+            // DebruijnIndex(1) because we are going to inject these in a `PolyFnSig`
+            .map(|i| ty::BoundTy::new(ty::DebruijnIndex::from(1usize), ty::BoundVar::from(i)))
+            .map(|t| tcx.mk_ty(ty::Bound(t)))
+    );
+
+    let fn_sig = ty::Binder::bind(ty::FnSig {
+        inputs_and_output,
+        variadic,
+        unsafety,
+        abi,
+    });
+    let fn_ptr = tcx.mk_fn_ptr(fn_sig);
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(fn_ptr)),
+        hypotheses: ty::List::empty(),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall <T1, ..., Tn+1> { WellFormed(for<> fn(T1, ..., Tn) -> Tn+1). }`
+    // where `n + 1` == `arity_and_output`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+fn program_clauses_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+    let ty = ty::Bound(
+        ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(0))
+    );
+    let ty = tcx.mk_ty(ty);
+
+    let slice_ty = tcx.mk_slice(ty);
+
+    let sized_trait = match tcx.lang_items().sized_trait() {
+        Some(def_id) => def_id,
+        None => return ty::List::empty(),
+    };
+    let sized_implemented = ty::TraitRef {
+        def_id: sized_trait,
+        substs: tcx.mk_substs_trait(ty, ty::List::empty()),
+    };
+    let sized_implemented: DomainGoal = ty::TraitPredicate {
+        trait_ref: sized_implemented
+    }.lower();
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(slice_ty)),
+        hypotheses: tcx.mk_goals(
+            iter::once(tcx.mk_goal(GoalKind::DomainGoal(sized_implemented)))
+        ),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall<T> { WellFormed([T]) :- Implemented(T: Sized). }`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+fn program_clauses_for_array<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    length: &'tcx ty::Const<'tcx>
+) -> Clauses<'tcx> {
+    let ty = ty::Bound(
+        ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(0))
+    );
+    let ty = tcx.mk_ty(ty);
+
+    let array_ty = tcx.mk_ty(ty::Array(ty, length));
+
+    let sized_trait = match tcx.lang_items().sized_trait() {
+        Some(def_id) => def_id,
+        None => return ty::List::empty(),
+    };
+    let sized_implemented = ty::TraitRef {
+        def_id: sized_trait,
+        substs: tcx.mk_substs_trait(ty, ty::List::empty()),
+    };
+    let sized_implemented: DomainGoal = ty::TraitPredicate {
+        trait_ref: sized_implemented
+    }.lower();
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(array_ty)),
+        hypotheses: tcx.mk_goals(
+            iter::once(tcx.mk_goal(GoalKind::DomainGoal(sized_implemented)))
+        ),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall<T> { WellFormed([T; length]) :- Implemented(T: Sized). }`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+fn program_clauses_for_tuple<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    arity: usize
+) -> Clauses<'tcx> {
+    let type_list = tcx.mk_type_list(
+        (0..arity).into_iter()
+            .map(|i| ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from(i)))
+            .map(|t| tcx.mk_ty(ty::Bound(t)))
+    );
+
+    let tuple_ty = tcx.mk_ty(ty::Tuple(type_list));
+
+    let sized_trait = match tcx.lang_items().sized_trait() {
+        Some(def_id) => def_id,
+        None => return ty::List::empty(),
+    };
+    let sized_implemented = type_list[0..arity - 1].iter()
+        .map(|ty| ty::TraitRef {
+            def_id: sized_trait,
+            substs: tcx.mk_substs_trait(*ty, ty::List::empty()),
+        })
+        .map(|trait_ref| ty::TraitPredicate { trait_ref })
+        .map(|predicate| predicate.lower());
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(tuple_ty)),
+        hypotheses: tcx.mk_goals(
+            sized_implemented.map(|domain_goal| {
+                tcx.mk_goal(GoalKind::DomainGoal(domain_goal))
+            })
+        ),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // ```
+    // forall<T1, ..., Tn-1, Tn> {
+    //     WellFormed((T1, ..., Tn)) :-
+    //         Implemented(T1: Sized),
+    //         ...
+    //         Implemented(Tn-1: Sized).
+    // }
+    // ```
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+fn program_clauses_for_ref<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+    let region = tcx.mk_region(
+        ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
+    );
+    let ty = tcx.mk_ty(
+        ty::Bound(ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(1)))
+    );
+
+    let ref_ty = tcx.mk_ref(region, ty::TypeAndMut {
+        ty,
+        mutbl: hir::Mutability::MutImmutable,
+    });
+
+    let outlives: DomainGoal = ty::OutlivesPredicate(ty, region).lower();
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(ref_ty)),
+        hypotheses: tcx.mk_goals(
+            iter::once(tcx.mk_goal(outlives.into_goal()))
+        ),
+        category: ProgramClauseCategory::ImpliedBound,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall<'a, T> { WellFormed(&'a T) :- Outlives(T: 'a). }`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+impl ChalkInferenceContext<'cx, 'gcx, 'tcx> {
+    pub(super) fn program_clauses_impl(
+        &self,
+        environment: &Environment<'tcx>,
+        goal: &DomainGoal<'tcx>,
+    ) -> Vec<Clause<'tcx>> {
+        use rustc::traits::WhereClause::*;
+
+        let mut clauses = match goal {
+            DomainGoal::Holds(Implemented(trait_predicate)) => {
+                // These come from:
+                // * implementations of the trait itself (rule `Implemented-From-Impl`)
+                // * the trait decl (rule `Implemented-From-Env`)
+
+                let mut clauses = vec![];
+                assemble_clauses_from_impls(
+                    self.infcx.tcx,
+                    trait_predicate.def_id(),
+                    &mut clauses
+                );
+
+                // FIXME: we need to add special rules for builtin impls:
+                // * `Copy` / `Clone`
+                // * `Sized`
+                // * `Unsize`
+                // * `Generator`
+                // * `FnOnce` / `FnMut` / `Fn`
+                // * trait objects
+                // * auto traits
+
+                // Rule `Implemented-From-Env` will be computed from the environment.
+                clauses
+            }
+
+            DomainGoal::Holds(ProjectionEq(projection_predicate)) => {
+                // These come from:
+                // * the assoc type definition (rule `ProjectionEq-Placeholder`)
+                // * normalization of the assoc ty values (rule `ProjectionEq-Normalize`)
+                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
+                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
+
+                let clauses = self.infcx.tcx.program_clauses_for(
+                    projection_predicate.projection_ty.item_def_id
+                ).into_iter()
+
+                    // only select `ProjectionEq-Placeholder` and `ProjectionEq-Normalize`
+                    .filter(|clause| clause.category() == ProgramClauseCategory::Other)
+
+                    .cloned()
+                    .collect::<Vec<_>>();
+
+                // Rules `Implied-Bound-From-Trait` and `Implied-Bound-From-Type` will be computed
+                // from the environment.
+                clauses
+            }
+
+            DomainGoal::Holds(RegionOutlives(..)) => {
+                // These come from:
+                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
+                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
+
+                // All of these rules are computed in the environment.
+                vec![]
+            }
+
+            DomainGoal::Holds(TypeOutlives(..)) => {
+                // These come from:
+                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
+                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
+
+                // All of these rules are computed in the environment.
+                vec![]
+            }
+
+            DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)) => {
+                // These come from -- the trait decl (rule `WellFormed-TraitRef`).
+                self.infcx.tcx.program_clauses_for(trait_predicate.def_id())
+                    .into_iter()
+
+                    // only select `WellFormed-TraitRef`
+                    .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
+
+                    .cloned()
+                    .collect()
+            }
+
+            DomainGoal::WellFormed(WellFormed::Ty(ty)) => {
+                // These come from:
+                // * the associated type definition if `ty` refers to an unnormalized
+                //   associated type (rule `WellFormed-AssocTy`)
+                // * custom rules for built-in types
+                // * the type definition otherwise (rule `WellFormed-Type`)
+                let clauses = match ty.sty {
+                    ty::Projection(data) => {
+                        self.infcx.tcx.program_clauses_for(data.item_def_id)
+                    }
+
+                    // These types are always WF and non-parametric.
+                    ty::Bool |
+                    ty::Char |
+                    ty::Int(..) |
+                    ty::Uint(..) |
+                    ty::Float(..) |
+                    ty::Str |
+                    ty::Never => {
+                        let wf_clause = ProgramClause {
+                            goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
+                            hypotheses: ty::List::empty(),
+                            category: ProgramClauseCategory::WellFormed,
+                        };
+                        let wf_clause = Clause::ForAll(ty::Binder::dummy(wf_clause));
+
+                        self.infcx.tcx.mk_clauses(iter::once(wf_clause))
+                    }
+
+                    // Always WF (recall that we do not check for parameters to be WF).
+                    ty::RawPtr(..) => program_clauses_for_raw_ptr(self.infcx.tcx),
+
+                    // Always WF (recall that we do not check for parameters to be WF).
+                    ty::FnPtr(fn_ptr) => {
+                        let fn_ptr = fn_ptr.skip_binder();
+                        program_clauses_for_fn_ptr(
+                            self.infcx.tcx,
+                            fn_ptr.inputs_and_output.len(),
+                            fn_ptr.variadic,
+                            fn_ptr.unsafety,
+                            fn_ptr.abi
+                        )
+                    }
+
+                    // WF if inner type is `Sized`.
+                    ty::Slice(..) => program_clauses_for_slice(self.infcx.tcx),
+
+                    // WF if inner type is `Sized`.
+                    ty::Array(_, length) => program_clauses_for_array(self.infcx.tcx, length),
+
+                    // WF if all types but the last one are `Sized`.
+                    ty::Tuple(types) => program_clauses_for_tuple(
+                        self.infcx.tcx,
+                        types.len()
+                    ),
+
+                    // WF if `sub_ty` outlives `region`.
+                    ty::Ref(..) => program_clauses_for_ref(self.infcx.tcx),
+
+                    ty::Dynamic(..) => {
+                        // FIXME: no rules yet for trait objects
+                        ty::List::empty()
+                    }
+
+                    ty::Adt(def, ..) => {
+                        self.infcx.tcx.program_clauses_for(def.did)
+                    }
+
+                    ty::Foreign(def_id) |
+                    ty::FnDef(def_id, ..) |
+                    ty::Closure(def_id, ..) |
+                    ty::Generator(def_id, ..) |
+                    ty::Opaque(def_id, ..) => {
+                        self.infcx.tcx.program_clauses_for(def_id)
+                    }
+
+                    ty::GeneratorWitness(..) |
+                    ty::UnnormalizedProjection(..) |
+                    ty::Infer(..) |
+                    ty::Bound(..) |
+                    ty::Param(..) |
+                    ty::Error => {
+                        bug!("unexpected type {:?}", ty)
+                    }
+                };
+
+                clauses.into_iter()
+                    .filter(|clause| clause.category() == ProgramClauseCategory::WellFormed)
+                    .cloned()
+                    .collect()
+            }
+
+            DomainGoal::FromEnv(FromEnv::Trait(..)) => {
+                // These come from:
+                // * implied bounds from trait definitions (rule `Implied-Bound-From-Trait`)
+                // * implied bounds from type definitions (rule `Implied-Bound-From-Type`)
+                // * implied bounds from assoc type defs (rules `Implied-Trait-From-AssocTy`,
+                //   `Implied-Bound-From-AssocTy` and `Implied-WC-From-AssocTy`)
+
+                // All of these rules are computed in the environment.
+                vec![]
+            }
+
+            DomainGoal::FromEnv(FromEnv::Ty(..)) => {
+                // There are no `FromEnv::Ty(..) :- ...` rules (this predicate only
+                // comes from the environment).
+                vec![]
+            }
+
+            DomainGoal::Normalize(projection_predicate) => {
+                // These come from -- assoc ty values (rule `Normalize-From-Impl`).
+                let mut clauses = vec![];
+
+                assemble_clauses_from_assoc_ty_values(
+                    self.infcx.tcx,
+                    projection_predicate.projection_ty.trait_ref(self.infcx.tcx).def_id,
+                    &mut clauses
+                );
+
+                clauses
+            }
+        };
+
+        let environment = self.infcx.tcx.lift_to_global(environment)
+            .expect("environment is not global");
+        clauses.extend(
+            self.infcx.tcx.program_clauses_for_env(environment)
+                .into_iter()
+                .cloned()
+        );
+        clauses
+    }
+}
diff --git a/src/librustc_traits/lib.rs b/src/librustc_traits/lib.rs
index 733804fb9b052..4a3806d6cb680 100644
--- a/src/librustc_traits/lib.rs
+++ b/src/librustc_traits/lib.rs
@@ -23,6 +23,7 @@ extern crate log;
 #[macro_use]
 extern crate rustc;
 extern crate rustc_data_structures;
+extern crate rustc_target;
 extern crate syntax;
 extern crate syntax_pos;
 extern crate smallvec;
diff --git a/src/librustc_traits/lowering/environment.rs b/src/librustc_traits/lowering/environment.rs
index 052ca37b31371..54f0c6e8da78a 100644
--- a/src/librustc_traits/lowering/environment.rs
+++ b/src/librustc_traits/lowering/environment.rs
@@ -20,6 +20,8 @@ use rustc::traits::{
 use rustc::ty::{self, TyCtxt, Ty};
 use rustc::hir::def_id::DefId;
 use rustc_data_structures::fx::FxHashSet;
+use super::Lower;
+use std::iter;
 
 struct ClauseVisitor<'set, 'a, 'tcx: 'a + 'set> {
     tcx: TyCtxt<'a, 'tcx, 'tcx>,
@@ -45,9 +47,32 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
                 );
             }
 
-            // forall<'a, T> { `Outlives(T, 'a) :- FromEnv(&'a T)` }
-            ty::Ref(_region, _sub_ty, ..) => {
-                // FIXME: we'd need bound tys in order to properly write the above rule
+            // forall<'a, T> { `Outlives(T: 'a) :- FromEnv(&'a T)` }
+            ty::Ref(..) => {
+                use rustc::hir;
+
+                let region = self.tcx.mk_region(
+                    ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
+                );
+                let ty = self.tcx.mk_ty(
+                    ty::Bound(ty::BoundTy::new(ty::INNERMOST, ty::BoundVar::from_u32(1)))
+                );
+
+                let ref_ty = self.tcx.mk_ref(region, ty::TypeAndMut {
+                    ty,
+                    mutbl: hir::Mutability::MutImmutable,
+                });
+                let from_env = DomainGoal::FromEnv(FromEnv::Ty(ref_ty));
+
+                let clause = ProgramClause {
+                    goal: ty::OutlivesPredicate(ty, region).lower(),
+                    hypotheses: self.tcx.mk_goals(
+                        iter::once(self.tcx.mk_goal(from_env.into_goal()))
+                    ),
+                    category: ProgramClauseCategory::ImpliedBound,
+                };
+                let clause = Clause::ForAll(ty::Binder::bind(clause));
+                self.round.insert(clause);
             }
 
             ty::Dynamic(..) => {
@@ -88,12 +113,12 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
             ty::FnPtr(..) |
             ty::Tuple(..) |
             ty::Never |
-            ty::Param(..) => (),
+            ty::Infer(..) |
+            ty::Bound(..) => (),
 
             ty::GeneratorWitness(..) |
             ty::UnnormalizedProjection(..) |
-            ty::Infer(..) |
-            ty::Bound(..) |
+            ty::Param(..) |
             ty::Error => {
                 bug!("unexpected type {:?}", ty);
             }
@@ -173,21 +198,28 @@ crate fn program_clauses_for_env<'a, 'tcx>(
     );
 }
 
-crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Environment<'tcx> {
+crate fn environment<'a, 'tcx>(
+    tcx: TyCtxt<'a, 'tcx, 'tcx>,
+    def_id: DefId
+) -> ty::Binder<Environment<'tcx>> {
     use super::{Lower, IntoFromEnvGoal};
     use rustc::hir::{Node, TraitItemKind, ImplItemKind, ItemKind, ForeignItemKind};
+    use rustc::ty::subst::{Subst, Substs};
 
     // The environment of an impl Trait type is its defining function's environment.
     if let Some(parent) = ty::is_impl_trait_defn(tcx, def_id) {
         return environment(tcx, parent);
     }
 
+    let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
+
     // Compute the bounds on `Self` and the type parameters.
-    let ty::InstantiatedPredicates { predicates } =
-        tcx.predicates_of(def_id).instantiate_identity(tcx);
+    let ty::InstantiatedPredicates { predicates } = tcx.predicates_of(def_id)
+        .instantiate_identity(tcx);
 
     let clauses = predicates.into_iter()
         .map(|predicate| predicate.lower())
+        .map(|predicate| predicate.subst(tcx, bound_vars))
         .map(|domain_goal| domain_goal.map_bound(|bound| bound.into_from_env_goal()))
         .map(|domain_goal| domain_goal.map_bound(|bound| bound.into_program_clause()))
 
@@ -228,33 +260,43 @@ crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> En
 
     let mut input_tys = FxHashSet::default();
 
-    // In an impl, we assume that the receiver type and all its constituents
+    // In an impl, we assume that the header trait ref and all its constituents
     // are well-formed.
     if is_impl {
-        let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
-        input_tys.extend(trait_ref.self_ty().walk());
+        let trait_ref = tcx.impl_trait_ref(def_id)
+            .expect("not an impl")
+            .subst(tcx, bound_vars);
+
+        input_tys.extend(
+            trait_ref.substs.types().flat_map(|ty| ty.walk())
+        );
     }
 
     // In an fn, we assume that the arguments and all their constituents are
     // well-formed.
     if is_fn {
-        let fn_sig = tcx.fn_sig(def_id);
+        // `skip_binder` because we move region parameters to the root binder,
+        // restored in the return type of this query
+        let fn_sig = tcx.fn_sig(def_id).skip_binder().subst(tcx, bound_vars);
+
         input_tys.extend(
-            // FIXME: `skip_binder` seems ok for now? In a real setting,
-            // the late bound regions would next be instantiated with things
-            // in the inference table.
-            fn_sig.skip_binder().inputs().iter().flat_map(|ty| ty.walk())
+            fn_sig.inputs().iter().flat_map(|ty| ty.walk())
         );
     }
 
     let clauses = clauses.chain(
         input_tys.into_iter()
+            // Filter out type parameters
+            .filter(|ty| match ty.sty {
+                ty::Bound(..) => false,
+                _ => true,
+            })
             .map(|ty| DomainGoal::FromEnv(FromEnv::Ty(ty)))
             .map(|domain_goal| domain_goal.into_program_clause())
             .map(Clause::Implies)
     );
 
-    Environment {
+    ty::Binder::bind(Environment {
         clauses: tcx.mk_clauses(clauses),
-    }
+    })
 }
diff --git a/src/librustc_traits/lowering/mod.rs b/src/librustc_traits/lowering/mod.rs
index 46581397aee2d..471c0e7abbca6 100644
--- a/src/librustc_traits/lowering/mod.rs
+++ b/src/librustc_traits/lowering/mod.rs
@@ -28,6 +28,7 @@ use rustc::traits::{
 };
 use rustc::ty::query::Providers;
 use rustc::ty::{self, List, TyCtxt};
+use rustc::ty::subst::{Subst, Substs};
 use syntax::ast;
 
 use std::iter;
@@ -112,13 +113,14 @@ impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
             Predicate::RegionOutlives(predicate) => predicate.lower(),
             Predicate::TypeOutlives(predicate) => predicate.lower(),
             Predicate::Projection(predicate) => predicate.lower(),
-            Predicate::WellFormed(ty) => {
-                ty::Binder::dummy(DomainGoal::WellFormed(WellFormed::Ty(*ty)))
+
+            Predicate::WellFormed(..) |
+            Predicate::ObjectSafe(..) |
+            Predicate::ClosureKind(..) |
+            Predicate::Subtype(..) |
+            Predicate::ConstEvaluatable(..) => {
+                bug!("unexpected predicate {}", self)
             }
-            Predicate::ObjectSafe(..)
-            | Predicate::ClosureKind(..)
-            | Predicate::Subtype(..)
-            | Predicate::ConstEvaluatable(..) => unimplemented!(),
         }
     }
 }
@@ -189,9 +191,14 @@ fn program_clauses_for_trait<'a, 'tcx>(
     // }
     // ```
 
+    let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
+
     // `Self: Trait<P1..Pn>`
     let trait_pred = ty::TraitPredicate {
-        trait_ref: ty::TraitRef::identity(tcx, def_id),
+        trait_ref: ty::TraitRef {
+            def_id,
+            substs: bound_vars,
+        },
     };
 
     // `Implemented(Self: Trait<P1..Pn>)`
@@ -208,11 +215,12 @@ fn program_clauses_for_trait<'a, 'tcx>(
         category: ProgramClauseCategory::ImpliedBound,
     };
 
-    let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
+    let implemented_from_env = Clause::ForAll(ty::Binder::bind(implemented_from_env));
 
     let where_clauses = &tcx.predicates_defined_on(def_id).predicates
         .into_iter()
         .map(|(wc, _)| wc.lower())
+        .map(|wc| wc.subst(tcx, bound_vars))
         .collect::<Vec<_>>();
 
     // Rule Implied-Bound-From-Trait
@@ -230,11 +238,22 @@ fn program_clauses_for_trait<'a, 'tcx>(
         .cloned()
 
         // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
-        .map(|wc| wc.map_bound(|goal| ProgramClause {
-            goal: goal.into_from_env_goal(),
-            hypotheses,
-            category: ProgramClauseCategory::ImpliedBound,
-        }))
+        .map(|wc| {
+            // we move binders to the left
+            wc.map_bound(|goal| ProgramClause {
+                goal: goal.into_from_env_goal(),
+
+                // FIXME: As where clauses can only bind lifetimes for now,
+                // and that named bound regions have a def-id, it is safe
+                // to just inject `hypotheses` (which contains named vars bound at index `0`)
+                // into this binding level. This may change if we ever allow where clauses
+                // to bind types (e.g. for GATs things), because bound types only use a `BoundVar`
+                // index (no def-id).
+                hypotheses,
+
+                category: ProgramClauseCategory::ImpliedBound,
+            })
+        })
         .map(Clause::ForAll);
 
     // Rule WellFormed-TraitRef
@@ -246,28 +265,27 @@ fn program_clauses_for_trait<'a, 'tcx>(
     // }
     // ```
 
-    // `Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
-    let wf_conditions = iter::once(ty::Binder::dummy(trait_pred.lower()))
-        .chain(
-            where_clauses
-                .into_iter()
-                .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()))
-        );
+    // `WellFormed(WC)`
+    let wf_conditions = where_clauses
+        .into_iter()
+        .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()));
 
     // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
     let wf_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
         hypotheses: tcx.mk_goals(
-            wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
+            iter::once(tcx.mk_goal(GoalKind::DomainGoal(impl_trait))).chain(
+                wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx)))
+            )
         ),
         category: ProgramClauseCategory::WellFormed,
     };
-    let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
 
     tcx.mk_clauses(
-        clauses
+        iter::once(implemented_from_env)
             .chain(implied_bound_clauses)
-            .chain(wf_clause)
+            .chain(iter::once(wf_clause))
     )
 }
 
@@ -286,7 +304,11 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
     // }
     // ```
 
-    let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
+    let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
+
+    let trait_ref = tcx.impl_trait_ref(def_id)
+        .expect("not an impl")
+        .subst(tcx, bound_vars);
 
     // `Implemented(A0: Trait<A1..An>)`
     let trait_pred = ty::TraitPredicate { trait_ref }.lower();
@@ -294,7 +316,8 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
     // `WC`
     let where_clauses = tcx.predicates_of(def_id).predicates
         .into_iter()
-        .map(|(wc, _)| wc.lower());
+        .map(|(wc, _)| wc.lower())
+        .map(|wc| wc.subst(tcx, bound_vars));
 
     // `Implemented(A0: Trait<A1..An>) :- WC`
     let clause = ProgramClause {
@@ -305,7 +328,7 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
         ),
         category: ProgramClauseCategory::Other,
     };
-    tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
+    tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::bind(clause))))
 }
 
 pub fn program_clauses_for_type_def<'a, 'tcx>(
@@ -322,17 +345,20 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
     // }
     // ```
 
+    let bound_vars = Substs::bound_vars_for_item(tcx, def_id);
+
     // `Ty<...>`
-    let ty = tcx.type_of(def_id);
+    let ty = tcx.type_of(def_id).subst(tcx, bound_vars);
 
     // `WC`
     let where_clauses = tcx.predicates_of(def_id).predicates
         .into_iter()
         .map(|(wc, _)| wc.lower())
+        .map(|wc| wc.subst(tcx, bound_vars))
         .collect::<Vec<_>>();
 
     // `WellFormed(Ty<...>) :- WC1, ..., WCm`
-    let well_formed = ProgramClause {
+    let well_formed_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
         hypotheses: tcx.mk_goals(
             where_clauses
@@ -342,10 +368,9 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
         ),
         category: ProgramClauseCategory::WellFormed,
     };
+    let well_formed_clause = Clause::ForAll(ty::Binder::bind(well_formed_clause));
 
-    let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
-
-    // Rule FromEnv-Type
+    // Rule Implied-Bound-From-Type
     //
     // For each where clause `WC`:
     // ```
@@ -363,22 +388,30 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
         .into_iter()
 
         // `FromEnv(WC) :- FromEnv(Ty<...>)`
-        .map(|wc| wc.map_bound(|goal| ProgramClause {
-            goal: goal.into_from_env_goal(),
-            hypotheses,
-            category: ProgramClauseCategory::ImpliedBound,
-        }))
+        .map(|wc| {
+            // move the binders to the left
+            wc.map_bound(|goal| ProgramClause {
+                goal: goal.into_from_env_goal(),
+
+                // FIXME: we inject `hypotheses` into this binding level,
+                // which may be incorrect in the future: see the FIXME in
+                // `program_clauses_for_trait`
+                hypotheses,
+
+                category: ProgramClauseCategory::ImpliedBound,
+            })
+        })
 
         .map(Clause::ForAll);
 
-    tcx.mk_clauses(well_formed_clause.chain(from_env_clauses))
+    tcx.mk_clauses(iter::once(well_formed_clause).chain(from_env_clauses))
 }
 
 pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
     tcx: TyCtxt<'a, 'tcx, 'tcx>,
     item_id: DefId,
 ) -> Clauses<'tcx> {
-    // Rule ProjectionEq-Skolemize
+    // Rule ProjectionEq-Placeholder
     //
     // ```
     // trait Trait<P1..Pn> {
@@ -403,7 +436,12 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
         ty::AssociatedItemContainer::TraitContainer(trait_id) => trait_id,
         _ => bug!("not an trait container"),
     };
-    let trait_ref = ty::TraitRef::identity(tcx, trait_id);
+
+    let trait_bound_vars = Substs::bound_vars_for_item(tcx, trait_id);
+    let trait_ref = ty::TraitRef {
+        def_id: trait_id,
+        substs: trait_bound_vars,
+    };
 
     let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
     let placeholder_ty = tcx.mk_ty(ty::UnnormalizedProjection(projection_ty));
@@ -417,6 +455,7 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
         hypotheses: ty::List::empty(),
         category: ProgramClauseCategory::Other,
     };
+    let projection_eq_clause = Clause::ForAll(ty::Binder::bind(projection_eq_clause));
 
     // Rule WellFormed-AssocTy
     // ```
@@ -430,11 +469,13 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
     let hypothesis = tcx.mk_goal(
         DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal()
     );
+
     let wf_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)),
         hypotheses: tcx.mk_goals(iter::once(hypothesis)),
         category: ProgramClauseCategory::WellFormed,
     };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
 
     // Rule Implied-Trait-From-AssocTy
     // ```
@@ -447,16 +488,17 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
     let hypothesis = tcx.mk_goal(
         DomainGoal::FromEnv(FromEnv::Ty(placeholder_ty)).into_goal()
     );
+
     let from_env_clause = ProgramClause {
         goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)),
         hypotheses: tcx.mk_goals(iter::once(hypothesis)),
         category: ProgramClauseCategory::ImpliedBound,
     };
+    let from_env_clause = Clause::ForAll(ty::Binder::bind(from_env_clause));
 
     let clauses = iter::once(projection_eq_clause)
         .chain(iter::once(wf_clause))
         .chain(iter::once(from_env_clause));
-    let clauses = clauses.map(|clause| Clause::ForAll(ty::Binder::dummy(clause)));
     tcx.mk_clauses(clauses)
 }
 
@@ -490,17 +532,18 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
         _ => bug!("not an impl container"),
     };
 
+    let impl_bound_vars = Substs::bound_vars_for_item(tcx, impl_id);
+
     // `A0 as Trait<A1..An>`
-    let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
+    let trait_ref = tcx.impl_trait_ref(impl_id)
+        .unwrap()
+        .subst(tcx, impl_bound_vars);
 
     // `T`
     let ty = tcx.type_of(item_id);
 
     // `Implemented(A0: Trait<A1..An>)`
-    let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower());
-
-    // `Implemented(A0: Trait<A1..An>)`
-    let hypotheses = vec![trait_implemented];
+    let trait_implemented: DomainGoal = ty::TraitPredicate { trait_ref }.lower();
 
     // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
     let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
@@ -509,16 +552,16 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
     let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
 
     // `Normalize(... -> T) :- ...`
-    let clause = ProgramClause {
+    let normalize_clause = ProgramClause {
         goal: normalize_goal,
         hypotheses: tcx.mk_goals(
-            hypotheses
-                .into_iter()
-                .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
+            iter::once(tcx.mk_goal(GoalKind::DomainGoal(trait_implemented)))
         ),
         category: ProgramClauseCategory::Other,
     };
-    tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
+    let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause));
+
+    tcx.mk_clauses(iter::once(normalize_clause))
 }
 
 pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
@@ -548,7 +591,7 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
 
             if attr.check_name("rustc_dump_env_program_clauses") {
                 let environment = self.tcx.environment(def_id);
-                clauses = Some(self.tcx.program_clauses_for_env(environment));
+                clauses = Some(self.tcx.program_clauses_for_env(*environment.skip_binder()));
             }
 
             if let Some(clauses) = clauses {
@@ -559,14 +602,7 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
 
                 let mut strings: Vec<_> = clauses
                     .iter()
-                    .map(|clause| {
-                        // Skip the top-level binder for a less verbose output
-                        let program_clause = match clause {
-                            Clause::Implies(program_clause) => program_clause,
-                            Clause::ForAll(program_clause) => program_clause.skip_binder(),
-                        };
-                        program_clause.to_string()
-                    })
+                    .map(|clause| clause.to_string())
                     .collect();
 
                 strings.sort();
diff --git a/src/librustc_typeck/check/callee.rs b/src/librustc_typeck/check/callee.rs
index de4293aaaeac7..411583b36b9e3 100644
--- a/src/librustc_typeck/check/callee.rs
+++ b/src/librustc_typeck/check/callee.rs
@@ -110,10 +110,11 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 // fnmut vs fnonce. If so, we have to defer further processing.
                 if self.closure_kind(def_id, substs).is_none() {
                     let closure_ty = self.closure_sig(def_id, substs);
-                    let fn_sig = self.replace_late_bound_regions_with_fresh_var(call_expr.span,
-                                                                   infer::FnCall,
-                                                                   &closure_ty)
-                        .0;
+                    let fn_sig = self.replace_bound_vars_with_fresh_vars(
+                        call_expr.span,
+                        infer::FnCall,
+                        &closure_ty
+                    ).0;
                     let adjustments = autoderef.adjust_steps(Needs::None);
                     self.record_deferred_call_resolution(def_id, DeferredCallResolution {
                         call_expr,
@@ -284,7 +285,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         // previously appeared within a `Binder<>` and hence would not
         // have been normalized before.
         let fn_sig =
-            self.replace_late_bound_regions_with_fresh_var(call_expr.span, infer::FnCall, &fn_sig)
+            self.replace_bound_vars_with_fresh_vars(call_expr.span, infer::FnCall, &fn_sig)
                 .0;
         let fn_sig = self.normalize_associated_types_in(call_expr.span, &fn_sig);
 
diff --git a/src/librustc_typeck/check/closure.rs b/src/librustc_typeck/check/closure.rs
index 010561d1001e5..10ac2448d007b 100644
--- a/src/librustc_typeck/check/closure.rs
+++ b/src/librustc_typeck/check/closure.rs
@@ -564,7 +564,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
             // `liberated_sig` is E'.
             {
                 // Instantiate (this part of..) S to S', i.e., with fresh variables.
-                let (supplied_ty, _) = self.infcx.replace_late_bound_regions_with_fresh_var(
+                let (supplied_ty, _) = self.infcx.replace_bound_vars_with_fresh_vars(
                     hir_ty.span,
                     LateBoundRegionConversionTime::FnCall,
                     &ty::Binder::bind(supplied_ty),
@@ -605,7 +605,7 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
                 );
             }
 
-            let (supplied_output_ty, _) = self.infcx.replace_late_bound_regions_with_fresh_var(
+            let (supplied_output_ty, _) = self.infcx.replace_bound_vars_with_fresh_vars(
                 decl.output.span(),
                 LateBoundRegionConversionTime::FnCall,
                 &supplied_sig.output(),
diff --git a/src/librustc_typeck/check/compare_method.rs b/src/librustc_typeck/check/compare_method.rs
index 45c5457c9e140..e30ebe07e5418 100644
--- a/src/librustc_typeck/check/compare_method.rs
+++ b/src/librustc_typeck/check/compare_method.rs
@@ -233,7 +233,7 @@ fn compare_predicate_entailment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
         let mut selcx = traits::SelectionContext::new(&infcx);
 
         let impl_m_own_bounds = impl_m_predicates.instantiate_own(tcx, impl_to_skol_substs);
-        let (impl_m_own_bounds, _) = infcx.replace_late_bound_regions_with_fresh_var(
+        let (impl_m_own_bounds, _) = infcx.replace_bound_vars_with_fresh_vars(
             impl_m_span,
             infer::HigherRankedType,
             &ty::Binder::bind(impl_m_own_bounds.predicates)
@@ -262,10 +262,11 @@ fn compare_predicate_entailment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>,
         // Compute placeholder form of impl and trait method tys.
         let tcx = infcx.tcx;
 
-        let (impl_sig, _) =
-            infcx.replace_late_bound_regions_with_fresh_var(impl_m_span,
-                                                            infer::HigherRankedType,
-                                                            &tcx.fn_sig(impl_m.def_id));
+        let (impl_sig, _) = infcx.replace_bound_vars_with_fresh_vars(
+            impl_m_span,
+            infer::HigherRankedType,
+            &tcx.fn_sig(impl_m.def_id)
+        );
         let impl_sig =
             inh.normalize_associated_types_in(impl_m_span,
                                               impl_m_node_id,
diff --git a/src/librustc_typeck/check/method/confirm.rs b/src/librustc_typeck/check/method/confirm.rs
index 75f5bf74c6aef..5144f3e41d4a9 100644
--- a/src/librustc_typeck/check/method/confirm.rs
+++ b/src/librustc_typeck/check/method/confirm.rs
@@ -245,7 +245,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
                     let original_poly_trait_ref = principal.with_self_ty(this.tcx, object_ty);
                     let upcast_poly_trait_ref = this.upcast(original_poly_trait_ref, trait_def_id);
                     let upcast_trait_ref =
-                        this.replace_late_bound_regions_with_fresh_var(&upcast_poly_trait_ref);
+                        this.replace_bound_vars_with_fresh_vars(&upcast_poly_trait_ref);
                     debug!("original_poly_trait_ref={:?} upcast_trait_ref={:?} target_trait={:?}",
                            original_poly_trait_ref,
                            upcast_trait_ref,
@@ -268,7 +268,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
             probe::WhereClausePick(ref poly_trait_ref) => {
                 // Where clauses can have bound regions in them. We need to instantiate
                 // those to convert from a poly-trait-ref to a trait-ref.
-                self.replace_late_bound_regions_with_fresh_var(&poly_trait_ref).substs
+                self.replace_bound_vars_with_fresh_vars(&poly_trait_ref).substs
             }
         }
     }
@@ -398,7 +398,7 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
         // NB: Instantiate late-bound regions first so that
         // `instantiate_type_scheme` can normalize associated types that
         // may reference those regions.
-        let method_sig = self.replace_late_bound_regions_with_fresh_var(&sig);
+        let method_sig = self.replace_bound_vars_with_fresh_vars(&sig);
         debug!("late-bound lifetimes from method instantiated, method_sig={:?}",
                method_sig);
 
@@ -633,11 +633,9 @@ impl<'a, 'gcx, 'tcx> ConfirmContext<'a, 'gcx, 'tcx> {
         upcast_trait_refs.into_iter().next().unwrap()
     }
 
-    fn replace_late_bound_regions_with_fresh_var<T>(&self, value: &ty::Binder<T>) -> T
+    fn replace_bound_vars_with_fresh_vars<T>(&self, value: &ty::Binder<T>) -> T
         where T: TypeFoldable<'tcx>
     {
-        self.fcx
-            .replace_late_bound_regions_with_fresh_var(self.span, infer::FnCall, value)
-            .0
+        self.fcx.replace_bound_vars_with_fresh_vars(self.span, infer::FnCall, value).0
     }
 }
diff --git a/src/librustc_typeck/check/method/mod.rs b/src/librustc_typeck/check/method/mod.rs
index 637f3eaae9a6a..ac338ba667865 100644
--- a/src/librustc_typeck/check/method/mod.rs
+++ b/src/librustc_typeck/check/method/mod.rs
@@ -311,9 +311,11 @@ impl<'a, 'gcx, 'tcx> FnCtxt<'a, 'gcx, 'tcx> {
         // `instantiate_type_scheme` can normalize associated types that
         // may reference those regions.
         let fn_sig = tcx.fn_sig(def_id);
-        let fn_sig = self.replace_late_bound_regions_with_fresh_var(span,
-                                                                    infer::FnCall,
-                                                                    &fn_sig).0;
+        let fn_sig = self.replace_bound_vars_with_fresh_vars(
+            span,
+            infer::FnCall,
+            &fn_sig
+        ).0;
         let fn_sig = fn_sig.subst(self.tcx, substs);
         let fn_sig = match self.normalize_associated_types_in_as_infer_ok(span, &fn_sig) {
             InferOk { value, obligations: o } => {
diff --git a/src/librustc_typeck/check/method/probe.rs b/src/librustc_typeck/check/method/probe.rs
index 305efd0d75af6..4c06cae1d0752 100644
--- a/src/librustc_typeck/check/method/probe.rs
+++ b/src/librustc_typeck/check/method/probe.rs
@@ -755,8 +755,11 @@ impl<'a, 'gcx, 'tcx> ProbeContext<'a, 'gcx, 'tcx> {
                 self.probe(|_| {
                     let substs = self.fresh_substs_for_item(self.span, method.def_id);
                     let fty = fty.subst(self.tcx, substs);
-                    let (fty, _) = self.replace_late_bound_regions_with_fresh_var(
-                        self.span, infer::FnCall, &fty);
+                    let (fty, _) = self.replace_bound_vars_with_fresh_vars(
+                        self.span,
+                        infer::FnCall,
+                        &fty
+                    );
 
                     if let Some(self_ty) = self_ty {
                         if self.at(&ObligationCause::dummy(), self.param_env)
diff --git a/src/librustc_typeck/check/mod.rs b/src/librustc_typeck/check/mod.rs
index 2e6797ef23ad2..41e0c6c0a1972 100644
--- a/src/librustc_typeck/check/mod.rs
+++ b/src/librustc_typeck/check/mod.rs
@@ -1921,11 +1921,11 @@ impl<'a, 'gcx, 'tcx> AstConv<'gcx, 'tcx> for FnCtxt<'a, 'gcx, 'tcx> {
                                         poly_trait_ref: ty::PolyTraitRef<'tcx>)
                                         -> Ty<'tcx>
     {
-        let (trait_ref, _) =
-            self.replace_late_bound_regions_with_fresh_var(
-                span,
-                infer::LateBoundRegionConversionTime::AssocTypeProjection(item_def_id),
-                &poly_trait_ref);
+        let (trait_ref, _) = self.replace_bound_vars_with_fresh_vars(
+            span,
+            infer::LateBoundRegionConversionTime::AssocTypeProjection(item_def_id),
+            &poly_trait_ref
+        );
 
         self.tcx().mk_projection(item_def_id, trait_ref.substs)
     }
diff --git a/src/librustc_typeck/collect.rs b/src/librustc_typeck/collect.rs
index 70af837076f1a..d2dc226aca250 100644
--- a/src/librustc_typeck/collect.rs
+++ b/src/librustc_typeck/collect.rs
@@ -1857,8 +1857,9 @@ fn explicit_predicates_of<'a, 'tcx>(
             &hir::WherePredicate::BoundPredicate(ref bound_pred) => {
                 let ty = icx.to_ty(&bound_pred.bounded_ty);
 
-                // Keep the type around in a WF predicate, in case of no bounds.
-                // That way, `where Ty:` is not a complete noop (see #53696).
+                // Keep the type around in a dummy predicate, in case of no bounds.
+                // That way, `where Ty:` is not a complete noop (see #53696) and `Ty`
+                // is still checked for WF.
                 if bound_pred.bounds.is_empty() {
                     if let ty::Param(_) = ty.sty {
                         // This is a `where T:`, which can be in the HIR from the
@@ -1869,7 +1870,10 @@ fn explicit_predicates_of<'a, 'tcx>(
                         // compiler/tooling bugs from not handling WF predicates.
                     } else {
                         let span = bound_pred.bounded_ty.span;
-                        predicates.push((ty::Predicate::WellFormed(ty), span));
+                        let predicate = ty::OutlivesPredicate(ty, tcx.mk_region(ty::ReEmpty));
+                        predicates.push(
+                            (ty::Predicate::TypeOutlives(ty::Binder::dummy(predicate)), span)
+                        );
                     }
                 }
 
diff --git a/src/librustdoc/clean/mod.rs b/src/librustdoc/clean/mod.rs
index f514cb83a1fed..77782c19b7252 100644
--- a/src/librustdoc/clean/mod.rs
+++ b/src/librustdoc/clean/mod.rs
@@ -1325,15 +1325,10 @@ impl<'a> Clean<WherePredicate> for ty::Predicate<'a> {
             Predicate::RegionOutlives(ref pred) => pred.clean(cx),
             Predicate::TypeOutlives(ref pred) => pred.clean(cx),
             Predicate::Projection(ref pred) => pred.clean(cx),
-            Predicate::WellFormed(ty) => {
-                // This comes from `where Ty:` (i.e. no bounds) (see #53696).
-                WherePredicate::BoundPredicate {
-                    ty: ty.clean(cx),
-                    bounds: vec![],
-                }
-            }
-            Predicate::ObjectSafe(_) => panic!("not user writable"),
-            Predicate::ClosureKind(..) => panic!("not user writable"),
+
+            Predicate::WellFormed(..) |
+            Predicate::ObjectSafe(..) |
+            Predicate::ClosureKind(..) |
             Predicate::ConstEvaluatable(..) => panic!("not user writable"),
         }
     }
diff --git a/src/test/ui/chalkify/lower_env1.rs b/src/test/ui/chalkify/lower_env1.rs
index fc20ad0e08b2a..b772db5ca5523 100644
--- a/src/test/ui/chalkify/lower_env1.rs
+++ b/src/test/ui/chalkify/lower_env1.rs
@@ -17,7 +17,7 @@ trait Foo { }
 trait Bar where Self: Foo { }
 
 #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
-fn bar<T: Bar>() {
+fn bar<T: Bar + ?Sized>() {
 }
 
 fn main() {
diff --git a/src/test/ui/chalkify/lower_env1.stderr b/src/test/ui/chalkify/lower_env1.stderr
index 3aa04cfeb67d4..4aa40bae31932 100644
--- a/src/test/ui/chalkify/lower_env1.stderr
+++ b/src/test/ui/chalkify/lower_env1.stderr
@@ -4,9 +4,9 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(Self: Foo) :- FromEnv(Self: Bar).
-   = note: Implemented(Self: Bar) :- FromEnv(Self: Bar).
-   = note: WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Foo).
+   = note: forall<Self> { FromEnv(Self: Foo) :- FromEnv(Self: Bar). }
+   = note: forall<Self> { Implemented(Self: Bar) :- FromEnv(Self: Bar). }
+   = note: forall<Self> { WellFormed(Self: Bar) :- Implemented(Self: Bar), WellFormed(Self: Foo). }
 
 error: program clause dump
   --> $DIR/lower_env1.rs:19:1
@@ -14,10 +14,9 @@ error: program clause dump
 LL | #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(Self: Foo) :- FromEnv(Self: Bar).
-   = note: Implemented(Self: Bar) :- FromEnv(Self: Bar).
-   = note: Implemented(Self: Foo) :- FromEnv(Self: Foo).
-   = note: Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized).
+   = note: forall<Self> { FromEnv(Self: Foo) :- FromEnv(Self: Bar). }
+   = note: forall<Self> { Implemented(Self: Bar) :- FromEnv(Self: Bar). }
+   = note: forall<Self> { Implemented(Self: Foo) :- FromEnv(Self: Foo). }
 
 error: aborting due to 2 previous errors
 
diff --git a/src/test/ui/chalkify/lower_env2.rs b/src/test/ui/chalkify/lower_env2.rs
index 0b50dbfdf95c6..2328db5b4f687 100644
--- a/src/test/ui/chalkify/lower_env2.rs
+++ b/src/test/ui/chalkify/lower_env2.rs
@@ -14,12 +14,12 @@
 trait Foo { }
 
 #[rustc_dump_program_clauses] //~ ERROR program clause dump
-struct S<'a, T> where T: Foo {
+struct S<'a, T: ?Sized> where T: Foo {
     data: &'a T,
 }
 
 #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
-fn bar<'a, T: Foo>(x: S<T>) {
+fn bar<T: Foo>(_x: S<'_, T>) { // note that we have an implicit `T: Sized` bound
 }
 
 fn main() {
diff --git a/src/test/ui/chalkify/lower_env2.stderr b/src/test/ui/chalkify/lower_env2.stderr
index 3b88ac1f22bea..74833ef064f9d 100644
--- a/src/test/ui/chalkify/lower_env2.stderr
+++ b/src/test/ui/chalkify/lower_env2.stderr
@@ -4,10 +4,9 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(T: Foo) :- FromEnv(S<'a, T>).
-   = note: FromEnv(T: std::marker::Sized) :- FromEnv(S<'a, T>).
-   = note: TypeOutlives(T : 'a) :- FromEnv(S<'a, T>).
-   = note: WellFormed(S<'a, T>) :- Implemented(T: std::marker::Sized), Implemented(T: Foo), TypeOutlives(T : 'a).
+   = note: forall<'a, T> { FromEnv(T: Foo) :- FromEnv(S<'a, T>). }
+   = note: forall<'a, T> { TypeOutlives(T: 'a) :- FromEnv(S<'a, T>). }
+   = note: forall<'a, T> { WellFormed(S<'a, T>) :- Implemented(T: Foo), TypeOutlives(T: 'a). }
 
 error: program clause dump
   --> $DIR/lower_env2.rs:21:1
@@ -15,11 +14,10 @@ error: program clause dump
 LL | #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(T: Foo) :- FromEnv(S<'a, T>).
-   = note: FromEnv(T: std::marker::Sized) :- FromEnv(S<'a, T>).
-   = note: Implemented(Self: Foo) :- FromEnv(Self: Foo).
-   = note: Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized).
-   = note: TypeOutlives(T : 'a) :- FromEnv(S<'a, T>).
+   = note: forall<'a, T> { FromEnv(T: Foo) :- FromEnv(S<'a, T>). }
+   = note: forall<'a, T> { TypeOutlives(T: 'a) :- FromEnv(S<'a, T>). }
+   = note: forall<Self> { Implemented(Self: Foo) :- FromEnv(Self: Foo). }
+   = note: forall<Self> { Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized). }
 
 error: aborting due to 2 previous errors
 
diff --git a/src/test/ui/chalkify/lower_env3.stderr b/src/test/ui/chalkify/lower_env3.stderr
index ac0f8e34cd437..eef6405f8f805 100644
--- a/src/test/ui/chalkify/lower_env3.stderr
+++ b/src/test/ui/chalkify/lower_env3.stderr
@@ -4,7 +4,8 @@ error: program clause dump
 LL |     #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: Implemented(Self: Foo) :- FromEnv(Self: Foo).
+   = note: forall<'^0, ^1> { TypeOutlives(^1: '^0) :- FromEnv(&^1). }
+   = note: forall<Self> { Implemented(Self: Foo) :- FromEnv(Self: Foo). }
 
 error: program clause dump
   --> $DIR/lower_env3.rs:20:5
@@ -12,9 +13,10 @@ error: program clause dump
 LL |     #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(Self: std::marker::Sized) :- FromEnv(Self: std::clone::Clone).
-   = note: Implemented(Self: std::clone::Clone) :- FromEnv(Self: std::clone::Clone).
-   = note: Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized).
+   = note: forall<'^0, ^1> { TypeOutlives(^1: '^0) :- FromEnv(&^1). }
+   = note: forall<Self> { FromEnv(Self: std::marker::Sized) :- FromEnv(Self: std::clone::Clone). }
+   = note: forall<Self> { Implemented(Self: std::clone::Clone) :- FromEnv(Self: std::clone::Clone). }
+   = note: forall<Self> { Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized). }
 
 error: aborting due to 2 previous errors
 
diff --git a/src/test/ui/chalkify/lower_impl.stderr b/src/test/ui/chalkify/lower_impl.stderr
index c497d76f8d4f9..92a209f673d5c 100644
--- a/src/test/ui/chalkify/lower_impl.stderr
+++ b/src/test/ui/chalkify/lower_impl.stderr
@@ -4,7 +4,7 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: Implemented(T: Foo) :- ProjectionEq(<T as std::iter::Iterator>::Item == i32), TypeOutlives(T : 'static), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized).
+   = note: forall<T> { Implemented(T: Foo) :- ProjectionEq(<T as std::iter::Iterator>::Item == i32), TypeOutlives(T: 'static), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized). }
 
 error: program clause dump
   --> $DIR/lower_impl.rs:23:5
@@ -12,7 +12,7 @@ error: program clause dump
 LL |     #[rustc_dump_program_clauses] //~ ERROR program clause dump
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: Normalize(<T as Bar>::Assoc == std::vec::Vec<T>) :- Implemented(T: Bar).
+   = note: forall<T> { Normalize(<T as Bar>::Assoc -> std::vec::Vec<T>) :- Implemented(T: Bar). }
 
 error: aborting due to 2 previous errors
 
diff --git a/src/test/ui/chalkify/lower_struct.rs b/src/test/ui/chalkify/lower_struct.rs
index 9287555a05684..9b4bba67112ea 100644
--- a/src/test/ui/chalkify/lower_struct.rs
+++ b/src/test/ui/chalkify/lower_struct.rs
@@ -11,8 +11,8 @@
 #![feature(rustc_attrs)]
 
 #[rustc_dump_program_clauses] //~ ERROR program clause dump
-struct Foo<T> where Box<T>: Clone {
-    _x: std::marker::PhantomData<T>,
+struct Foo<'a, T> where Box<T>: Clone {
+    _x: std::marker::PhantomData<&'a T>,
 }
 
 fn main() { }
diff --git a/src/test/ui/chalkify/lower_struct.stderr b/src/test/ui/chalkify/lower_struct.stderr
index d6cc9c8e9a401..a0dd9369700af 100644
--- a/src/test/ui/chalkify/lower_struct.stderr
+++ b/src/test/ui/chalkify/lower_struct.stderr
@@ -4,9 +4,10 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(T: std::marker::Sized) :- FromEnv(Foo<T>).
-   = note: FromEnv(std::boxed::Box<T>: std::clone::Clone) :- FromEnv(Foo<T>).
-   = note: WellFormed(Foo<T>) :- Implemented(T: std::marker::Sized), Implemented(std::boxed::Box<T>: std::clone::Clone).
+   = note: forall<'a, T> { FromEnv(T: std::marker::Sized) :- FromEnv(Foo<'a, T>). }
+   = note: forall<'a, T> { FromEnv(std::boxed::Box<T>: std::clone::Clone) :- FromEnv(Foo<'a, T>). }
+   = note: forall<'a, T> { TypeOutlives(T: 'a) :- FromEnv(Foo<'a, T>). }
+   = note: forall<'a, T> { WellFormed(Foo<'a, T>) :- Implemented(T: std::marker::Sized), Implemented(std::boxed::Box<T>: std::clone::Clone), TypeOutlives(T: 'a). }
 
 error: aborting due to previous error
 
diff --git a/src/test/ui/chalkify/lower_trait.stderr b/src/test/ui/chalkify/lower_trait.stderr
index dc2375277e734..6a3f7aa63765f 100644
--- a/src/test/ui/chalkify/lower_trait.stderr
+++ b/src/test/ui/chalkify/lower_trait.stderr
@@ -4,10 +4,10 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(<Self as Foo<S, T>>::Assoc: Bar) :- FromEnv(Self: Foo<S, T>).
-   = note: FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<S, T>).
-   = note: Implemented(Self: Foo<S, T>) :- FromEnv(Self: Foo<S, T>).
-   = note: WellFormed(Self: Foo<S, T>) :- Implemented(Self: Foo<S, T>), WellFormed(S: std::marker::Sized), WellFormed(<Self as Foo<S, T>>::Assoc: Bar).
+   = note: forall<Self, S, T> { FromEnv(<Self as Foo<S, T>>::Assoc: Bar) :- FromEnv(Self: Foo<S, T>). }
+   = note: forall<Self, S, T> { FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<S, T>). }
+   = note: forall<Self, S, T> { Implemented(Self: Foo<S, T>) :- FromEnv(Self: Foo<S, T>). }
+   = note: forall<Self, S, T> { WellFormed(Self: Foo<S, T>) :- Implemented(Self: Foo<S, T>), WellFormed(S: std::marker::Sized), WellFormed(<Self as Foo<S, T>>::Assoc: Bar). }
 
 error: program clause dump
   --> $DIR/lower_trait.rs:17:5
@@ -15,9 +15,9 @@ error: program clause dump
 LL |     #[rustc_dump_program_clauses] //~ ERROR program clause dump
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(Self: Foo<S, T>) :- FromEnv(Unnormalized(<Self as Foo<S, T>>::Assoc)).
-   = note: ProjectionEq(<Self as Foo<S, T>>::Assoc == Unnormalized(<Self as Foo<S, T>>::Assoc)).
-   = note: WellFormed(Unnormalized(<Self as Foo<S, T>>::Assoc)) :- Implemented(Self: Foo<S, T>).
+   = note: forall<Self, S, T> { FromEnv(Self: Foo<S, T>) :- FromEnv(Unnormalized(<Self as Foo<S, T>>::Assoc)). }
+   = note: forall<Self, S, T> { ProjectionEq(<Self as Foo<S, T>>::Assoc == Unnormalized(<Self as Foo<S, T>>::Assoc)). }
+   = note: forall<Self, S, T> { WellFormed(Unnormalized(<Self as Foo<S, T>>::Assoc)) :- Implemented(Self: Foo<S, T>). }
 
 error: aborting due to 2 previous errors
 
diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.rs b/src/test/ui/chalkify/lower_trait_higher_rank.rs
index 7fc48cfd56ddc..c0e1d8fc4c828 100644
--- a/src/test/ui/chalkify/lower_trait_higher_rank.rs
+++ b/src/test/ui/chalkify/lower_trait_higher_rank.rs
@@ -11,9 +11,8 @@
 #![feature(rustc_attrs)]
 
 #[rustc_dump_program_clauses] //~ ERROR program clause dump
-trait Foo<F> where for<'a> F: Fn(&'a (u8, u16)) -> &'a u8
+trait Foo<F: ?Sized> where for<'a> F: Fn(&'a (u8, u16)) -> &'a u8
 {
-    fn s(_: F) -> F;
 }
 
 fn main() {
diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.stderr b/src/test/ui/chalkify/lower_trait_higher_rank.stderr
index afb2cd4b56332..6d3e0ec55b276 100644
--- a/src/test/ui/chalkify/lower_trait_higher_rank.stderr
+++ b/src/test/ui/chalkify/lower_trait_higher_rank.stderr
@@ -4,11 +4,10 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(F: std::marker::Sized) :- FromEnv(Self: Foo<F>).
-   = note: FromEnv(F: std::ops::Fn<(&'a (u8, u16),)>) :- FromEnv(Self: Foo<F>).
-   = note: Implemented(Self: Foo<F>) :- FromEnv(Self: Foo<F>).
-   = note: ProjectionEq(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) :- FromEnv(Self: Foo<F>).
-   = note: WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), WellFormed(F: std::marker::Sized), forall<> { WellFormed(F: std::ops::Fn<(&'a (u8, u16),)>) }, forall<> { ProjectionEq(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) }.
+   = note: forall<'a, Self, F> { FromEnv(F: std::ops::Fn<(&'a (u8, u16),)>) :- FromEnv(Self: Foo<F>). }
+   = note: forall<'a, Self, F> { ProjectionEq(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) :- FromEnv(Self: Foo<F>). }
+   = note: forall<Self, F> { Implemented(Self: Foo<F>) :- FromEnv(Self: Foo<F>). }
+   = note: forall<Self, F> { WellFormed(Self: Foo<F>) :- Implemented(Self: Foo<F>), forall<'a> { WellFormed(F: std::ops::Fn<(&'a (u8, u16),)>) }, forall<'a> { ProjectionEq(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) }. }
 
 error: aborting due to previous error
 
diff --git a/src/test/ui/chalkify/lower_trait_where_clause.rs b/src/test/ui/chalkify/lower_trait_where_clause.rs
index 5305591b84345..ac58c0bf2fe37 100644
--- a/src/test/ui/chalkify/lower_trait_where_clause.rs
+++ b/src/test/ui/chalkify/lower_trait_where_clause.rs
@@ -10,22 +10,16 @@
 
 #![feature(rustc_attrs)]
 
-use std::fmt::{Debug, Display};
 use std::borrow::Borrow;
 
 #[rustc_dump_program_clauses] //~ ERROR program clause dump
-trait Foo<'a, 'b, S, T, U>
+trait Foo<'a, 'b, T, U>
 where
-    S: Debug,
-    T: Borrow<U>,
-    U: ?Sized,
+    T: Borrow<U> + ?Sized,
+    U: ?Sized + 'b,
     'a: 'b,
-    U: 'b,
-    Vec<T>:, // NOTE(#53696) this checks an empty list of bounds.
+    Box<T>:, // NOTE(#53696) this checks an empty list of bounds.
 {
-    fn s(_: S) -> S;
-    fn t(_: T) -> T;
-    fn u(_: U) -> U;
 }
 
 fn main() {
diff --git a/src/test/ui/chalkify/lower_trait_where_clause.stderr b/src/test/ui/chalkify/lower_trait_where_clause.stderr
index ad3546da1a25b..fcd516c89ba33 100644
--- a/src/test/ui/chalkify/lower_trait_where_clause.stderr
+++ b/src/test/ui/chalkify/lower_trait_where_clause.stderr
@@ -1,18 +1,15 @@
 error: program clause dump
-  --> $DIR/lower_trait_where_clause.rs:16:1
+  --> $DIR/lower_trait_where_clause.rs:15:1
    |
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(S: std::fmt::Debug) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: FromEnv(T: std::borrow::Borrow<U>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: FromEnv(T: std::marker::Sized) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: Implemented(Self: Foo<'a, 'b, S, T, U>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: RegionOutlives('a : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: TypeOutlives(U : 'b) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
-   = note: WellFormed(Self: Foo<'a, 'b, S, T, U>) :- Implemented(Self: Foo<'a, 'b, S, T, U>), WellFormed(S: std::marker::Sized), WellFormed(T: std::marker::Sized), WellFormed(S: std::fmt::Debug), WellFormed(T: std::borrow::Borrow<U>), RegionOutlives('a : 'b), TypeOutlives(U : 'b), WellFormed(std::vec::Vec<T>).
-   = note: WellFormed(std::vec::Vec<T>) :- FromEnv(Self: Foo<'a, 'b, S, T, U>).
+   = note: forall<'a, 'b, Self, T, U> { FromEnv(T: std::borrow::Borrow<U>) :- FromEnv(Self: Foo<'a, 'b, T, U>). }
+   = note: forall<'a, 'b, Self, T, U> { Implemented(Self: Foo<'a, 'b, T, U>) :- FromEnv(Self: Foo<'a, 'b, T, U>). }
+   = note: forall<'a, 'b, Self, T, U> { RegionOutlives('a: 'b) :- FromEnv(Self: Foo<'a, 'b, T, U>). }
+   = note: forall<'a, 'b, Self, T, U> { TypeOutlives(U: 'b) :- FromEnv(Self: Foo<'a, 'b, T, U>). }
+   = note: forall<'a, 'b, Self, T, U> { TypeOutlives(std::boxed::Box<T>: '<empty>) :- FromEnv(Self: Foo<'a, 'b, T, U>). }
+   = note: forall<'a, 'b, Self, T, U> { WellFormed(Self: Foo<'a, 'b, T, U>) :- Implemented(Self: Foo<'a, 'b, T, U>), WellFormed(T: std::borrow::Borrow<U>), TypeOutlives(U: 'b), RegionOutlives('a: 'b), TypeOutlives(std::boxed::Box<T>: '<empty>). }
 
 error: aborting due to previous error
 
diff --git a/src/test/ui/nll/user-annotations/dump-fn-method.rs b/src/test/ui/nll/user-annotations/dump-fn-method.rs
index 7f726d13a33ed..ef5fb8eadc355 100644
--- a/src/test/ui/nll/user-annotations/dump-fn-method.rs
+++ b/src/test/ui/nll/user-annotations/dump-fn-method.rs
@@ -39,7 +39,7 @@ fn main() {
     // Here: we only want the `T` to be given, the rest should be variables.
     //
     // (`T` refers to the declaration of `Bazoom`)
-    let x = <_ as Bazoom<u32>>::method::<_>; //~ ERROR [?0, u32, ?1]
+    let x = <_ as Bazoom<u32>>::method::<_>; //~ ERROR [^0, u32, ^1]
     x(&22, 44, 66);
 
     // Here: all are given
@@ -51,7 +51,7 @@ fn main() {
     //
     // (`U` refers to the declaration of `Bazoom`)
     let y = 22_u32;
-    y.method::<u32>(44, 66); //~ ERROR [?0, ?1, u32]
+    y.method::<u32>(44, 66); //~ ERROR [^0, ^1, u32]
 
     // Here: nothing is given, so we don't have any annotation.
     let y = 22_u32;
diff --git a/src/test/ui/nll/user-annotations/dump-fn-method.stderr b/src/test/ui/nll/user-annotations/dump-fn-method.stderr
index 3beb994a4e8a5..359423d0cfbea 100644
--- a/src/test/ui/nll/user-annotations/dump-fn-method.stderr
+++ b/src/test/ui/nll/user-annotations/dump-fn-method.stderr
@@ -4,10 +4,10 @@ error: user substs: Canonical { max_universe: U0, variables: [], value: UserSubs
 LL |     let x = foo::<u32>; //~ ERROR [u32]
    |             ^^^^^^^^^^
 
-error: user substs: Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Ty(General) }, CanonicalVarInfo { kind: Ty(General) }], value: UserSubsts { substs: [?0, u32, ?1], user_self_ty: None } }
+error: user substs: Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Ty(General) }, CanonicalVarInfo { kind: Ty(General) }], value: UserSubsts { substs: [^0, u32, ^1], user_self_ty: None } }
   --> $DIR/dump-fn-method.rs:42:13
    |
-LL |     let x = <_ as Bazoom<u32>>::method::<_>; //~ ERROR [?0, u32, ?1]
+LL |     let x = <_ as Bazoom<u32>>::method::<_>; //~ ERROR [^0, u32, ^1]
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 error: user substs: Canonical { max_universe: U0, variables: [], value: UserSubsts { substs: [u8, u16, u32], user_self_ty: None } }
@@ -16,10 +16,10 @@ error: user substs: Canonical { max_universe: U0, variables: [], value: UserSubs
 LL |     let x = <u8 as Bazoom<u16>>::method::<u32>; //~ ERROR [u8, u16, u32]
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-error: user substs: Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Ty(General) }, CanonicalVarInfo { kind: Ty(General) }], value: UserSubsts { substs: [?0, ?1, u32], user_self_ty: None } }
+error: user substs: Canonical { max_universe: U0, variables: [CanonicalVarInfo { kind: Ty(General) }, CanonicalVarInfo { kind: Ty(General) }], value: UserSubsts { substs: [^0, ^1, u32], user_self_ty: None } }
   --> $DIR/dump-fn-method.rs:54:5
    |
-LL |     y.method::<u32>(44, 66); //~ ERROR [?0, ?1, u32]
+LL |     y.method::<u32>(44, 66); //~ ERROR [^0, ^1, u32]
    |     ^^^^^^^^^^^^^^^^^^^^^^^
 
 error: aborting due to 4 previous errors