now that we can handle subtyping, fix higher-ranked equality

3 files changed, 28 insertions, 22 deletions

diff --git a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
index 9ed4ec8eec1..195a284e69e 100644
--- a/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
+++ b/src/librustc_mir/borrow_check/nll/type_check/relate_tys.rs
@@ -458,19 +458,30 @@ impl<'cx, 'bccx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx>
             self.b_scopes.push(b_scope);
             self.a_scopes.push(a_scope);
 
-            // FIXME -- to be fully correct, we would set the ambient
-            // variance to Covariant here. As is, we will sometimes
-            // propagate down an ambient variance of Equal -- this in
-            // turn causes us to report errors in some cases where
-            // types perhaps *ought* to be equal. See the
-            // `hr-fn-aau-eq-abu.rs` test for an example. Fixing this
-            // though is a bit nontrivial: in particular, it would
-            // require a more involved handling of canonical
-            // variables, since we would no longer be able to rely on
-            // having an `==` relationship for canonical variables.
+            // Reset the ambient variance to covariant. This is needed
+            // to correctly handle cases like
+            //
+            //     for<'a> fn(&'a u32, &'a u3) == for<'b, 'c> fn(&'b u32, &'c u32)
+            //
+            // Somewhat surprisingly, these two types are actually
+            // **equal**, even though the one on the right looks more
+            // polymorphic. The reason is due to subtyping. To see it,
+            // consider that each function can call the other:
+            //
+            // - The left function can call the right with `'b` and
+            //   `'c` both equal to `'a`
+            //
+            // - The right function can call the left with `'a` set to
+            //   `{P}`, where P is the point in the CFG where the call
+            //   itself occurs. Note that `'b` and `'c` must both
+            //   include P. At the point, the call works because of
+            //   subtyping (i.e., `&'b u32 <: &{P} u32`).
+            let variance = ::std::mem::replace(&mut self.ambient_variance, ty::Variance::Covariant);
 
             self.relate(a.skip_binder(), b.skip_binder())?;
 
+            self.ambient_variance = variance;
+
             self.b_scopes.pop().unwrap();
             self.a_scopes.pop().unwrap();
         }
@@ -491,8 +502,14 @@ impl<'cx, 'bccx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx>
             self.a_scopes.push(a_scope);
             self.b_scopes.push(b_scope);
 
+            // Reset ambient variance to contravariance. See the
+            // covariant case above for an explanation.
+            let variance = ::std::mem::replace(&mut self.ambient_variance, ty::Variance::Contravariant);
+
             self.relate(a.skip_binder(), b.skip_binder())?;
 
+            self.ambient_variance = variance;
+
             self.b_scopes.pop().unwrap();
             self.a_scopes.pop().unwrap();
         }
diff --git a/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.rs b/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.rs
index 9b8268d9736..bc7b031f72c 100644
--- a/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.rs
+++ b/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.rs
@@ -16,9 +16,7 @@
 // another -- effectively, the single lifetime `'a` is just inferred
 // to be the intersection of the two distinct lifetimes.
 //
-// FIXME: However, we currently reject this example with an error,
-// because of how we handle binders and equality in `relate_tys`.
-//
+// compile-pass
 // compile-flags:-Zno-leak-check
 
 #![feature(nll)]
@@ -31,7 +29,6 @@ fn make_cell_aa() -> Cell<for<'a> fn(&'a u32, &'a u32)> {
 
 fn aa_eq_ab() {
     let a: Cell<for<'a, 'b> fn(&'a u32, &'b u32)> = make_cell_aa();
-    //~^ ERROR higher-ranked subtype error
     drop(a);
 }
 
diff --git a/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.stderr b/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.stderr
deleted file mode 100644
index 17e8a32cb2a..00000000000
--- a/src/test/ui/nll/relate_tys/hr-fn-aau-eq-abu.stderr
+++ /dev/null
@@ -1,8 +0,0 @@
-error: higher-ranked subtype error
-  --> $DIR/hr-fn-aau-eq-abu.rs:33:53
-   |
-LL |     let a: Cell<for<'a, 'b> fn(&'a u32, &'b u32)> = make_cell_aa();
-   |                                                     ^^^^^^^^^^^^^^
-
-error: aborting due to previous error
-