diff --git a/src/librustc/infer/combine.rs b/src/librustc/infer/combine.rs
index 1bac512e209..82578f6aa61 100644
--- a/src/librustc/infer/combine.rs
+++ b/src/librustc/infer/combine.rs
@@ -42,9 +42,8 @@ use super::{MiscVariable, TypeTrace};
 use ty::{IntType, UintType};
 use ty::{self, Ty, TyCtxt};
 use ty::error::TypeError;
-use ty::fold::TypeFoldable;
-use ty::relate::{RelateResult, TypeRelation};
-use traits::PredicateObligations;
+use ty::relate::{self, Relate, RelateResult, TypeRelation};
+use traits::{Obligation, PredicateObligations};
 
 use syntax::ast;
 use syntax_pos::Span;
@@ -207,11 +206,16 @@ impl<'infcx, 'gcx, 'tcx> CombineFields<'infcx, 'gcx, 'tcx> {
         // `'?2` and `?3` are fresh region/type inference
         // variables. (Down below, we will relate `a_ty <: b_ty`,
         // adding constraints like `'x: '?2` and `?1 <: ?3`.)
-        let b_ty = self.generalize(a_ty, b_vid, dir == EqTo)?;
+        let Generalization { ty: b_ty, needs_wf } = self.generalize(a_ty, b_vid, dir)?;
         debug!("instantiate(a_ty={:?}, dir={:?}, b_vid={:?}, generalized b_ty={:?})",
                a_ty, dir, b_vid, b_ty);
         self.infcx.type_variables.borrow_mut().instantiate(b_vid, b_ty);
 
+        if needs_wf {
+            self.obligations.push(Obligation::new(self.trace.cause.clone(),
+                                                  ty::Predicate::WellFormed(b_ty)));
+        }
+
         // Finally, relate `b_ty` to `a_ty`, as described in previous comment.
         //
         // FIXME(#16847): This code is non-ideal because all these subtype
@@ -230,10 +234,9 @@ impl<'infcx, 'gcx, 'tcx> CombineFields<'infcx, 'gcx, 'tcx> {
 
     /// Attempts to generalize `ty` for the type variable `for_vid`.
     /// This checks for cycle -- that is, whether the type `ty`
-    /// references `for_vid`. If `is_eq_relation` is false, it will
-    /// also replace all regions/unbound-type-variables with fresh
-    /// variables. Returns `TyError` in the case of a cycle, `Ok`
-    /// otherwise.
+    /// references `for_vid`. The `dir` is the "direction" for which we
+    /// a performing the generalization (i.e., are we producing a type
+    /// that can be used as a supertype etc).
     ///
     /// Preconditions:
     ///
@@ -241,22 +244,33 @@ impl<'infcx, 'gcx, 'tcx> CombineFields<'infcx, 'gcx, 'tcx> {
     fn generalize(&self,
                   ty: Ty<'tcx>,
                   for_vid: ty::TyVid,
-                  is_eq_relation: bool)
-                  -> RelateResult<'tcx, Ty<'tcx>>
+                  dir: RelationDir)
+                  -> RelateResult<'tcx, Generalization<'tcx>>
     {
+        // Determine the ambient variance within which `ty` appears.
+        // The surrounding equation is:
+        //
+        //     ty [op] ty2
+        //
+        // where `op` is either `==`, `<:`, or `:>`. This maps quite
+        // naturally.
+        let ambient_variance = match dir {
+            RelationDir::EqTo => ty::Invariant,
+            RelationDir::SubtypeOf => ty::Covariant,
+            RelationDir::SupertypeOf => ty::Contravariant,
+        };
+
         let mut generalize = Generalizer {
             infcx: self.infcx,
             span: self.trace.cause.span,
             for_vid_sub_root: self.infcx.type_variables.borrow_mut().sub_root_var(for_vid),
-            is_eq_relation: is_eq_relation,
-            cycle_detected: false
+            ambient_variance: ambient_variance,
+            needs_wf: false,
         };
-        let u = ty.fold_with(&mut generalize);
-        if generalize.cycle_detected {
-            Err(TypeError::CyclicTy)
-        } else {
-            Ok(u)
-        }
+
+        let ty = generalize.relate(&ty, &ty)?;
+        let needs_wf = generalize.needs_wf;
+        Ok(Generalization { ty, needs_wf })
     }
 }
 
@@ -264,16 +278,81 @@ struct Generalizer<'cx, 'gcx: 'cx+'tcx, 'tcx: 'cx> {
     infcx: &'cx InferCtxt<'cx, 'gcx, 'tcx>,
     span: Span,
     for_vid_sub_root: ty::TyVid,
-    is_eq_relation: bool,
-    cycle_detected: bool,
+    ambient_variance: ty::Variance,
+    needs_wf: bool, // see the field `needs_wf` in `Generalization`
 }
 
-impl<'cx, 'gcx, 'tcx> ty::fold::TypeFolder<'gcx, 'tcx> for Generalizer<'cx, 'gcx, 'tcx> {
-    fn tcx<'a>(&'a self) -> TyCtxt<'a, 'gcx, 'tcx> {
+/// Result from a generalization operation. This includes
+/// not only the generalized type, but also a bool flag
+/// indicating whether further WF checks are needed.q
+struct Generalization<'tcx> {
+    ty: Ty<'tcx>,
+
+    /// If true, then the generalized type may not be well-formed,
+    /// even if the source type is well-formed, so we should add an
+    /// additional check to enforce that it is. This arises in
+    /// particular around 'bivariant' type parameters that are only
+    /// constrained by a where-clause. As an example, imagine a type:
+    ///
+    ///     struct Foo<A, B> where A: Iterator<Item=B> {
+    ///         data: A
+    ///     }
+    ///
+    /// here, `A` will be covariant, but `B` is
+    /// unconstrained. However, whatever it is, for `Foo` to be WF, it
+    /// must be equal to `A::Item`. If we have an input `Foo<?A, ?B>`,
+    /// then after generalization we will wind up with a type like
+    /// `Foo<?C, ?D>`. When we enforce that `Foo<?A, ?B> <: Foo<?C,
+    /// ?D>` (or `>:`), we will wind up with the requirement that `?A
+    /// <: ?C`, but no particular relationship between `?B` and `?D`
+    /// (after all, we do not know the variance of the normalized form
+    /// of `A::Item` with respect to `A`). If we do nothing else, this
+    /// may mean that `?D` goes unconstrained (as in #41677).  So, in
+    /// this scenario where we create a new type variable in a
+    /// bivariant context, we set the `needs_wf` flag to true. This
+    /// will force the calling code to check that `WF(Foo<?C, ?D>)`
+    /// holds, which in turn implies that `?C::Item == ?D`. So once
+    /// `?C` is constrained, that should suffice to restrict `?D`.
+    needs_wf: bool,
+}
+
+impl<'cx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx> for Generalizer<'cx, 'gcx, 'tcx> {
+    fn tcx(&self) -> TyCtxt<'cx, 'gcx, 'tcx> {
         self.infcx.tcx
     }
 
-    fn fold_ty(&mut self, t: Ty<'tcx>) -> Ty<'tcx> {
+    fn tag(&self) -> &'static str {
+        "Generalizer"
+    }
+
+    fn a_is_expected(&self) -> bool {
+        true
+    }
+
+    fn binders<T>(&mut self, a: &ty::Binder<T>, b: &ty::Binder<T>)
+                  -> RelateResult<'tcx, ty::Binder<T>>
+        where T: Relate<'tcx>
+    {
+        Ok(ty::Binder(self.relate(a.skip_binder(), b.skip_binder())?))
+    }
+
+    fn relate_with_variance<T: Relate<'tcx>>(&mut self,
+                                             variance: ty::Variance,
+                                             a: &T,
+                                             b: &T)
+                                             -> RelateResult<'tcx, T>
+    {
+        let old_ambient_variance = self.ambient_variance;
+        self.ambient_variance = self.ambient_variance.xform(variance);
+
+        let result = self.relate(a, b);
+        self.ambient_variance = old_ambient_variance;
+        result
+    }
+
+    fn tys(&mut self, t: Ty<'tcx>, t2: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
+        assert_eq!(t, t2); // we are abusing TypeRelation here; both LHS and RHS ought to be ==
+
         // Check to see whether the type we are genealizing references
         // any other type variable related to `vid` via
         // subtyping. This is basically our "occurs check", preventing
@@ -286,41 +365,63 @@ impl<'cx, 'gcx, 'tcx> ty::fold::TypeFolder<'gcx, 'tcx> for Generalizer<'cx, 'gcx
                 if sub_vid == self.for_vid_sub_root {
                     // If sub-roots are equal, then `for_vid` and
                     // `vid` are related via subtyping.
-                    self.cycle_detected = true;
-                    self.tcx().types.err
+                    return Err(TypeError::CyclicTy);
                 } else {
                     match variables.probe_root(vid) {
                         Some(u) => {
                             drop(variables);
-                            self.fold_ty(u)
+                            self.relate(&u, &u)
                         }
                         None => {
-                            if !self.is_eq_relation {
-                                let origin = variables.origin(vid);
-                                let new_var_id = variables.new_var(false, origin, None);
-                                let u = self.tcx().mk_var(new_var_id);
-                                debug!("generalize: replacing original vid={:?} with new={:?}",
-                                       vid, u);
-                                u
-                            } else {
-                                t
+                            match self.ambient_variance {
+                                // Invariant: no need to make a fresh type variable.
+                                ty::Invariant => return Ok(t),
+
+                                // Bivariant: make a fresh var, but we
+                                // may need a WF predicate. See
+                                // comment on `needs_wf` field for
+                                // more info.
+                                ty::Bivariant => self.needs_wf = true,
+
+                                // Co/contravariant: this will be
+                                // sufficiently constrained later on.
+                                ty::Covariant | ty::Contravariant => (),
                             }
+
+                            let origin = variables.origin(vid);
+                            let new_var_id = variables.new_var(false, origin, None);
+                            let u = self.tcx().mk_var(new_var_id);
+                            debug!("generalize: replacing original vid={:?} with new={:?}",
+                                   vid, u);
+                            return Ok(u);
                         }
                     }
                 }
             }
+            ty::TyInfer(ty::IntVar(_)) |
+            ty::TyInfer(ty::FloatVar(_)) => {
+                // No matter what mode we are in,
+                // integer/floating-point types must be equal to be
+                // relatable.
+                Ok(t)
+            }
             _ => {
-                t.super_fold_with(self)
+                relate::super_relate_tys(self, t, t)
             }
         }
     }
 
-    fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
+    fn regions(&mut self, r: ty::Region<'tcx>, r2: ty::Region<'tcx>)
+               -> RelateResult<'tcx, ty::Region<'tcx>> {
+        assert_eq!(r, r2); // we are abusing TypeRelation here; both LHS and RHS ought to be ==
+
         match *r {
             // Never make variables for regions bound within the type itself,
             // nor for erased regions.
             ty::ReLateBound(..) |
-            ty::ReErased => { return r; }
+            ty::ReErased => {
+                return Ok(r);
+            }
 
             // Early-bound regions should really have been substituted away before
             // we get to this point.
@@ -342,15 +443,16 @@ impl<'cx, 'gcx, 'tcx> ty::fold::TypeFolder<'gcx, 'tcx> for Generalizer<'cx, 'gcx
             ty::ReScope(..) |
             ty::ReVar(..) |
             ty::ReFree(..) => {
-                if self.is_eq_relation {
-                    return r;
+                match self.ambient_variance {
+                    ty::Invariant => return Ok(r),
+                    ty::Bivariant | ty::Covariant | ty::Contravariant => (),
                 }
             }
         }
 
         // FIXME: This is non-ideal because we don't give a
         // very descriptive origin for this region variable.
-        self.infcx.next_region_var(MiscVariable(self.span))
+        Ok(self.infcx.next_region_var(MiscVariable(self.span)))
     }
 }
 
diff --git a/src/librustc/ty/mod.rs b/src/librustc/ty/mod.rs
index 51cdba56cf1..f5d510c11ae 100644
--- a/src/librustc/ty/mod.rs
+++ b/src/librustc/ty/mod.rs
@@ -330,6 +330,66 @@ pub struct CrateVariancesMap {
     pub empty_variance: Rc<Vec<ty::Variance>>,
 }
 
+impl Variance {
+    /// `a.xform(b)` combines the variance of a context with the
+    /// variance of a type with the following meaning.  If we are in a
+    /// context with variance `a`, and we encounter a type argument in
+    /// a position with variance `b`, then `a.xform(b)` is the new
+    /// variance with which the argument appears.
+    ///
+    /// Example 1:
+    ///
+    ///     *mut Vec<i32>
+    ///
+    /// Here, the "ambient" variance starts as covariant. `*mut T` is
+    /// invariant with respect to `T`, so the variance in which the
+    /// `Vec<i32>` appears is `Covariant.xform(Invariant)`, which
+    /// yields `Invariant`. Now, the type `Vec<T>` is covariant with
+    /// respect to its type argument `T`, and hence the variance of
+    /// the `i32` here is `Invariant.xform(Covariant)`, which results
+    /// (again) in `Invariant`.
+    ///
+    /// Example 2:
+    ///
+    ///     fn(*const Vec<i32>, *mut Vec<i32)
+    ///
+    /// The ambient variance is covariant. A `fn` type is
+    /// contravariant with respect to its parameters, so the variance
+    /// within which both pointer types appear is
+    /// `Covariant.xform(Contravariant)`, or `Contravariant`.  `*const
+    /// T` is covariant with respect to `T`, so the variance within
+    /// which the first `Vec<i32>` appears is
+    /// `Contravariant.xform(Covariant)` or `Contravariant`.  The same
+    /// is true for its `i32` argument. In the `*mut T` case, the
+    /// variance of `Vec<i32>` is `Contravariant.xform(Invariant)`,
+    /// and hence the outermost type is `Invariant` with respect to
+    /// `Vec<i32>` (and its `i32` argument).
+    ///
+    /// Source: Figure 1 of "Taming the Wildcards:
+    /// Combining Definition- and Use-Site Variance" published in PLDI'11.
+    pub fn xform(self, v: ty::Variance) -> ty::Variance {
+        match (self, v) {
+            // Figure 1, column 1.
+            (ty::Covariant, ty::Covariant) => ty::Covariant,
+            (ty::Covariant, ty::Contravariant) => ty::Contravariant,
+            (ty::Covariant, ty::Invariant) => ty::Invariant,
+            (ty::Covariant, ty::Bivariant) => ty::Bivariant,
+
+            // Figure 1, column 2.
+            (ty::Contravariant, ty::Covariant) => ty::Contravariant,
+            (ty::Contravariant, ty::Contravariant) => ty::Covariant,
+            (ty::Contravariant, ty::Invariant) => ty::Invariant,
+            (ty::Contravariant, ty::Bivariant) => ty::Bivariant,
+
+            // Figure 1, column 3.
+            (ty::Invariant, _) => ty::Invariant,
+
+            // Figure 1, column 4.
+            (ty::Bivariant, _) => ty::Bivariant,
+        }
+    }
+}
+
 #[derive(Clone, Copy, Debug, RustcDecodable, RustcEncodable)]
 pub struct MethodCallee<'tcx> {
     /// Impl method ID, for inherent methods, or trait method ID, otherwise.
diff --git a/src/librustc_typeck/variance/constraints.rs b/src/librustc_typeck/variance/constraints.rs
index e986a381cd9..cb2ee7dd1bc 100644
--- a/src/librustc_typeck/variance/constraints.rs
+++ b/src/librustc_typeck/variance/constraints.rs
@@ -27,7 +27,6 @@ use rustc_data_structures::transitive_relation::TransitiveRelation;
 
 use super::terms::*;
 use super::terms::VarianceTerm::*;
-use super::xform::*;
 
 pub struct ConstraintContext<'a, 'tcx: 'a> {
     pub terms_cx: TermsContext<'a, 'tcx>,
diff --git a/src/librustc_typeck/variance/xform.rs b/src/librustc_typeck/variance/xform.rs
index 507734ce35e..7106ca4d420 100644
--- a/src/librustc_typeck/variance/xform.rs
+++ b/src/librustc_typeck/variance/xform.rs
@@ -10,35 +10,6 @@
 
 use rustc::ty;
 
-pub trait Xform {
-    fn xform(self, v: Self) -> Self;
-}
-
-impl Xform for ty::Variance {
-    fn xform(self, v: ty::Variance) -> ty::Variance {
-        // "Variance transformation", Figure 1 of The Paper
-        match (self, v) {
-            // Figure 1, column 1.
-            (ty::Covariant, ty::Covariant) => ty::Covariant,
-            (ty::Covariant, ty::Contravariant) => ty::Contravariant,
-            (ty::Covariant, ty::Invariant) => ty::Invariant,
-            (ty::Covariant, ty::Bivariant) => ty::Bivariant,
-
-            // Figure 1, column 2.
-            (ty::Contravariant, ty::Covariant) => ty::Contravariant,
-            (ty::Contravariant, ty::Contravariant) => ty::Covariant,
-            (ty::Contravariant, ty::Invariant) => ty::Invariant,
-            (ty::Contravariant, ty::Bivariant) => ty::Bivariant,
-
-            // Figure 1, column 3.
-            (ty::Invariant, _) => ty::Invariant,
-
-            // Figure 1, column 4.
-            (ty::Bivariant, _) => ty::Bivariant,
-        }
-    }
-}
-
 pub fn glb(v1: ty::Variance, v2: ty::Variance) -> ty::Variance {
     // Greatest lower bound of the variance lattice as
     // defined in The Paper:
diff --git a/src/test/compile-fail/region-invariant-static-error-reporting.rs b/src/test/compile-fail/region-invariant-static-error-reporting.rs
index d25674a74b1..646ae8183a2 100644
--- a/src/test/compile-fail/region-invariant-static-error-reporting.rs
+++ b/src/test/compile-fail/region-invariant-static-error-reporting.rs
@@ -13,9 +13,8 @@
 // over time, but this test used to exhibit some pretty bogus messages
 // that were not remotely helpful.
 
-// error-pattern:cannot infer
-// error-pattern:cannot outlive the lifetime 'a
-// error-pattern:must be valid for the static lifetime
+// error-pattern:the lifetime 'a
+// error-pattern:the static lifetime
 
 struct Invariant<'a>(Option<&'a mut &'a mut ()>);
 
diff --git a/src/test/compile-fail/regions-trait-object-subtyping.rs b/src/test/compile-fail/regions-trait-object-subtyping.rs
index e8ada6a1755..948fb7e1ef6 100644
--- a/src/test/compile-fail/regions-trait-object-subtyping.rs
+++ b/src/test/compile-fail/regions-trait-object-subtyping.rs
@@ -22,7 +22,7 @@ fn foo2<'a:'b,'b>(x: &'b mut (Dummy+'a)) -> &'b mut (Dummy+'b) {
 
 fn foo3<'a,'b>(x: &'a mut Dummy) -> &'b mut Dummy {
     // Without knowing 'a:'b, we can't coerce
-    x //~ ERROR cannot infer an appropriate lifetime
+    x //~ ERROR lifetime bound not satisfied
      //~^ ERROR cannot infer an appropriate lifetime
 }
 
diff --git a/src/test/compile-fail/variance-contravariant-arg-object.rs b/src/test/compile-fail/variance-contravariant-arg-object.rs
index d3bf92e85f4..1795ac95358 100644
--- a/src/test/compile-fail/variance-contravariant-arg-object.rs
+++ b/src/test/compile-fail/variance-contravariant-arg-object.rs
@@ -21,7 +21,7 @@ fn get_min_from_max<'min, 'max>(v: Box<Get<&'max i32>>)
                                 -> Box<Get<&'min i32>>
     where 'max : 'min
 {
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn get_max_from_min<'min, 'max, G>(v: Box<Get<&'min i32>>)
@@ -29,7 +29,7 @@ fn get_max_from_min<'min, 'max, G>(v: Box<Get<&'min i32>>)
     where 'max : 'min
 {
     // Previously OK:
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn main() { }
diff --git a/src/test/compile-fail/variance-covariant-arg-object.rs b/src/test/compile-fail/variance-covariant-arg-object.rs
index 0e94e35df28..ad059a467f5 100644
--- a/src/test/compile-fail/variance-covariant-arg-object.rs
+++ b/src/test/compile-fail/variance-covariant-arg-object.rs
@@ -22,14 +22,14 @@ fn get_min_from_max<'min, 'max>(v: Box<Get<&'max i32>>)
     where 'max : 'min
 {
     // Previously OK, now an error as traits are invariant.
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn get_max_from_min<'min, 'max, G>(v: Box<Get<&'min i32>>)
                                    -> Box<Get<&'max i32>>
     where 'max : 'min
 {
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn main() { }
diff --git a/src/test/compile-fail/variance-invariant-arg-object.rs b/src/test/compile-fail/variance-invariant-arg-object.rs
index aa3e06c015d..9edb510b826 100644
--- a/src/test/compile-fail/variance-invariant-arg-object.rs
+++ b/src/test/compile-fail/variance-invariant-arg-object.rs
@@ -18,14 +18,14 @@ fn get_min_from_max<'min, 'max>(v: Box<Get<&'max i32>>)
                                 -> Box<Get<&'min i32>>
     where 'max : 'min
 {
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn get_max_from_min<'min, 'max, G>(v: Box<Get<&'min i32>>)
                                    -> Box<Get<&'max i32>>
     where 'max : 'min
 {
-    v //~ ERROR cannot infer an appropriate lifetime
+    v //~ ERROR mismatched types
 }
 
 fn main() { }
diff --git a/src/test/run-pass/issue-41677.rs b/src/test/run-pass/issue-41677.rs
new file mode 100644
index 00000000000..d014382ca39
--- /dev/null
+++ b/src/test/run-pass/issue-41677.rs
@@ -0,0 +1,37 @@
+// Copyright 2016 The Rust Project Developers. See the COPYRIGHT
+// file at the top-level directory of this distribution and at
+// http://rust-lang.org/COPYRIGHT.
+//
+// Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+// Regression test for #41677. The local variable was winding up with
+// a type `Receiver<?T, H>` where `?T` was unconstrained, because we
+// failed to enforce the WF obligations and `?T` is a bivariant type
+// parameter position.
+
+#![allow(unused_variables, dead_code)]
+
+use std::marker::PhantomData;
+
+trait Handle {
+    type Inner;
+}
+
+struct ResizingHandle<H>(PhantomData<H>);
+impl<H> Handle for ResizingHandle<H> {
+    type Inner = H;
+}
+
+struct Receiver<T, H: Handle<Inner=T>>(PhantomData<H>);
+
+fn channel<T>(size: usize) -> Receiver<T, ResizingHandle<T>> {
+    let rx = Receiver(PhantomData);
+    rx
+}
+
+fn main() {
+}