move the sub-unify check and extend the documentation a bit

I didn't like the sub-unify code executing when a predicate was
ENQUEUED, that felt fragile. I would have preferred to move the
sub-unify code so that it only occurred during generalization, but
that impacted diagnostics, so having it also occur when we process
subtype predicates felt pretty reasonable. (I guess we only need one
or the other, but I kind of prefer both, since the generalizer
ultimately feels like the *right* place to guarantee the properties we
want.)

Author: nikomatsakis

compiler/rustc_infer/src/infer/combine.rs

@@ -641,6 +641,11 @@ impl TypeRelation<'tcx> for Generalizer<'_, 'tcx> {
                                 .type_variables()
                                 .new_var(self.for_universe, Diverging::NotDiverging, origin);
                             let u = self.tcx().mk_ty_var(new_var_id);
+
+                            // Record that we replaced `vid` with `new_var_id` as part of a generalization
+                            // operation. This is needed to detect cyclic types. To see why, see the
+                            // docs in the `type_variables` module.
+                            self.infcx.inner.borrow_mut().type_variables().sub(vid, new_var_id);
                             debug!("generalize: replacing original vid={:?} with new={:?}", vid, u);
                             Ok(u)
                         }

compiler/rustc_infer/src/infer/mod.rs

@@ -961,23 +961,26 @@ impl<'a, 'tcx> InferCtxt<'a, 'tcx> {
         param_env: ty::ParamEnv<'tcx>,
         predicate: ty::PolySubtypePredicate<'tcx>,
     ) -> Option<InferResult<'tcx, ()>> {
-        // Subtle: it's ok to skip the binder here and resolve because
-        // `shallow_resolve` just ignores anything that is not a type
-        // variable, and because type variable's can't (at present, at
-        // least) capture any of the things bound by this binder.
+        // Check for two unresolved inference variables, in which case we can
+        // make no progress. This is partly a micro-optimization, but it's
+        // also an opportunity to "sub-unify" the variables. This isn't
+        // *necessary* to prevent cycles, because they would eventually be sub-unified
+        // anyhow during generalization, but it helps with diagnostics (we can detect
+        // earlier that they are sub-unified).
         //
-        // NOTE(nmatsakis): really, there is no *particular* reason to do this
-        // `shallow_resolve` here except as a micro-optimization.
-        // Naturally I could not resist.
-        let two_unbound_type_vars = {
-            let a = self.shallow_resolve(predicate.skip_binder().a);
-            let b = self.shallow_resolve(predicate.skip_binder().b);
-            a.is_ty_var() && b.is_ty_var()
-        };
-
-        if two_unbound_type_vars {
-            // Two unbound type variables? Can't make progress.
-            return None;
+        // Note that we can just skip the binders here because
+        // type variables can't (at present, at
+        // least) capture any of the things bound by this binder.
+        {
+            let r_a = self.shallow_resolve(predicate.skip_binder().a);
+            let r_b = self.shallow_resolve(predicate.skip_binder().b);
+            match (r_a.kind(), r_b.kind()) {
+                (&ty::Infer(ty::TyVar(a_vid)), &ty::Infer(ty::TyVar(b_vid))) => {
+                    self.inner.borrow_mut().type_variables().sub(a_vid, b_vid);
+                    return None;
+                }
+                _ => {}
+            }
         }
 
         Some(self.commit_if_ok(|_snapshot| {

compiler/rustc_infer/src/infer/sub.rs

@@ -84,7 +84,7 @@ impl TypeRelation<'tcx> for Sub<'combine, 'infcx, 'tcx> {
         let a = infcx.inner.borrow_mut().type_variables().replace_if_possible(a);
         let b = infcx.inner.borrow_mut().type_variables().replace_if_possible(b);
         match (a.kind(), b.kind()) {
-            (&ty::Infer(TyVar(a_vid)), &ty::Infer(TyVar(b_vid))) => {
+            (&ty::Infer(TyVar(_)), &ty::Infer(TyVar(_))) => {
                 // Shouldn't have any LBR here, so we can safely put
                 // this under a binder below without fear of accidental
                 // capture.
@@ -96,7 +96,6 @@ impl TypeRelation<'tcx> for Sub<'combine, 'infcx, 'tcx> {
                 // have to record in the `type_variables` tracker that
                 // the two variables are equal modulo subtyping, which
                 // is important to the occurs check later on.
-                infcx.inner.borrow_mut().type_variables().sub(a_vid, b_vid);
                 self.fields.obligations.push(Obligation::new(
                     self.fields.trace.cause.clone(),
                     self.fields.param_env,

compiler/rustc_infer/src/infer/type_variable.rs

@@ -75,14 +75,30 @@ pub struct TypeVariableStorage<'tcx> {
     ///     ?1 <: ?3
     ///     Box<?3> <: ?1
     ///
-    /// This works because `?1` and `?3` are unified in the
-    /// `sub_relations` relation (not in `eq_relations`). Then when we
-    /// process the `Box<?3> <: ?1` constraint, we do an occurs check
-    /// on `Box<?3>` and find a potential cycle.
+    /// Without this second table, what would happen in a case like
+    /// this is that we would instantiate `?1` with a generalized
+    /// type like `Box<?6>`. We would then relate `Box<?3> <: Box<?6>`
+    /// and infer that `?3 <: ?6`. Next, since `?1` was instantiated,
+    /// we would process `?1 <: ?3`, generalize `?1 = Box<?6>` to `Box<?9>`,
+    /// and instantiate `?3` with `Box<?9>`. Finally, we would relate
+    /// `?6 <: ?9`. But now that we instantiated `?3`, we can process
+    /// `?3 <: ?6`, which gives us `Box<?9> <: ?6`... and the cycle
+    /// continues. (This is `occurs-check-2.rs`.)
+    ///
+    /// What prevents this cycle is that when we generalize
+    /// `Box<?3>` to `Box<?6>`, we also sub-unify `?3` and `?6`
+    /// (in the generalizer). When we then process `Box<?6> <: ?3`,
+    /// the occurs check then fails because `?6` and `?3` are sub-unified,
+    /// and hence generalization fails.
     ///
     /// This is reasonable because, in Rust, subtypes have the same
     /// "skeleton" and hence there is no possible type such that
     /// (e.g.)  `Box<?3> <: ?3` for any `?3`.
+    ///
+    /// In practice, we sometimes sub-unify variables in other spots, such
+    /// as when processing subtype predicates. This is not necessary but is
+    /// done to aid diagnostics, as it allows us to be more effective when
+    /// we guide the user towards where they should insert type hints.
     sub_relations: ut::UnificationTableStorage<ty::TyVid>,
 }