Auto merge of #58305 - scalexm:chalk-continued, r=nikomatsakis

(WIP) Small fixes in chalkification

Small fixes around region constraints and builtin impls. There are still some type inference errors, for example the following code errors out:
```rust
fn main() {
    let mut x: Vec<i32> = Vec::new();
    //                    ^^^^^^^^ cannot infer type for `std::vec::Vec<_>`
}
```
but explicitly specifying `Vec::<i32>::new` works.

With these few fixes, the following code now passes type-checking:
```rust
fn main() {
    let mut x: Vec<i32> = Vec::<i32>::new();
    x.push(5);
    println!("{:?}", x);
}
```

I also fixed the implied bounds bug as discussed on Zulip and in https://github.com/rust-lang-nursery/chalk/pull/206

cc @tmandry
r? @nikomatsakis

13 files changed, 946 insertions, 696 deletions

diff --git a/src/librustc/infer/nll_relate/mod.rs b/src/librustc/infer/nll_relate/mod.rs
index 7140af36acb..d8e7328c274 100644
--- a/src/librustc/infer/nll_relate/mod.rs
+++ b/src/librustc/infer/nll_relate/mod.rs
@@ -22,13 +22,14 @@
 //!   constituents)
 
 use crate::infer::InferCtxt;
+use crate::traits::DomainGoal;
+use crate::ty::error::TypeError;
 use crate::ty::fold::{TypeFoldable, TypeVisitor};
 use crate::ty::relate::{self, Relate, RelateResult, TypeRelation};
 use crate::ty::subst::Kind;
 use crate::ty::{self, Ty, TyCtxt};
-use crate::ty::error::TypeError;
-use crate::traits::DomainGoal;
 use rustc_data_structures::fx::FxHashMap;
+use std::fmt::Debug;
 
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
 pub enum NormalizationStrategy {
@@ -239,6 +240,7 @@ where
         first_free_index: ty::DebruijnIndex,
         scopes: &[BoundRegionScope<'tcx>],
     ) -> ty::Region<'tcx> {
+        debug!("replace_bound_regions(scopes={:?})", scopes);
         if let ty::ReLateBound(debruijn, br) = r {
             Self::lookup_bound_region(*debruijn, br, first_free_index, scopes)
         } else {
@@ -265,7 +267,7 @@ where
     fn relate_projection_ty(
         &mut self,
         projection_ty: ty::ProjectionTy<'tcx>,
-        value_ty: ty::Ty<'tcx>
+        value_ty: ty::Ty<'tcx>,
     ) -> Ty<'tcx> {
         use crate::infer::type_variable::TypeVariableOrigin;
         use crate::traits::WhereClause;
@@ -273,7 +275,9 @@ where
 
         match value_ty.sty {
             ty::Projection(other_projection_ty) => {
-                let var = self.infcx.next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
+                let var = self
+                    .infcx
+                    .next_ty_var(TypeVariableOrigin::MiscVariable(DUMMY_SP));
                 self.relate_projection_ty(projection_ty, var);
                 self.relate_projection_ty(other_projection_ty, var);
                 var
@@ -284,32 +288,55 @@ where
                     projection_ty,
                     ty: value_ty,
                 };
-                self.delegate.push_domain_goal(
-                    DomainGoal::Holds(WhereClause::ProjectionEq(projection))
-                );
+                self.delegate
+                    .push_domain_goal(DomainGoal::Holds(WhereClause::ProjectionEq(projection)));
                 value_ty
             }
         }
     }
 
-    /// Relate a type inference variable with a value type.
-    fn relate_ty_var(
+    /// Relate a type inference variable with a value type. This works
+    /// by creating a "generalization" G of the value where all the
+    /// lifetimes are replaced with fresh inference values. This
+    /// genearlization G becomes the value of the inference variable,
+    /// and is then related in turn to the value. So e.g. if you had
+    /// `vid = ?0` and `value = &'a u32`, we might first instantiate
+    /// `?0` to a type like `&'0 u32` where `'0` is a fresh variable,
+    /// and then relate `&'0 u32` with `&'a u32` (resulting in
+    /// relations between `'0` and `'a`).
+    ///
+    /// The variable `pair` can be either a `(vid, ty)` or `(ty, vid)`
+    /// -- in other words, it is always a (unresolved) inference
+    /// variable `vid` and a type `ty` that are being related, but the
+    /// vid may appear either as the "a" type or the "b" type,
+    /// depending on where it appears in the tuple. The trait
+    /// `VidValuePair` lets us work with the vid/type while preserving
+    /// the "sidedness" when necessary -- the sidedness is relevant in
+    /// particular for the variance and set of in-scope things.
+    fn relate_ty_var<PAIR: VidValuePair<'tcx>>(
         &mut self,
-        vid: ty::TyVid,
-        value_ty: Ty<'tcx>
+        pair: PAIR,
     ) -> RelateResult<'tcx, Ty<'tcx>> {
-        debug!("relate_ty_var(vid={:?}, value_ty={:?})", vid, value_ty);
+        debug!("relate_ty_var({:?})", pair);
 
+        let vid = pair.vid();
+        let value_ty = pair.value_ty();
+
+        // FIXME -- this logic assumes invariance, but that is wrong.
+        // This only presently applies to chalk integration, as NLL
+        // doesn't permit type variables to appear on both sides (and
+        // doesn't use lazy norm).
         match value_ty.sty {
             ty::Infer(ty::TyVar(value_vid)) => {
                 // Two type variables: just equate them.
-                self.infcx.type_variables.borrow_mut().equate(vid, value_vid);
+                self.infcx
+                    .type_variables
+                    .borrow_mut()
+                    .equate(vid, value_vid);
                 return Ok(value_ty);
             }
 
-            ty::Projection(projection_ty)
-                if D::normalization() == NormalizationStrategy::Lazy =>
-            {
+            ty::Projection(projection_ty) if D::normalization() == NormalizationStrategy::Lazy => {
                 return Ok(self.relate_projection_ty(projection_ty, self.infcx.tcx.mk_ty_var(vid)));
             }
 
@@ -326,19 +353,22 @@ where
             assert!(!generalized_ty.has_infer_types());
         }
 
-        self.infcx.type_variables.borrow_mut().instantiate(vid, generalized_ty);
+        self.infcx
+            .type_variables
+            .borrow_mut()
+            .instantiate(vid, generalized_ty);
 
         // The generalized values we extract from `canonical_var_values` have
         // been fully instantiated and hence the set of scopes we have
         // doesn't matter -- just to be sure, put an empty vector
         // in there.
-        let old_a_scopes = ::std::mem::replace(&mut self.a_scopes, vec![]);
+        let old_a_scopes = ::std::mem::replace(pair.vid_scopes(self), vec![]);
 
         // Relate the generalized kind to the original one.
-        let result = self.relate(&generalized_ty, &value_ty);
+        let result = pair.relate_generalized_ty(self, generalized_ty);
 
         // Restore the old scopes now.
-        self.a_scopes = old_a_scopes;
+        *pair.vid_scopes(self) = old_a_scopes;
 
         debug!("relate_ty_var: complete, result = {:?}", result);
         result
@@ -347,7 +377,7 @@ where
     fn generalize_value<T: Relate<'tcx>>(
         &mut self,
         value: T,
-        for_vid: ty::TyVid
+        for_vid: ty::TyVid,
     ) -> RelateResult<'tcx, T> {
         let universe = self.infcx.probe_ty_var(for_vid).unwrap_err();
 
@@ -364,6 +394,104 @@ where
     }
 }
 
+/// When we instantiate a inference variable with a value in
+/// `relate_ty_var`, we always have the pair of a `TyVid` and a `Ty`,
+/// but the ordering may vary (depending on whether the inference
+/// variable was found on the `a` or `b` sides). Therefore, this trait
+/// allows us to factor out common code, while preserving the order
+/// when needed.
+trait VidValuePair<'tcx>: Debug {
+    /// Extract the inference variable (which could be either the
+    /// first or second part of the tuple).
+    fn vid(&self) -> ty::TyVid;
+
+    /// Extract the value it is being related to (which will be the
+    /// opposite part of the tuple from the vid).
+    fn value_ty(&self) -> Ty<'tcx>;
+
+    /// Extract the scopes that apply to whichever side of the tuple
+    /// the vid was found on.  See the comment where this is called
+    /// for more details on why we want them.
+    fn vid_scopes<D: TypeRelatingDelegate<'tcx>>(
+        &self,
+        relate: &'r mut TypeRelating<'_, '_, 'tcx, D>,
+    ) -> &'r mut Vec<BoundRegionScope<'tcx>>;
+
+    /// Given a generalized type G that should replace the vid, relate
+    /// G to the value, putting G on whichever side the vid would have
+    /// appeared.
+    fn relate_generalized_ty<D>(
+        &self,
+        relate: &mut TypeRelating<'_, '_, 'tcx, D>,
+        generalized_ty: Ty<'tcx>,
+    ) -> RelateResult<'tcx, Ty<'tcx>>
+    where
+        D: TypeRelatingDelegate<'tcx>;
+}
+
+impl VidValuePair<'tcx> for (ty::TyVid, Ty<'tcx>) {
+    fn vid(&self) -> ty::TyVid {
+        self.0
+    }
+
+    fn value_ty(&self) -> Ty<'tcx> {
+        self.1
+    }
+
+    fn vid_scopes<D>(
+        &self,
+        relate: &'r mut TypeRelating<'_, '_, 'tcx, D>,
+    ) -> &'r mut Vec<BoundRegionScope<'tcx>>
+    where
+        D: TypeRelatingDelegate<'tcx>,
+    {
+        &mut relate.a_scopes
+    }
+
+    fn relate_generalized_ty<D>(
+        &self,
+        relate: &mut TypeRelating<'_, '_, 'tcx, D>,
+        generalized_ty: Ty<'tcx>,
+    ) -> RelateResult<'tcx, Ty<'tcx>>
+    where
+        D: TypeRelatingDelegate<'tcx>,
+    {
+        relate.relate(&generalized_ty, &self.value_ty())
+    }
+}
+
+// In this case, the "vid" is the "b" type.
+impl VidValuePair<'tcx> for (Ty<'tcx>, ty::TyVid) {
+    fn vid(&self) -> ty::TyVid {
+        self.1
+    }
+
+    fn value_ty(&self) -> Ty<'tcx> {
+        self.0
+    }
+
+    fn vid_scopes<D>(
+        &self,
+        relate: &'r mut TypeRelating<'_, '_, 'tcx, D>,
+    ) -> &'r mut Vec<BoundRegionScope<'tcx>>
+    where
+        D: TypeRelatingDelegate<'tcx>,
+    {
+        &mut relate.b_scopes
+    }
+
+    fn relate_generalized_ty<D>(
+        &self,
+        relate: &mut TypeRelating<'_, '_, 'tcx, D>,
+        generalized_ty: Ty<'tcx>,
+    ) -> RelateResult<'tcx, Ty<'tcx>>
+    where
+        D: TypeRelatingDelegate<'tcx>,
+    {
+        relate.relate(&self.value_ty(), &generalized_ty)
+    }
+}
+
 impl<D> TypeRelation<'me, 'gcx, 'tcx> for TypeRelating<'me, 'gcx, 'tcx, D>
 where
     D: TypeRelatingDelegate<'tcx>,
@@ -421,11 +549,11 @@ where
                     // Forbid inference variables in the RHS.
                     bug!("unexpected inference var {:?}", b)
                 } else {
-                    self.relate_ty_var(vid, a)
+                    self.relate_ty_var((a, vid))
                 }
             }
 
-            (&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var(vid, b),
+            (&ty::Infer(ty::TyVar(vid)), _) => self.relate_ty_var((vid, b)),
 
             (&ty::Projection(projection_ty), _)
                 if D::normalization() == NormalizationStrategy::Lazy =>
@@ -752,7 +880,9 @@ where
                             drop(variables);
                             self.relate(&u, &u)
                         }
-                        TypeVariableValue::Unknown { universe: _universe } => {
+                        TypeVariableValue::Unknown {
+                            universe: _universe,
+                        } => {
                             if self.ambient_variance == ty::Bivariant {
                                 // FIXME: we may need a WF predicate (related to #54105).
                             }
@@ -767,8 +897,7 @@ where
                             let u = self.tcx().mk_ty_var(new_var_id);
                             debug!(
                                 "generalize: replacing original vid={:?} with new={:?}",
-                                vid,
-                                u
+                                vid, u
                             );
                             return Ok(u);
                         }
@@ -776,8 +905,7 @@ where
                 }
             }
 
-            ty::Infer(ty::IntVar(_)) |
-            ty::Infer(ty::FloatVar(_)) => {
+            ty::Infer(ty::IntVar(_)) | ty::Infer(ty::FloatVar(_)) => {
                 // No matter what mode we are in,
                 // integer/floating-point types must be equal to be
                 // relatable.
@@ -788,9 +916,8 @@ where
                 if self.universe.cannot_name(placeholder.universe) {
                     debug!(
                         "TypeGeneralizer::tys: root universe {:?} cannot name\
-                        placeholder in universe {:?}",
-                        self.universe,
-                        placeholder.universe
+                         placeholder in universe {:?}",
+                        self.universe, placeholder.universe
                     );
                     Err(TypeError::Mismatch)
                 } else {
@@ -798,9 +925,7 @@ where
                 }
             }
 
-            _ => {
-                relate::super_relate_tys(self, a, a)
-            }
+            _ => relate::super_relate_tys(self, a, a),
         }
     }
 
diff --git a/src/librustc_traits/chalk_context/program_clauses.rs b/src/librustc_traits/chalk_context/program_clauses.rs
deleted file mode 100644
index 8d5d2b8a9a2..00000000000
--- a/src/librustc_traits/chalk_context/program_clauses.rs
+++ /dev/null
@@ -1,621 +0,0 @@
-use rustc::traits::{
-    WellFormed,
-    FromEnv,
-    DomainGoal,
-    GoalKind,
-    Clause,
-    Clauses,
-    ProgramClause,
-    ProgramClauseCategory,
-    Environment,
-};
-use rustc::ty;
-use rustc::ty::subst::{InternalSubsts, Subst};
-use rustc::hir;
-use rustc::hir::def_id::DefId;
-use rustc_target::spec::abi;
-use super::ChalkInferenceContext;
-use crate::lowering::Lower;
-use crate::generic_types;
-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 assemble_builtin_sized_impls<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    sized_def_id: DefId,
-    ty: ty::Ty<'tcx>,
-    clauses: &mut Vec<Clause<'tcx>>
-) {
-    let mut push_builtin_impl = |ty: ty::Ty<'tcx>, nested: &[ty::Ty<'tcx>]| {
-        let clause = ProgramClause {
-            goal: ty::TraitPredicate {
-                trait_ref: ty::TraitRef {
-                    def_id: sized_def_id,
-                    substs: tcx.mk_substs_trait(ty, &[]),
-                },
-            }.lower(),
-            hypotheses: tcx.mk_goals(
-                nested.iter()
-                    .cloned()
-                    .map(|nested_ty| ty::TraitRef {
-                        def_id: sized_def_id,
-                        substs: tcx.mk_substs_trait(nested_ty, &[]),
-                    })
-                    .map(|trait_ref| ty::TraitPredicate { trait_ref })
-                    .map(|pred| GoalKind::DomainGoal(pred.lower()))
-                    .map(|goal_kind| tcx.mk_goal(goal_kind))
-            ),
-            category: ProgramClauseCategory::Other,
-        };
-        // Bind innermost bound vars that may exist in `ty` and `nested`.
-        clauses.push(Clause::ForAll(ty::Binder::bind(clause)));
-    };
-
-    match &ty.sty {
-        // Non parametric primitive types.
-        ty::Bool |
-        ty::Char |
-        ty::Int(..) |
-        ty::Uint(..) |
-        ty::Float(..) |
-        ty::Error |
-        ty::Never => push_builtin_impl(ty, &[]),
-
-        // These ones are always `Sized`.
-        &ty::Array(_, length) => {
-            push_builtin_impl(tcx.mk_ty(ty::Array(generic_types::bound(tcx, 0), length)), &[]);
-        }
-        ty::RawPtr(ptr) => {
-            push_builtin_impl(generic_types::raw_ptr(tcx, ptr.mutbl), &[]);
-        }
-        &ty::Ref(_, _, mutbl) => {
-            push_builtin_impl(generic_types::ref_ty(tcx, mutbl), &[]);
-        }
-        ty::FnPtr(fn_ptr) => {
-            let fn_ptr = fn_ptr.skip_binder();
-            let fn_ptr = generic_types::fn_ptr(
-                tcx,
-                fn_ptr.inputs_and_output.len(),
-                fn_ptr.c_variadic,
-                fn_ptr.unsafety,
-                fn_ptr.abi
-            );
-            push_builtin_impl(fn_ptr, &[]);
-        }
-        &ty::FnDef(def_id, ..) => {
-            push_builtin_impl(generic_types::fn_def(tcx, def_id), &[]);
-        }
-        &ty::Closure(def_id, ..) => {
-            push_builtin_impl(generic_types::closure(tcx, def_id), &[]);
-        }
-        &ty::Generator(def_id, ..) => {
-            push_builtin_impl(generic_types::generator(tcx, def_id), &[]);
-        }
-
-        // `Sized` if the last type is `Sized` (because else we will get a WF error anyway).
-        &ty::Tuple(type_list) => {
-            let type_list = generic_types::type_list(tcx, type_list.len());
-            push_builtin_impl(tcx.mk_ty(ty::Tuple(type_list)), &**type_list);
-        }
-
-        // Struct def
-        ty::Adt(adt_def, _) => {
-            let substs = InternalSubsts::bound_vars_for_item(tcx, adt_def.did);
-            let adt = tcx.mk_ty(ty::Adt(adt_def, substs));
-            let sized_constraint = adt_def.sized_constraint(tcx)
-                .iter()
-                .map(|ty| ty.subst(tcx, substs))
-                .collect::<Vec<_>>();
-            push_builtin_impl(adt, &sized_constraint);
-        }
-
-        // Artificially trigger an ambiguity.
-        ty::Infer(..) => {
-            // Everybody can find at least two types to unify against:
-            // general ty vars, int vars and float vars.
-            push_builtin_impl(tcx.types.i32, &[]);
-            push_builtin_impl(tcx.types.u32, &[]);
-            push_builtin_impl(tcx.types.f32, &[]);
-            push_builtin_impl(tcx.types.f64, &[]);
-        }
-
-        ty::Projection(_projection_ty) => {
-            // FIXME: add builtin impls from the associated type values found in
-            // trait impls of `projection_ty.trait_ref(tcx)`.
-        }
-
-        // The `Sized` bound can only come from the environment.
-        ty::Param(..) |
-        ty::Placeholder(..) |
-        ty::UnnormalizedProjection(..) => (),
-
-        // Definitely not `Sized`.
-        ty::Foreign(..) |
-        ty::Str |
-        ty::Slice(..) |
-        ty::Dynamic(..) |
-        ty::Opaque(..) => (),
-
-        ty::Bound(..) |
-        ty::GeneratorWitness(..) => bug!("unexpected type {:?}", ty),
-    }
-}
-
-fn wf_clause_for_raw_ptr<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    mutbl: hir::Mutability
-) -> Clauses<'tcx> {
-    let ptr_ty = generic_types::raw_ptr(tcx, mutbl);
-
-    let wf_clause = ProgramClause {
-        goal: DomainGoal::WellFormed(WellFormed::Ty(ptr_ty)),
-        hypotheses: ty::List::empty(),
-        category: ProgramClauseCategory::WellFormed,
-    };
-    let wf_clause = Clause::Implies(wf_clause);
-
-    // `forall<T> { WellFormed(*const T). }`
-    tcx.mk_clauses(iter::once(wf_clause))
-}
-
-fn wf_clause_for_fn_ptr<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    arity_and_output: usize,
-    c_variadic: bool,
-    unsafety: hir::Unsafety,
-    abi: abi::Abi
-) -> Clauses<'tcx> {
-    let fn_ptr = generic_types::fn_ptr(tcx, arity_and_output, c_variadic, unsafety, abi);
-
-    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 wf_clause_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
-    let ty = generic_types::bound(tcx, 0);
-    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 wf_clause_for_array<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    length: &'tcx ty::Const<'tcx>
-) -> Clauses<'tcx> {
-    let ty = generic_types::bound(tcx, 0);
-    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 wf_clause_for_tuple<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    arity: usize
-) -> Clauses<'tcx> {
-    let type_list = generic_types::type_list(tcx, arity);
-    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(),
-    };
-
-    // If `arity == 0` (i.e. the unit type) or `arity == 1`, this list of
-    // hypotheses is actually empty.
-    let sized_implemented = type_list[0 .. std::cmp::max(arity, 1) - 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 wf_clause_for_ref<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    mutbl: hir::Mutability
-) -> Clauses<'tcx> {
-    let region = tcx.mk_region(
-        ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
-    );
-    let ty = generic_types::bound(tcx, 1);
-    let ref_ty = tcx.mk_ref(region, ty::TypeAndMut {
-        ty,
-        mutbl,
-    });
-
-    let _outlives: DomainGoal<'_> = ty::OutlivesPredicate(ty, region).lower();
-    let wf_clause = ProgramClause {
-        goal: DomainGoal::WellFormed(WellFormed::Ty(ref_ty)),
-        hypotheses: ty::List::empty(),
-
-        // FIXME: restore this later once we get better at handling regions
-        // hypotheses: tcx.mk_goals(
-        //     iter::once(tcx.mk_goal(outlives.into_goal()))
-        // ),
-        category: ProgramClauseCategory::WellFormed,
-    };
-    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))
-}
-
-fn wf_clause_for_fn_def<'tcx>(
-    tcx: ty::TyCtxt<'_, '_, 'tcx>,
-    def_id: DefId
-) -> Clauses<'tcx> {
-    let fn_def = generic_types::fn_def(tcx, def_id);
-
-    let wf_clause = ProgramClause {
-        goal: DomainGoal::WellFormed(WellFormed::Ty(fn_def)),
-        hypotheses: ty::List::empty(),
-        category: ProgramClauseCategory::WellFormed,
-    };
-    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
-
-    // `forall <T1, ..., Tn+1> { WellFormed(fn some_fn(T1, ..., Tn) -> Tn+1). }`
-    // where `def_id` maps to the `some_fn` function definition
-    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::*;
-        use rustc::infer::canonical::OriginalQueryValues;
-
-        let goal = self.infcx.resolve_type_vars_if_possible(goal);
-
-        debug!("program_clauses(goal = {:?})", goal);
-
-        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
-                );
-
-                if Some(trait_predicate.def_id()) == self.infcx.tcx.lang_items().sized_trait() {
-                    assemble_builtin_sized_impls(
-                        self.infcx.tcx,
-                        trait_predicate.def_id(),
-                        trait_predicate.self_ty(),
-                        &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.
-                    ty::Bool |
-                    ty::Char |
-                    ty::Int(..) |
-                    ty::Uint(..) |
-                    ty::Float(..) |
-                    ty::Str |
-                    ty::Param(..) |
-                    ty::Placeholder(..) |
-                    ty::Error |
-                    ty::Never => {
-                        let wf_clause = ProgramClause {
-                            goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
-                            hypotheses: ty::List::empty(),
-                            category: ProgramClauseCategory::WellFormed,
-                        };
-                        let wf_clause = Clause::Implies(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(ptr) => wf_clause_for_raw_ptr(self.infcx.tcx, ptr.mutbl),
-
-                    // Always WF (recall that we do not check for parameters to be WF).
-                    ty::FnPtr(fn_ptr) => {
-                        let fn_ptr = fn_ptr.skip_binder();
-                        wf_clause_for_fn_ptr(
-                            self.infcx.tcx,
-                            fn_ptr.inputs_and_output.len(),
-                            fn_ptr.c_variadic,
-                            fn_ptr.unsafety,
-                            fn_ptr.abi
-                        )
-                    }
-
-                    // WF if inner type is `Sized`.
-                    ty::Slice(..) => wf_clause_for_slice(self.infcx.tcx),
-
-                    // WF if inner type is `Sized`.
-                    ty::Array(_, length) => wf_clause_for_array(self.infcx.tcx, length),
-
-                    // WF if all types but the last one are `Sized`.
-                    ty::Tuple(types) => wf_clause_for_tuple(
-                        self.infcx.tcx,
-                        types.len()
-                    ),
-
-                    // WF if `sub_ty` outlives `region`.
-                    ty::Ref(_, _, mutbl) => wf_clause_for_ref(self.infcx.tcx, mutbl),
-
-                    ty::FnDef(def_id, ..) => wf_clause_for_fn_def(self.infcx.tcx, def_id),
-
-                    ty::Dynamic(..) => {
-                        // FIXME: no rules yet for trait objects
-                        ty::List::empty()
-                    }
-
-                    ty::Adt(def, ..) => {
-                        self.infcx.tcx.program_clauses_for(def.did)
-                    }
-
-                    // FIXME: these are probably wrong
-                    ty::Foreign(def_id) |
-                    ty::Closure(def_id, ..) |
-                    ty::Generator(def_id, ..) |
-                    ty::Opaque(def_id, ..) => {
-                        self.infcx.tcx.program_clauses_for(def_id)
-                    }
-
-                    // Artificially trigger an ambiguity.
-                    ty::Infer(..) => {
-                        let tcx = self.infcx.tcx;
-                        let types = [tcx.types.i32, tcx.types.u32, tcx.types.f32, tcx.types.f64];
-                        let clauses = types.iter()
-                            .cloned()
-                            .map(|ty| ProgramClause {
-                                goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
-                                hypotheses: ty::List::empty(),
-                                category: ProgramClauseCategory::WellFormed,
-                            })
-                            .map(|clause| Clause::Implies(clause));
-                        tcx.mk_clauses(clauses)
-                    }
-
-                    ty::GeneratorWitness(..) |
-                    ty::UnnormalizedProjection(..) |
-                    ty::Bound(..) => {
-                        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
-            }
-        };
-
-        debug!("program_clauses: clauses = {:?}", clauses);
-        debug!("program_clauses: adding clauses from environment = {:?}", environment);
-
-        let mut _orig_query_values = OriginalQueryValues::default();
-        let canonical_environment = self.infcx.canonicalize_query(
-            environment,
-            &mut _orig_query_values
-        ).value;
-        let env_clauses = self.infcx.tcx.program_clauses_for_env(canonical_environment);
-
-        debug!("program_clauses: env_clauses = {:?}", env_clauses);
-
-        clauses.extend(env_clauses.into_iter().cloned());
-        clauses.extend(environment.clauses.iter().cloned());
-        clauses
-    }
-}
diff --git a/src/librustc_traits/chalk_context/program_clauses/builtin.rs b/src/librustc_traits/chalk_context/program_clauses/builtin.rs
new file mode 100644
index 00000000000..ae9f1a27b94
--- /dev/null
+++ b/src/librustc_traits/chalk_context/program_clauses/builtin.rs
@@ -0,0 +1,208 @@
+use rustc::traits::{
+    GoalKind,
+    Clause,
+    ProgramClause,
+    ProgramClauseCategory,
+};
+use rustc::ty;
+use rustc::ty::subst::{InternalSubsts, Subst};
+use rustc::hir::def_id::DefId;
+use crate::lowering::Lower;
+use crate::generic_types;
+
+crate fn assemble_builtin_unsize_impls<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    unsize_def_id: DefId,
+    source: ty::Ty<'tcx>,
+    target: ty::Ty<'tcx>,
+    clauses: &mut Vec<Clause<'tcx>>
+) {
+    match (&source.sty, &target.sty) {
+        (ty::Dynamic(data_a, ..), ty::Dynamic(data_b, ..)) => {
+            if data_a.principal_def_id() != data_b.principal_def_id()
+                || data_b.auto_traits().any(|b| data_a.auto_traits().all(|a| a != b))
+            {
+                return;
+            }
+
+            // FIXME: rules for trait upcast
+        }
+
+        (_, &ty::Dynamic(..)) => {
+            // FIXME: basically, we should have something like:
+            // ```
+            // forall<T> {
+            //     Implemented(T: Unsize< for<...> dyn Trait<...> >) :-
+            //         for<...> Implemented(T: Trait<...>).
+            // }
+            // ```
+            // The question is: how to correctly handle the higher-ranked
+            // `for<...>` binder in order to have a generic rule?
+            // (Having generic rules is useful for caching, as we may be able
+            // to turn this function and others into tcx queries later on).
+        }
+
+        (ty::Array(_, length), ty::Slice(_)) => {
+            let ty_param = generic_types::bound(tcx, 0);
+            let array_ty = tcx.mk_ty(ty::Array(ty_param, length));
+            let slice_ty = tcx.mk_ty(ty::Slice(ty_param));
+
+            // `forall<T> { Implemented([T; N]: Unsize<[T]>). }`
+            let clause = ProgramClause {
+                goal: ty::TraitPredicate {
+                    trait_ref: ty::TraitRef {
+                        def_id: unsize_def_id,
+                        substs: tcx.mk_substs_trait(array_ty, &[slice_ty.into()])
+                    },
+                }.lower(),
+                hypotheses: ty::List::empty(),
+                category: ProgramClauseCategory::Other,
+            };
+
+            clauses.push(Clause::ForAll(ty::Binder::bind(clause)));
+        }
+
+        (ty::Infer(ty::TyVar(_)), _) | (_, ty::Infer(ty::TyVar(_))) => {
+            // FIXME: ambiguous
+        }
+
+        (ty::Adt(def_id_a, ..), ty::Adt(def_id_b, ..)) => {
+            if def_id_a != def_id_b {
+                return;
+            }
+
+            // FIXME: rules for struct unsizing
+        }
+
+        (&ty::Tuple(tys_a), &ty::Tuple(tys_b)) => {
+            if tys_a.len() != tys_b.len() {
+                return;
+            }
+
+            // FIXME: rules for tuple unsizing
+        }
+
+        _ => (),
+    }
+}
+
+crate fn assemble_builtin_sized_impls<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    sized_def_id: DefId,
+    ty: ty::Ty<'tcx>,
+    clauses: &mut Vec<Clause<'tcx>>
+) {
+    let mut push_builtin_impl = |ty: ty::Ty<'tcx>, nested: &[ty::Ty<'tcx>]| {
+        let clause = ProgramClause {
+            goal: ty::TraitPredicate {
+                trait_ref: ty::TraitRef {
+                    def_id: sized_def_id,
+                    substs: tcx.mk_substs_trait(ty, &[]),
+                },
+            }.lower(),
+            hypotheses: tcx.mk_goals(
+                nested.iter()
+                    .cloned()
+                    .map(|nested_ty| ty::TraitRef {
+                        def_id: sized_def_id,
+                        substs: tcx.mk_substs_trait(nested_ty, &[]),
+                    })
+                    .map(|trait_ref| ty::TraitPredicate { trait_ref })
+                    .map(|pred| GoalKind::DomainGoal(pred.lower()))
+                    .map(|goal_kind| tcx.mk_goal(goal_kind))
+            ),
+            category: ProgramClauseCategory::Other,
+        };
+        // Bind innermost bound vars that may exist in `ty` and `nested`.
+        clauses.push(Clause::ForAll(ty::Binder::bind(clause)));
+    };
+
+    match &ty.sty {
+        // Non parametric primitive types.
+        ty::Bool |
+        ty::Char |
+        ty::Int(..) |
+        ty::Uint(..) |
+        ty::Float(..) |
+        ty::Error |
+        ty::Never => push_builtin_impl(ty, &[]),
+
+        // These ones are always `Sized`.
+        &ty::Array(_, length) => {
+            push_builtin_impl(tcx.mk_ty(ty::Array(generic_types::bound(tcx, 0), length)), &[]);
+        }
+        ty::RawPtr(ptr) => {
+            push_builtin_impl(generic_types::raw_ptr(tcx, ptr.mutbl), &[]);
+        }
+        &ty::Ref(_, _, mutbl) => {
+            push_builtin_impl(generic_types::ref_ty(tcx, mutbl), &[]);
+        }
+        ty::FnPtr(fn_ptr) => {
+            let fn_ptr = fn_ptr.skip_binder();
+            let fn_ptr = generic_types::fn_ptr(
+                tcx,
+                fn_ptr.inputs_and_output.len(),
+                fn_ptr.c_variadic,
+                fn_ptr.unsafety,
+                fn_ptr.abi
+            );
+            push_builtin_impl(fn_ptr, &[]);
+        }
+        &ty::FnDef(def_id, ..) => {
+            push_builtin_impl(generic_types::fn_def(tcx, def_id), &[]);
+        }
+        &ty::Closure(def_id, ..) => {
+            push_builtin_impl(generic_types::closure(tcx, def_id), &[]);
+        }
+        &ty::Generator(def_id, ..) => {
+            push_builtin_impl(generic_types::generator(tcx, def_id), &[]);
+        }
+
+        // `Sized` if the last type is `Sized` (because else we will get a WF error anyway).
+        &ty::Tuple(type_list) => {
+            let type_list = generic_types::type_list(tcx, type_list.len());
+            push_builtin_impl(tcx.mk_ty(ty::Tuple(type_list)), &**type_list);
+        }
+
+        // Struct def
+        ty::Adt(adt_def, _) => {
+            let substs = InternalSubsts::bound_vars_for_item(tcx, adt_def.did);
+            let adt = tcx.mk_ty(ty::Adt(adt_def, substs));
+            let sized_constraint = adt_def.sized_constraint(tcx)
+                .iter()
+                .map(|ty| ty.subst(tcx, substs))
+                .collect::<Vec<_>>();
+            push_builtin_impl(adt, &sized_constraint);
+        }
+
+        // Artificially trigger an ambiguity.
+        ty::Infer(..) => {
+            // Everybody can find at least two types to unify against:
+            // general ty vars, int vars and float vars.
+            push_builtin_impl(tcx.types.i32, &[]);
+            push_builtin_impl(tcx.types.u32, &[]);
+            push_builtin_impl(tcx.types.f32, &[]);
+            push_builtin_impl(tcx.types.f64, &[]);
+        }
+
+        ty::Projection(_projection_ty) => {
+            // FIXME: add builtin impls from the associated type values found in
+            // trait impls of `projection_ty.trait_ref(tcx)`.
+        }
+
+        // The `Sized` bound can only come from the environment.
+        ty::Param(..) |
+        ty::Placeholder(..) |
+        ty::UnnormalizedProjection(..) => (),
+
+        // Definitely not `Sized`.
+        ty::Foreign(..) |
+        ty::Str |
+        ty::Slice(..) |
+        ty::Dynamic(..) |
+        ty::Opaque(..) => (),
+
+        ty::Bound(..) |
+        ty::GeneratorWitness(..) => bug!("unexpected type {:?}", ty),
+    }
+}
diff --git a/src/librustc_traits/chalk_context/program_clauses/mod.rs b/src/librustc_traits/chalk_context/program_clauses/mod.rs
new file mode 100644
index 00000000000..80fbd97c587
--- /dev/null
+++ b/src/librustc_traits/chalk_context/program_clauses/mod.rs
@@ -0,0 +1,310 @@
+mod builtin;
+mod primitive;
+
+use rustc::traits::{
+    WellFormed,
+    FromEnv,
+    DomainGoal,
+    Clause,
+    ProgramClause,
+    ProgramClauseCategory,
+    Environment,
+};
+use rustc::ty;
+use rustc::hir::def_id::DefId;
+use super::ChalkInferenceContext;
+use std::iter;
+
+use self::primitive::*;
+use self::builtin::*;
+
+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()
+            );
+        }
+    });
+}
+
+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::*;
+        use rustc::infer::canonical::OriginalQueryValues;
+
+        let goal = self.infcx.resolve_type_vars_if_possible(goal);
+
+        debug!("program_clauses(goal = {:?})", goal);
+
+        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
+                );
+
+                if Some(trait_predicate.def_id()) == self.infcx.tcx.lang_items().sized_trait() {
+                    assemble_builtin_sized_impls(
+                        self.infcx.tcx,
+                        trait_predicate.def_id(),
+                        trait_predicate.self_ty(),
+                        &mut clauses
+                    );
+                }
+
+                if Some(trait_predicate.def_id()) == self.infcx.tcx.lang_items().unsize_trait() {
+                    let source = trait_predicate.self_ty();
+                    let target = trait_predicate.trait_ref.substs.type_at(1);
+                    assemble_builtin_unsize_impls(
+                        self.infcx.tcx,
+                        trait_predicate.def_id(),
+                        source,
+                        target,
+                        &mut clauses
+                    );
+                }
+
+                // FIXME: we need to add special rules for other builtin impls:
+                // * `Copy` / `Clone`
+                // * `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
+            }
+
+            // For outlive requirements, just assume they hold. `ResolventOps::resolvent_clause`
+            // will register them as actual region constraints later.
+            DomainGoal::Holds(RegionOutlives(..)) | DomainGoal::Holds(TypeOutlives(..)) => {
+                vec![Clause::Implies(ProgramClause {
+                    goal,
+                    hypotheses: ty::List::empty(),
+                    category: ProgramClauseCategory::Other,
+                })]
+            }
+
+            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.
+                    ty::Bool |
+                    ty::Char |
+                    ty::Int(..) |
+                    ty::Uint(..) |
+                    ty::Float(..) |
+                    ty::Str |
+                    ty::Param(..) |
+                    ty::Placeholder(..) |
+                    ty::Error |
+                    ty::Never => {
+                        let wf_clause = ProgramClause {
+                            goal,
+                            hypotheses: ty::List::empty(),
+                            category: ProgramClauseCategory::WellFormed,
+                        };
+                        let wf_clause = Clause::Implies(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(ptr) => wf_clause_for_raw_ptr(self.infcx.tcx, ptr.mutbl),
+
+                    // Always WF (recall that we do not check for parameters to be WF).
+                    ty::FnPtr(fn_ptr) => {
+                        let fn_ptr = fn_ptr.skip_binder();
+                        wf_clause_for_fn_ptr(
+                            self.infcx.tcx,
+                            fn_ptr.inputs_and_output.len(),
+                            fn_ptr.c_variadic,
+                            fn_ptr.unsafety,
+                            fn_ptr.abi
+                        )
+                    }
+
+                    // WF if inner type is `Sized`.
+                    ty::Slice(..) => wf_clause_for_slice(self.infcx.tcx),
+
+                    // WF if inner type is `Sized`.
+                    ty::Array(_, length) => wf_clause_for_array(self.infcx.tcx, length),
+
+                    // WF if all types but the last one are `Sized`.
+                    ty::Tuple(types) => wf_clause_for_tuple(
+                        self.infcx.tcx,
+                        types.len()
+                    ),
+
+                    // WF if `sub_ty` outlives `region`.
+                    ty::Ref(_, _, mutbl) => wf_clause_for_ref(self.infcx.tcx, mutbl),
+
+                    ty::FnDef(def_id, ..) => wf_clause_for_fn_def(self.infcx.tcx, def_id),
+
+                    ty::Dynamic(..) => {
+                        // FIXME: no rules yet for trait objects
+                        ty::List::empty()
+                    }
+
+                    ty::Adt(def, ..) => {
+                        self.infcx.tcx.program_clauses_for(def.did)
+                    }
+
+                    // FIXME: these are probably wrong
+                    ty::Foreign(def_id) |
+                    ty::Closure(def_id, ..) |
+                    ty::Generator(def_id, ..) |
+                    ty::Opaque(def_id, ..) => {
+                        self.infcx.tcx.program_clauses_for(def_id)
+                    }
+
+                    // Artificially trigger an ambiguity.
+                    ty::Infer(..) => {
+                        let tcx = self.infcx.tcx;
+                        let types = [tcx.types.i32, tcx.types.u32, tcx.types.f32, tcx.types.f64];
+                        let clauses = types.iter()
+                            .cloned()
+                            .map(|ty| ProgramClause {
+                                goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
+                                hypotheses: ty::List::empty(),
+                                category: ProgramClauseCategory::WellFormed,
+                            })
+                            .map(|clause| Clause::Implies(clause));
+                        tcx.mk_clauses(clauses)
+                    }
+
+                    ty::GeneratorWitness(..) |
+                    ty::UnnormalizedProjection(..) |
+                    ty::Bound(..) => {
+                        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
+            }
+        };
+
+        debug!("program_clauses: clauses = {:?}", clauses);
+        debug!("program_clauses: adding clauses from environment = {:?}", environment);
+
+        let mut _orig_query_values = OriginalQueryValues::default();
+        let canonical_environment = self.infcx.canonicalize_query(
+            environment,
+            &mut _orig_query_values
+        ).value;
+        let env_clauses = self.infcx.tcx.program_clauses_for_env(canonical_environment);
+
+        debug!("program_clauses: env_clauses = {:?}", env_clauses);
+
+        clauses.extend(env_clauses.into_iter().cloned());
+        clauses.extend(environment.clauses.iter().cloned());
+        clauses
+    }
+}
diff --git a/src/librustc_traits/chalk_context/program_clauses/primitive.rs b/src/librustc_traits/chalk_context/program_clauses/primitive.rs
new file mode 100644
index 00000000000..fc6d4091474
--- /dev/null
+++ b/src/librustc_traits/chalk_context/program_clauses/primitive.rs
@@ -0,0 +1,204 @@
+use rustc::traits::{
+    WellFormed,
+    DomainGoal,
+    GoalKind,
+    Clause,
+    Clauses,
+    ProgramClause,
+    ProgramClauseCategory,
+};
+use rustc::ty;
+use rustc::hir;
+use rustc::hir::def_id::DefId;
+use rustc_target::spec::abi;
+use crate::lowering::Lower;
+use crate::generic_types;
+use std::iter;
+
+crate fn wf_clause_for_raw_ptr<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    mutbl: hir::Mutability
+) -> Clauses<'tcx> {
+    let ptr_ty = generic_types::raw_ptr(tcx, mutbl);
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(ptr_ty)),
+        hypotheses: ty::List::empty(),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::Implies(wf_clause);
+
+    // `forall<T> { WellFormed(*const T). }`
+    tcx.mk_clauses(iter::once(wf_clause))
+}
+
+crate fn wf_clause_for_fn_ptr<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    arity_and_output: usize,
+    variadic: bool,
+    unsafety: hir::Unsafety,
+    abi: abi::Abi
+) -> Clauses<'tcx> {
+    let fn_ptr = generic_types::fn_ptr(tcx, arity_and_output, variadic, unsafety, abi);
+
+    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))
+}
+
+crate fn wf_clause_for_slice<'tcx>(tcx: ty::TyCtxt<'_, '_, 'tcx>) -> Clauses<'tcx> {
+    let ty = generic_types::bound(tcx, 0);
+    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))
+}
+
+crate fn wf_clause_for_array<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    length: &'tcx ty::Const<'tcx>
+) -> Clauses<'tcx> {
+    let ty = generic_types::bound(tcx, 0);
+    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))
+}
+
+crate fn wf_clause_for_tuple<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    arity: usize
+) -> Clauses<'tcx> {
+    let type_list = generic_types::type_list(tcx, arity);
+    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(),
+    };
+
+    // If `arity == 0` (i.e. the unit type) or `arity == 1`, this list of
+    // hypotheses is actually empty.
+    let sized_implemented = type_list[0 .. std::cmp::max(arity, 1) - 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))
+}
+
+crate fn wf_clause_for_ref<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    mutbl: hir::Mutability
+) -> Clauses<'tcx> {
+    let region = tcx.mk_region(
+        ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
+    );
+    let ty = generic_types::bound(tcx, 1);
+    let ref_ty = tcx.mk_ref(region, ty::TypeAndMut {
+        ty,
+        mutbl,
+    });
+
+    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::WellFormed,
+    };
+    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))
+}
+
+crate fn wf_clause_for_fn_def<'tcx>(
+    tcx: ty::TyCtxt<'_, '_, 'tcx>,
+    def_id: DefId
+) -> Clauses<'tcx> {
+    let fn_def = generic_types::fn_def(tcx, def_id);
+
+    let wf_clause = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(fn_def)),
+        hypotheses: ty::List::empty(),
+        category: ProgramClauseCategory::WellFormed,
+    };
+    let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
+
+    // `forall <T1, ..., Tn+1> { WellFormed(fn some_fn(T1, ..., Tn) -> Tn+1). }`
+    // where `def_id` maps to the `some_fn` function definition
+    tcx.mk_clauses(iter::once(wf_clause))
+}
diff --git a/src/librustc_traits/chalk_context/resolvent_ops.rs b/src/librustc_traits/chalk_context/resolvent_ops.rs
index 932501cc04f..41f983e6aca 100644
--- a/src/librustc_traits/chalk_context/resolvent_ops.rs
+++ b/src/librustc_traits/chalk_context/resolvent_ops.rs
@@ -8,6 +8,7 @@ use rustc::infer::{InferCtxt, LateBoundRegionConversionTime};
 use rustc::infer::canonical::{Canonical, CanonicalVarValues};
 use rustc::traits::{
     DomainGoal,
+    WhereClause,
     Goal,
     GoalKind,
     Clause,
@@ -75,6 +76,23 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
                 })
             );
 
+            // If we have a goal of the form `T: 'a` or `'a: 'b`, then just
+            // assume it is true (no subgoals) and register it as a constraint
+            // instead.
+            match goal {
+                DomainGoal::Holds(WhereClause::RegionOutlives(pred)) => {
+                    assert_eq!(ex_clause.subgoals.len(), 0);
+                    ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
+                }
+
+                DomainGoal::Holds(WhereClause::TypeOutlives(pred)) => {
+                    assert_eq!(ex_clause.subgoals.len(), 0);
+                    ex_clause.constraints.push(ty::OutlivesPredicate(pred.0.into(), pred.1));
+                }
+
+                _ => (),
+            };
+
             let canonical_ex_clause = self.canonicalize_ex_clause(&ex_clause);
             Ok(canonical_ex_clause)
         });
@@ -112,10 +130,8 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         substitutor.relate(&answer_table_goal.value, &selected_goal)
             .map_err(|_| NoSolution)?;
 
-        let ex_clause = substitutor.ex_clause;
-
-        // FIXME: restore this later once we get better at handling regions
-        // ex_clause.constraints.extend(answer_subst.constraints);
+        let mut ex_clause = substitutor.ex_clause;
+        ex_clause.constraints.extend(answer_subst.constraints);
 
         debug!("apply_answer_subst: ex_clause = {:?}", ex_clause);
         Ok(ex_clause)
diff --git a/src/librustc_traits/lowering/environment.rs b/src/librustc_traits/lowering/environment.rs
index c908c6993e1..3570cb10246 100644
--- a/src/librustc_traits/lowering/environment.rs
+++ b/src/librustc_traits/lowering/environment.rs
@@ -10,9 +10,6 @@ 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 crate::generic_types;
-use std::iter;
 
 struct ClauseVisitor<'set, 'a, 'tcx: 'a + 'set> {
     tcx: TyCtxt<'a, 'tcx, 'tcx>,
@@ -38,30 +35,6 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
                 );
             }
 
-            // forall<'a, T> { `Outlives(T: 'a) :- FromEnv(&'a T)` }
-            ty::Ref(_, _, mutbl) => {
-                let region = self.tcx.mk_region(
-                    ty::ReLateBound(ty::INNERMOST, ty::BoundRegion::BrAnon(0))
-                );
-                let ty = generic_types::bound(self.tcx, 1);
-                let ref_ty = self.tcx.mk_ref(region, ty::TypeAndMut {
-                    ty,
-                    mutbl,
-                });
-
-                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(..) => {
                 // FIXME: trait object rules are not yet implemented
             }
@@ -99,6 +72,7 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
             ty::RawPtr(..) |
             ty::FnPtr(..) |
             ty::Tuple(..) |
+            ty::Ref(..) |
             ty::Never |
             ty::Infer(..) |
             ty::Placeholder(..) |
diff --git a/src/librustc_traits/lowering/mod.rs b/src/librustc_traits/lowering/mod.rs
index 44883d438a1..c3cbdb03762 100644
--- a/src/librustc_traits/lowering/mod.rs
+++ b/src/librustc_traits/lowering/mod.rs
@@ -209,6 +209,10 @@ fn program_clauses_for_trait<'a, 'tcx>(
     let implemented_from_env = Clause::ForAll(ty::Binder::bind(implemented_from_env));
 
     let predicates = &tcx.predicates_defined_on(def_id).predicates;
+
+    // Warning: these where clauses are not substituted for bound vars yet,
+    // so that we don't need to adjust binders in the `FromEnv` rules below
+    // (see the FIXME).
     let where_clauses = &predicates
         .iter()
         .map(|(wc, _)| wc.lower())
@@ -258,6 +262,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
     // `WellFormed(WC)`
     let wf_conditions = where_clauses
         .into_iter()
+        .map(|wc| wc.subst(tcx, bound_vars))
         .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()));
 
     // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
@@ -332,7 +337,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
     //
     // ```
     // forall<P1..Pn> {
-    //   WellFormed(Ty<...>) :- WC1, ..., WCm`
+    //   WellFormed(Ty<...>) :- WellFormed(WC1), ..., WellFormed(WCm)`
     // }
     // ```
 
@@ -341,19 +346,22 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
     // `Ty<...>`
     let ty = tcx.type_of(def_id).subst(tcx, bound_vars);
 
-    // `WC`
+    // Warning: these where clauses are not substituted for bound vars yet,
+    // so that we don't need to adjust binders in the `FromEnv` rules below
+    // (see the FIXME).
     let where_clauses = tcx.predicates_of(def_id).predicates
         .iter()
         .map(|(wc, _)| wc.lower())
         .collect::<Vec<_>>();
 
-    // `WellFormed(Ty<...>) :- WC1, ..., WCm`
+    // `WellFormed(Ty<...>) :- WellFormed(WC1), ..., WellFormed(WCm)`
     let well_formed_clause = ProgramClause {
         goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
         hypotheses: tcx.mk_goals(
             where_clauses
                 .iter()
                 .map(|wc| wc.subst(tcx, bound_vars))
+                .map(|wc| wc.map_bound(|bound| bound.into_well_formed_goal()))
                 .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
         ),
         category: ProgramClauseCategory::WellFormed,
@@ -450,13 +458,13 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
     // ```
     // forall<Self, P1..Pn, Pn+1..Pm> {
     //     WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
-    //         :- Implemented(Self: Trait<P1..Pn>)
+    //         :- WellFormed(Self: Trait<P1..Pn>)
     // }
     // ```
 
     let trait_predicate = ty::TraitPredicate { trait_ref };
     let hypothesis = tcx.mk_goal(
-        DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal()
+        DomainGoal::WellFormed(WellFormed::Trait(trait_predicate)).into_goal()
     );
 
     let wf_clause = ProgramClause {
diff --git a/src/test/compile-fail/chalkify/recursive_where_clause_on_type.rs b/src/test/compile-fail/chalkify/recursive_where_clause_on_type.rs
new file mode 100644
index 00000000000..861f86e6165
--- /dev/null
+++ b/src/test/compile-fail/chalkify/recursive_where_clause_on_type.rs
@@ -0,0 +1,28 @@
+// compile-flags: -Z chalk
+
+#![feature(trivial_bounds)]
+
+trait Bar {
+    fn foo();
+}
+trait Foo: Bar { }
+
+struct S where S: Foo;
+
+impl Foo for S {
+}
+
+fn bar<T: Bar>() {
+    T::foo();
+}
+
+fn foo<T: Foo>() {
+    bar::<T>()
+}
+
+fn main() {
+    // For some reason, the error is duplicated...
+
+    foo::<S>() //~ ERROR the type `S` is not well-formed (chalk)
+    //~^ ERROR the type `S` is not well-formed (chalk)
+}
diff --git a/src/test/ui/chalkify/lower_env2.stderr b/src/test/ui/chalkify/lower_env2.stderr
index 2a71fa9df5e..613a568a854 100644
--- a/src/test/ui/chalkify/lower_env2.stderr
+++ b/src/test/ui/chalkify/lower_env2.stderr
@@ -6,7 +6,7 @@ LL | #[rustc_dump_program_clauses]
    |
    = 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). }
+   = note: forall<'a, T> { WellFormed(S<'a, T>) :- WellFormed(T: Foo), TypeOutlives(T: 'a). }
 
 error: program clause dump
   --> $DIR/lower_env2.rs:11:1
diff --git a/src/test/ui/chalkify/lower_env3.stderr b/src/test/ui/chalkify/lower_env3.stderr
index 46e08368689..a1fc83bfea8 100644
--- a/src/test/ui/chalkify/lower_env3.stderr
+++ b/src/test/ui/chalkify/lower_env3.stderr
@@ -4,7 +4,6 @@ error: program clause dump
 LL |     #[rustc_dump_env_program_clauses]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: forall<'^0, ^1> { TypeOutlives(^1: '^0) :- FromEnv(&^1). }
    = note: forall<Self> { Implemented(Self: Foo) :- FromEnv(Self: Foo). }
 
 error: program clause dump
@@ -13,7 +12,6 @@ error: program clause dump
 LL |     #[rustc_dump_env_program_clauses]
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = 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). }
diff --git a/src/test/ui/chalkify/lower_struct.stderr b/src/test/ui/chalkify/lower_struct.stderr
index 91525c3ba55..0331c2fca16 100644
--- a/src/test/ui/chalkify/lower_struct.stderr
+++ b/src/test/ui/chalkify/lower_struct.stderr
@@ -7,7 +7,7 @@ LL | #[rustc_dump_program_clauses]
    = 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). }
+   = note: forall<'a, T> { WellFormed(Foo<'a, T>) :- WellFormed(T: std::marker::Sized), WellFormed(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 423c5573083..ed3bded398a 100644
--- a/src/test/ui/chalkify/lower_trait.stderr
+++ b/src/test/ui/chalkify/lower_trait.stderr
@@ -18,7 +18,7 @@ LL |     #[rustc_dump_program_clauses]
    = note: forall<Self, S, T, ^3> { ProjectionEq(<Self as Foo<S, T>>::Assoc == ^3) :- Normalize(<Self as Foo<S, T>>::Assoc -> ^3). }
    = 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>). }
+   = note: forall<Self, S, T> { WellFormed(Unnormalized(<Self as Foo<S, T>>::Assoc)) :- WellFormed(Self: Foo<S, T>). }
 
 error: aborting due to 2 previous errors