diff --git a/src/cast.rs b/src/cast.rs
index afec6ddfe33..7a05e4147ae 100644
--- a/src/cast.rs
+++ b/src/cast.rs
@@ -24,7 +24,6 @@ macro_rules! reflexive_impl {
 
 reflexive_impl!(TraitRef);
 reflexive_impl!(WhereClause);
-reflexive_impl!(WhereClauseGoal);
 
 impl Cast<WhereClause> for TraitRef {
     fn cast(self) -> WhereClause {
@@ -32,53 +31,32 @@ impl Cast<WhereClause> for TraitRef {
     }
 }
 
-impl Cast<WhereClauseGoal> for TraitRef {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Implemented(self)
-    }
-}
-
 impl Cast<WhereClause> for Normalize {
     fn cast(self) -> WhereClause {
         WhereClause::Normalize(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Normalize {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::Normalize(self)
-    }
-}
-
-impl Cast<WhereClauseGoal> for WellFormed {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::WellFormed(self)
+impl Cast<WhereClause> for WellFormed {
+    fn cast(self) -> WhereClause {
+        WhereClause::WellFormed(self)
     }
 }
 
 impl Cast<Goal> for WellFormed {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: WhereClause = self.cast();
         wcg.cast()
     }
 }
 
 impl Cast<Goal> for Normalize {
     fn cast(self) -> Goal {
-        let wcg: WhereClauseGoal = self.cast();
+        let wcg: WhereClause = self.cast();
         wcg.cast()
     }
 }
 
-impl Cast<WhereClauseGoal> for WhereClause {
-    fn cast(self) -> WhereClauseGoal {
-        match self {
-            WhereClause::Implemented(a) => a.cast(),
-            WhereClause::Normalize(a) => a.cast(),
-        }
-    }
-}
-
 impl Cast<Goal> for TraitRef {
     fn cast(self) -> Goal {
         Goal::Leaf(self.cast())
@@ -86,26 +64,20 @@ impl Cast<Goal> for TraitRef {
 }
 
 impl Cast<Goal> for WhereClause {
-    fn cast(self) -> Goal {
-        Goal::Leaf(self.cast())
-    }
-}
-
-impl Cast<Goal> for WhereClauseGoal {
     fn cast(self) -> Goal {
         Goal::Leaf(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Unify<Ty> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyTys(self)
+impl Cast<WhereClause> for Unify<Ty> {
+    fn cast(self) -> WhereClause {
+        WhereClause::UnifyTys(self)
     }
 }
 
-impl Cast<WhereClauseGoal> for Unify<Lifetime> {
-    fn cast(self) -> WhereClauseGoal {
-        WhereClauseGoal::UnifyLifetimes(self)
+impl Cast<WhereClause> for Unify<Lifetime> {
+    fn cast(self) -> WhereClause {
+        WhereClause::UnifyLifetimes(self)
     }
 }
 
diff --git a/src/fold/mod.rs b/src/fold/mod.rs
index 51b4b8e28e3..e103543abe9 100644
--- a/src/fold/mod.rs
+++ b/src/fold/mod.rs
@@ -178,9 +178,8 @@ macro_rules! enum_fold {
 }
 
 enum_fold!(ParameterKind[T,L] { Ty(a), Lifetime(a) } where T: Fold, L: Fold);
-enum_fold!(WhereClause[] { Implemented(a), Normalize(a) });
 enum_fold!(WellFormed[] { Ty(a), TraitRef(a) });
-enum_fold!(WhereClauseGoal[] { Implemented(a), Normalize(a), UnifyTys(a),
+enum_fold!(WhereClause[] { Implemented(a), Normalize(a), UnifyTys(a),
                                UnifyLifetimes(a), WellFormed(a) });
 enum_fold!(Constraint[] { LifetimeEq(a, b) });
 enum_fold!(Goal[] { Quantified(qkind, subgoal), Implies(wc, subgoal), And(g1, g2), Leaf(wc) });
diff --git a/src/ir/debug.rs b/src/ir/debug.rs
index 6ee7da3a075..d0700f8b305 100644
--- a/src/ir/debug.rs
+++ b/src/ir/debug.rs
@@ -156,24 +156,9 @@ impl Debug for WhereClause {
                        n.trait_id,
                        Angle(&n.parameters[1..]))
             }
-        }
-    }
-}
-
-impl Debug for WhereClauseGoal {
-    fn fmt(&self, fmt: &mut Formatter) -> Result<(), Error> {
-        match *self {
-            WhereClauseGoal::Normalize(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::Implemented(ref n) => {
-                write!(fmt,
-                       "{:?}: {:?}{:?}",
-                       n.parameters[0],
-                       n.trait_id,
-                       Angle(&n.parameters[1..]))
-            }
-            WhereClauseGoal::UnifyTys(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::UnifyLifetimes(ref n) => write!(fmt, "{:?}", n),
-            WhereClauseGoal::WellFormed(ref n) => write!(fmt, "{:?}", n),
+            WhereClause::UnifyTys(ref n) => write!(fmt, "{:?}", n),
+            WhereClause::UnifyLifetimes(ref n) => write!(fmt, "{:?}", n),
+            WhereClause::WellFormed(ref n) => write!(fmt, "{:?}", n),
         }
     }
 }
diff --git a/src/ir/mod.rs b/src/ir/mod.rs
index 91f3d5a914c..c90f04ae201 100644
--- a/src/ir/mod.rs
+++ b/src/ir/mod.rs
@@ -130,6 +130,7 @@ impl Environment {
                     };
                     push_clause(trait_ref.cast());
                 }
+                _ => (),
             }
         }
 
@@ -370,12 +371,6 @@ pub struct TraitRef {
 pub enum WhereClause {
     Implemented(TraitRef),
     Normalize(Normalize),
-}
-
-#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
-pub enum WhereClauseGoal {
-    Implemented(TraitRef),
-    Normalize(Normalize),
     UnifyTys(Unify<Ty>),
     UnifyLifetimes(Unify<Lifetime>),
     WellFormed(WellFormed),
@@ -436,7 +431,7 @@ pub struct ProgramClause {
 /// Represents one clause of the form `consequence :- conditions`.
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct ProgramClauseImplication {
-    pub consequence: WhereClauseGoal,
+    pub consequence: WhereClause,
     pub conditions: Vec<Goal>,
 }
 
@@ -480,7 +475,7 @@ pub enum Goal {
     Quantified(QuantifierKind, Binders<Box<Goal>>),
     Implies(Vec<WhereClause>, Box<Goal>),
     And(Box<Goal>, Box<Goal>),
-    Leaf(WhereClauseGoal),
+    Leaf(WhereClause),
 }
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, PartialOrd, Ord)]
diff --git a/src/lower/mod.rs b/src/lower/mod.rs
index 50ef427a68f..90c982d235a 100644
--- a/src/lower/mod.rs
+++ b/src/lower/mod.rs
@@ -362,40 +362,17 @@ trait LowerWhereClause<T> {
     fn lower(&self, env: &Env) -> Result<T>;
 }
 
-/// Lowers a where-clause in the context of a clause; this is limited
-/// to the kinds of where-clauses users can actually type in Rust.
 impl LowerWhereClause<ir::WhereClause> for WhereClause {
     fn lower(&self, env: &Env) -> Result<ir::WhereClause> {
         Ok(match *self {
             WhereClause::Implemented { ref trait_ref } => {
-                ir::WhereClause::Implemented(trait_ref.lower(env)?)
+                trait_ref.lower(env)?.cast()
             }
             WhereClause::ProjectionEq { ref projection, ref ty  } => {
-                ir::WhereClause::Normalize(ir::Normalize {
+                ir::Normalize {
                     projection: projection.lower(env)?,
                     ty: ty.lower(env)?,
-                })
-            }
-            WhereClause::TyWellFormed { .. } |
-            WhereClause::TraitRefWellFormed { .. } |
-            WhereClause::UnifyTys { .. } |
-            WhereClause::UnifyLifetimes { .. } => {
-                bail!("this form of where-clause not allowed here")
-            }
-        })
-    }
-}
-
-/// Lowers a where-clause in the context of a goal; this is richer in
-/// terms of the legal sorts of where-clauses that can appear, because
-/// it includes all the sorts of things that the compiler must verify.
-impl LowerWhereClause<ir::WhereClauseGoal> for WhereClause {
-    fn lower(&self, env: &Env) -> Result<ir::WhereClauseGoal> {
-        Ok(match *self {
-            WhereClause::Implemented { .. } |
-            WhereClause::ProjectionEq { .. } => {
-                let wc: ir::WhereClause = self.lower(env)?;
-                wc.cast()
+                }.cast()
             }
             WhereClause::TyWellFormed { ref ty } => {
                 ir::WellFormed::Ty(ty.lower(env)?).cast()
@@ -403,7 +380,7 @@ impl LowerWhereClause<ir::WhereClauseGoal> for WhereClause {
             WhereClause::TraitRefWellFormed { ref trait_ref } => {
                 ir::WellFormed::TraitRef(trait_ref.lower(env)?).cast()
             }
-            WhereClause::UnifyTys { ref a, ref b} => {
+            WhereClause::UnifyTys { ref a, ref b } => {
                 ir::Unify {
                     a: a.lower(env)?,
                     b: b.lower(env)?,
@@ -820,6 +797,7 @@ impl ir::AssociatedTyValue {
         // 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.up_shift(self.value.len());
+
         let conditions: Vec<ir::Goal> =
             Some(impl_trait_ref.clone().cast())
             .into_iter()
diff --git a/src/solve/fulfill.rs b/src/solve/fulfill.rs
index ff14e2731f6..15b11ed3a93 100644
--- a/src/solve/fulfill.rs
+++ b/src/solve/fulfill.rs
@@ -12,7 +12,7 @@ use zip::Zip;
 pub struct Fulfill<'s> {
     solver: &'s mut Solver,
     infer: InferenceTable,
-    obligations: Vec<InEnvironment<WhereClauseGoal>>,
+    obligations: Vec<InEnvironment<WhereClause>>,
     constraints: HashSet<InEnvironment<Constraint>>,
 }
 
@@ -79,13 +79,13 @@ impl<'s> Fulfill<'s> {
     /// Adds the given where-clauses to the internal list of
     /// obligations that must be solved.
     pub fn extend<WC>(&mut self, wc: WC)
-        where WC: IntoIterator<Item=InEnvironment<WhereClauseGoal>>
+        where WC: IntoIterator<Item=InEnvironment<WhereClause>>
     {
         self.obligations.extend(wc);
     }
 
     /// Return current list of pending obligations; used for unit testing primarily
-    pub fn pending_obligations(&self) -> &[InEnvironment<WhereClauseGoal>] {
+    pub fn pending_obligations(&self) -> &[InEnvironment<WhereClause>] {
         &self.obligations
     }
 
@@ -210,7 +210,7 @@ impl<'s> Fulfill<'s> {
     }
 
     fn solve_one(&mut self,
-                 wc: &InEnvironment<WhereClauseGoal>,
+                 wc: &InEnvironment<WhereClause>,
                  inference_progress: &mut bool)
                  -> Result<Successful> {
         debug!("fulfill::solve_one(wc={:?})", wc);
diff --git a/src/solve/infer/unify.rs b/src/solve/infer/unify.rs
index 73e67fcfb64..434aefd3a1f 100644
--- a/src/solve/infer/unify.rs
+++ b/src/solve/infer/unify.rs
@@ -32,13 +32,13 @@ struct Unifier<'t> {
     table: &'t mut InferenceTable,
     environment: &'t Arc<Environment>,
     snapshot: InferenceSnapshot,
-    goals: Vec<InEnvironment<WhereClauseGoal>>,
+    goals: Vec<InEnvironment<WhereClause>>,
     constraints: Vec<InEnvironment<Constraint>>,
 }
 
 #[derive(Debug)]
 pub struct UnificationResult {
-    pub goals: Vec<InEnvironment<WhereClauseGoal>>,
+    pub goals: Vec<InEnvironment<WhereClause>>,
     pub constraints: Vec<InEnvironment<Constraint>>,
 }
 
diff --git a/src/solve/match_any.rs b/src/solve/match_any.rs
index c4f5ecfa433..b2ad4fb3357 100644
--- a/src/solve/match_any.rs
+++ b/src/solve/match_any.rs
@@ -20,7 +20,7 @@ enum Technique<'t> {
 }
 
 impl<'s, G> MatchAny<'s, G>
-    where G: Cast<WhereClause> + Cast<WhereClauseGoal> + Clone + Hash + Eq + Fold<Result = G>
+    where G: Cast<WhereClause> + Clone + Hash + Eq + Fold<Result = G>
 {
     pub fn new(solver: &'s mut Solver, env_goal: &'s Query<InEnvironment<G>>) -> Self {
         MatchAny {
diff --git a/src/solve/match_program_clause.rs b/src/solve/match_program_clause.rs
index e205fa6ad6e..7e328e91f14 100644
--- a/src/solve/match_program_clause.rs
+++ b/src/solve/match_program_clause.rs
@@ -15,7 +15,7 @@ pub struct MatchProgramClause<'s, G: 's> {
 }
 
 impl<'s, G> MatchProgramClause<'s, G>
-    where G: Clone + Cast<WhereClauseGoal> + Fold<Result = G>
+    where G: Clone + Cast<WhereClause> + Fold<Result = G>
 {
     pub fn new(solver: &'s mut Solver,
                q: &'s Query<InEnvironment<G>>,
diff --git a/src/solve/mod.rs b/src/solve/mod.rs
index ac1019d23c9..39dcd252165 100644
--- a/src/solve/mod.rs
+++ b/src/solve/mod.rs
@@ -8,6 +8,7 @@ pub mod match_clause;
 pub mod match_program_clause;
 pub mod normalize;
 pub mod normalize_application;
+pub mod well_formed;
 pub mod prove;
 pub mod solver;
 pub mod unify;
diff --git a/src/solve/prove.rs b/src/solve/prove.rs
index 7dfc32d91b1..f871604638d 100644
--- a/src/solve/prove.rs
+++ b/src/solve/prove.rs
@@ -6,7 +6,7 @@ use solve::Solution;
 
 pub struct Prove<'s> {
     fulfill: Fulfill<'s>,
-    goals: Vec<InEnvironment<WhereClauseGoal>>,
+    goals: Vec<InEnvironment<WhereClause>>,
 }
 
 impl<'s> Prove<'s> {
@@ -21,7 +21,7 @@ impl<'s> Prove<'s> {
         prove
     }
 
-    pub fn solve(mut self) -> Result<Solution<Vec<WhereClauseGoal>>> {
+    pub fn solve(mut self) -> Result<Solution<Vec<WhereClause>>> {
         let successful = self.fulfill.solve_all()?;
         let goals: Vec<_> = self.goals.into_iter().map(|g| g.goal).collect();
         let refined_goal = self.fulfill.refine_goal(goals);
diff --git a/src/solve/solver/mod.rs b/src/solve/solver/mod.rs
index ced953dab0d..16ca01dad51 100644
--- a/src/solve/solver/mod.rs
+++ b/src/solve/solver/mod.rs
@@ -1,8 +1,8 @@
 use cast::Cast;
 use errors::*;
-use solve::match_program_clause::MatchProgramClause;
 use solve::normalize::SolveNormalize;
 use solve::implemented::Implemented;
+use solve::well_formed::SolveWellFormed;
 use solve::unify::SolveUnify;
 use std::collections::HashSet;
 use std::fmt::Debug;
@@ -14,7 +14,7 @@ use super::*;
 pub struct Solver {
     pub(super) program: Arc<ProgramEnvironment>,
     overflow_depth: usize,
-    stack: Vec<Query<InEnvironment<WhereClauseGoal>>>,
+    stack: Vec<Query<InEnvironment<WhereClause>>>,
 }
 
 impl Solver {
@@ -25,8 +25,8 @@ impl Solver {
     /// Tries to solve one **closed** where-clause `wc` (in the given
     /// environment).
     pub fn solve(&mut self,
-                 wc_env: Query<InEnvironment<WhereClauseGoal>>)
-                 -> Result<Solution<InEnvironment<WhereClauseGoal>>> {
+                 wc_env: Query<InEnvironment<WhereClause>>)
+                 -> Result<Solution<InEnvironment<WhereClause>>> {
         debug_heading!("Solver::solve({:?})", wc_env);
 
         if self.stack.contains(&wc_env) || self.stack.len() > self.overflow_depth {
@@ -43,45 +43,40 @@ impl Solver {
         let Query { value: InEnvironment { environment, goal: wc }, binders } = wc_env;
 
         let result = match wc {
-            WhereClauseGoal::Implemented(trait_ref) => {
+            WhereClause::Implemented(trait_ref) => {
                 let q = Query {
                     value: InEnvironment::new(&environment, trait_ref),
                     binders: binders,
                 };
                 Implemented::new(self, q).solve().cast()
             }
-            WhereClauseGoal::Normalize(normalize_to) => {
+            WhereClause::Normalize(normalize_to) => {
                 let q = Query {
                     value: InEnvironment::new(&environment, normalize_to),
                     binders: binders,
                 };
                 SolveNormalize::new(self, q).solve().cast()
             }
-            WhereClauseGoal::UnifyTys(unify) => {
+            WhereClause::UnifyTys(unify) => {
                 let q = Query {
                     value: InEnvironment::new(&environment, unify),
                     binders: binders,
                 };
                 SolveUnify::new(self, q).solve().cast()
             }
-            WhereClauseGoal::UnifyLifetimes(unify) => {
+            WhereClause::UnifyLifetimes(unify) => {
                 let q = Query {
                     value: InEnvironment::new(&environment, unify),
                     binders: binders,
                 };
                 SolveUnify::new(self, q).solve().cast()
             }
-            WhereClauseGoal::WellFormed(_) => {
-                // Currently, we don't allow `WF` types into the environment,
-                // there we just have to search for program clauses.
-                let program = self.program.clone();
+            WhereClause::WellFormed(wf) => {
                 let q = Query {
-                    value: InEnvironment::new(&environment, wc),
-                    binders: binders
-                }; // reconstruct `wc_env`
-                self.solve_any(program.program_clauses.iter(), &q, |this, program_clause| {
-                    MatchProgramClause::new(this, &q, &program_clause).solve()
-                })
+                    value: InEnvironment::new(&environment, wf),
+                    binders: binders,
+                };
+                SolveWellFormed::new(self, q).solve().cast()
             }
         };
 
diff --git a/src/solve/test.rs b/src/solve/test.rs
index cff0755dd6f..98828d5e79a 100644
--- a/src/solve/test.rs
+++ b/src/solve/test.rs
@@ -1226,3 +1226,22 @@ fn mixed_indices_normalize_application() {
         }
     }
 }
+
+#[test]
+fn extended_where_clauses() {
+    test! {
+        program {
+            trait Foo { }
+        }
+
+        goal {
+            forall<T> {
+                if (WellFormed(T: Foo)) {
+                    WellFormed(T: Foo)
+                }
+            }
+        } yields {
+            "Solution { successful: Yes"
+        }
+    }
+}
diff --git a/src/solve/well_formed.rs b/src/solve/well_formed.rs
new file mode 100644
index 00000000000..6575605f7f4
--- /dev/null
+++ b/src/solve/well_formed.rs
@@ -0,0 +1,24 @@
+use errors::*;
+use ir::*;
+use solve::match_any::MatchAny;
+use solve::solver::Solver;
+use solve::Solution;
+
+pub struct SolveWellFormed<'s> {
+    solver: &'s mut Solver,
+    env_goal: Query<InEnvironment<WellFormed>>,
+}
+
+impl<'s> SolveWellFormed<'s> {
+    pub fn new(solver: &'s mut Solver, env_goal: Query<InEnvironment<WellFormed>>) -> Self {
+        SolveWellFormed {
+            solver: solver,
+            env_goal: env_goal,
+        }
+    }
+
+    pub fn solve(self) -> Result<Solution<InEnvironment<WellFormed>>> {
+        let SolveWellFormed { solver, env_goal } = self;
+        MatchAny::new(solver, &env_goal).solve()
+    }
+}
diff --git a/src/zip.rs b/src/zip.rs
index 55ab33c00cb..ff6972fa569 100644
--- a/src/zip.rs
+++ b/src/zip.rs
@@ -155,6 +155,5 @@ macro_rules! enum_zip {
     }
 }
 
-enum_zip!(WhereClause { Implemented, Normalize });
-enum_zip!(WhereClauseGoal { Implemented, Normalize, UnifyTys, UnifyLifetimes, WellFormed });
+enum_zip!(WhereClause { Implemented, Normalize, UnifyTys, UnifyLifetimes, WellFormed });
 enum_zip!(WellFormed { Ty, TraitRef });