Auto merge of #51433 - scalexm:finish-rules, r=nikomatsakis

[chalkify] Small refactoring and WF/FromEnv rules for types

r? @nikomatsakis

8 files changed, 335 insertions, 139 deletions

diff --git a/src/librustc/ich/impls_ty.rs b/src/librustc/ich/impls_ty.rs
index 5e67065d1c1..684a1d29658 100644
--- a/src/librustc/ich/impls_ty.rs
+++ b/src/librustc/ich/impls_ty.rs
@@ -1373,16 +1373,46 @@ impl_stable_hash_for!(enum infer::canonical::Certainty {
     Proven, Ambiguous
 });
 
-impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClauseAtom<'tcx> {
+impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClause<'tcx> {
     fn hash_stable<W: StableHasherResult>(&self,
                                           hcx: &mut StableHashingContext<'a>,
                                           hasher: &mut StableHasher<W>) {
-        use traits::WhereClauseAtom::*;
+        use traits::WhereClause::*;
 
         mem::discriminant(self).hash_stable(hcx, hasher);
         match self {
             Implemented(trait_ref) => trait_ref.hash_stable(hcx, hasher),
             ProjectionEq(projection) => projection.hash_stable(hcx, hasher),
+            TypeOutlives(ty_outlives) => ty_outlives.hash_stable(hcx, hasher),
+            RegionOutlives(region_outlives) => region_outlives.hash_stable(hcx, hasher),
+        }
+    }
+}
+
+impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WellFormed<'tcx> {
+    fn hash_stable<W: StableHasherResult>(&self,
+                                          hcx: &mut StableHashingContext<'a>,
+                                          hasher: &mut StableHasher<W>) {
+        use traits::WellFormed::*;
+
+        mem::discriminant(self).hash_stable(hcx, hasher);
+        match self {
+            Trait(trait_ref) => trait_ref.hash_stable(hcx, hasher),
+            Ty(ty) => ty.hash_stable(hcx, hasher),
+        }
+    }
+}
+
+impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::FromEnv<'tcx> {
+    fn hash_stable<W: StableHasherResult>(&self,
+                                          hcx: &mut StableHashingContext<'a>,
+                                          hasher: &mut StableHasher<W>) {
+        use traits::FromEnv::*;
+
+        mem::discriminant(self).hash_stable(hcx, hasher);
+        match self {
+            Trait(trait_ref) => trait_ref.hash_stable(hcx, hasher),
+            Ty(ty) => ty.hash_stable(hcx, hasher),
         }
     }
 }
@@ -1395,15 +1425,10 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::DomainGoal<'tcx>
 
         mem::discriminant(self).hash_stable(hcx, hasher);
         match self {
-            Holds(where_clause) |
-            WellFormed(where_clause) |
-            FromEnv(where_clause) => where_clause.hash_stable(hcx, hasher),
-
-            WellFormedTy(ty) => ty.hash_stable(hcx, hasher),
+            Holds(wc) => wc.hash_stable(hcx, hasher),
+            WellFormed(wf) => wf.hash_stable(hcx, hasher),
+            FromEnv(from_env) => from_env.hash_stable(hcx, hasher),
             Normalize(projection) => projection.hash_stable(hcx, hasher),
-            FromEnvTy(ty) => ty.hash_stable(hcx, hasher),
-            RegionOutlives(predicate) => predicate.hash_stable(hcx, hasher),
-            TypeOutlives(predicate) => predicate.hash_stable(hcx, hasher),
         }
     }
 }
diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs
index 761de001438..354debf87dc 100644
--- a/src/librustc/traits/mod.rs
+++ b/src/librustc/traits/mod.rs
@@ -269,7 +269,9 @@ pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
 pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
 
 /// The following types:
-/// * `WhereClauseAtom`
+/// * `WhereClause`
+/// * `WellFormed`
+/// * `FromEnv`
 /// * `DomainGoal`
 /// * `Goal`
 /// * `Clause`
@@ -277,21 +279,31 @@ pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
 /// logic programming clauses. They are part of the interface
 /// for the chalk SLG solver.
 #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
-pub enum WhereClauseAtom<'tcx> {
+pub enum WhereClause<'tcx> {
     Implemented(ty::TraitPredicate<'tcx>),
     ProjectionEq(ty::ProjectionPredicate<'tcx>),
+    RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
+    TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
+pub enum WellFormed<'tcx> {
+    Trait(ty::TraitPredicate<'tcx>),
+    Ty(Ty<'tcx>),
+}
+
+#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
+pub enum FromEnv<'tcx> {
+    Trait(ty::TraitPredicate<'tcx>),
+    Ty(Ty<'tcx>),
 }
 
 #[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
 pub enum DomainGoal<'tcx> {
-    Holds(WhereClauseAtom<'tcx>),
-    WellFormed(WhereClauseAtom<'tcx>),
-    FromEnv(WhereClauseAtom<'tcx>),
-    WellFormedTy(Ty<'tcx>),
+    Holds(WhereClause<'tcx>),
+    WellFormed(WellFormed<'tcx>),
+    FromEnv(FromEnv<'tcx>),
     Normalize(ty::ProjectionPredicate<'tcx>),
-    FromEnvTy(Ty<'tcx>),
-    RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
-    TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
 }
 
 pub type PolyDomainGoal<'tcx> = ty::Binder<DomainGoal<'tcx>>;
@@ -314,27 +326,27 @@ pub enum Goal<'tcx> {
 
 pub type Goals<'tcx> = &'tcx Slice<Goal<'tcx>>;
 
+impl<'tcx> DomainGoal<'tcx> {
+    pub fn into_goal(self) -> Goal<'tcx> {
+        Goal::DomainGoal(self)
+    }
+}
+
 impl<'tcx> Goal<'tcx> {
     pub fn from_poly_domain_goal<'a>(
         domain_goal: PolyDomainGoal<'tcx>,
         tcx: TyCtxt<'a, 'tcx, 'tcx>,
     ) -> Goal<'tcx> {
         match domain_goal.no_late_bound_regions() {
-            Some(p) => p.into(),
+            Some(p) => p.into_goal(),
             None => Goal::Quantified(
                 QuantifierKind::Universal,
-                domain_goal.map_bound(|p| tcx.mk_goal(Goal::from(p)))
+                domain_goal.map_bound(|p| tcx.mk_goal(p.into_goal()))
             ),
         }
     }
 }
 
-impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
-    fn from(domain_goal: DomainGoal<'tcx>) -> Self {
-        Goal::DomainGoal(domain_goal)
-    }
-}
-
 /// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
 /// Harrop Formulas".
 #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
diff --git a/src/librustc/traits/structural_impls.rs b/src/librustc/traits/structural_impls.rs
index d1304a0a3f8..d24c84b2556 100644
--- a/src/librustc/traits/structural_impls.rs
+++ b/src/librustc/traits/structural_impls.rs
@@ -405,13 +405,37 @@ BraceStructTypeFoldableImpl! {
     } where T: TypeFoldable<'tcx>
 }
 
-impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
+impl<'tcx> fmt::Display for traits::WhereClause<'tcx> {
     fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
-        use traits::WhereClauseAtom::*;
+        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),
         }
     }
 }
@@ -419,19 +443,12 @@ impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
 impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
     fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
         use traits::DomainGoal::*;
-        use traits::WhereClauseAtom::*;
 
         match self {
             Holds(wc) => write!(fmt, "{}", wc),
-            WellFormed(Implemented(trait_ref)) => write!(fmt, "WellFormed({})", trait_ref),
-            WellFormed(ProjectionEq(projection)) => write!(fmt, "WellFormed({})", projection),
-            FromEnv(Implemented(trait_ref)) => write!(fmt, "FromEnv({})", trait_ref),
-            FromEnv(ProjectionEq(projection)) => write!(fmt, "FromEnv({})", projection),
-            WellFormedTy(ty) => write!(fmt, "WellFormed({})", ty),
+            WellFormed(wf) => write!(fmt, "{}", wf),
+            FromEnv(from_env) => write!(fmt, "{}", from_env),
             Normalize(projection) => write!(fmt, "Normalize({})", projection),
-            FromEnvTy(ty) => write!(fmt, "FromEnv({})", ty),
-            RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
-            TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
         }
     }
 }
@@ -506,30 +523,60 @@ impl<'tcx> fmt::Display for traits::Clause<'tcx> {
 }
 
 EnumTypeFoldableImpl! {
-    impl<'tcx> TypeFoldable<'tcx> for traits::WhereClauseAtom<'tcx> {
-        (traits::WhereClauseAtom::Implemented)(trait_ref),
-        (traits::WhereClauseAtom::ProjectionEq)(projection),
+    impl<'tcx> TypeFoldable<'tcx> for 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::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),
+        (traits::WellFormed::Ty)(ty),
+    }
+}
+
+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),
+        (traits::FromEnv::Ty)(ty),
     }
 }
 
 EnumLiftImpl! {
-    impl<'a, 'tcx> Lift<'tcx> for traits::WhereClauseAtom<'a> {
-        type Lifted = traits::WhereClauseAtom<'tcx>;
-        (traits::WhereClauseAtom::Implemented)(trait_ref),
-        (traits::WhereClauseAtom::ProjectionEq)(projection),
+    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),
-        (traits::DomainGoal::WellFormed)(wc),
-        (traits::DomainGoal::FromEnv)(wc),
-        (traits::DomainGoal::WellFormedTy)(ty),
+        (traits::DomainGoal::WellFormed)(wf),
+        (traits::DomainGoal::FromEnv)(from_env),
         (traits::DomainGoal::Normalize)(projection),
-        (traits::DomainGoal::FromEnvTy)(ty),
-        (traits::DomainGoal::RegionOutlives)(predicate),
-        (traits::DomainGoal::TypeOutlives)(predicate),
     }
 }
 
@@ -537,13 +584,9 @@ EnumLiftImpl! {
     impl<'a, 'tcx> Lift<'tcx> for traits::DomainGoal<'a> {
         type Lifted = traits::DomainGoal<'tcx>;
         (traits::DomainGoal::Holds)(wc),
-        (traits::DomainGoal::WellFormed)(wc),
-        (traits::DomainGoal::FromEnv)(wc),
-        (traits::DomainGoal::WellFormedTy)(ty),
+        (traits::DomainGoal::WellFormed)(wf),
+        (traits::DomainGoal::FromEnv)(from_env),
         (traits::DomainGoal::Normalize)(projection),
-        (traits::DomainGoal::FromEnvTy)(ty),
-        (traits::DomainGoal::RegionOutlives)(predicate),
-        (traits::DomainGoal::TypeOutlives)(predicate),
     }
 }
 
diff --git a/src/librustc_traits/chalk_context.rs b/src/librustc_traits/chalk_context.rs
index bf26409c3ef..a1242621cb1 100644
--- a/src/librustc_traits/chalk_context.rs
+++ b/src/librustc_traits/chalk_context.rs
@@ -14,7 +14,16 @@ use rustc::infer::canonical::{
     Canonical, CanonicalVarValues, Canonicalize, QueryRegionConstraint, QueryResult,
 };
 use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
-use rustc::traits::{DomainGoal, ExClauseFold, ExClauseLift, Goal, ProgramClause, QuantifierKind};
+use rustc::traits::{
+    WellFormed,
+    FromEnv,
+    DomainGoal,
+    ExClauseFold,
+    ExClauseLift,
+    Goal,
+    ProgramClause,
+    QuantifierKind
+};
 use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
 use rustc::ty::subst::Kind;
 use rustc::ty::{self, TyCtxt};
@@ -314,11 +323,10 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
         _environment: &ty::ParamEnv<'tcx>,
         goal: &DomainGoal<'tcx>,
     ) -> Vec<ProgramClause<'tcx>> {
-        use rustc::traits::DomainGoal::*;
-        use rustc::traits::WhereClauseAtom::*;
+        use rustc::traits::WhereClause::*;
 
         match goal {
-            Holds(Implemented(_trait_predicate)) => {
+            DomainGoal::Holds(Implemented(_trait_predicate)) => {
                 // These come from:
                 //
                 // - Trait definitions (implied bounds)
@@ -326,31 +334,31 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
                 panic!()
             }
 
-            Holds(ProjectionEq(_projection_predicate)) => {
+            DomainGoal::Holds(ProjectionEq(_projection_predicate)) => {
                 // These come from:
                 panic!()
             }
 
-            WellFormed(Implemented(_trait_predicate)) => {
-                // These come from -- the trait decl.
+            DomainGoal::Holds(RegionOutlives(_region_outlives)) => {
                 panic!()
             }
 
-            WellFormed(ProjectionEq(_projection_predicate)) => panic!(),
-
-            FromEnv(Implemented(_trait_predicate)) => panic!(),
-
-            FromEnv(ProjectionEq(_projection_predicate)) => panic!(),
+            DomainGoal::Holds(TypeOutlives(_type_outlives)) => {
+                panic!()
+            }
 
-            WellFormedTy(_ty) => panic!(),
+            DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => {
+                // These come from -- the trait decl.
+                panic!()
+            }
 
-            FromEnvTy(_ty) => panic!(),
+            DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(),
 
-            RegionOutlives(_region_outlives) => panic!(),
+            DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(),
 
-            TypeOutlives(_type_outlives) => panic!(),
+            DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(),
 
-            Normalize(_) => panic!(),
+            DomainGoal::Normalize(_) => panic!(),
         }
     }
 
diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs
index 32f18a62abe..0270e970976 100644
--- a/src/librustc_traits/lowering.rs
+++ b/src/librustc_traits/lowering.rs
@@ -13,7 +13,7 @@ use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
 use rustc::hir::map::definitions::DefPathData;
 use rustc::hir::{self, ImplPolarity};
 use rustc::traits::{Clause, Clauses, DomainGoal, Goal, PolyDomainGoal, ProgramClause,
-                    WhereClauseAtom};
+                    WhereClause, FromEnv, WellFormed};
 use rustc::ty::subst::Substs;
 use rustc::ty::{self, Slice, TyCtxt};
 use rustc_data_structures::fx::FxHashSet;
@@ -23,7 +23,7 @@ use syntax::ast;
 use std::iter;
 
 crate trait Lower<T> {
-    /// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
+    /// Lower a rustc construct (e.g. `ty::TraitPredicate`) to a chalk-like type.
     fn lower(&self) -> T;
 }
 
@@ -36,36 +36,36 @@ where
     }
 }
 
-impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::TraitPredicate<'tcx> {
-    fn lower(&self) -> WhereClauseAtom<'tcx> {
-        WhereClauseAtom::Implemented(*self)
+impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
+    fn lower(&self) -> WhereClause<'tcx> {
+        WhereClause::Implemented(*self)
     }
 }
 
-impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::ProjectionPredicate<'tcx> {
-    fn lower(&self) -> WhereClauseAtom<'tcx> {
-        WhereClauseAtom::ProjectionEq(*self)
+impl<'tcx> Lower<WhereClause<'tcx>> for ty::ProjectionPredicate<'tcx> {
+    fn lower(&self) -> WhereClause<'tcx> {
+        WhereClause::ProjectionEq(*self)
     }
 }
 
-impl<'tcx, T> Lower<DomainGoal<'tcx>> for T
-where
-    T: Lower<WhereClauseAtom<'tcx>>,
-{
-    fn lower(&self) -> DomainGoal<'tcx> {
-        DomainGoal::Holds(self.lower())
+impl<'tcx> Lower<WhereClause<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
+    fn lower(&self) -> WhereClause<'tcx> {
+        WhereClause::RegionOutlives(*self)
     }
 }
 
-impl<'tcx> Lower<DomainGoal<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
-    fn lower(&self) -> DomainGoal<'tcx> {
-        DomainGoal::RegionOutlives(*self)
+impl<'tcx> Lower<WhereClause<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
+    fn lower(&self) -> WhereClause<'tcx> {
+        WhereClause::TypeOutlives(*self)
     }
 }
 
-impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
+impl<'tcx, T> Lower<DomainGoal<'tcx>> for T
+where
+    T: Lower<WhereClause<'tcx>>,
+{
     fn lower(&self) -> DomainGoal<'tcx> {
-        DomainGoal::TypeOutlives(*self)
+        DomainGoal::Holds(self.lower())
     }
 }
 
@@ -86,15 +86,20 @@ where
 
 impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
     fn lower(&self) -> PolyDomainGoal<'tcx> {
-        use rustc::ty::Predicate::*;
+        use rustc::ty::Predicate;
 
         match self {
-            Trait(predicate) => predicate.lower(),
-            RegionOutlives(predicate) => predicate.lower(),
-            TypeOutlives(predicate) => predicate.lower(),
-            Projection(predicate) => predicate.lower(),
-            WellFormed(ty) => ty::Binder::dummy(DomainGoal::WellFormedTy(*ty)),
-            ObjectSafe(..) | ClosureKind(..) | Subtype(..) | ConstEvaluatable(..) => {
+            Predicate::Trait(predicate) => predicate.lower(),
+            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::ObjectSafe(..) |
+            Predicate::ClosureKind(..) |
+            Predicate::Subtype(..) |
+            Predicate::ConstEvaluatable(..) => {
                 unimplemented!()
             }
         }
@@ -110,11 +115,13 @@ trait IntoFromEnvGoal {
 
 impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
     fn into_from_env_goal(self) -> DomainGoal<'tcx> {
-        use self::DomainGoal::*;
+        use self::WhereClause::*;
+
         match self {
-            Holds(wc_atom) => FromEnv(wc_atom),
-            WellFormed(..) | FromEnv(..) | WellFormedTy(..) | FromEnvTy(..) | Normalize(..)
-            | RegionOutlives(..) | TypeOutlives(..) => self,
+            DomainGoal::Holds(Implemented(trait_ref)) => DomainGoal::FromEnv(
+                FromEnv::Trait(trait_ref)
+            ),
+            other => other,
         }
     }
 }
@@ -127,6 +134,8 @@ crate fn program_clauses_for<'a, 'tcx>(
         DefPathData::Trait(_) => program_clauses_for_trait(tcx, def_id),
         DefPathData::Impl => program_clauses_for_impl(tcx, def_id),
         DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id),
+        DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id),
+        DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id),
         _ => Slice::empty(),
     }
 }
@@ -212,16 +221,20 @@ fn program_clauses_for_trait<'a, 'tcx>(
             substs: Substs::identity_for_item(tcx, def_id),
         },
     };
-    // `FromEnv(Self: Trait<P1..Pn>)`
-    let from_env = Goal::from(DomainGoal::FromEnv(trait_pred.lower()));
+
     // `Implemented(Self: Trait<P1..Pn>)`
-    let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred));
+    let impl_trait: DomainGoal = trait_pred.lower();
+
+     // `FromEnv(Self: Trait<P1..Pn>)`
+    let from_env_goal = impl_trait.into_from_env_goal().into_goal();
+    let hypotheses = tcx.intern_goals(&[from_env_goal]);
 
     // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
     let implemented_from_env = ProgramClause {
         goal: impl_trait,
-        hypotheses: tcx.intern_goals(&[from_env]),
+        hypotheses,
     };
+
     let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
 
     // Rule Implied-Bound-From-Trait
@@ -239,25 +252,17 @@ fn program_clauses_for_trait<'a, 'tcx>(
     let where_clauses = &tcx.predicates_of(def_id).predicates;
     let implied_bound_clauses = where_clauses[1..]
         .into_iter()
-        .map(|wc| implied_bound_from_trait(tcx, trait_pred, wc));
+        .map(|wc| wc.lower())
 
-    tcx.mk_clauses(clauses.chain(implied_bound_clauses))
-}
+        // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
+        .map(|wc| wc.map_bound(|goal| ProgramClause {
+            goal: goal.into_from_env_goal(),
+            hypotheses,
+        }))
 
-/// For a given `where_clause`, returns a clause `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`.
-fn implied_bound_from_trait<'a, 'tcx>(
-    tcx: TyCtxt<'a, 'tcx, 'tcx>,
-    trait_pred: ty::TraitPredicate<'tcx>,
-    where_clause: &ty::Predicate<'tcx>,
-) -> Clause<'tcx> {
-    // `FromEnv(Self: Trait<P1..Pn>)`
-    let impl_trait = DomainGoal::FromEnv(WhereClauseAtom::Implemented(trait_pred));
-
-    // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
-    Clause::ForAll(where_clause.lower().map_bound(|goal| ProgramClause {
-        goal: goal.into_from_env_goal(),
-        hypotheses: tcx.intern_goals(&[Goal::from(impl_trait)]),
-    }))
+        .map(Clause::ForAll);
+
+    tcx.mk_clauses(clauses.chain(implied_bound_clauses))
 }
 
 fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> {
@@ -275,9 +280,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).unwrap();
+    let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
+
     // `Implemented(A0: Trait<A1..An>)`
     let trait_pred = ty::TraitPredicate { trait_ref }.lower();
+
     // `WC`
     let where_clauses = tcx.predicates_of(def_id).predicates.lower();
 
@@ -293,6 +300,72 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
     tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
 }
 
+pub fn program_clauses_for_type_def<'a, 'tcx>(
+    tcx: TyCtxt<'a, 'tcx, 'tcx>,
+    def_id: DefId,
+) -> Clauses<'tcx> {
+
+    // Rule WellFormed-Type
+    //
+    // `struct Ty<P1..Pn> where WC1, ..., WCm`
+    //
+    // ```
+    // forall<P1..Pn> {
+    //   WellFormed(Ty<...>) :- WC1, ..., WCm`
+    // }
+    // ```
+
+    // `Ty<...>`
+    let ty = tcx.type_of(def_id);
+
+    // `WC`
+    let where_clauses = tcx.predicates_of(def_id).predicates.lower();
+
+    // `WellFormed(Ty<...>) :- WC1, ..., WCm`
+    let well_formed = ProgramClause {
+        goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
+        hypotheses: tcx.mk_goals(
+            where_clauses.iter().cloned().map(|wc| Goal::from_poly_domain_goal(wc, tcx))
+        ),
+    };
+
+    let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
+
+    // Rule FromEnv-Type
+    //
+    // For each where clause `WC`:
+    // ```
+    // forall<P1..Pn> {
+    //   FromEnv(WC) :- FromEnv(Ty<...>)
+    // }
+    // ```
+
+    // `FromEnv(Ty<...>)`
+    let from_env_goal = DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal();
+    let hypotheses = tcx.intern_goals(&[from_env_goal]);
+
+    // For each where clause `WC`:
+    let from_env_clauses = where_clauses
+        .into_iter()
+
+        // `FromEnv(WC) :- FromEnv(Ty<...>)`
+        .map(|wc| wc.map_bound(|goal| ProgramClause {
+            goal: goal.into_from_env_goal(),
+            hypotheses,
+        }))
+
+        .map(Clause::ForAll);
+
+    tcx.mk_clauses(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> {
+    unimplemented!()
+}
+
 pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
     tcx: TyCtxt<'a, 'tcx, 'tcx>,
     item_id: DefId,
@@ -301,45 +374,50 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
     //
     // ```impl<P0..Pn> Trait<A1..An> for A0
     // {
-    //     type AssocType<Pn+1..Pm> where WC = T;
+    //     type AssocType<Pn+1..Pm> = T;
     // }```
     //
+    // FIXME: For the moment, we don't account for where clauses written on the associated
+    // ty definition (i.e. in the trait def, as in `type AssocType<T> where T: Sized`).
     // ```
     // forall<P0..Pm> {
     //   forall<Pn+1..Pm> {
     //     Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
-    //       Implemented(A0: Trait<A1..An>) && WC
+    //       Implemented(A0: Trait<A1..An>)
     //   }
     // }
     // ```
 
     let item = tcx.associated_item(item_id);
     debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
-    let impl_id = if let ty::AssociatedItemContainer::ImplContainer(impl_id) = item.container {
-        impl_id
-    } else {
-        bug!()
+    let impl_id = match item.container {
+        ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id,
+        _ => bug!("not an impl container"),
     };
+
     // `A0 as Trait<A1..An>`
     let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
+
     // `T`
     let ty = tcx.type_of(item_id);
+
     // `Implemented(A0: Trait<A1..An>)`
     let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower());
-    // `WC`
-    let item_where_clauses = tcx.predicates_of(item_id).predicates.lower();
-    // `Implemented(A0: Trait<A1..An>) && WC`
-    let mut where_clauses = vec![trait_implemented];
-    where_clauses.extend(item_where_clauses);
+
+    // `Implemented(A0: Trait<A1..An>)`
+    let hypotheses = vec![trait_implemented];
+
     // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
     let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.name);
+
     // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)`
     let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
+
     // `Normalize(... -> T) :- ...`
     let clause = ProgramClause {
         goal: normalize_goal,
         hypotheses: tcx.mk_goals(
-            where_clauses
+            hypotheses
                 .into_iter()
                 .map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
         ),
diff --git a/src/test/ui/chalkify/lower_struct.rs b/src/test/ui/chalkify/lower_struct.rs
new file mode 100644
index 00000000000..9287555a056
--- /dev/null
+++ b/src/test/ui/chalkify/lower_struct.rs
@@ -0,0 +1,18 @@
+// 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.
+
+#![feature(rustc_attrs)]
+
+#[rustc_dump_program_clauses] //~ ERROR program clause dump
+struct Foo<T> where Box<T>: Clone {
+    _x: std::marker::PhantomData<T>,
+}
+
+fn main() { }
diff --git a/src/test/ui/chalkify/lower_struct.stderr b/src/test/ui/chalkify/lower_struct.stderr
new file mode 100644
index 00000000000..d6cc9c8e9a4
--- /dev/null
+++ b/src/test/ui/chalkify/lower_struct.stderr
@@ -0,0 +1,12 @@
+error: program clause dump
+  --> $DIR/lower_struct.rs:13:1
+   |
+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).
+
+error: aborting due to previous error
+
diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.stderr b/src/test/ui/chalkify/lower_trait_higher_rank.stderr
index 7f6f503c6ff..ea275d647fa 100644
--- a/src/test/ui/chalkify/lower_trait_higher_rank.stderr
+++ b/src/test/ui/chalkify/lower_trait_higher_rank.stderr
@@ -4,10 +4,10 @@ error: program clause dump
 LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
-   = note: FromEnv(<F as std::ops::FnOnce<(&'a (u8, u16),)>>::Output == &'a u8) :- FromEnv(Self: Foo<F>).
    = 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>).
 
 error: aborting due to previous error