mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

clean up skolemiza in traits

This commit is contained in:
csmoe 2018-10-24 14:46:43 +08:00 committed by Who? Me?!
parent 3c318049dc
commit e4df53b93d
3 changed files with 18 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/traits/associated-types.md
View File

@ -154,7 +154,7 @@ The key point is that, on success, unification can also give back to
us a set of subgoals that still remain to be proven (it can also give us a set of subgoals that still remain to be proven (it can also give
back region constraints, but those are not relevant here). back region constraints, but those are not relevant here).
Whenever unification encounters an (unskolemized!) associated type Whenever unification encounters an (un-placeholder!) associated type
projection P being equated with some other type T, it always succeeds, projection P being equated with some other type T, it always succeeds,
but it produces a subgoal `ProjectionEq(P = T)` that is propagated but it produces a subgoal `ProjectionEq(P = T)` that is propagated
back up. Thus it falls to the ordinary workings of the trait system back up. Thus it falls to the ordinary workings of the trait system

6
src/traits/caching.md
View File

@ -11,10 +11,10 @@ but *replay* its effects on the type variables.
## An example ## An example
The high-level idea of how the cache works is that we first replace The high-level idea of how the cache works is that we first replace
all unbound inference variables with skolemized versions. Therefore, all unbound inference variables with placeholder versions. Therefore,
if we had a trait reference `usize : Foo<$t>`, where `$t` is an unbound if we had a trait reference `usize : Foo<$t>`, where `$t` is an unbound
inference variable, we might replace it with `usize : Foo<$0>`, where inference variable, we might replace it with `usize : Foo<$0>`, where
`$0` is a skolemized type. We would then look this up in the cache. `$0` is a placeholder type. We would then look this up in the cache.
If we found a hit, the hit would tell us the immediate next step to If we found a hit, the hit would tell us the immediate next step to
take in the selection process (e.g. apply impl #22, or apply where take in the selection process (e.g. apply impl #22, or apply where
@ -37,7 +37,7 @@ we would [confirm] `ImplCandidate(22)`, which would (as a side-effect) unify
[confirm]: ./resolution.html#confirmation [confirm]: ./resolution.html#confirmation
Now, at some later time, we might come along and see a `usize : Now, at some later time, we might come along and see a `usize :
Foo<$u>`. When skolemized, this would yield `usize : Foo<$0>`, just as Foo<$u>`. When placeholder, this would yield `usize : Foo<$0>`, just as
before, and hence the cache lookup would succeed, yielding before, and hence the cache lookup would succeed, yielding
`ImplCandidate(22)`. We would confirm `ImplCandidate(22)` which would `ImplCandidate(22)`. We would confirm `ImplCandidate(22)` which would
(as a side-effect) unify `$u` with `isize`. (as a side-effect) unify `$u` with `isize`.

28
src/traits/hrtb.md
View File

@ -5,7 +5,7 @@ bounds*. An example of such a bound is `for<'a> MyTrait<&'a isize>`.
Let's walk through how selection on higher-ranked trait references Let's walk through how selection on higher-ranked trait references
works. works.
## Basic matching and skolemization leaks ## Basic matching and placeholder leaks
Suppose we have a trait `Foo`: Suppose we have a trait `Foo`:
@ -36,11 +36,11 @@ to the subtyping for higher-ranked types (which is described [here][hrsubtype]
and also in a [paper by SPJ]. If you wish to understand higher-ranked and also in a [paper by SPJ]. If you wish to understand higher-ranked
subtyping, we recommend you read the paper). There are a few parts: subtyping, we recommend you read the paper). There are a few parts:
**TODO**: We should define _skolemize_. **TODO**: We should define _placeholder_.
1. _Skolemize_ the obligation. 1. _Skolemize_ the obligation.
2. Match the impl against the skolemized obligation. 2. Match the impl against the placeholder obligation.
3. Check for _skolemization leaks_. 3. Check for _placeholder leaks_.
[hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md [hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md
[paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/ [paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/
@ -48,8 +48,8 @@ subtyping, we recommend you read the paper). There are a few parts:
So let's work through our example. So let's work through our example.
1. The first thing we would do is to 1. The first thing we would do is to
skolemize the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0` placeholder the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`
represents skolemized region #0). Note that we now have no quantifiers; represents placeholder region #0). Note that we now have no quantifiers;
in terms of the compiler type, this changes from a `ty::PolyTraitRef` in terms of the compiler type, this changes from a `ty::PolyTraitRef`
to a `TraitRef`. We would then create the `TraitRef` from the impl, to a `TraitRef`. We would then create the `TraitRef` from the impl,
using fresh variables for it's bound regions (and thus getting using fresh variables for it's bound regions (and thus getting
@ -59,10 +59,10 @@ using fresh variables for it's bound regions (and thus getting
we relate the two trait refs, yielding a graph with the constraint we relate the two trait refs, yielding a graph with the constraint
that `'0 == '$a`. that `'0 == '$a`.
3. Finally, we check for skolemization "leaks" – a 3. Finally, we check for placeholder "leaks" – a
leak is basically any attempt to relate a skolemized region to another leak is basically any attempt to relate a placeholder region to another
skolemized region, or to any region that pre-existed the impl match. placeholder region, or to any region that pre-existed the impl match.
The leak check is done by searching from the skolemized region to find The leak check is done by searching from the placeholder region to find
the set of regions that it is related to in any way. This is called the set of regions that it is related to in any way. This is called
the "taint" set. To pass the check, that set must consist *solely* of the "taint" set. To pass the check, that set must consist *solely* of
itself and region variables from the impl. If the taint set includes itself and region variables from the impl. If the taint set includes
@ -78,7 +78,7 @@ impl Foo<&'static isize> for StaticInt;
We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be
considered unsatisfied. The check begins just as before. `'a` is considered unsatisfied. The check begins just as before. `'a` is
skolemized to `'0` and the impl trait reference is instantiated to placeholder to `'0` and the impl trait reference is instantiated to
`Foo<&'static isize>`. When we relate those two, we get a constraint `Foo<&'static isize>`. When we relate those two, we get a constraint
like `'static == '0`. This means that the taint set for `'0` is `{'0, like `'static == '0`. This means that the taint set for `'0` is `{'0,
'static}`, which fails the leak check. 'static}`, which fails the leak check.
@ -111,16 +111,16 @@ Now let's say we have a obligation `Baz: for<'a> Foo<&'a isize>` and we match
this impl. What obligation is generated as a result? We want to get this impl. What obligation is generated as a result? We want to get
`Baz: for<'a> Bar<&'a isize>`, but how does that happen? `Baz: for<'a> Bar<&'a isize>`, but how does that happen?
After the matching, we are in a position where we have a skolemized After the matching, we are in a position where we have a placeholder
substitution like `X => &'0 isize`. If we apply this substitution to the substitution like `X => &'0 isize`. If we apply this substitution to the
impl obligations, we get `F : Bar<&'0 isize>`. Obviously this is not impl obligations, we get `F : Bar<&'0 isize>`. Obviously this is not
directly usable because the skolemized region `'0` cannot leak out of directly usable because the placeholder region `'0` cannot leak out of
our computation. our computation.
What we do is to create an inverse mapping from the taint set of `'0` What we do is to create an inverse mapping from the taint set of `'0`
back to the original bound region (`'a`, here) that `'0` resulted back to the original bound region (`'a`, here) that `'0` resulted
from. (This is done in `higher_ranked::plug_leaks`). We know that the from. (This is done in `higher_ranked::plug_leaks`). We know that the
leak check passed, so this taint set consists solely of the skolemized leak check passed, so this taint set consists solely of the placeholder
region itself plus various intermediate region variables. We then walk region itself plus various intermediate region variables. We then walk
the trait-reference and convert every region in that taint set back to the trait-reference and convert every region in that taint set back to
a late-bound region, so in this case we'd wind up with a late-bound region, so in this case we'd wind up with