replace bound region with placeholder

This commit is contained in:
csmoe 2018-10-25 11:01:08 +08:00 committed by Who? Me?!
parent e4df53b93d
commit 68d30b64cf
3 changed files with 15 additions and 16 deletions

View File

@ -53,7 +53,7 @@ rib | a data structure in the name resolver that keeps trac
sess | the compiler session, which stores global data used throughout compilation
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.
sigil | like a keyword but composed entirely of non-alphanumeric tokens. For example, `&` is a sigil for references.
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.
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.
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").
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.
substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)

View File

@ -80,8 +80,8 @@ The kinds of region elements are as follows:
to the remainder of program execution after this function returns.
- There is an element `!1` for each placeholder region `!1`. This
corresponds (intuitively) to some unknown set of other elements
for details on placeholder, see the section
[placeholder and universes](#placeholder).
for details on placeholders, see the section
[placeholders and universes](#placeholder).
## Causal tracking
@ -117,7 +117,7 @@ for its argument, and `bar` wants to be given a function that that
accepts **any** reference (so it can call it with something on its
stack, for example). But *how* do we reject it and *why*?
### Subtyping and Placeholder
### Subtyping and Placeholders
When we type-check `main`, and in particular the call `bar(foo)`, we
are going to wind up with a subtyping relationship like this one:
@ -129,8 +129,7 @@ the type of `foo` the type `bar` expects
```
We handle this sort of subtyping by taking the variables that are
bound in the supertype and **placeholder** them: this means that we
replace them with
bound in the supertype and replace them with
[universally quantified](../appendix/background.html#quantified)
representatives, written like `!1`. We call these regions "placeholder
regions" they represent, basically, "some unknown region".
@ -198,7 +197,7 @@ fn bar<'a, T>(t: &'a T) {
```
Here, the name `'b` is not part of the root universe. Instead, when we
"enter" into this `for<'b>` (e.g., by placeholder it), we will create
"enter" into this `for<'b>` (e.g., by replace it with a placeholder), we will create
a child universe of the root, let's call it U1:
```text
@ -411,7 +410,7 @@ for<'a> fn(&'a u32, &'a u32)
for<'b, 'c> fn(&'b u32, &'c u32)
```
Here we would placeholer the supertype, as before, yielding:
Here we would replace the bound region in the supertype with a placeholder, as before, yielding:
```text
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
to return one of its two arguments, to a fn that is promising to return the
first one. That is unsound. Let's see how it plays out.
First, we placeholder the supertype:
First, we replace the bound region in the supertype with a placeholder:
```text
for<'a> fn(&'a u32, &'a u32) -> &'a u32

View File

@ -36,20 +36,20 @@ 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
subtyping, we recommend you read the paper). There are a few parts:
**TODO**: We should define _placeholder_.
1. _Skolemize_ the obligation.
2. Match the impl against the placeholder obligation.
1. replace bound regions in the obligation with placeholders.
2. Match the impl against the [placeholder] obligation.
3. Check for _placeholder leaks_.
[placeholder]: ../appendix/glossary.html#appendix-c-glossary
[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/
So let's work through our example.
1. The first thing we would do is to
placeholder the obligation, yielding `AnyInt : Foo<&'0 isize>` (here `'0`
represents placeholder region #0). Note that we now have no quantifiers;
replace the bound region in the obligation with a placeholder, yielding
`AnyInt : Foo<&'0 isize>` (here `'0` represents placeholder region #0).
Note that we now have no quantifiers;
in terms of the compiler type, this changes from a `ty::PolyTraitRef`
to a `TraitRef`. We would then create the `TraitRef` from the impl,
using fresh variables for it's bound regions (and thus getting
@ -78,7 +78,7 @@ impl Foo<&'static isize> for StaticInt;
We want the obligation `StaticInt : for<'a> Foo<&'a isize>` to be
considered unsatisfied. The check begins just as before. `'a` is
placeholder to `'0` and the impl trait reference is instantiated to
replaced with a placeholder `'0` and the impl trait reference is instantiated to
`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,
'static}`, which fails the leak check.