Skip to content

Commit

Permalink
fix some comments (rust-lang#2059)
Browse files Browse the repository at this point in the history
Signed-off-by: cuishuang <[email protected]>
  • Loading branch information
cuishuang authored Sep 9, 2024
1 parent fc6bd7e commit 0ed9229
Show file tree
Hide file tree
Showing 6 changed files with 7 additions and 7 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ fn bad<'a>() -> Opaque<'a, 'a> {}
//~^ ERROR
```

**Semantic lifetime equlity:**
**Semantic lifetime equality:**
One complexity with lifetimes compared to type parameters is that
two lifetimes that are syntactically different may be semantically equal.
Therefore, we need to be cautious when verifying that the lifetimes are unique.
Expand Down Expand Up @@ -219,7 +219,7 @@ fn test::{closure#0}(_upvar: &'?8 str) -> Opaque<'?6, '?7> {
return _upvar
}
// where `['?8, '?6, ?7] are universal lifetimes *external* to the closure.
// where `['?8, '?6, ?7]` are universal lifetimes *external* to the closure.
// There are no known relations between them *inside* the closure.
// But in the parent fn it is known that `'?6: '?8`.
//
Expand Down
2 changes: 1 addition & 1 deletion src/queries/query-evaluation-model-in-detail.md
Original file line number Diff line number Diff line change
Expand Up @@ -174,7 +174,7 @@ Since query providers are regular functions, this would behave much as expected:
Evaluation would get stuck in an infinite recursion. A query like this would not
be very useful either. However, sometimes certain kinds of invalid user input
can result in queries being called in a cyclic way. The query engine includes
a check for cyclic invocations of queries with the same input aguments.
a check for cyclic invocations of queries with the same input arguments.
And, because cycles are an irrecoverable error, will abort execution with a
"cycle error" message that tries to be human readable.

Expand Down
2 changes: 1 addition & 1 deletion src/tests/headers.md
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ The following header commands will check rustc build settings and target setting
(`rust.lld = true` in `config.toml`)
* `needs-threads` — ignores if the target does not have threading support
* `needs-symlink` — ignores if the target does not support symlinks. This can be the case on Windows
if the developer did not enable priviledged symlink permissions.
if the developer did not enable privileged symlink permissions.

The following header commands will check LLVM support:

Expand Down
2 changes: 1 addition & 1 deletion src/ty_module/binders.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# `Binder` and Higher ranked regions

Sometimes we define generic parmeters not on an item but as part of a type or a where clauses. As an example the type `for<'a> fn(&'a u32)` or the where clause `for<'a> T: Trait<'a>` both introduce a generic lifetime named `'a`. Currently there is no stable syntax for `for<T>` or `for<const N: usize>` but on nightly `feature(non_lifetime_binders)` feature can be used to write where clauses (but not types) using `for<T>`/`for<const N: usize>`.
Sometimes we define generic parameters not on an item but as part of a type or a where clauses. As an example the type `for<'a> fn(&'a u32)` or the where clause `for<'a> T: Trait<'a>` both introduce a generic lifetime named `'a`. Currently there is no stable syntax for `for<T>` or `for<const N: usize>` but on nightly `feature(non_lifetime_binders)` feature can be used to write where clauses (but not types) using `for<T>`/`for<const N: usize>`.

The `for` is referred to as a "binder" because it brings new names into scope. In rustc we use the `Binder` type to track where these parameters are introduced and what the parameters are (i.e. how many and whether they the parameter is a type/const/region). A type such as `for<'a> fn(&'a u32)` would be
represented in rustc as:
Expand Down
2 changes: 1 addition & 1 deletion src/ty_module/early_binder.md
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ fn main() {

When type checking `main` we cannot just naively look at the return type of `foo` and assign the type `T` to the variable `c`, The function `main` does not define any generic parameters, `T` is completely meaningless in this context. More generally whenever an item introduces (binds) generic parameters, when accessing types inside the item from outside, the generic parameters must be instantiated with values from the outer item.

In rustc we track this via the [`EarlyBinder`] type, the return type of `foo` is represented as an `EarlyBinder<Ty>` with the only way to acess `Ty` being to provide arguments for any generic parameters `Ty` might be using. This is implemented via the [`EarlyBinder::instantiate`] method which discharges the binder returning the inner value with all the generic parameters replaced by the provided arguments.
In rustc we track this via the [`EarlyBinder`] type, the return type of `foo` is represented as an `EarlyBinder<Ty>` with the only way to access `Ty` being to provide arguments for any generic parameters `Ty` might be using. This is implemented via the [`EarlyBinder::instantiate`] method which discharges the binder returning the inner value with all the generic parameters replaced by the provided arguments.

To go back to our example, when type checking `main` the return type of `foo` would be represented as `EarlyBinder(T/#0)`. Then, because we called the function with `i32, u128` for the generic arguments, we would call `EarlyBinder::instantiate` on the return type with `[i32, u128]` for the args. This would result in an instantiated return type of `i32` that we can use as the type of the local `c`.

Expand Down
2 changes: 1 addition & 1 deletion src/ty_module/instantiating_binders.md
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ Given these trait implementations `u32: Bar` should _not_ hold. `&'a u32` only i
- There is a where clause `for<'a> &'^0 T: Trait` on the impl, as we instantiated the early binder with `u32` we actually have to prove `for<'a> &'^0 u32: Trait`
- We find the `impl<T> Trait for T` impl, we would wind up instantiating the `EarlyBinder` with `&'^0 u32`
- There is a where clause `for<'a> T: Other<'^0>`, as we instantiated the early binder with `&'^0 u32` we actually have to prove `for<'a> &'^0 u32: Other<'^0>`
- We find the `impl<'a> Other<'a> for &'a u32` and this impl is enoguh to prove the bound as the lifetime on the borrow and on the trait are both `'^0`
- We find the `impl<'a> Other<'a> for &'a u32` and this impl is enough to prove the bound as the lifetime on the borrow and on the trait are both `'^0`

This end result is incorrect as we had two separate binders introducing their own generic parameters, the trait bound should have ended up as something like `for<'a1, 'a2> &'^1 u32: Other<'^0>` which is _not_ satisfied by the `impl<'a> Other<'a> for &'a u32`.

Expand Down

0 comments on commit 0ed9229

Please sign in to comment.