Skip to content

Commit 659386f

Browse files
committed
replace bound region with placeholder
1 parent c7c309d commit 659386f

File tree

3 files changed

+15
-16
lines changed

3 files changed

+15
-16
lines changed

src/appendix/glossary.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ rib | a data structure in the name resolver that keeps trac
5353
sess | the compiler session, which stores global data used throughout compilation
5454
side tables | because the AST and HIR are immutable once created, we often carry extra information about them in the form of hashtables, indexed by the id of a particular node.
5555
sigil | like a keyword but composed entirely of non-alphanumeric tokens. For example, `&` is a sigil for references.
56-
placeholder | a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on placeholder and universes](../borrow_check/region_inference.html#placeholder) for more details.
56+
placeholder | **NOTE: skolemization is deprecated by placeholder** a way of handling subtyping around "for-all" types (e.g., `for<'a> fn(&'a u32)`) as well as solving higher-ranked trait bounds (e.g., `for<'a> T: Trait<'a>`). See [the chapter on placeholder and universes](../borrow_check/region_inference.html#placeholder) for more details.
5757
soundness | soundness is a technical term in type theory. Roughly, if a type system is sound, then if a program type-checks, it is type-safe; i.e. I can never (in safe rust) force a value into a variable of the wrong type. (see "completeness").
5858
span | a location in the user's source code, used for error reporting primarily. These are like a file-name/line-number/column tuple on steroids: they carry a start/end point, and also track macro expansions and compiler desugaring. All while being packed into a few bytes (really, it's an index into a table). See the Span datatype for more.
5959
substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)

src/borrow_check/region_inference.md

+7-8
Original file line numberDiff line numberDiff line change
@@ -80,8 +80,8 @@ The kinds of region elements are as follows:
8080
to the remainder of program execution after this function returns.
8181
- There is an element `!1` for each placeholder region `!1`. This
8282
corresponds (intuitively) to some unknown set of other elements –
83-
for details on placeholder, see the section
84-
[placeholder and universes](#placeholder).
83+
for details on placeholders, see the section
84+
[placeholders and universes](#placeholder).
8585

8686
## Causal tracking
8787

@@ -117,7 +117,7 @@ for its argument, and `bar` wants to be given a function that that
117117
accepts **any** reference (so it can call it with something on its
118118
stack, for example). But *how* do we reject it and *why*?
119119

120-
### Subtyping and Placeholder
120+
### Subtyping and Placeholders
121121

122122
When we type-check `main`, and in particular the call `bar(foo)`, we
123123
are going to wind up with a subtyping relationship like this one:
@@ -129,8 +129,7 @@ the type of `foo` the type `bar` expects
129129
```
130130

131131
We handle this sort of subtyping by taking the variables that are
132-
bound in the supertype and **placeholder** them: this means that we
133-
replace them with
132+
bound in the supertype and replace them with
134133
[universally quantified](../appendix/background.html#quantified)
135134
representatives, written like `!1`. We call these regions "placeholder
136135
regions" – they represent, basically, "some unknown region".
@@ -198,7 +197,7 @@ fn bar<'a, T>(t: &'a T) {
198197
```
199198

200199
Here, the name `'b` is not part of the root universe. Instead, when we
201-
"enter" into this `for<'b>` (e.g., by placeholder it), we will create
200+
"enter" into this `for<'b>` (e.g., by replace it with a placeholder), we will create
202201
a child universe of the root, let's call it U1:
203202

204203
```text
@@ -411,7 +410,7 @@ for<'a> fn(&'a u32, &'a u32)
411410
for<'b, 'c> fn(&'b u32, &'c u32)
412411
```
413412

414-
Here we would placeholer the supertype, as before, yielding:
413+
Here we would replace the bound region in the supertype with a placeholder, as before, yielding:
415414

416415
```text
417416
for<'a> fn(&'a u32, &'a u32)
@@ -476,7 +475,7 @@ an error. That's good: the problem is that we've gone from a fn that promises
476475
to return one of its two arguments, to a fn that is promising to return the
477476
first one. That is unsound. Let's see how it plays out.
478477

479-
First, we placeholder the supertype:
478+
First, we replace the bound region in the supertype with a placeholder:
480479

481480
```text
482481
for<'a> fn(&'a u32, &'a u32) -> &'a u32

src/traits/hrtb.md

+7-7
Original file line numberDiff line numberDiff line change
@@ -36,20 +36,20 @@ to the subtyping for higher-ranked types (which is described [here][hrsubtype]
3636
and also in a [paper by SPJ]. If you wish to understand higher-ranked
3737
subtyping, we recommend you read the paper). There are a few parts:
3838

39-
**TODO**: We should define _placeholder_.
40-
41-
1. _Skolemize_ the obligation.
42-
2. Match the impl against the placeholder obligation.
39+
1. replace bound regions in the obligation with placeholders.
40+
2. Match the impl against the [placeholder] obligation.
4341
3. Check for _placeholder leaks_.
4442

43+
[placeholder]: ../appendix/glossary.html#appendix-c-glossary
4544
[hrsubtype]: https://github.com/rust-lang/rust/tree/master/src/librustc/infer/higher_ranked/README.md
4645
[paper by SPJ]: http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/
4746

4847
So let's work through our example.
4948

5049
1. The first thing we would do is to
51-
placeholder the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`
52-
represents placeholder region #0). Note that we now have no quantifiers;
50+
replace the bound region in the obligation with a placeholder, yielding
51+
`AnyInt : Foo<&'0 isize>` (here `'0` represents placeholder region #0).
52+
Note that we now have no quantifiers;
5353
in terms of the compiler type, this changes from a `ty::PolyTraitRef`
5454
to a `TraitRef`. We would then create the `TraitRef` from the impl,
5555
using fresh variables for it's bound regions (and thus getting
@@ -78,7 +78,7 @@ impl Foo<&'static isize> for StaticInt;
7878

7979
We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be
8080
considered unsatisfied. The check begins just as before. `'a` is
81-
placeholder to `'0` and the impl trait reference is instantiated to
81+
replaced with a placeholder `'0` and the impl trait reference is instantiated to
8282
`Foo<&'static isize>`. When we relate those two, we get a constraint
8383
like `'static == '0`. This means that the taint set for `'0` is `{'0,
8484
'static}`, which fails the leak check.

0 commit comments

Comments
 (0)