diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs
index 65131ca7bb1..d6d15769a6b 100644
--- a/chalk-parse/src/ast.rs
+++ b/chalk-parse/src/ast.rs
@@ -87,7 +87,7 @@ pub struct TraitBound {
 pub struct ProjectionEqBound {
     pub trait_bound: TraitBound,
     pub name: Identifier,
-    pub parameters: Vec<Parameter>,
+    pub args: Vec<Parameter>,
     pub value: Ty,
 }
 
diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop
index a780d031658..fb8c0904010 100644
--- a/chalk-parse/src/parser.lalrpop
+++ b/chalk-parse/src/parser.lalrpop
@@ -109,7 +109,7 @@ ProjectionEqBound: ProjectionEqBound = {
             args_no_self: a.unwrap_or(vec![]),
         },
         name,
-        parameters: a2,
+        args: a2,
         value: ty,
     }
 };
diff --git a/src/fold.rs b/src/fold.rs
index bcd60778ed2..f0bbd17df2a 100644
--- a/src/fold.rs
+++ b/src/fold.rs
@@ -431,6 +431,7 @@ enum_fold!(Constraint[] { LifetimeEq(a, b) });
 enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Not(g),
                     Leaf(wc), CannotProve(a) });
 enum_fold!(ProgramClause[] { Implies(a), ForAll(a) });
+enum_fold!(InlineBound[] { TraitBound(a), ProjectionEqBound(a) });
 
 macro_rules! struct_fold {
     ($s:ident $([$($tt_args:tt)*])? { $($name:ident),* $(,)* } $($w:tt)*) => {
@@ -582,4 +583,16 @@ struct_fold!(ConstrainedSubst {
     constraints,
 });
 
+struct_fold!(TraitBound {
+    trait_id,
+    args_no_self,
+});
+
+struct_fold!(ProjectionEqBound {
+    trait_bound,
+    associated_ty_id,
+    parameters,
+    value,
+});
+
 // struct_fold!(ApplicationTy { name, parameters }); -- intentionally omitted, folded through Ty
diff --git a/src/ir.rs b/src/ir.rs
index b631f72c4b2..03b2f51fed5 100644
--- a/src/ir.rs
+++ b/src/ir.rs
@@ -5,6 +5,7 @@ use fold::shift::Shift;
 use lalrpop_intern::InternedString;
 use std::collections::{BTreeMap, BTreeSet};
 use std::sync::Arc;
+use std::iter;
 
 #[macro_use]
 mod macros;
@@ -259,6 +260,80 @@ pub struct TraitFlags {
     pub deref: bool,
 }
 
+/// An inline bound, e.g. `: Foo<K>` in `impl<K, T: Foo<K>> SomeType<T>`.
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub enum InlineBound {
+    TraitBound(TraitBound),
+    ProjectionEqBound(ProjectionEqBound),
+}
+
+impl InlineBound {
+    /// Applies the `InlineBound` to `self_ty` and lowers to a [`DomainGoal`].
+    /// 
+    /// Because an `InlineBound` does not know anything about what it's binding,
+    /// you must provide that type as `self_ty`.
+    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+        match self {
+            InlineBound::TraitBound(b) => b.lower_with_self(self_ty),
+            InlineBound::ProjectionEqBound(b) => b.lower_with_self(self_ty),
+        }
+    }
+}
+
+/// Represents a trait bound on e.g. a type or type parameter.
+/// Does not know anything about what it's binding.
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct TraitBound {
+    crate trait_id: ItemId,
+    crate args_no_self: Vec<Parameter>,
+}
+
+impl TraitBound {
+    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+        let trait_ref = self.as_trait_ref(self_ty);
+        vec![DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref))]
+    }
+
+    fn as_trait_ref(&self, self_ty: Ty) -> TraitRef {
+        let self_ty = ParameterKind::Ty(self_ty);
+        TraitRef {
+            trait_id: self.trait_id,
+            parameters: iter::once(self_ty).chain(self.args_no_self.iter().cloned()).collect(),
+        }
+    }
+}
+
+/// Represents a projection equality bound on e.g. a type or type parameter.
+/// Does not know anything about what it's binding.
+#[derive(Clone, Debug, PartialEq, Eq, Hash)]
+pub struct ProjectionEqBound {
+    crate trait_bound: TraitBound,
+    crate associated_ty_id: ItemId,
+    /// Does not include trait parameters.
+    crate parameters: Vec<Parameter>,
+    crate value: Ty,
+}
+
+impl ProjectionEqBound {
+    crate fn lower_with_self(&self, self_ty: Ty) -> Vec<DomainGoal> {
+        let trait_ref = self.trait_bound.as_trait_ref(self_ty);
+
+        let mut parameters = self.parameters.clone();
+        parameters.extend(trait_ref.parameters.clone());
+
+        vec![
+            DomainGoal::Holds(WhereClauseAtom::Implemented(trait_ref)),
+            DomainGoal::Holds(WhereClauseAtom::ProjectionEq(ProjectionEq {
+                projection: ProjectionTy {
+                    associated_ty_id: self.associated_ty_id,
+                    parameters: parameters,
+                },
+                ty: self.value.clone(),
+            }))
+        ]
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct AssociatedTyDatum {
     /// The trait this associated type is defined in.
@@ -274,12 +349,37 @@ pub struct AssociatedTyDatum {
     /// but possibly including more.
     crate parameter_kinds: Vec<ParameterKind<Identifier>>,
 
-    // FIXME: inline bounds on the associated ty need to be implemented
+    /// Bounds on the associated type itself.
+    ///
+    /// These must be proven by the implementer, for all possible parameters that
+    /// would result in a well-formed projection.
+    crate bounds: Vec<InlineBound>,
 
-    /// Where clauses that must hold for the projection be well-formed.
+    /// Where clauses that must hold for the projection to be well-formed.
     crate where_clauses: Vec<QuantifiedDomainGoal>,
 }
 
+impl AssociatedTyDatum {
+    /// Returns the associated ty's bounds applied to the projection type, e.g.:
+    ///
+    /// ```notrust
+    /// Implemented(<?0 as Foo>::Item<?1>: Sized)
+    /// ```
+    crate fn bounds_on_self(&self) -> Vec<DomainGoal> {
+        let parameters = self.parameter_kinds
+                             .anonymize()
+                             .iter()
+                             .zip(0..)
+                             .map(|p| p.to_parameter())
+                             .collect();
+        let self_ty = Ty::Projection(ProjectionTy {
+            associated_ty_id: self.id,
+            parameters
+        });
+        self.bounds.iter().flat_map(|b| b.lower_with_self(self_ty.clone())).collect()
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct AssociatedTyValue {
     crate associated_ty_id: ItemId,
@@ -612,7 +712,9 @@ impl DomainGoal {
     /// Same as `into_well_formed_goal` but with the `FromEnv` predicate instead of `WellFormed`.
     crate fn into_from_env_goal(self) -> DomainGoal {
         match self {
-            DomainGoal::Holds(wca) => DomainGoal::FromEnv(wca),
+            DomainGoal::Holds(wca @ WhereClauseAtom::Implemented(..)) => {
+                DomainGoal::FromEnv(wca)
+            }
             goal => goal,
         }
     }
diff --git a/src/ir/lowering.rs b/src/ir/lowering.rs
index e4c8ac4ba62..5a26041a00f 100644
--- a/src/ir/lowering.rs
+++ b/src/ir/lowering.rs
@@ -191,6 +191,7 @@ impl LowerProgram for Program {
                                 id: info.id,
                                 name: defn.name.str,
                                 parameter_kinds: parameter_kinds,
+                                bounds: defn.bounds.lower(&env)?,
                                 where_clauses: defn.where_clauses.lower(&env)?,
                             },
                         );
@@ -441,32 +442,37 @@ trait LowerWhereClause<T> {
 /// type in Rust and well-formedness checks.
 impl LowerWhereClause<ir::DomainGoal> for WhereClause {
     fn lower(&self, env: &Env) -> Result<Vec<ir::DomainGoal>> {
-        let goal = match self {
+        let goals = match self {
             WhereClause::Implemented { trait_ref } => {
-                ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
+                vec![ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))]
             }
             WhereClause::ProjectionEq {
                 projection,
                 ty,
-            } => ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq {
-                projection: projection.lower(env)?,
-                ty: ty.lower(env)?,
-            })),
+            } => vec![
+                ir::DomainGoal::Holds(ir::WhereClauseAtom::ProjectionEq(ir::ProjectionEq {
+                    projection: projection.lower(env)?,
+                    ty: ty.lower(env)?,
+                })),
+                ir::DomainGoal::Holds(ir::WhereClauseAtom::Implemented(
+                    projection.trait_ref.lower(env)?
+                )),
+            ],
             WhereClause::Normalize {
                 projection,
                 ty,
-            } => ir::DomainGoal::Normalize(ir::Normalize {
+            } => vec![ir::DomainGoal::Normalize(ir::Normalize {
                 projection: projection.lower(env)?,
                 ty: ty.lower(env)?,
-            }),
-            WhereClause::TyWellFormed { ty } => ir::DomainGoal::WellFormedTy(ty.lower(env)?),
-            WhereClause::TraitRefWellFormed { trait_ref } => {
+            })],
+            WhereClause::TyWellFormed { ty } => vec![ir::DomainGoal::WellFormedTy(ty.lower(env)?)],
+            WhereClause::TraitRefWellFormed { trait_ref } => vec![
                 ir::DomainGoal::WellFormed(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
-            }
-            WhereClause::TyFromEnv { ty } => ir::DomainGoal::FromEnvTy(ty.lower(env)?),
-            WhereClause::TraitRefFromEnv { trait_ref } => {
+            ],
+            WhereClause::TyFromEnv { ty } => vec![ir::DomainGoal::FromEnvTy(ty.lower(env)?)],
+            WhereClause::TraitRefFromEnv { trait_ref } => vec![
                 ir::DomainGoal::FromEnv(ir::WhereClauseAtom::Implemented(trait_ref.lower(env)?))
-            }
+            ],
             WhereClause::UnifyTys { .. } | WhereClause::UnifyLifetimes { .. } => {
                 bail!("this form of where-clause not allowed here")
             }
@@ -480,19 +486,19 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
                     bail!(ErrorKind::NotTrait(trait_name));
                 }
 
-                ir::DomainGoal::InScope(id)
+                vec![ir::DomainGoal::InScope(id)]
             }
-            WhereClause::Derefs { source, target } => {
+            WhereClause::Derefs { source, target } => vec![
                 ir::DomainGoal::Derefs(ir::Derefs {
                     source: source.lower(env)?,
                     target: target.lower(env)?
                 })
-            }
-            WhereClause::TyIsLocal { ty } => {
+            ],
+            WhereClause::TyIsLocal { ty } => vec![
                 ir::DomainGoal::IsLocalTy(ty.lower(env)?)
-            }
+            ],
         };
-        Ok(vec![goal])
+        Ok(goals)
     }
 }
 
@@ -638,6 +644,107 @@ impl LowerTraitRef for TraitRef {
     }
 }
 
+trait LowerTraitBound {
+    fn lower_trait_bound(&self, env: &Env) -> Result<ir::TraitBound>;
+}
+
+impl LowerTraitBound for TraitBound {
+    fn lower_trait_bound(&self, env: &Env) -> Result<ir::TraitBound> {
+        let id = match env.lookup(self.trait_name)? {
+            NameLookup::Type(id) => id,
+            NameLookup::Parameter(_) => bail!(ErrorKind::NotTrait(self.trait_name)),
+        };
+
+        let k = env.type_kind(id);
+        if k.sort != ir::TypeSort::Trait {
+            bail!(ErrorKind::NotTrait(self.trait_name));
+        }
+
+        let parameters = self.args_no_self
+                             .iter()
+                             .map(|a| Ok(a.lower(env)?))
+                             .collect::<Result<Vec<_>>>()?;
+
+        if parameters.len() != k.binders.len() {
+            bail!(
+                "wrong number of parameters, expected `{:?}`, got `{:?}`",
+                k.binders.len(),
+                parameters.len()
+            )
+        }
+
+        for (binder, param) in k.binders.binders.iter().zip(parameters.iter()) {
+            check_type_kinds("incorrect kind for trait parameter", binder, param)?;
+        }
+
+        Ok(ir::TraitBound {
+            trait_id: id,
+            args_no_self: parameters,
+        })
+    }
+}
+
+trait LowerInlineBound {
+    fn lower(&self, env: &Env) -> Result<ir::InlineBound>;
+}
+
+impl LowerInlineBound for TraitBound {
+    fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
+        Ok(ir::InlineBound::TraitBound(self.lower_trait_bound(&env)?))
+    }
+}
+
+impl LowerInlineBound for ProjectionEqBound {
+    fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
+        let trait_bound = self.trait_bound.lower_trait_bound(env)?;
+        let info = match env.associated_ty_infos.get(&(trait_bound.trait_id, self.name.str)) {
+            Some(info) => info,
+            None => bail!("no associated type `{}` defined in trait", self.name.str),
+        };
+        let args: Vec<_> = try!(self.args.iter().map(|a| a.lower(env)).collect());
+
+        if args.len() != info.addl_parameter_kinds.len() {
+            bail!(
+                "wrong number of parameters for associated type (expected {}, got {})",
+                info.addl_parameter_kinds.len(),
+                args.len()
+            )
+        }
+
+        for (param, arg) in info.addl_parameter_kinds.iter().zip(args.iter()) {
+            check_type_kinds("incorrect kind for associated type parameter", param, arg)?;
+        }
+
+        Ok(ir::InlineBound::ProjectionEqBound(ir::ProjectionEqBound {
+            trait_bound,
+            associated_ty_id: info.id,
+            parameters: args,
+            value: self.value.lower(env)?,
+        }))
+    }
+}
+
+impl LowerInlineBound for InlineBound {
+    fn lower(&self, env: &Env) -> Result<ir::InlineBound> {
+        match self {
+            InlineBound::TraitBound(b) => b.lower(&env),
+            InlineBound::ProjectionEqBound(b) => b.lower(&env),
+        }
+    }
+}
+
+trait LowerInlineBounds {
+    fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>>;
+}
+
+impl LowerInlineBounds for Vec<InlineBound> {
+    fn lower(&self, env: &Env) -> Result<Vec<ir::InlineBound>> {
+        self.iter()
+            .map(|b| b.lower(env))
+            .collect()
+    }
+}
+
 trait LowerPolarizedTraitRef {
     fn lower(&self, env: &Env) -> Result<ir::PolarizedTraitRef>;
 }
diff --git a/src/ir/lowering/test.rs b/src/ir/lowering/test.rs
index 01e90afb944..d5019bba568 100644
--- a/src/ir/lowering/test.rs
+++ b/src/ir/lowering/test.rs
@@ -228,7 +228,14 @@ fn atc_accounting() {
         println!("{}", goal_text);
         assert_eq!(
             goal_text,
-            "ForAll<type> { ForAll<lifetime> { ForAll<type> { ProjectionEq(<?2 as Iterable>::Iter<'?1> = ?0) } } }"
+            "ForAll<type> { \
+                ForAll<lifetime> { \
+                    ForAll<type> { \
+                        (ProjectionEq(<?2 as Iterable>::Iter<'?1> = ?0), \
+                        Implemented(?2: Iterable)) \
+                    } \
+                } \
+            }"
         );
     });
 }
@@ -308,6 +315,7 @@ fn gat_parse() {
     lowering_success! {
         program {
             trait Sized {}
+            trait Clone {}
 
             trait Foo {
                 type Item<'a, T>: Sized + Clone where Self: Sized;
@@ -372,6 +380,33 @@ fn duplicate_parameters() {
 }
 
 #[test]
+fn external_items() {
+    lowering_success! {
+        program {
+            extern trait Send { }
+            extern struct Vec<T> { }
+        }
+    }
+}
+
+#[test]
+fn deref_trait() {
+    lowering_success! {
+        program {
+            #[lang_deref] trait Deref { type Target; }
+        }
+    }
+
+    lowering_error! {
+        program {
+            #[lang_deref] trait Deref { }
+            #[lang_deref] trait DerefDupe { }
+        } error_msg {
+            "Duplicate lang item `DerefTrait`"
+        }
+    }
+}
+
 fn fundamental_multiple_type_parameters() {
     lowering_error! {
         program {
diff --git a/src/rules.rs b/src/rules.rs
index 990198abc3b..26b4bfd9b6f 100644
--- a/src/rules.rs
+++ b/src/rules.rs
@@ -1,6 +1,8 @@
 use cast::{Cast, Caster};
 use fold::shift::Shift;
+use fold::Subst;
 use ir::{self, ToParameter};
+use std::iter;
 
 mod default;
 mod wf;
@@ -181,26 +183,45 @@ impl ir::AssociatedTyValue {
         program: &ir::Program,
         impl_datum: &ir::ImplDatum,
     ) -> Vec<ir::ProgramClause> {
+        let associated_ty = &program.associated_ty_data[&self.associated_ty_id];
+
         // Begin with the innermost parameters (`'a`) and then add those from impl (`T`).
         let all_binders: Vec<_> = self.value
             .binders
             .iter()
+            .chain(impl_datum.binders.binders.iter())
             .cloned()
-            .chain(impl_datum.binders.binders.iter().cloned())
             .collect();
 
+        let impl_trait_ref = impl_datum.binders
+                                       .value
+                                       .trait_ref
+                                       .trait_ref()
+                                       .up_shift(self.value.len());
+
+        let all_parameters: Vec<_> =
+            self.value.binders
+                      .iter()
+                      .zip(0..)
+                      .map(|p| p.to_parameter())
+                      .chain(impl_trait_ref.parameters.iter().cloned())
+                      .collect();
+
         // Assemble the full list of conditions for projection to be valid.
         // This comes in two parts, marked as (1) and (2) in example above:
         //
         // 1. require that the trait is implemented
         // 2. any where-clauses from the `type` declaration in the impl
-        let impl_trait_ref = impl_datum
-            .binders
-            .value
-            .trait_ref
-            .trait_ref()
-            .up_shift(self.value.len());
-        let conditions: Vec<ir::Goal> = vec![impl_trait_ref.clone().cast()];
+        let where_clauses =
+            associated_ty.where_clauses
+                         .iter()
+                         .map(|wc| Subst::apply(&all_parameters, wc))
+                         .casted();
+
+        let conditions: Vec<ir::Goal> =
+            where_clauses
+            .chain(Some(impl_trait_ref.clone().cast()))
+            .collect();
 
         // Bound parameters + `Self` type of the trait-ref
         let parameters: Vec<_> = {
@@ -216,7 +237,7 @@ impl ir::AssociatedTyValue {
         let projection = ir::ProjectionTy {
             associated_ty_id: self.associated_ty_id,
 
-            // Add the remaining parameters of the trait-ref if any
+            // Add the remaining parameters of the trait-ref, if any
             parameters: parameters.iter()
                                   .chain(&impl_trait_ref.parameters[1..])
                                   .cloned()
@@ -233,14 +254,12 @@ impl ir::AssociatedTyValue {
             binders: all_binders.clone(),
             value: ir::ProgramClauseImplication {
                 consequence: normalize_goal.clone(),
-                conditions: conditions.clone(),
+                conditions: conditions,
             },
         }.cast();
 
         let unselected_projection = ir::UnselectedProjectionTy {
-            type_name: program.associated_ty_data[&self.associated_ty_id]
-                .name
-                .clone(),
+            type_name: associated_ty.name.clone(),
             parameters: parameters,
         };
 
@@ -443,23 +462,22 @@ impl ir::AssociatedTyDatum {
         // equality" rules. There are always two; one for a successful normalization,
         // and one for the "fallback" notion of equality.
         //
-        // Given:
+        // Given: (here, `'a` and `T` represent zero or more parameters)
         //
         //    trait Foo {
-        //        type Assoc;
+        //        type Assoc<'a, T>: Bounds where WC;
         //    }
         //
         // we generate the 'fallback' rule:
         //
-        //    forall<T> {
-        //        ProjectionEq(<T as Foo>::Assoc = (Foo::Assoc)<T>) :-
-        //            T: Foo
+        //    forall<Self, 'a, T> {
+        //        ProjectionEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>).
         //    }
         //
         // and
         //
-        //    forall<T> {
-        //        ProjectionEq(<T as Foo>::Assoc = U) :-
+        //    forall<Self, 'a, T, U> {
+        //        ProjectionEq(<T as Foo>::Assoc<'a, T> = U) :-
         //            Normalize(<T as Foo>::Assoc -> U)
         //    }
         //
@@ -506,106 +524,113 @@ impl ir::AssociatedTyDatum {
         };
         let app_ty = ir::Ty::Apply(app);
 
-        let mut clauses = vec![];
+        let projection_eq = ir::ProjectionEq {
+            projection: projection.clone(),
+            ty: app_ty.clone(),
+        };
 
-        //    forall<T> {
-        //        ProjectionEq(<T as Foo>::Assoc = (Foo::Assoc)<T>) :-
-        //            T: Foo
-        //    }
-        clauses.push(ir::Binders {
-            binders: binders.clone(),
-            value: ir::ProgramClauseImplication {
-                consequence: ir::ProjectionEq {
-                    projection: projection.clone(),
-                    ty: app_ty.clone(),
-                }.cast(),
-                conditions: vec![trait_ref.clone().cast()],
-            },
-        }.cast());
+        let mut clauses = vec![];
 
-        // The above application type is always well-formed, and `<T as Foo>::Assoc` will
-        // unify with `(Foo::Assoc)<T>` only if `T: Foo`, because of the above rule, so we have:
+        // Fallback rule. The solver uses this to move between the projection
+        // and skolemized type.
         //
-        //    forall<T> {
-        //        WellFormed((Foo::Assoc)<T>).
+        //    forall<Self> {
+        //        ProjectionEq(<Self as Foo>::Assoc = (Foo::Assoc)<Self>).
         //    }
         clauses.push(ir::Binders {
             binders: binders.clone(),
             value: ir::ProgramClauseImplication {
-                consequence: ir::DomainGoal::WellFormedTy(app_ty).cast(),
+                consequence: projection_eq.clone().cast(),
                 conditions: vec![],
             },
         }.cast());
 
-        // add new type parameter U
-        let mut binders = binders;
-        binders.push(ir::ParameterKind::Ty(()));
-        let ty = ir::Ty::Var(binders.len() - 1);
-
-        // `Normalize(<T as Foo>::Assoc -> U)`
-        let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() };
-
-        // `ProjectionEq(<T as Foo>::Assoc = U)`
-        let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty };
-
-        //    forall<T> {
-        //        ProjectionEq(<T as Foo>::Assoc = U) :-
-        //            Normalize(<T as Foo>::Assoc -> U)
+        // Well-formedness of projection type.
+        //
+        //    forall<Self> {
+        //        WellFormed((Foo::Assoc)<Self>) :- Self: Foo, WC.
         //    }
         clauses.push(ir::Binders {
             binders: binders.clone(),
             value: ir::ProgramClauseImplication {
-                consequence: projection_eq.clone().cast(),
-                conditions: vec![normalize.clone().cast()],
+                consequence: ir::DomainGoal::WellFormedTy(app_ty.clone()).cast(),
+                conditions: iter::once(trait_ref.clone().cast())
+                                .chain(self.where_clauses.iter().cloned().casted())
+                                .collect(),
             },
         }.cast());
 
-
-        let projection_wc = ir::WhereClauseAtom::ProjectionEq(projection_eq.clone());
-        let trait_ref_wc = ir::WhereClauseAtom::Implemented(trait_ref.clone());
-
-        // We generate a proxy rule for the well-formedness of `T: Foo<Assoc = U>` which really
-        // means two things: `T: Foo` and `Normalize(<T as Foo>::Assoc -> U)`. So we have the
-        // following rule:
+        // Assuming well-formedness of projection type means we can assume
+        // the trait ref as well. Mostly used in function bodies.
         //
-        //    forall<T> {
-        //        WellFormed(T: Foo<Assoc = U>) :-
-        //            WellFormed(T: Foo), ProjectionEq(<T as Foo>::Assoc = U)
+        //    forall<Self> {
+        //        FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>).
         //    }
         clauses.push(ir::Binders {
             binders: binders.clone(),
             value: ir::ProgramClauseImplication {
-                consequence: ir::DomainGoal::WellFormed(projection_wc.clone()),
-                conditions: vec![
-                    ir::DomainGoal::WellFormed(trait_ref_wc.clone()).cast(),
-                    projection_eq.clone().cast()
-                ],
+                consequence: ir::DomainGoal::FromEnv(trait_ref.clone().cast()),
+                conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).cast()],
             }
         }.cast());
 
-        // We also have two proxy reverse rules, the first one being:
+        // Reverse rule for where clauses.
         //
-        //    forall<T> {
-        //        FromEnv(T: Foo) :- FromEnv(T: Foo<Assoc = U>)
+        //    forall<Self> {
+        //        FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>).
         //    }
-        clauses.push(ir::Binders {
-            binders: binders.clone(),
-            value: ir::ProgramClauseImplication {
-                consequence: ir::DomainGoal::FromEnv(trait_ref_wc).cast(),
-                conditions: vec![ir::DomainGoal::FromEnv(projection_wc.clone()).cast()],
-            },
-        }.cast());
+        //
+        // This is really a family of clauses, one for each where clause.
+        clauses.extend(self.where_clauses.iter().map(|wc| {
+            let shift = wc.binders.len();
+            ir::Binders {
+                binders: wc.binders.iter().chain(binders.iter()).cloned().collect(),
+                value: ir::ProgramClauseImplication {
+                    consequence: wc.value.clone().into_from_env_goal(),
+                    conditions: vec![ir::DomainGoal::FromEnvTy(app_ty.clone()).up_shift(shift).cast()],
+                }
+            }.cast()
+        }));
 
-        // And the other one being:
+        // Reverse rule for implied bounds.
         //
         //    forall<T> {
-        //        ProjectionEq(<T as Foo>::Assoc = U) :- FromEnv(T: Foo<Assoc = U>)
+        //        FromEnv(<T as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo)
+        //    }
+        clauses.extend(self.bounds_on_self().into_iter().map(|bound| {
+            ir::Binders {
+                binders: binders.clone(),
+                value: ir::ProgramClauseImplication {
+                    consequence: bound.into_from_env_goal(),
+                    conditions: vec![
+                        ir::DomainGoal::FromEnv(trait_ref.clone().cast()).cast()
+                    ],
+                }
+            }.cast()
+        }));
+
+        // add new type parameter U
+        let mut binders = binders;
+        binders.push(ir::ParameterKind::Ty(()));
+        let ty = ir::Ty::Var(binders.len() - 1);
+
+        // `Normalize(<T as Foo>::Assoc -> U)`
+        let normalize = ir::Normalize { projection: projection.clone(), ty: ty.clone() };
+
+        // `ProjectionEq(<T as Foo>::Assoc = U)`
+        let projection_eq = ir::ProjectionEq { projection: projection.clone(), ty };
+
+        // Projection equality rule from above.
+        //
+        //    forall<T, U> {
+        //        ProjectionEq(<T as Foo>::Assoc = U) :-
+        //            Normalize(<T as Foo>::Assoc -> U).
         //    }
         clauses.push(ir::Binders {
-            binders,
+            binders: binders.clone(),
             value: ir::ProgramClauseImplication {
                 consequence: projection_eq.clone().cast(),
-                conditions: vec![ir::DomainGoal::FromEnv(projection_wc).cast()],
+                conditions: vec![normalize.clone().cast()],
             },
         }.cast());
 
diff --git a/src/rules/wf.rs b/src/rules/wf.rs
index b48851bb2ec..ddf4a83805a 100644
--- a/src/rules/wf.rs
+++ b/src/rules/wf.rs
@@ -5,6 +5,8 @@ use errors::*;
 use cast::*;
 use solve::SolverChoice;
 use itertools::Itertools;
+use fold::*;
+use fold::shift::Shift;
 
 mod test;
 
@@ -209,13 +211,11 @@ impl WfSolver {
         let mut input_types = Vec::new();
         impl_datum.binders.value.where_clauses.fold(&mut input_types);
 
-        // We partition the input types of the type on which we implement the trait in two categories:
-        // * projection types, e.g. `<T as Iterator>::Item`: we will have to prove that these types
-        //   are well-formed, e.g. that we can show that `T: Iterator` holds
-        // * any other types, e.g. `HashSet<K>`: we will *assume* that these types are well-formed, e.g.
-        //   we will be able to derive that `K: Hash` holds without writing any where clause.
+        // We retrieve all the input types of the type on which we implement the trait: we will
+        // *assume* that these types are well-formed, e.g. we will be able to derive that
+        // `K: Hash` holds without writing any where clause.
         //
-        // Examples:
+        // Example:
         // ```
         // struct HashSet<K> where K: Hash { ... }
         //
@@ -223,24 +223,8 @@ impl WfSolver {
         //     // Inside here, we can rely on the fact that `K: Hash` holds
         // }
         // ```
-        //
-        // ```
-        // impl<T> Foo for <T as Iterator>::Item {
-        //     // The impl is not well-formed, as an exception we do not assume that
-        //     // `<T as Iterator>::Item` is well-formed and instead want to prove it.
-        // }
-        // ```
-        //
-        // ```
-        // impl<T> Foo for <T as Iterator>::Item where T: Iterator {
-        //     // Now ok.
-        // }
-        // ```
         let mut header_input_types = Vec::new();
         trait_ref.fold(&mut header_input_types);
-        let (header_projection_types, header_other_types): (Vec<_>, Vec<_>) =
-            header_input_types.into_iter()
-                              .partition(|ty| ty.is_projection());
 
         // Associated type values are special because they can be parametric (independently of
         // the impl), so we issue a special goal which is quantified using the binders of the
@@ -256,16 +240,54 @@ impl WfSolver {
         // ```
         // we would issue the following subgoal: `forall<'a> { WellFormed(Box<&'a T>) }`.
         let compute_assoc_ty_goal = |assoc_ty: &AssociatedTyValue| {
+            let assoc_ty_datum = &self.env.associated_ty_data[&assoc_ty.associated_ty_id];
+            let bounds = &assoc_ty_datum.bounds;
+
             let mut input_types = Vec::new();
             assoc_ty.value.value.ty.fold(&mut input_types);
 
-            if input_types.is_empty() {
-                return None;
-            }
+            let wf_goals =
+                input_types.into_iter()
+                           .map(|ty| DomainGoal::WellFormedTy(ty));
+            
+            let trait_ref = trait_ref.up_shift(assoc_ty.value.binders.len());
+
+            let all_parameters: Vec<_> =
+                assoc_ty.value.binders.iter()
+                                      .zip(0..)
+                                      .map(|p| p.to_parameter())
+                                      .chain(trait_ref.parameters.iter().cloned())
+                                      .collect();
+
+            // Add bounds from the trait. Because they are defined on the trait,
+            // their parameters must be substituted with those of the impl.
+            let bound_goals =
+                bounds.iter()
+                      .map(|b| Subst::apply(&all_parameters, b))
+                      .flat_map(|b| b.lower_with_self(assoc_ty.value.value.ty.clone()))
+                      .map(|g| g.into_well_formed_goal());
+            
+            let goals = wf_goals.chain(bound_goals).casted();
+            let goal = match goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf))) {
+                Some(goal) => goal,
+                None => return None,
+            };
+
+            // Add where clauses from the associated ty definition. We must
+            // substitute parameters here, like we did with the bounds above.
+            let hypotheses =
+                assoc_ty_datum.where_clauses
+                              .iter()
+                              .map(|wc| Subst::apply(&all_parameters, wc))
+                              .map(|wc| wc.map(|bound| bound.into_from_env_goal()))
+                              .casted()
+                              .collect();
+
+            let goal = Goal::Implies(
+                hypotheses,
+                Box::new(goal)
+            );
 
-            let goals = input_types.into_iter().map(|ty| DomainGoal::WellFormedTy(ty).cast());
-            let goal = goals.fold1(|goal, leaf| Goal::And(Box::new(goal), Box::new(leaf)))
-                            .expect("at least one goal");
             Some(goal.quantify(QuantifierKind::ForAll, assoc_ty.value.binders.clone()))
         };
 
@@ -283,7 +305,6 @@ impl WfSolver {
         );
         let goals =
             input_types.into_iter()
-                       .chain(header_projection_types.into_iter())
                        .map(|ty| DomainGoal::WellFormedTy(ty).cast())
                        .chain(assoc_ty_goals)
                        .chain(Some(trait_ref_wf).cast());
@@ -302,12 +323,14 @@ impl WfSolver {
                       .cloned()
                       .map(|wc| wc.map(|bound| bound.into_from_env_goal()))
                       .casted()
-                      .chain(header_other_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
+                      .chain(header_input_types.into_iter().map(|ty| DomainGoal::FromEnvTy(ty).cast()))
                       .collect();
 
         let goal = Goal::Implies(hypotheses, Box::new(goal))
             .quantify(QuantifierKind::ForAll, impl_datum.binders.binders.clone());
 
+        debug!("WF trait goal: {:?}", goal);
+
         match self.solver_choice.solve_root_goal(&self.env, &goal.into_closed_goal()).unwrap() {
             Some(sol) => sol.is_unique(),
             None => false,
diff --git a/src/rules/wf/test.rs b/src/rules/wf/test.rs
index e190caae516..befb4214e89 100644
--- a/src/rules/wf/test.rs
+++ b/src/rules/wf/test.rs
@@ -217,7 +217,7 @@ fn projection_type_in_header() {
 
             // Projection types in an impl header are not assumed to be well-formed,
             // an explicit where clause is needed (see below).
-            impl<T> Bar for <T as Foo>::Value { }
+            impl<T> Bar for T where <T as Foo>::Value: Bar { }
         } error_msg {
             "trait impl for \"Bar\" does not meet well-formedness requirements"
         }
@@ -231,17 +231,209 @@ fn projection_type_in_header() {
 
             trait Bar { }
 
-            impl<T> Bar for <T as Foo>::Value where T: Foo { }
+            impl<T> Bar for T where T: Foo, <T as Foo>::Value: Bar { }
         }
     }
 }
 
 #[test]
-fn external_items() {
+fn bound_in_header_from_env() {
     lowering_success! {
         program {
-            extern trait Send { }
-            extern struct Vec<T> { }
+            trait Foo { }
+
+            trait Bar {
+                type Item: Foo;
+            }
+
+            struct Stuff<T> { }
+
+            impl<T> Bar for Stuff<T> where T: Foo {
+                // Should have FromEnv(T: Foo) here.
+                type Item = T;
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Foo { }
+            trait Baz { }
+
+            trait Bar {
+                type Item: Baz;
+            }
+
+            struct Stuff<T> { }
+
+            impl<T> Bar for Stuff<T> where T: Foo {
+                // No T: Baz here.
+                type Item = T;
+            }
+        } error_msg {
+            "trait impl for \"Bar\" does not meet well-formedness requirements"
+        }
+    }
+}
+
+#[test]
+fn mixed_indices_check_projection_bounds() {
+    lowering_success! {
+        program {
+            trait Foo<T> { }
+
+            trait Bar<T> {
+                type Item: Foo<T>;
+            }
+
+            struct Stuff<T, U> { }
+
+            impl<T, U> Bar<T> for Stuff<T, U> where U: Foo<T> {
+                type Item = U;
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Foo<T> { }
+            trait Baz<T> { }
+
+            trait Bar<T> {
+                type Item: Baz<T>;
+            }
+
+            struct Stuff<T, U> { }
+
+            impl<T, U> Bar<T> for Stuff<T, U> where U: Foo<T> {
+                type Item = U;
+            }
+        } error_msg {
+            "trait impl for \"Bar\" does not meet well-formedness requirements"
+        }
+    }
+}
+
+#[test]
+fn mixed_indices_check_generic_projection_bounds() {
+    lowering_success! {
+        program {
+            struct Stuff<T, U> { }
+
+            trait Foo<T> { }
+
+            // A type that impls Foo<T> as long as U: Foo<T>.
+            struct Fooey<U, V> { }
+            impl<T, U, V> Foo<T> for Fooey<U, V> where U: Foo<T> { }
+
+            trait Bar<T> {
+                type Item<V>: Foo<T> where V: Foo<T>;
+            }
+
+            impl<T, U> Bar<T> for Stuff<T, U> where U: Foo<T> {
+                type Item<V> = Fooey<U, V>;
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            struct Stuff<T, U> { }
+
+            trait Foo<T> { }
+            trait Baz<T> { }
+
+            // A type that impls Foo<T> as long as U: Foo<T>.
+            struct Fooey<U, V> { }
+            impl<T, U, V> Foo<T> for Fooey<U, V> where U: Foo<T> { }
+
+            trait Bar<T> {
+                type Item<V>: Baz<T> where V: Foo<T>;
+            }
+
+            impl<T, U> Bar<T> for Stuff<T, U> where U: Foo<T> {
+                type Item<V> = Fooey<U, V>;
+            }
+        } error_msg {
+            "trait impl for \"Bar\" does not meet well-formedness requirements"
+        }
+    }
+}
+
+#[test]
+fn generic_projection_where_clause() {
+    lowering_success! {
+        program {
+            trait PointerFamily { type Pointer<T>; }
+
+            struct Cow<T> { }
+            struct CowFamily { }
+            impl PointerFamily for CowFamily { type Pointer<T> = Cow<T>; }
+
+            struct String { }
+            struct Foo<P> where P: PointerFamily {
+                bar: <P as PointerFamily>::Pointer<String>
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Copy { }
+            trait PointerFamily { type Pointer<T> where T: Copy; }
+
+            struct Cow<T> { }
+            struct CowFamily { }
+            impl PointerFamily for CowFamily { type Pointer<T> = Cow<T>; }
+
+            struct String { }
+            struct Foo<P> where P: PointerFamily {
+                // No impl Copy for String, so this will fail.
+                bar: <P as PointerFamily>::Pointer<String>
+            }
+        } error_msg {
+            "type declaration \"Foo\" does not meet well-formedness requirements"
+        }
+    }
+}
+
+#[test]
+fn generic_projection_bound() {
+    lowering_success! {
+        program {
+            trait Clone { }
+            trait PointerFamily { type Pointer<T>: Clone where T: Clone; }
+
+            struct Cow<T> { }
+            impl<T> Clone for Cow<T> where T: Clone { }
+
+            struct CowFamily { }
+
+            // impl is WF due because of:
+            // - `where T: Clone` clause on PointerFamily::Pointer<T>
+            // - impl<T> Clone for Cow<T> where T: Clone
+            impl PointerFamily for CowFamily { type Pointer<T> = Cow<T>; }
+
+            struct String { }
+            impl Clone for String { }
+            struct Foo<P> where P: PointerFamily {
+                bar: <P as PointerFamily>::Pointer<String>
+            }
+        }
+    }
+
+    lowering_error! {
+        program {
+            trait Clone { }
+            trait PointerFamily { type Pointer<T>: Clone where T: Clone; }
+
+            struct Cow<T> { }
+            struct CowFamily { }
+
+            // No impl Clone for Cow<T>, so this will fail.
+            impl PointerFamily for CowFamily { type Pointer<T> = Cow<T>; }
+        } error_msg {
+            "trait impl for \"PointerFamily\" does not meet well-formedness requirements"
         }
     }
 }
@@ -272,6 +464,24 @@ fn higher_ranked_trait_bounds() {
     }
 }
 
+#[test]
+fn higher_ranked_trait_bound_on_gat() {
+    lowering_success! {
+        program {
+            trait Foo<'a> { }
+            struct i32 { }
+
+            trait Bar<'a> {
+                type Item<V>: Foo<'a> where forall<'b> V: Foo<'b>;
+            }
+
+            impl<'a> Bar<'a> for i32 {
+                type Item<V> = V;
+            }
+        }
+    }
+}
+
 // See `cyclic_traits`, this is essentially the same but with higher-ranked co-inductive WF goals.
 #[test]
 fn higher_ranked_cyclic_requirements() {
@@ -309,21 +519,3 @@ fn higher_ranked_cyclic_requirements() {
         }
     }
 }
-
-#[test]
-fn deref_trait() {
-    lowering_success! {
-        program {
-            #[lang_deref] trait Deref { type Target; }
-        }
-    }
-
-    lowering_error! {
-        program {
-            #[lang_deref] trait Deref { }
-            #[lang_deref] trait DerefDupe { }
-        } error_msg {
-            "Duplicate lang item `DerefTrait`"
-        }
-    }
-}
diff --git a/src/solve/test.rs b/src/solve/test.rs
index 487e6ee7c0d..db5e4b26348 100644
--- a/src/solve/test.rs
+++ b/src/solve/test.rs
@@ -547,7 +547,200 @@ fn normalize_basic() {
 }
 
 #[test]
-fn normalize_implied_bound() {
+fn normalize_gat1() {
+    test! {
+        program {
+            struct Vec<T> { }
+
+            trait Iterable {
+                type Iter<'a>;
+            }
+
+            impl<T> Iterable for Vec<T> {
+                type Iter<'a> = Iter<'a, T>;
+            }
+
+            trait Iterator {
+                type Item;
+            }
+
+            struct Iter<'a, T> { }
+            struct Ref<'a, T> { }
+
+            impl<'a, T> Iterator for Iter<'a, T> {
+                type Item = Ref<'a, T>;
+            }
+        }
+
+        goal {
+            forall<T> {
+                forall<'a> {
+                    exists<U> {
+                        Normalize(<Vec<T> as Iterable>::Iter<'a> -> U)
+                    }
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn normalize_gat2() {
+    test! {
+        program {
+            trait StreamingIterator<T> { type Item<'a>; }
+            struct Span<'a, T> { }
+            struct StreamIterMut<T> { }
+            struct u32 { }
+            impl<T> StreamingIterator<T> for StreamIterMut<T> {
+                type Item<'a> = Span<'a, T>;
+            }
+        }
+
+        goal {
+            forall<'a, T> {
+                exists<U> {
+                    Normalize(<StreamIterMut<T> as StreamingIterator<T>>::Item<'a> -> U)
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := Span<'!1, !2>], lifetime constraints []"
+        }
+
+        goal {
+            forall<'a, T> {
+                <StreamIterMut<T> as StreamingIterator<T>>::Item<'a> = Span<'a, T>
+            }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+
+        goal {
+            forall<'a, T, U> {
+                if (T: StreamingIterator<U, Item<'a> = Span<'a, U>>) {
+                    <T as StreamingIterator<U>>::Item<'a> = Span<'a, U>
+                }
+            }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn normalize_gat_with_where_clause() {
+    test! {
+        program {
+            trait Sized { }
+            trait Foo {
+                type Item<T> where T: Sized;
+            }
+
+            struct Value<T> { }
+            struct Sometype { }
+            impl Foo for Sometype {
+                type Item<T> = Value<T>;
+            }
+        }
+
+        goal {
+            forall<T> {
+                exists<U> {
+                    Normalize(<Sometype as Foo>::Item<T> -> U)
+                }
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<T> {
+                exists<U> {
+                    if (T: Sized) {
+                        Normalize(<Sometype as Foo>::Item<T> -> U)
+                    }
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := Value<!1>]"
+        }
+    }
+}
+
+#[test]
+fn normalize_gat_with_where_clause2() {
+    test! {
+        program {
+            trait Bar<T> { }
+            trait Foo<T> {
+                type Item<U> where U: Bar<T>;
+            }
+
+            struct i32 { }
+            impl<T> Foo<T> for i32 {
+                type Item<U> = U;
+            }
+        }
+
+        goal {
+            forall<T, U> {
+                exists<V> {
+                    Normalize(<i32 as Foo<T>>::Item<U> -> V)
+                }
+            }
+        } yields {
+            "No possible solution"
+        }
+
+        goal {
+            forall<T, U> {
+                exists<V> {
+                    if (U: Bar<T>) {
+                        Normalize(<i32 as Foo<T>>::Item<U> -> V)
+                    }
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := !2]"
+        }
+    }
+}
+
+#[test]
+fn normalize_gat_with_higher_ranked_trait_bound() {
+    test! {
+        program {
+            trait Foo<'a, T> { }
+            struct i32 { }
+
+            trait Bar<'a, T> {
+                type Item<V>: Foo<'a, T> where forall<'b> V: Foo<'b, T>;
+            }
+
+            impl<'a, T> Foo<'a, T> for i32 { }
+            impl<'a, T> Bar<'a, T> for i32 {
+                type Item<V> = i32;
+            }
+        }
+
+        goal {
+            forall<'a, T, V> {
+                if (forall<'b> { V: Foo<'b, T> }) {
+                    exists<U> {
+                        Normalize(<i32 as Bar<'a, T>>::Item<V> -> U)
+                    }
+                }
+            }
+        } yields {
+            "Unique; substitution [?0 := i32], lifetime constraints []"
+        }
+    }
+}
+
+#[test]
+fn implied_bounds() {
     test! {
         program {
             trait Clone { }
@@ -567,6 +760,76 @@ fn normalize_implied_bound() {
     }
 }
 
+#[test]
+fn gat_implied_bounds() {
+    test! {
+        program {
+            trait Clone { }
+            trait Foo { type Item<T>: Clone; }
+            struct u32 { }
+        }
+
+        goal {
+            forall<T, U, V> {
+                if (T: Foo<Item<U> = V>) {
+                    V: Clone
+                }
+            }
+        } yields {
+            "Unique; substitution []"
+        }
+    }
+
+    test! {
+        program {
+            trait Clone { }
+            trait Foo { type Item<T>; }
+            struct u32 { }
+        }
+
+        goal {
+            forall<T, U, V> {
+                if (T: Foo<Item<U> = V>) {
+                    // Without the bound Item<T>: Clone, there is no way to infer this.
+                    V: Clone
+                }
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
+#[test]
+fn implied_from_env() {
+    test! {
+        program {
+            trait Clone { }
+            trait Foo<U> { type Item<V>; }
+        }
+
+        goal {
+            forall<T, U, V> {
+                if (FromEnv(<T as Foo<U>>::Item<V>)) {
+                    FromEnv(T: Foo<U>)
+                }
+            }
+        } yields {
+            "Unique"
+        }
+
+        goal {
+            forall<T, U, V> {
+                if (FromEnv(<T as Foo<U>>::Item<V>)) {
+                    FromEnv(T: Clone)
+                }
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
 /// Demonstrates that, given the expected value of the associated
 /// type, we can use that to narrow down the relevant impls.
 #[test]
@@ -590,6 +853,31 @@ fn normalize_rev_infer() {
     }
 }
 
+/// Demonstrates that, given the expected value of the associated
+/// type, we can use that to narrow down the relevant impls.
+#[test]
+fn normalize_rev_infer_gat() {
+    test! {
+        program {
+            trait Combine { type Item<T>; }
+            struct u32 { }
+            struct i32 { }
+            struct Either<T, U> { }
+            impl Combine for u32 { type Item<U> = Either<u32, U>; }
+            impl Combine for i32 { type Item<U> = Either<i32, U>; }
+        }
+
+        goal {
+            exists<T, U> {
+                T: Combine<Item<U> = Either<u32, i32>>
+            }
+        } yields {
+            // T is ?1 and U is ?0, so this is surprising, but correct! (See #126.)
+            "Unique; substitution [?0 := i32, ?1 := u32]"
+        }
+    }
+}
+
 /// Demonstrates that, given the expected value of the associated
 /// type, we can use that to narrow down the relevant impls.
 #[test]
@@ -689,42 +977,58 @@ fn forall_projection() {
     }
 }
 
+/// Demonstrates that, given the expected value of the associated
+/// type, we can use that to narrow down the relevant impls.
 #[test]
-fn atc1() {
+fn forall_projection_gat() {
     test! {
         program {
-            struct Vec<T> { }
+            trait Eq<T> { }
+            impl<T> Eq<T> for T { }
 
-            trait Iterable {
-                type Iter<'a>;
-            }
+            trait Sized { }
 
-            impl<T> Iterable for Vec<T> {
-                type Iter<'a> = Iter<'a, T>;
-            }
+            trait DropOuter<'a> { type Item<U> where U: Sized; }
+            impl<'a, T> DropOuter<'a> for T { type Item<U> = T; }
 
-            trait Iterator {
-                type Item;
+            struct Unit { }
+            struct Ref<'a, T> { }
+        }
+
+        goal {
+            forall<T> {
+                for<'a> <Unit as DropOuter<'a>>::Item<T>: Eq<Unit>
             }
+        } yields {
+            "No possible solution"
+        }
 
-            struct Iter<'a, T> { }
-            struct Ref<'a, T> { }
+        goal {
+            forall<T> {
+                if (T: Sized) {
+                    for<'a> <Unit as DropOuter<'a>>::Item<T>: Eq<Unit>
+                }
+            }
+        } yields {
+            "Unique; substitution [], lifetime constraints []"
+        }
 
-            impl<'a, T> Iterator for Iter<'a, T> {
-                type Item = Ref<'a, T>;
+        goal {
+            forall<'a, T> {
+                WellFormed(<Unit as DropOuter<'a>>::Item<T>)
             }
+        } yields {
+            "No possible solution"
         }
 
         goal {
             forall<T> {
-                forall<'a> {
-                    exists<U> {
-                        Normalize(<Vec<T> as Iterable>::Iter<'a> -> U)
-                    }
+                if (T: Sized) {
+                    WellFormed(for<'a> <Unit as DropOuter<'a>>::Item<T>: Eq<Unit>)
                 }
             }
         } yields {
-            "Unique; substitution [?0 := Iter<'!2, !1>], lifetime constraints []"
+            "Unique; substitution [], lifetime constraints []"
         }
     }
 }
@@ -1020,6 +1324,34 @@ fn mixed_indices_normalize_application() {
     }
 }
 
+#[test]
+fn mixed_indices_normalize_gat_application() {
+    test! {
+        program {
+            struct Either<T, U> { }
+            struct Ref<'a, T> { }
+            trait Foo {
+                type T<X>;
+            }
+
+            impl<U, 'a> Foo for Ref<'a, U> {
+                type T<X> = Either<X, U>;
+            }
+        }
+
+        goal {
+            exists<T, 'a, U, Y, X> {
+                Normalize(<Ref<'a, T> as Foo>::T<X> -> Either<U, Y>)
+            }
+        } yields {
+            // Our GAT parameter <X> is mapped to ?0; all others appear left to right
+            // in our Normalize(...) goal.
+            "Unique; for<?U0,?U0,?U0> { \
+                substitution [?0 := ?0, ?1 := '?1, ?2 := ?2, ?3 := ?0, ?4 := ?2], "
+        }
+    }
+}
+
 #[test]
 // Test that we properly detect failure even if there are applicable impls at
 // the top level, if we can't find anything to fill in those impls with
@@ -1766,7 +2098,7 @@ fn unselected_projection() {
 }
 
 #[test]
-fn unselected_projection_with_atc() {
+fn unselected_projection_with_gat() {
     test! {
         program {
             trait Foo {
@@ -1780,6 +2112,7 @@ fn unselected_projection_with_atc() {
                 type Item<'a> = Ref<'a, i32>;
             }
         }
+
         goal {
             forall<'a> {
                 if (InScope(Foo)) {
@@ -1789,6 +2122,16 @@ fn unselected_projection_with_atc() {
         } yields {
             "Unique"
         }
+
+        goal {
+            forall<'a> {
+                if (InScope(Foo)) {
+                    WellFormed(i32::Item<'a>)
+                }
+            }
+        } yields {
+            "Unique"
+        }
     }
 }
 
@@ -1877,6 +2220,47 @@ fn projection_from_env() {
     }
 }
 
+#[test]
+fn gat_unify_with_implied_wc() {
+    test! {
+        program {
+            struct Slice<T> { }
+
+            trait Cast<T> { }
+            trait CastingIter<T> {
+                type Item<U>: Cast<U> where T: Cast<U>;
+            }
+
+            impl<T> CastingIter<T> for Slice<T> {
+                type Item<U> = Castable<T, U>;
+            }
+
+            struct Castable<T, U> { }
+            impl<T, U> Cast<U> for Castable<T, U> { }
+        }
+
+        goal {
+            forall<T, U, V> {
+                if (
+                    FromEnv(<Slice<T> as CastingIter<T>>::Item<U>)
+                ) {
+                    T: Cast<U>
+                }
+            }
+        } yields {
+            "Unique"
+        }
+
+        goal {
+            forall<T, U, V> {
+                T: Cast<U>
+            }
+        } yields {
+            "No possible solution"
+        }
+    }
+}
+
 // This variant of the above test used to be achingly slow on SLG
 // solvers, before the "trivial answer" green cut was introduced.
 //
diff --git a/src/test_util.rs b/src/test_util.rs
index 89662355c57..0a1921b8db2 100644
--- a/src/test_util.rs
+++ b/src/test_util.rs
@@ -22,11 +22,15 @@ macro_rules! lowering_success {
         let program_text = stringify!($program);
         assert!(program_text.starts_with("{"));
         assert!(program_text.ends_with("}"));
+        let result = parse_and_lower_program(
+            &program_text[1..program_text.len()-1],
+            $crate::solve::SolverChoice::slg()
+        );
+        if let Err(ref e) = result {
+            println!("lowering error: {}", e);
+        }
         assert!(
-            parse_and_lower_program(
-                &program_text[1..program_text.len()-1],
-                $crate::solve::SolverChoice::slg()
-            ).is_ok()
+            result.is_ok()
         );
     }
 }