diff --git a/src/rules.rs b/src/rules.rs
index 92f20a53874..ff9d1963431 100644
--- a/src/rules.rs
+++ b/src/rules.rs
@@ -107,7 +107,7 @@ impl ImplDatum {
     /// Given `impl<T: Clone> Clone for Vec<T>`, generate:
     ///
     /// ```notrust
-    /// forall<T> { (Vec<T>: Clone) :- (T: Clone) }
+    /// forall<T> { Implemented(Vec<T>: Clone) :- Implemented(T: Clone) }
     /// ```
     fn to_program_clause(&self) -> ProgramClause {
         self.binders
@@ -137,9 +137,9 @@ impl DefaultImplDatum {
     ///
     /// ```notrust
     /// forall<T> {
-    ///     (MyList<T>: Send) :-
-    ///         (T: Send),
-    ///         (Box<Option<MyList<T>>>: Send)
+    ///     Implemented(MyList<T>: Send) :-
+    ///         Implemented(T: Send),
+    ///         Implemented(Box<Option<MyList<T>>>: Send)
     /// }
     /// ```
     fn to_program_clause(&self) -> ProgramClause {
@@ -179,8 +179,8 @@ impl AssociatedTyValue {
     /// ```notrust
     /// forall<'a, T> {
     ///     Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :-
-    ///         (Vec<T>: Iterable),  // (1)
-    ///         (Iter<'a, T>: 'a)    // (2)
+    ///         Implemented(Vec<T>: Iterable),  // (1)
+    ///         Implemented(Iter<'a, T>: 'a)    // (2)
     /// }
     /// ```
     ///
@@ -304,7 +304,7 @@ impl StructDatum {
         //
         // we generate the following clauses:
         //
-        //    forall<T> { WF(Foo<T>) :- (T: Eq). }
+        //    forall<T> { WF(Foo<T>) :- Implemented(T: Eq). }
         //    forall<T> { FromEnv(T: Eq) :- FromEnv(Foo<T>). }
         //    forall<T> { IsFullyVisible(Foo<T>) :- IsFullyVisible(T) }
         //
@@ -456,7 +456,7 @@ impl TraitDatum {
         // we generate the following clause:
         //
         //    forall<Self, T> {
-        //        WF(Self: Ord<T>) :- (Self: Ord<T>), WF(Self: Eq<T>)
+        //        WF(Self: Ord<T>) :- Implemented(Self: Ord<T>), WF(Self: Eq<T>)
         //    }
         //
         // and the reverse rules:
@@ -786,7 +786,7 @@ impl AssociatedTyDatum {
         // Well-formedness of projection type.
         //
         //    forall<Self> {
-        //        WellFormed((Foo::Assoc)<Self>) :- Self: Foo, WC.
+        //        WellFormed((Foo::Assoc)<Self>) :- Implemented(Self: Foo), WC.
         //    }
         clauses.push(
             Binders {
@@ -837,12 +837,23 @@ impl AssociatedTyDatum {
 
         // Reverse rule for implied bounds.
         //
-        //    forall<T> {
-        //        FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
+        //    forall<Self> {
+        //        FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), FromEnv(WC)
         //    }
         clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
             // Same as above in case of higher-ranked inline bounds.
             let shift = bound.binders.len();
+            let from_env_trait = iter::once(
+                FromEnv::Trait(trait_ref.clone()).shifted_in(shift).cast()
+            );
+
+            let where_clauses = self.where_clauses
+                .iter()
+                .cloned()
+                // `wc` may be a higher-ranked where clause
+                .map(|wc| wc.map(|value| value.into_from_env_goal()))
+                .casted();
+
             Binders {
                 binders: bound
                     .binders
@@ -852,7 +863,7 @@ impl AssociatedTyDatum {
                     .collect(),
                 value: ProgramClauseImplication {
                     consequence: bound.value.clone().into_from_env_goal(),
-                    conditions: vec![FromEnv::Trait(trait_ref.clone()).shifted_in(shift).cast()],
+                    conditions: from_env_trait.chain(where_clauses).collect(),
                 },
             }.cast()
         }));
diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs
index 0a5e62fa45b..7763c69a3a9 100644
--- a/src/rules/wf/test.rs
+++ b/src/rules/wf/test.rs
@@ -563,3 +563,78 @@ fn higher_ranked_inline_bound_on_gat() {
         }
     }
 }
+
+#[test]
+fn assoc_type_recursive_bound() {
+    lowering_error! {
+        program {
+            trait Sized { }
+            trait Print {
+                // fn print();
+            }
+
+            trait Foo {
+                type Item: Sized where <Self as Foo>::Item: Sized;
+            }
+
+            struct i32 { }
+            struct str { } // not sized
+
+            impl Foo for i32 {
+                // Well-formedness checks require that the following
+                // goal is true:
+                // ```
+                // if (str: Sized) { # if the where clauses hold
+                //     str: Sized # then the bound on the associated type hold
+                // }
+                // ```
+                // which it is :)
+                type Item = str;
+            }
+
+            struct OnlySized<T> where T: Sized { }
+            impl<T> Print for OnlySized<T> {
+                // fn print() {
+                //     println!("{}", std::mem::size_of::<T>());
+                // }
+            }
+
+            trait Bar {
+                type Assoc: Print;
+            }
+
+            impl<T> Bar for T where T: Foo {
+                type Assoc = OnlySized<<T as Foo>::Item>;
+            }
+
+            // Above, we used to incorrectly assume that `OnlySized<<T as Foo>::Item>`
+            // is well-formed because of the `FromEnv(T: Foo)`, hence making the `T: Bar`
+            // impl pass the well-formedness check. But the following query will
+            // (and should) always succeed, as there is no where clauses on `Assoc`:
+            // ```
+            // forall<T> { if (T: Bar) { WellFormed(<T as Bar>::Assoc) } }
+            // ```
+            //
+            // This may lead to the following code to compile:
+
+            // ```
+            // fn foo<T: Print>() {
+            //     T::print() // oops, in fact `T = OnlySized<str>` which is ill-formed
+            // }
+
+            // fn bar<T: Bar> {
+            //     // ok, we have `FromEnv(T: Bar)` hence 
+            //     // `<T as Bar>::Assoc` is well-formed and
+            //     // `Implemented(<T as Bar>::Assoc: Print)` hold
+            //     foo<<T as Bar>::Assoc>(
+            // }
+
+            // fn main() {
+            //     bar::<i32>() // ok, `Implemented(i32: Bar)` hold
+            // }
+            // ```
+        } error_msg {
+            "trait impl for \"Bar\" does not meet well-formedness requirements"
+        }
+    }
+}