Skip to content

Describe Type Alias Impl Trait (TAIT) Inference Algorithm #1297

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

Merged
merged 6 commits into from
Jul 17, 2022
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
obey line length limit (part 3)
  • Loading branch information
tshepang authored Jul 17, 2022
commit e8b0c1ac44c79efec74aab5e83a125c65cf628fd
27 changes: 20 additions & 7 deletions src/opaque-types-type-alias-impl-trait-inference.md
Original file line number Diff line number Diff line change
Expand Up @@ -43,9 +43,14 @@ pub fn main() {
* `m::produce_singleton`
* `m::produce_doubleton`
* In the `main` function, the opaque type is out of scope:
* When `main` calls `m::produce_singleton`, it gets back a reference to the opaque type `Seq<i32>`.
* The `is_send` call checks that `Seq<i32>: Send`. `Send` is not listed amongst the bounds of the impl trait, but because of auto-trait leakage, we are able to infer that it holds.
* The for loop desugaring requires that `Seq<T>: IntoIterator`, which is provable from the bounds declared on `Seq<T>`.
* When `main` calls `m::produce_singleton`,
it gets back a reference to the opaque type `Seq<i32>`.
* The `is_send` call checks that `Seq<i32>:
Send`. `Send` is not listed amongst the bounds of the impl trait,
but because of auto-trait leakage,
we are able to infer that it holds.
* The for loop desugaring requires that `Seq<T>: IntoIterator`,
which is provable from the bounds declared on `Seq<T>`.

### Type-checking `main`

Expand Down Expand Up @@ -97,7 +102,9 @@ flowchart TD

### Within the `type_of` query

The `type_of` query, when applied to an opaque type O, returns the hidden type. That hidden type is computed by combining the results from each constraining function within defining scope of O.
The `type_of` query, when applied to an opaque type O, returns the hidden type.
That hidden type is computed by combining the results from each constraining function
within defining scope of O.

```mermaid
flowchart TD
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Expand Down Expand Up @@ -164,7 +171,9 @@ flowchart TD

### Interactions with queries

When queries encounter a `opaque_ty_obligation`, they do not try to process them, but instead just store the constraints into the infcx.
When queries encounter a `opaque_ty_obligation`,
they do not try to process them,
but instead just store the constraints into the infcx.

```mermaid
graph TD
Copy link
Contributor Author

Choose a reason for hiding this comment

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

Expand All @@ -184,9 +193,13 @@ graph TD
end
```

The registered hidden types are stored into the `QueryResponse` struct in the `opaque_types` field (the function `take_opaque_types_for_query_response` reads them out).
The registered hidden types are stored into the `QueryResponse` struct in
the `opaque_types` field
(the function `take_opaque_types_for_query_response` reads them out).

When the `QueryResponse` is instantiated into the surrounding infcx in `query_response_substitution_guess`, we convert each hidden type constraint by invoking `handle_opaque_type` (as above).
When the `QueryResponse` is instantiated into the surrounding infcx in
`query_response_substitution_guess`,
we convert each hidden type constraint by invoking `handle_opaque_type` (as above).

There is one bit of "weirdness".
The instantiated opaque types are stored in a *map*,
Expand Down