diff --git a/chalk-parse/src/ast.rs b/chalk-parse/src/ast.rs
index d1d9128ba6e..f1e64ce2c34 100644
--- a/chalk-parse/src/ast.rs
+++ b/chalk-parse/src/ast.rs
@@ -162,7 +162,10 @@ pub struct Field {
 pub enum Goal {
     ForAll(Vec<ParameterKind>, Box<Goal>),
     Exists(Vec<ParameterKind>, Box<Goal>),
-    Implies(Vec<WhereClause>, Box<Goal>),
+
+    // The `bool` flag indicates whether we should elaborate where clauses or not
+    Implies(Vec<WhereClause>, Box<Goal>, bool),
+
     And(Box<Goal>, Box<Goal>),
     Not(Box<Goal>),
 
diff --git a/chalk-parse/src/parser.lalrpop b/chalk-parse/src/parser.lalrpop
index 7029cd9ece8..7c99ffe4287 100644
--- a/chalk-parse/src/parser.lalrpop
+++ b/chalk-parse/src/parser.lalrpop
@@ -28,11 +28,16 @@ pub Goal: Box<Goal> = {
 Goal1: Box<Goal> = {
     "forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
     "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
-    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
+    <i:IfKeyword> "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, i)),
     "not" "{" <g:Goal> "}" => Box::new(Goal::Not(g)),
     <w:WhereClause> => Box::new(Goal::Leaf(w)),
 };
 
+IfKeyword: bool = {
+    "if" => true,
+    "if_raw" => false,
+};
+
 StructDefn: StructDefn = {
     "struct" <n:Id><p:Angle<ParameterKind>> <w:WhereClauses> "{" <f:Fields> "}" => StructDefn {
         name: n,
diff --git a/src/cast.rs b/src/cast.rs
index 028c2b73552..aba2dc8eed0 100644
--- a/src/cast.rs
+++ b/src/cast.rs
@@ -1,4 +1,5 @@
 use ir::*;
+use std::marker::PhantomData;
 
 pub trait Cast<T>: Sized {
     fn cast(self) -> T;
@@ -130,7 +131,7 @@ impl<T, U> Cast<Vec<U>> for Vec<T>
     where T: Cast<U>
 {
     fn cast(self) -> Vec<U> {
-        self.into_iter().map(|v| v.cast()).collect()
+        self.into_iter().casted().collect()
     }
 }
 
@@ -145,3 +146,33 @@ impl Cast<Parameter> for Lifetime {
         ParameterKind::Lifetime(self)
     }
 }
+
+pub struct Casted<I, U> {
+    iterator: I,
+    _cast: PhantomData<U>,
+}
+
+impl<I: Iterator, U> Iterator for Casted<I, U> where I::Item: Cast<U> {
+    type Item = U;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        self.iterator.next().map(|item| item.cast())
+    }
+
+    fn size_hint(&self) -> (usize, Option<usize>) {
+        self.iterator.size_hint()
+    }
+}
+
+pub trait Caster<U>: Sized {
+    fn casted(self) -> Casted<Self, U>;
+}
+
+impl<I: Iterator, U> Caster<U> for I {
+    fn casted(self) -> Casted<Self, U> {
+        Casted {
+            iterator: self,
+            _cast: PhantomData,
+        }
+    }
+}
diff --git a/src/ir/mod.rs b/src/ir/mod.rs
index b4327207293..15580e1eeac 100644
--- a/src/ir/mod.rs
+++ b/src/ir/mod.rs
@@ -1,9 +1,8 @@
 use cast::Cast;
 use chalk_parse::ast;
-use fold::Subst;
 use lalrpop_intern::InternedString;
 use solve::infer::{TyInferenceVariable, LifetimeInferenceVariable};
-use std::collections::{HashSet, HashMap, BTreeMap};
+use std::collections::{HashMap, BTreeMap};
 use std::sync::Arc;
 
 pub type Identifier = InternedString;
@@ -95,58 +94,6 @@ impl Environment {
         env.universe = UniverseIndex { counter: self.universe.counter + 1 };
         Arc::new(env)
     }
-
-    /// Generate the full set of clauses that are "syntactically implied" by the
-    /// clauses in this environment. Currently this consists of two kinds of expansions:
-    ///
-    /// - Supertraits are added, so `T: Ord` would expand to `T: Ord, T: PartialOrd`
-    /// - Projections imply that a trait is implemented, to `T: Iterator<Item=Foo>` expands to
-    ///   `T: Iterator, T: Iterator<Item=Foo>`
-    pub fn elaborated_clauses(&self, program: &ProgramEnvironment) -> impl Iterator<Item = DomainGoal> {
-        let mut set = HashSet::new();
-        set.extend(self.clauses.iter().cloned());
-
-        let mut stack: Vec<_> = set.iter().cloned().collect();
-
-        while let Some(clause) = stack.pop() {
-            let mut push_clause = |clause: DomainGoal| {
-                if !set.contains(&clause) {
-                    set.insert(clause.clone());
-                    stack.push(clause);
-                }
-            };
-
-            match clause {
-                DomainGoal::Implemented(ref trait_ref) => {
-                    // trait Foo<A> where Self: Bar<A> { }
-                    // T: Foo<U>
-                    // ----------------------------------------------------------
-                    // T: Bar<U>
-
-                    let trait_datum = &program.trait_data[&trait_ref.trait_id];
-                    for where_clause in &trait_datum.binders.value.where_clauses {
-                        let where_clause = Subst::apply(&trait_ref.parameters, where_clause);
-                        push_clause(where_clause);
-                    }
-                }
-                DomainGoal::Normalize(Normalize { ref projection, ty: _ }) => {
-                    // <T as Trait<U>>::Foo ===> V
-                    // ----------------------------------------------------------
-                    // T: Trait<U>
-
-                    let (associated_ty_data, trait_params, _) = program.split_projection(projection);
-                    let trait_ref = TraitRef {
-                        trait_id: associated_ty_data.trait_id,
-                        parameters: trait_params.to_owned()
-                    };
-                    push_clause(trait_ref.cast());
-                }
-                _ => {}
-            }
-        }
-
-        set.into_iter()
-    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
@@ -249,6 +196,7 @@ pub struct StructDatum {
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct StructDatumBound {
     pub self_ty: ApplicationTy,
+    pub fields: Vec<Ty>,
     pub where_clauses: Vec<DomainGoal>,
 }
 
@@ -420,6 +368,28 @@ impl DomainGoal {
             fallback_clause: false,
         }
     }
+
+    /// A clause of the form (T: Foo) expands to (T: Foo), WF(T: Foo).
+    /// A clause of the form (T: Foo<Item = U>) expands to (T: Foo<Item = U>), WF(T: Foo).
+    pub fn expanded(self, program: &Program) -> impl Iterator<Item = DomainGoal> {
+        let mut expanded = vec![];
+        match self {
+            DomainGoal::Implemented(ref trait_ref) => {
+                expanded.push(WellFormed::TraitRef(trait_ref.clone()).cast());
+            }
+            DomainGoal::Normalize(Normalize { ref projection, .. }) => {
+                let (associated_ty_data, trait_params, _) = program.split_projection(&projection);
+                let trait_ref = TraitRef {
+                    trait_id: associated_ty_data.trait_id,
+                    parameters: trait_params.to_owned()
+                };
+                expanded.push(WellFormed::TraitRef(trait_ref).cast());
+            }
+            _ => ()
+        };
+        expanded.push(self.cast());
+        expanded.into_iter()
+    }
 }
 
 #[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
diff --git a/src/lower/mod.rs b/src/lower/mod.rs
index d5259bc2d93..0aab85e1158 100644
--- a/src/lower/mod.rs
+++ b/src/lower/mod.rs
@@ -3,7 +3,7 @@ use std::collections::HashMap;
 use chalk_parse::ast::*;
 use lalrpop_intern::intern;
 
-use cast::Cast;
+use cast::{Cast, Caster};
 use errors::*;
 use ir;
 
@@ -156,17 +156,9 @@ impl LowerProgram for Program {
                 Item::TraitDefn(ref d) => {
                     trait_data.insert(item_id, d.lower_trait(item_id, &empty_env)?);
 
-                    let trait_datum = &trait_data[&item_id];
                     for defn in &d.assoc_ty_defns {
                         let info = &associated_ty_infos[&(item_id, defn.name.str)];
 
-                        // `trait_ref` is the trait ref defined by
-                        // this impl, but shifted to account for the
-                        // add'l bindings that are in scope w/in the
-                        // assoc-ty-value.
-                        let offset = info.addl_parameter_kinds.len();
-                        let trait_ref = trait_datum.binders.value.trait_ref.up_shift(offset);
-
                         let mut parameter_kinds = defn.all_parameters();
                         parameter_kinds.extend(d.all_parameters());
 
@@ -175,7 +167,7 @@ impl LowerProgram for Program {
                             id: info.id,
                             name: defn.name.str,
                             parameter_kinds: parameter_kinds,
-                            where_clauses: vec![ir::DomainGoal::Implemented(trait_ref)]
+                            where_clauses: vec![],
                         });
                     }
                 }
@@ -377,7 +369,7 @@ trait LowerWhereClause<T> {
 
 /// Lowers a where-clause in the context of a clause (i.e. in "negative"
 /// position); this is limited to the kinds of where-clauses users can actually
-/// type in Rust.
+/// type in Rust and well-formedness checks.
 impl LowerWhereClause<ir::DomainGoal> for WhereClause {
     fn lower(&self, env: &Env) -> Result<ir::DomainGoal> {
         Ok(match *self {
@@ -390,8 +382,12 @@ impl LowerWhereClause<ir::DomainGoal> for WhereClause {
                     ty: ty.lower(env)?,
                 })
             }
-            WhereClause::TyWellFormed { .. } |
-            WhereClause::TraitRefWellFormed { .. } |
+            WhereClause::TyWellFormed { ref ty } => {
+                ir::WellFormed::Ty(ty.lower(env)?).cast()
+            }
+            WhereClause::TraitRefWellFormed { ref trait_ref } => {
+                ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast()
+            }
             WhereClause::UnifyTys { .. } |
             WhereClause::UnifyLifetimes { .. } => {
                 bail!("this form of where-clause not allowed here")
@@ -452,9 +448,10 @@ impl LowerStructDefn for StructDefn {
                                 .collect()
             };
 
+            let fields: Result<_> = self.fields.iter().map(|f| f.ty.lower(env)).collect();
             let where_clauses = self.lower_where_clauses(env)?;
 
-            Ok(ir::StructDatumBound { self_ty, where_clauses })
+            Ok(ir::StructDatumBound { self_ty, fields: fields?, where_clauses })
         })?;
 
         Ok(ir::StructDatum { binders })
@@ -729,8 +726,19 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
                 g.lower_quantified(env, ir::QuantifierKind::ForAll, ids),
             Goal::Exists(ref ids, ref g) =>
                 g.lower_quantified(env, ir::QuantifierKind::Exists, ids),
-            Goal::Implies(ref wc, ref g) =>
-                Ok(Box::new(ir::Goal::Implies(wc.lower(env)?, g.lower(env)?))),
+            Goal::Implies(ref wc, ref g, elaborate) => {
+                let mut where_clauses = wc.lower(env)?;
+                if elaborate {
+                    where_clauses = ir::with_current_program(|program| {
+                        let program = program.expect("cannot elaborate without a program");
+                        where_clauses.into_iter()
+                                     .flat_map(|wc| wc.expanded(program))
+                                     .casted()
+                                     .collect()
+                    });
+                }
+                Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?)))
+            }
             Goal::And(ref g1, ref g2) =>
                 Ok(Box::new(ir::Goal::And(g1.lower(env)?, g2.lower(env)?))),
             Goal::Not(ref g) =>
@@ -774,12 +782,12 @@ impl ir::Program {
         //       forall P0...Pn. Something :- Conditions
         let mut program_clauses = vec![];
 
-        program_clauses.extend(self.struct_data.values().flat_map(|d| d.to_program_clauses()));
-        program_clauses.extend(self.trait_data.values().flat_map(|d| d.to_program_clauses()));
-        program_clauses.extend(self.associated_ty_data.values().flat_map(|d| d.to_program_clauses()));
+        program_clauses.extend(self.struct_data.values().flat_map(|d| d.to_program_clauses(self)));
+        program_clauses.extend(self.trait_data.values().flat_map(|d| d.to_program_clauses(self)));
+        program_clauses.extend(self.associated_ty_data.values().flat_map(|d| d.to_program_clauses(self)));
 
         for datum in self.impl_data.values() {
-            program_clauses.push(datum.to_program_clause());
+            program_clauses.push(datum.to_program_clause(self));
             program_clauses.extend(datum.binders.value.associated_ty_values.iter().flat_map(|atv| {
                 atv.to_program_clauses(datum)
             }));
@@ -796,14 +804,19 @@ impl ir::ImplDatum {
     /// Given `impl<T: Clone> Clone for Vec<T>`, generate:
     ///
     /// ```notrust
-    /// forall<T> { (Vec<T>: Clone) :- (T: Clone) }
+    /// forall<T> { (Vec<T>: Clone) :- (T: Clone), WF(T: Clone) }
     /// ```
-    fn to_program_clause(&self) -> ir::ProgramClause {
+    fn to_program_clause(&self, program: &ir::Program) -> ir::ProgramClause {
         ir::ProgramClause {
             implication: self.binders.map_ref(|bound| {
                 ir::ProgramClauseImplication {
                     consequence: bound.trait_ref.clone().cast(),
-                    conditions: bound.where_clauses.clone().cast(),
+                    conditions: bound.where_clauses
+                                     .iter()
+                                     .cloned()
+                                     .flat_map(|wc| wc.expanded(program))
+                                     .casted()
+                                     .collect(),
                 }
             }),
             fallback_clause: false,
@@ -914,24 +927,36 @@ impl Anonymize for [ir::ParameterKind<ir::Identifier>] {
 }
 
 impl ir::StructDatum {
-    fn to_program_clauses(&self) -> Vec<ir::ProgramClause> {
+    fn to_program_clauses(&self, program: &ir::Program) -> Vec<ir::ProgramClause> {
         // Given:
         //
-        //    struct Foo<T: Eq> { ... }
+        //    struct Foo<T: Eq> { }
         //
         // we generate the following clause:
         //
-        //    for<?T> WF(Foo<?T>) :- (?T: Eq).
+        //    for<?T> WF(Foo<?T>) :- WF(?T), (?T: Eq), WF(?T: Eq).
 
         let wf = ir::ProgramClause {
             implication: self.binders.map_ref(|bound_datum| {
                 ir::ProgramClauseImplication {
                     consequence: ir::WellFormed::Ty(bound_datum.self_ty.clone().cast()).cast(),
 
-                    conditions: bound_datum.where_clauses.iter()
-                                                         .cloned()
-                                                         .map(|wc| wc.cast())
-                                                         .collect(),
+                    conditions: {
+                        let tys = bound_datum.self_ty
+                                             .parameters
+                                             .iter()
+                                             .filter_map(|pk| pk.as_ref().ty())
+                                             .cloned()
+                                             .map(|ty| ir::WellFormed::Ty(ty))
+                                             .casted();
+
+                        let where_clauses = bound_datum.where_clauses.iter()
+                                                       .cloned()
+                                                       .flat_map(|wc| wc.expanded(program))
+                                                       .casted();
+
+                        tys.chain(where_clauses).collect()
+                    }
                 }
             }),
             fallback_clause: false,
@@ -942,19 +967,28 @@ impl ir::StructDatum {
 }
 
 impl ir::TraitDatum {
-    fn to_program_clauses(&self) -> Vec<ir::ProgramClause> {
+    fn to_program_clauses(&self, program: &ir::Program) -> Vec<ir::ProgramClause> {
         // Given:
         //
         //    trait Ord<T> where Self: Eq<T> { ... }
         //
-        // we generate the following clause:
+        // we generate the following clauses:
         //
         //    for<?Self, ?T> WF(?Self: Ord<?T>) :-
         //        // types are well-formed:
         //        WF(?Self),
         //        WF(?T),
         //        // where clauses declared on the trait are met:
-        //        (?Self: Eq<?T>),
+        //        (?Self: Eq<?T>), WF(?Self: Eq<?T>)
+        //
+        //    for<?Self, ?T> (?Self: Eq<T>) :- WF(?Self: Ord<T>)
+        //    for<?Self, ?T> WF(?Self: Ord<?T>) :- WF(?Self: Ord<T>)
+
+        let where_clauses = self.binders.value.where_clauses
+            .iter()
+            .cloned()
+            .flat_map(|wc| wc.expanded(program))
+            .collect::<Vec<_>>();
 
         let wf = ir::ProgramClause {
             implication: self.binders.map_ref(|bound| {
@@ -965,25 +999,37 @@ impl ir::TraitDatum {
                         let tys = bound.trait_ref.parameters
                                                  .iter()
                                                  .filter_map(|pk| pk.as_ref().ty())
-                                                 .map(|ty| ir::WellFormed::Ty(ty.clone()).cast());
+                                                 .cloned()
+                                                 .map(|ty| ir::WellFormed::Ty(ty))
+                                                 .casted();
 
-                        let where_clauses = bound.where_clauses.iter()
-                                                               .cloned()
-                                                               .map(|wc| wc.cast());
-
-                        tys.chain(where_clauses).collect()
+                        tys.chain(where_clauses.iter().cloned().casted()).collect()
                     }
                 }
             }),
             fallback_clause: false,
         };
 
-        vec![wf]
+        let mut clauses = vec![wf];
+
+        for wc in where_clauses {
+            clauses.push(ir::ProgramClause {
+                implication: self.binders.map_ref(|bound| {
+                    ir::ProgramClauseImplication {
+                        consequence: wc,
+                        conditions: vec![ir::WellFormed::TraitRef(bound.trait_ref.clone()).cast()]
+                    }
+                }),
+                fallback_clause: false,
+            });
+        }
+
+        clauses
     }
 }
 
 impl ir::AssociatedTyDatum {
-    fn to_program_clauses(&self) -> Vec<ir::ProgramClause> {
+    fn to_program_clauses(&self, program: &ir::Program) -> Vec<ir::ProgramClause> {
         // For each associated type, we define a normalization "fallback" for
         // projecting when we don't have constraints to say anything interesting
         // about an associated type.
@@ -996,7 +1042,8 @@ impl ir::AssociatedTyDatum {
         //
         // we generate:
         //
-        //    <?T as Foo>::Assoc ==> (Foo::Assoc)<?T>.
+        //    <?T as Foo>::Assoc ==> (Foo::Assoc)<?T> :- (?T: Foo)
+        //    forall<U> { (?T: Foo) :- <?T as Foo>::Assoc ==> U }
 
         let binders: Vec<_> = self.parameter_kinds.iter().map(|pk| pk.map(|_| ())).collect();
         let parameters: Vec<_> = binders.iter().zip(0..).map(|p| p.to_parameter()).collect();
@@ -1005,6 +1052,15 @@ impl ir::AssociatedTyDatum {
             parameters: parameters.clone(),
         };
 
+        // Retrieve the trait ref embedding the associated type
+        let trait_ref = {
+            let (associated_ty_data, trait_params, _) = program.split_projection(&projection);
+            ir::TraitRef {
+                trait_id: associated_ty_data.trait_id,
+                parameters: trait_params.to_owned()
+            }
+        };
+
         let fallback = {
             // Construct an application from the projection. So if we have `<T as Iterator>::Item`,
             // we would produce `(Iterator::Item)<T>`.
@@ -1013,17 +1069,34 @@ impl ir::AssociatedTyDatum {
 
             ir::ProgramClause {
                 implication: ir::Binders {
-                    binders,
+                    binders: binders.clone(),
                     value: ir::ProgramClauseImplication {
                         consequence: ir::Normalize { projection: projection.clone(), ty }.cast(),
-                        // TODO: should probably include the TraitRef here
-                        conditions: vec![],
+                        conditions: vec![trait_ref.clone().cast()],
                     }
                 },
                 fallback_clause: true,
             }
         };
 
-        vec![fallback]
+        let elaborate = {
+            // add new type parameter U
+            let mut binders = binders;
+            binders.push(ir::ParameterKind::Ty(()));
+            let ty = ir::Ty::Var(binders.len() - 1);
+
+            ir::ProgramClause {
+                implication: ir::Binders {
+                    binders,
+                    value: ir::ProgramClauseImplication {
+                        consequence: trait_ref.cast(),
+                        conditions: vec![ir::Normalize { projection, ty }.cast()],
+                    }
+                },
+                fallback_clause: false,
+            }
+        };
+
+        vec![fallback, elaborate]
     }
 }
diff --git a/src/solve/solver.rs b/src/solve/solver.rs
index 545e2707287..078665770f5 100644
--- a/src/solve/solver.rs
+++ b/src/solve/solver.rs
@@ -144,9 +144,8 @@ impl Solver {
                     // or from the lowered program, which includes fallback
                     // clauses. We try each approach in turn:
 
-                    let env_clauses = value
-                        .environment
-                        .elaborated_clauses(&self.program)
+                    let env_clauses = value.environment.clauses.iter()
+                        .cloned()
                         .map(DomainGoal::into_program_clause);
                     let env_solution = self.solve_from_clauses(&binders, &value, env_clauses);
 
diff --git a/src/solve/test.rs b/src/solve/test.rs
index 5ba31a533cd..d89c15c1fca 100644
--- a/src/solve/test.rs
+++ b/src/solve/test.rs
@@ -182,6 +182,18 @@ fn prove_forall() {
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        // This fails because we used `if_raw`, and hence we do not
+        // know that `WF(T: Clone)` holds.
+        goal {
+            forall<T> {
+                if_raw (T: Clone) {
+                    Vec<T>: Clone
+                }
+            }
+        } yields {
+            "CannotProve"
+        }
     }
 }
 
@@ -582,10 +594,16 @@ fn elaborate_normalize() {
     test! {
         program {
             trait Eq { }
+            struct i32 { }
 
             trait Item where <Self as Item>::Out: Eq {
                 type Out;
             }
+
+            impl Eq for i32 { }
+            impl Item for i32 {
+                type Out = i32;
+            }
         }
 
         goal {
@@ -597,6 +615,26 @@ fn elaborate_normalize() {
         } yields {
             "Unique; substitution [], lifetime constraints []"
         }
+
+        goal {
+            forall<T, U> {
+                if (T: Item<Out = U>) {
+                    T: Item
+                }
+            }
+        } yields {
+            "Unique"
+        }
+
+        goal {
+            forall<T> {
+                if (T: Item<Out = i32>) {
+                    T: Item
+                }
+            }
+        } yields {
+            "Unique"
+        }
     }
 }
 
@@ -727,6 +765,8 @@ fn trait_wf() {
 
             impl Ord<Int> for Int { }
             impl<T> Ord<Vec<T>> for Vec<T> where T: Ord<T> { }
+
+            impl<T> Ord<Slice<T>> for Slice<T> { }
         }
 
         goal {
@@ -753,13 +793,19 @@ fn trait_wf() {
             "Unique; substitution [], lifetime constraints []"
         }
 
+        goal {
+            Slice<Int>: Ord<Slice<Int>>
+        } yields {
+            "Unique"
+        }
+
         goal {
             Slice<Int>: Eq<Slice<Int>>
         } yields {
             "No possible solution"
         }
 
-        // not WF because previous equation doesn't hold
+        // not WF because previous equation doesn't hold, despite Slice<Int> having an impl for Ord<Int> 
         goal {
             WellFormed(Slice<Int>: Ord<Slice<Int>>)
         } yields {
@@ -955,6 +1001,10 @@ fn mixed_indices_normalize_application() {
             trait Foo {
                 type T;
             }
+
+            impl<U, 'a> Foo for Ref<'a, U> {
+                type T = U;
+            }
         }
 
         goal {