diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 213a645ab..efe963c3f 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -39,11 +39,11 @@ - [Equality and associated types](./traits/associated-types.md) - [Implied bounds](./traits/implied-bounds.md) - [Region constraints](./traits/regions.md) + - [The lowering module in rustc](./traits/lowering-module.md) + - [Lowering rules](./traits/lowering-rules.md) + - [Well-formedness checking](./traits/wf.md) - [Canonical queries](./traits/canonical-queries.md) - [Canonicalization](./traits/canonicalization.md) - - [Lowering rules](./traits/lowering-rules.md) - - [The lowering module in rustc](./traits/lowering-module.md) - - [Well-formedness checking](./traits/wf.md) - [The SLG solver](./traits/slg.md) - [An Overview of Chalk](./traits/chalk-overview.md) - [Bibliography](./traits/bibliography.md) diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md index 1fffa3ff8..d35fb71e1 100644 --- a/src/traits/associated-types.md +++ b/src/traits/associated-types.md @@ -5,7 +5,7 @@ associated types. The full system consists of several moving parts, which we will introduce one by one: - Projection and the `Normalize` predicate -- Skolemization +- Placeholder associated type projections - The `ProjectionEq` predicate - Integration with unification @@ -14,11 +14,11 @@ which we will introduce one by one: When a trait defines an associated type (e.g., [the `Item` type in the `IntoIterator` trait][intoiter-item]), that type can be referenced by the user using an **associated type -projection** like ` as IntoIterator>::Item`. (Often, -though, people will use the shorthand syntax `T::Item` – presently, -that syntax is expanded during -["type collection"](../type-checking.html) into the explicit form, -though that is something we may want to change in the future.) +projection** like ` as IntoIterator>::Item`. + +> Often, people will use the shorthand syntax `T::Item`. Presently, that +> syntax is expanded during ["type collection"](../type-checking.html) into the +> explicit form, though that is something we may want to change in the future. [intoiter-item]: https://doc.rust-lang.org/nightly/core/iter/trait.IntoIterator.html#associatedtype.Item @@ -41,10 +41,11 @@ IntoIterator>::Item` to just `u32`. In this case, the projection was a "monomorphic" one – that is, it did not have any type parameters. Monomorphic projections are special -because they can **always** be fully normalized – but often we can -normalize other associated type projections as well. For example, -` as IntoIterator>::Item` (where `?T` is an inference -variable) can be normalized to just `?T`. +because they can **always** be fully normalized. + +Often, we can normalize other associated type projections as well. For +example, ` as IntoIterator>::Item`, where `?T` is an inference +variable, can be normalized to just `?T`. In our logic, normalization is defined by a predicate `Normalize`. The `Normalize` clauses arise only from @@ -60,9 +61,8 @@ forall { where in this case, the one `Implemented` condition is always true. -(An aside: since we do not permit quantification over traits, this is -really more like a family of program clauses, one for each associated -type.) +> Since we do not permit quantification over traits, this is really more like +> a family of program clauses, one for each associated type. We could apply that rule to normalize either of the examples that we've seen so far. @@ -76,17 +76,18 @@ normalized. For example, consider this function: fn foo(...) { ... } ``` -In this context, how would we normalize the type `T::Item`? Without -knowing what `T` is, we can't really do so. To represent this case, we -introduce a type called a **placeholder associated type -projection**. This is written like so `(IntoIterator::Item)`. You -may note that it looks a lot like a regular type (e.g., `Option`), -except that the "name" of the type is `(IntoIterator::Item)`. This is -not an accident: placeholder associated type projections work just like -ordinary types like `Vec` when it comes to unification. That is, -they are only considered equal if (a) they are both references to the -same associated type, like `IntoIterator::Item` and (b) their type -arguments are equal. +In this context, how would we normalize the type `T::Item`? + +Without knowing what `T` is, we can't really do so. To represent this case, +we introduce a type called a **placeholder associated type projection**. This +is written like so: `(IntoIterator::Item)`. + +You may note that it looks a lot like a regular type (e.g., `Option`), +except that the "name" of the type is `(IntoIterator::Item)`. This is not an +accident: placeholder associated type projections work just like ordinary +types like `Vec` when it comes to unification. That is, they are only +considered equal if (a) they are both references to the same associated type, +like `IntoIterator::Item` and (b) their type arguments are equal. Placeholder associated types are never written directly by the user. They are used internally by the trait system only, as we will see @@ -106,9 +107,10 @@ placeholder associated types (see the `TypeName` enum declared in So far we have seen two ways to answer the question of "When can we consider an associated type projection equal to another type?": -- the `Normalize` predicate could be used to transform associated type - projections when we knew which impl was applicable; -- **placeholder** associated types can be used when we don't. +- the `Normalize` predicate could be used to transform projections when we + knew which impl applied; +- **placeholder** associated types can be used when we don't. This is also + known as **lazy normalization**. We now introduce the `ProjectionEq` predicate to bring those two cases together. The `ProjectionEq` predicate looks like so: @@ -151,16 +153,16 @@ might just fail, in which case we get back `Err(NoSolution)`. This would happen, for example, if we tried to unify `u32` and `i32`. 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). -Whenever unification encounters an (un-placeholder!) associated type +Whenever unification encounters a non-placeholder associated type projection P being equated with some other type T, it always succeeds, but it produces a subgoal `ProjectionEq(P = T)` that is propagated back up. Thus it falls to the ordinary workings of the trait system to process that constraint. -(If we unify two projections P1 and P2, then unification produces a -variable X and asks us to prove that `ProjectionEq(P1 = X)` and -`ProjectionEq(P2 = X)`. That used to be needed in an older system to -prevent cycles; I rather doubt it still is. -nmatsakis) +> If we unify two projections P1 and P2, then unification produces a +> variable X and asks us to prove that `ProjectionEq(P1 = X)` and +> `ProjectionEq(P2 = X)`. (That used to be needed in an older system to +> prevent cycles; I rather doubt it still is. -nmatsakis) diff --git a/src/traits/index.md b/src/traits/index.md index 053a26bab..84f812394 100644 --- a/src/traits/index.md +++ b/src/traits/index.md @@ -1,17 +1,26 @@ # Trait solving (new-style) -🚧 This chapter describes "new-style" trait solving. This is still in the -[process of being implemented][wg]; this chapter serves as a kind of -in-progress design document. If you would prefer to read about how the -current trait solver works, check out -[this other chapter](./resolution.html). (By the way, if you -would like to help in hacking on the new solver, you will find -instructions for getting involved in the -[Traits Working Group tracking issue][wg].) 🚧 +> 🚧 This chapter describes "new-style" trait solving. This is still in the +> [process of being implemented][wg]; this chapter serves as a kind of +> in-progress design document. If you would prefer to read about how the +> current trait solver works, check out +> [this other chapter](./resolution.html). 🚧 +> +> By the way, if you would like to help in hacking on the new solver, you will +> find instructions for getting involved in the +> [Traits Working Group tracking issue][wg]! [wg]: https://github.com/rust-lang/rust/issues/48416 -Trait solving is based around a few key ideas: +The new-style trait solver is based on the work done in [chalk][chalk]. Chalk +recasts Rust's trait system explicitly in terms of logic programming. It does +this by "lowering" Rust code into a kind of logic program we can then execute +queries against. + +You can read more about chalk itself in the +[Overview of Chalk](./chalk-overview.md) section. + +Trait solving in rustc is based around a few key ideas: - [Lowering to logic](./lowering-to-logic.html), which expresses Rust traits in terms of standard logical terms. @@ -19,30 +28,36 @@ Trait solving is based around a few key ideas: describes the precise form of rules we use, and [lowering rules](./lowering-rules.html) gives the complete set of lowering rules in a more reference-like form. + - [Lazy normalization](./associated-types.html), which is the + technique we use to accommodate associated types when figuring out + whether types are equal. + - [Region constraints](./regions.html), which are accumulated + during trait solving but mostly ignored. This means that trait + solving effectively ignores the precise regions involved, always – + but we still remember the constraints on them so that those + constraints can be checked by the type checker. - [Canonical queries](./canonical-queries.html), which allow us to solve trait problems (like "is `Foo` implemented for the type `Bar`?") once, and then apply that same result independently in many different inference contexts. -- [Lazy normalization](./associated-types.html), which is the - technique we use to accommodate associated types when figuring out - whether types are equal. -- [Region constraints](./regions.html), which are accumulated - during trait solving but mostly ignored. This means that trait - solving effectively ignores the precise regions involved, always – - but we still remember the constraints on them so that those - constraints can be checked by thet type checker. -Note: this is not a complete list of topics. See the sidebar for more. +> This is not a complete list of topics. See the sidebar for more. +## Ongoing work The design of the new-style trait solving currently happens in two places: -* The [chalk][chalk] repository is where we experiment with new ideas and - designs for the trait system. It basically consists of a unit testing framework - for the correctness and feasibility of the logical rules defining the new-style - trait system. It also provides the [`chalk_engine`][chalk_engine] crate, which - defines the new-style trait solver used both in the unit testing framework and - in rustc. -* Once we are happy with the logical rules, we proceed to implementing them in - rustc. This mainly happens in [`librustc_traits`][librustc_traits]. + +**chalk**. The [chalk][chalk] repository is where we experiment with new ideas +and designs for the trait system. It primarily consists of two parts: +* a unit testing framework + for the correctness and feasibility of the logical rules defining the + new-style trait system. +* the [`chalk_engine`][chalk_engine] crate, which + defines the new-style trait solver used both in the unit testing framework + and in rustc. + +**rustc**. Once we are happy with the logical rules, we proceed to +implementing them in rustc. This mainly happens in +[`librustc_traits`][librustc_traits]. [chalk]: https://github.com/rust-lang-nursery/chalk [chalk_engine]: https://github.com/rust-lang-nursery/chalk/tree/master/chalk-engine diff --git a/src/traits/regions.md b/src/traits/regions.md index baa3582b6..4657529dc 100644 --- a/src/traits/regions.md +++ b/src/traits/regions.md @@ -1,3 +1,9 @@ # Region constraints -*to be written* +*To be written.* + +Chalk does not have the concept of region constraints, and as of this +writing, work on rustc was not far enough to worry about them. + +In the meantime, you can read about region constraints in the +[type inference](../type-inference.html#region-constraints) section.