Auto merge of rust-lang#54649 - nikomatsakis:universes-refactor-1, r=scalexm

adopt "placeholders" to represent universally quantified regions

This does a few preliminary refactorings that lay some groundwork for moving towards universe integration. Two things, primarily:

- Rename from "skolemized" to "placeholder"
- When instantiating `for<'a, 'b, 'c>`, just create one universe for all 3 regions, and distinguish them from one another using the `BoundRegion`.
    - This is more accurate, and I think that in general we'll be moving towards a model of separating "binder" (universe, debruijn index) from "index within binder" in a number of places.
    - In principle, it feels the current setup of making lots of universes could lead to us doing the wrong thing, but I've actually not been able to come up with an example where this is so.

r? @scalexm
cc @arielb1

Author: bors

src/librustc/ich/impls_ty.rs

@@ -131,7 +131,7 @@ for ty::RegionKind {
             }
             ty::ReLateBound(..) |
             ty::ReVar(..) |
-            ty::ReSkolemized(..) => {
+            ty::RePlaceholder(..) => {
                 bug!("StableHasher: unexpected region {:?}", *self)
             }
         }

src/librustc/infer/canonical/canonicalizer.rs

@@ -224,7 +224,7 @@ impl<'cx, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for Canonicalizer<'cx, 'gcx, 'tcx>
             ty::ReEarlyBound(..)
             | ty::ReFree(_)
             | ty::ReScope(_)
-            | ty::ReSkolemized(..)
+            | ty::RePlaceholder(..)
             | ty::ReEmpty
             | ty::ReErased => {
                 if self.canonicalize_region_mode.other_free_regions {

src/librustc/infer/combine.rs

@@ -458,9 +458,10 @@ impl<'cx, 'gcx, 'tcx> TypeRelation<'cx, 'gcx, 'tcx> for Generalizer<'cx, 'gcx, '
                 return Ok(r);
             }
 
-            // Always make a fresh region variable for skolemized regions;
-            // the higher-ranked decision procedures rely on this.
-            ty::ReSkolemized(..) => { }
+            // Always make a fresh region variable for placeholder
+            // regions; the higher-ranked decision procedures rely on
+            // this.
+            ty::RePlaceholder(..) => { }
 
             // For anything else, we make a region variable, unless we
             // are *equating*, in which case it's just wasteful.

src/librustc/infer/error_reporting/mod.rs

@@ -142,12 +142,12 @@ impl<'a, 'gcx, 'tcx> TyCtxt<'a, 'gcx, 'tcx> {
 
             ty::ReEmpty => ("the empty lifetime".to_owned(), None),
 
-            // FIXME(#13998) ReSkolemized should probably print like
+            // FIXME(#13998) RePlaceholder should probably print like
             // ReFree rather than dumping Debug output on the user.
             //
             // We shouldn't really be having unification failures with ReVar
             // and ReLateBound though.
-            ty::ReSkolemized(..) | ty::ReVar(_) | ty::ReLateBound(..) | ty::ReErased => {
+            ty::RePlaceholder(..) | ty::ReVar(_) | ty::ReLateBound(..) | ty::ReErased => {
                 (format!("lifetime {:?}", region), None)
             }
 

src/librustc/infer/freshen.rs

@@ -107,7 +107,7 @@ impl<'a, 'gcx, 'tcx> TypeFolder<'gcx, 'tcx> for TypeFreshener<'a, 'gcx, 'tcx> {
             ty::ReFree(_) |
             ty::ReScope(_) |
             ty::ReVar(_) |
-            ty::ReSkolemized(..) |
+            ty::RePlaceholder(..) |
             ty::ReEmpty |
             ty::ReErased => {
                 // replace all free regions with 'erased

src/librustc/infer/higher_ranked/README.md

@@ -72,11 +72,11 @@ the same lifetime, but not the reverse.
 Here is the algorithm we use to perform the subtyping check:
 
 1. Replace all bound regions in the subtype with new variables
-2. Replace all bound regions in the supertype with skolemized
-   equivalents. A "skolemized" region is just a new fresh region
+2. Replace all bound regions in the supertype with placeholder
+   equivalents. A "placeholder" region is just a new fresh region
    name.
 3. Check that the parameter and return types match as normal
-4. Ensure that no skolemized regions 'leak' into region variables
+4. Ensure that no placeholder regions 'leak' into region variables
    visible from "the outside"
 
 Let's walk through some examples and see how this algorithm plays out.
@@ -95,7 +95,7 @@ like so:
 Here the upper case `&A` indicates a *region variable*, that is, a
 region whose value is being inferred by the system. I also replaced
 `&b` with `&x`---I'll use letters late in the alphabet (`x`, `y`, `z`)
-to indicate skolemized region names. We can assume they don't appear
+to indicate placeholder region names. We can assume they don't appear
 elsewhere. Note that neither the sub- nor the supertype bind any
 region names anymore (as indicated by the absence of `<` and `>`).
 
@@ -133,7 +133,7 @@ match. This will ultimately require (as before) that `'a` <= `&x`
 must hold: but this does not hold. `self` and `x` are both distinct
 free regions. So the subtype check fails.
 
-#### Checking for skolemization leaks
+#### Checking for placeholder leaks
 
 You may be wondering about that mysterious last step in the algorithm.
 So far it has not been relevant. The purpose of that last step is to
@@ -159,7 +159,7 @@ Now we compare the return types, which are covariant, and hence we have:
 
     fn(&'A T) <: for<'b> fn(&'b T)?
 
-Here we skolemize the bound region in the supertype to yield:
+Here we replace the bound region in the supertype with a placeholder to yield:
 
     fn(&'A T) <: fn(&'x T)?
 
@@ -175,23 +175,23 @@ region `x` and think that everything is happy. In fact, this behavior
 is *necessary*, it was key to the first example we walked through.
 
 The difference between this example and the first one is that the variable
-`A` already existed at the point where the skolemization occurred. In
+`A` already existed at the point where the placeholders were added. In
 the first example, you had two functions:
 
     for<'a> fn(&'a T) <: for<'b> fn(&'b T)
 
 and hence `&A` and `&x` were created "together". In general, the
-intention of the skolemized names is that they are supposed to be
+intention of the placeholder names is that they are supposed to be
 fresh names that could never be equal to anything from the outside.
 But when inference comes into play, we might not be respecting this
 rule.
 
 So the way we solve this is to add a fourth step that examines the
-constraints that refer to skolemized names. Basically, consider a
+constraints that refer to placeholder names. Basically, consider a
 non-directed version of the constraint graph. Let `Tainted(x)` be the
-set of all things reachable from a skolemized variable `x`.
+set of all things reachable from a placeholder variable `x`.
 `Tainted(x)` should not contain any regions that existed before the
-step at which the skolemization was performed. So this case here
+step at which the placeholders were created. So this case here
 would fail because `&x` was created alone, but is relatable to `&A`.
 
 ## Computing the LUB and GLB