Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adopt "placeholders" to represent universally quantified regions #54649

Merged
merged 10 commits into from
Oct 4, 2018
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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are still some occurences of "skolemization" and "skolemize" used as a verb :p

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