Skip to content

Commit

Permalink
Auto merge of #54649 - nikomatsakis:universes-refactor-1, r=scalexm
Browse files Browse the repository at this point in the history
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
  • Loading branch information
bors committed Oct 4, 2018
2 parents a57f1c9 + 85b9956 commit 8c4ad4e
Show file tree
Hide file tree
Showing 34 changed files with 1,883 additions and 1,547 deletions.
2 changes: 1 addition & 1 deletion src/librustc/ich/impls_ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ for ty::RegionKind {
}
ty::ReLateBound(..) |
ty::ReVar(..) |
ty::ReSkolemized(..) => {
ty::RePlaceholder(..) => {
bug!("StableHasher: unexpected region {:?}", *self)
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/librustc/infer/canonical/canonicalizer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
7 changes: 4 additions & 3 deletions src/librustc/infer/combine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions src/librustc/infer/error_reporting/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}

Expand Down
2 changes: 1 addition & 1 deletion src/librustc/infer/freshen.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
22 changes: 11 additions & 11 deletions src/librustc/infer/higher_ranked/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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 `>`).

Expand Down Expand Up @@ -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
Expand All @@ -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)?

Expand All @@ -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
Expand Down
Loading

0 comments on commit 8c4ad4e

Please sign in to comment.