mirror
/
rustc-dev-guide
mirror of https://github.com/rust-lang/rustc-dev-guide.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #70 from nikomatsakis/traits 

work on traits chapters
This commit is contained in:
Niko Matsakis 2018-03-10 07:13:31 -05:00 committed by GitHub
parent d4fd74f3de b30174cf00
commit 8c9205cbae
16 changed files with 1322 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/SUMMARY.md
View File

@ -17,10 +17,22 @@
- [The HIR (High-level IR)](./hir.md)
- [The `ty` module: representing types](./ty.md)
- [Type inference](./type-inference.md)
- [Trait resolution](./trait-resolution.md)
- [Trait solving (old-style)](./trait-resolution.md)
- [Higher-ranked trait bounds](./trait-hrtb.md)
- [Caching subtleties](./trait-caching.md)
- [Speciailization](./trait-specialization.md)
- [Specialization](./trait-specialization.md)
- [Trait solving (new-style)](./traits.md)
- [Lowering to logic](./traits-lowering-to-logic.md)
- [Goals and clauses](./traits-goals-and-clauses.md)
- [Equality and associated types](./traits-associated-types.md)
- [Implied bounds](./traits-implied-bounds.md)
- [Region constraints](./traits-regions.md)
- [Canonical queries](./traits-canonical-queries.md)
- [Canonicalization](./traits-canonicalization.md)
- [Lowering rules](./traits-lowering-rules.md)
- [Well-formedness checking](./traits-wf.md)
- [The SLG solver](./traits-slg.md)
- [Bibliography](./traits-bibliography.md)
- [Type checking](./type-checking.md)
- [The MIR (Mid-level IR)](./mir.md)
- [MIR construction](./mir-construction.md)

3
src/glossary.md
View File

@ -31,10 +31,12 @@ LTO | Link-Time Optimizations. A set of optimizations offer
[LLVM] | (actually not an acronym :P) an open-source compiler backend. It accepts LLVM IR and outputs native binaries. Various languages (e.g. Rust) can then implement a compiler front-end that output LLVM IR and use LLVM to compile to all the platforms LLVM supports.
MIR | the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html))
miri | an interpreter for MIR used for constant evaluation ([see more](./miri.html))
normalize | a general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](./traits-associated-types.html#normalize)
newtype | a "newtype" is a wrapper around some other type (e.g., `struct Foo(T)` is a "newtype" for `T`). This is commonly used in Rust to give a stronger type for indices.
NLL | [non-lexical lifetimes](./mir-regionck.html), an extension to Rust's borrowing system to make it be based on the control-flow graph.
node-id or NodeId | an index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`.
obligation | something that must be proven by the trait system ([see more](trait-resolution.html))
projection | a general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](./traits-goals-and-clauses.html#trait-ref)
promoted constants | constants extracted from a function and lifted to static scope; see [this section](./mir.html#promoted) for more details.
provider | the function that executes a query ([see more](query.html))
quantified | in math or logic, existential and universal quantification are used to ask questions like "is there any type T for which is true?" or "is this true for all types T?"; see [the background chapter for more](./background.html#quantified)
@ -49,6 +51,7 @@ span | a location in the user's source code, used for error
substs | the substitutions for a given generic type or item (e.g. the `i32`, `u32` in `HashMap<i32, u32>`)
tcx | the "typing context", main data structure of the compiler ([see more](ty.html))
'tcx | the lifetime of the currently active inference context ([see more](ty.html))
trait reference | the name of a trait along with a suitable set of input type/lifetimes ([see more](./traits-goals-and-clauses.html#trait-ref))
token | the smallest unit of parsing. Tokens are produced after lexing ([see more](the-parser.html)).
[TLS] | Thread-Local Storage. Variables may be defined so that each thread has its own copy (rather than all threads sharing the variable). This has some interactions with LLVM. Not all platforms support TLS.
trans | the code to translate MIR into LLVM IR.

7
src/trait-resolution.md
View File

@ -1,8 +1,13 @@
# Trait resolution
# Trait resolution (old-style)
This chapter describes the general process of _trait resolution_ and points out
some non-obvious things.
**Note:** This chapter (and its subchapters) describe how the trait
solver **currently** works. However, we are in the process of
designing a new trait solver. If you'd prefer to read about *that*,
see [*this* traits chapter](./traits.html).
## Major concepts
Trait resolution is the process of pairing up an impl with each

145
src/traits-associated-types.md Normal file
View File

@ -0,0 +1,145 @@
# Equality and associated types
This section covers how the trait system handles equality between
associated types. The full system consists of several moving parts,
which we will introduce one by one:
- Projection and the `Normalize` predicate
- Skolemization
- The `ProjectionEq` predicate
- Integration with unification
## Associated type projection and normalization
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 `<Option<u32> 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.)
<a name=normalize>
In some cases, associated type projections can be **normalized** --
that is, simplified -- based on the types given in an impl. So, to
continue with our example, the impl of `IntoIterator` for `Option<T>`
declares (among other things) that `Item = T`:
```rust
impl<T> IntoIterator for Option<T> {
type Item = T;
..
}
```
This means we can normalize the projection `<Option<u32> as
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,
`<Option<?T> 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
impls. For example, the `impl` of `IntoIterator` for `Option<T>` that
we saw above would be lowered to a program clause like so:
forall<T> {
Normalize(<Option<T> as IntoIterator>::Item -> T)
}
(An aside: since we do not permit quantification over traits, this is
really more like a family of predicates, one for each associated
type.)
We could apply that rule to normalize either of the examples that
we've seen so far.
## Skolemized associated types
Sometimes however we want to work with associated types that cannot be
normalized. For example, consider this function:
```rust
fn foo<T: IntoIterator>(...) { ... }
```
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 **skolemized associated type
projection**. This is written like so `(IntoIterator::Item)<T>`. You
may note that it looks a lot like a regular type (e.g., `Option<T>`),
except that the "name" of the type is `(IntoIterator::Item)`. This is
not an accident: skolemized associated type projections work just like
ordinary types like `Vec<T>` 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.
Skolemized associated types are never written directly by the user.
They are used internally by the trait system only, as we will see
shortly.
## Projection equality
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;
- **skolemized** associated types can be used when we don't.
We now introduce the `ProjectionEq` predicate to bring those two cases
together. The `ProjectionEq` predicate looks like so:
ProjectionEq(<T as IntoIterator>::Item = U)
and we will see that it can be proven *either* via normalization or
skolemization. As part of lowering an associated type declaration from
some trait, we create two program clauses for `ProjectionEq`:
forall<T, U> {
ProjectionEq(<T as IntoIterator>::Item = U) :-
Normalize(<T as IntoIterator>::Item -> U)
}
forall<T> {
ProjectionEq(<T as IntoIterator>::Item = (IntoIterator::Item)<T>)
}
These are the only two `ProjectionEq` program clauses we ever make for
any given associated item.
## Integration with unification
Now we are ready to discuss how associated type equality integrates
with unification. As described in the
[type inference](./type-inference.html) section, unification is
basically a procedure with a signature like this:
Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution>
In other words, we try to unify two things A and B. That procedure
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
back region constraints, but those are not relevant here).
Whenever unification encounters an (unskolemized!) 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)

28
src/traits-bibliography.md Normal file
View File

@ -0,0 +1,28 @@
# Bibliography
If you'd like to read more background material, here are some
recommended texts and papers:
[Programming with Higher-order Logic][phl], by Dale Miller and Gopalan
Nadathur, covers the key concepts of Lambda prolog. Although it's a
slim little volume, it's the kind of book where you learn something
new every time you open it.
[phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X
<a name=pphhf>
["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf],
by Gopalan Nadathur. This paper covers the basics of universes,
environments, and Lambda Prolog-style proof search. Quite readable.
[pphhf]: https://dl.acm.org/citation.cfm?id=868380
<a name=slg>
["A new formulation of tabled resolution with delay"][nftrd], by
[Theresa Swift]. This paper gives a kind of abstract treatment of the
SLG formulation that is the basis for our on-demand solver.
[nftrd]: https://dl.acm.org/citation.cfm?id=651202
[ts]: http://www3.cs.stonybrook.edu/~tswift/

230
src/traits-canonical-queries.md Normal file
View File

@ -0,0 +1,230 @@
# Canonical queries
The "start" of the trait system is the **canonical query** (these are
both queries in the more general sense of the word -- something you
would like to know the answer to -- and in the
[rustc-specific sense](./query.html)). The idea is that the type
checker or other parts of the system, may in the course of doing their
thing want to know whether some trait is implemented for some type
(e.g., is `u32: Debug` true?). Or they may want to
[normalize some associated type](./traits-associated-types.html).
This section covers queries at a fairly high level of abstraction. The
subsections look a bit more closely at how these ideas are implemented
in rustc.
## The traditional, interactive Prolog query
In a traditional Prolog system, when you start a query, the solver
will run off and start supplying you with every possible answer it can
find. So given something like this:
?- Vec<i32>: AsRef<?U>
The solver might answer:
Vec<i32>: AsRef<[i32]>
continue? (y/n)
This `continue` bit is interesting. The idea in Prolog is that the
solver is finding **all possible** instantiations of your query that
are true. In this case, if we instantiate `?U = [i32]`, then the query
is true (note that a traditional Prolog interface does not, directly,
tell us a value for `?U`, but we can infer one by unifying the
response with our original query -- Rust's solver gives back a
substitution instead). If we were to hit `y`, the solver might then
give us another possible answer:
Vec<i32>: AsRef<Vec<i32>>
continue? (y/n)
This answer derives from the fact that there is a reflexive impl
(`impl<T> AsRef<T> for T`) for `AsRef`. If were to hit `y` again,
then we might get back a negative response:
no
Naturally, in some cases, there may be no possible answers, and hence
the solver will just give me back `no` right away:
?- Box<i32>: Copy
no
In some cases, there might be an infinite number of responses. So for
example if I gave this query, and I kept hitting `y`, then the solver
would never stop giving me back answers:
?- Vec<?U>: Clone
Vec<i32>: Clone
continue? (y/n)
Vec<Box<i32>>: Clone
continue? (y/n)
Vec<Box<Box<i32>>>: Clone
continue? (y/n)
Vec<Box<Box<Box<i32>>>>: Clone
continue? (y/n)
As you can imagine, the solver will gleefully keep adding another
layer of `Box` until we ask it to stop, or it runs out of memory.
Another interesting thing is that queries might still have variables
in them. For example:
?- Rc<?T>: Clone
might produce the answer:
Rc<?T>: Clone
continue? (y/n)
After all, `Rc<?T>` is true **no matter what type `?T` is**.
## A trait query in rustc
The trait queries in rustc work somewhat differently. Instead of
trying to enumerate **all possible** answers for you, they are looking
for an **unambiguous** answer. In particular, when they tells you the
value for a type variable, that means that this is the **only possible
instantiation** that you could use, given the current set of impls and
where-clauses, that would be provable. (Internally within the solver,
though, they can potentially enumerate all possible answers. See
[the description of the SLG solver](./traits-slg.html) for details.)
<a name=query-response>
The response to a trait query in rustc is typically a
`Result<QueryResult<T>, NoSolution>` (where the `T` will vary a bit
depending on the query itself). The `Err(NoSolution)` case indicates
that the query was false and had no answers (e.g., `Box<i32>: Copy`).
Otherwise, the `QueryResult` gives back information about the possible answer(s)
we did find. It consists of four parts:
- **Certainty:** tells you how sure we are of this answer. It can have two values:
- `Proven` means that the result is known to be true.
- This might be the result for trying to prove `Vec<i32>: Clone`,
say, or `Rc<?T>: Clone`.
- `Ambiguous` means that there were things we could not yet prove to
be either true *or* false, typically because more type information
was needed. (We'll see an example shortly.)
- This might be the result for trying to prove `Vec<?T>: Clone`.
- **Var values:** Values for each of the unbound inference variables
(like `?T`) that appeared in your original query. (Remember that in Prolog,
we had to infer these.)
- As we'll see in the example below, we can get back var values even
for `Ambiguous` cases.
- **Region constraints:** these are relations that must hold between
the lifetimes that you supplied as inputs. We'll ignore these here,
but see the
[section on handling regions in traits](./traits-regions.html) for
more details.
- **Value:** The query result also comes with a value of type `T`. For
some specialized queries -- like normalizing associated types --
this is used to carry back an extra result, but it's often just
`()`.
### Examples
Let's work through an example query to see what all the parts mean.
Consider [the `Borrow` trait][borrow]. This trait has a number of
impls; among them, there are these two (for clarify, I've written the
`Sized` bounds explicitly):
[borrow]: https://doc.rust-lang.org/std/borrow/trait.Borrow.html
```rust
impl<T> Borrow<T> for T where T: ?Sized
impl<T> Borrow<[T]> for Vec<T> where T: Sized
```
**Example 1.** Imagine we are type-checking this (rather artificial)
bit of code:
```rust
fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
fn main() {
let mut t: Vec<_> = vec![]; // Type: Vec<?T>
let mut u: Option<_> = None; // Type: Option<?U>
foo(t, u); // Example 1: requires `Vec<?T>: Borrow<?U>`
...
}
```
As the comments indicate, we first create two variables `t` and `u`;
`t` is an empty vector and `u` is a `None` option. Both of these
variables have unbound inference variables in their type: `?T`
represents the elements in the vector `t` and `?U` represents the
value stored in the option `u`. Next, we invoke `foo`; comparing the
signature of `foo` to its arguments, we wind up with `A = Vec<?T>` and
`B = ?U`.Therefore, the where clause on `foo` requires that `Vec<?T>:
Borrow<?U>`. This is thus our first example trait query.
There are many possible solutions to the query `Vec<?T>: Borrow<?U>`;
for example:
- `?U = Vec<?T>`,
- `?U = [?T]`,
- `?T = u32, ?U = [u32]`
- and so forth.
Therefore, the result we get back would be as follows (I'm going to
ignore region constraints and the "value"):
- Certainty: `Ambiguous` -- we're not sure yet if this holds
- Var values: `[?T = ?T, ?U = ?U]` -- we learned nothing about the values of the variables
In short, the query result says that it is too soon to say much about
whether this trait is proven. During type-checking, this is not an
immediate error: instead, the type checker would hold on to this
requirement (`Vec<?T>: Borrow<?U>`) and wait. As we'll see in the next
example, it may happen that `?T` and `?U` wind up constrained from
other sources, in which case we can try the trait query again.
**Example 2.** We can now extend our previous example a bit,
and assign a value to `u`:
```rust
fn foo<A, B>(a: A, vec_b: Option<B>) where A: Borrow<B> { }
fn main() {
// What we saw before:
let mut t: Vec<_> = vec![]; // Type: Vec<?T>
let mut u: Option<_> = None; // Type: Option<?U>
foo(t, u); // `Vec<?T>: Borrow<?U>` => ambiguous
// New stuff:
u = Some(vec![]); // ?U = Vec<?V>
}
```
As a result of this assignment, the type of `u` is forced to be
`Option<Vec<?V>>`, where `?V` represents the element type of the
vector. This in turn implies that `?U` is [unified] to `Vec<?V>`.
[unified]: ./type-checking.html
Let's suppose that the type checker decides to revisit the
"as-yet-unproven" trait obligation we saw before, `Vec<?T>:
Borrow<?U>`. `?U` is no longer an unbound inference variable; it now
has a value, &. So, if we "refresh" the query with that value, we get:
Vec<?T>: Borrow<Vec<?V>>
This time, there is only one impl that applies, the reflexive impl:
impl<T> Borrow<T> for T where T: ?Sized
Therefore, the trait checker will answer:
- Certainty: `Proven`
- Var values: `[?T = ?T, ?V = ?T]`
Here, it is saying that we have indeed proven that the obligation
holds, and we also know that `?T` and `?V` are the same type (but we
don't know what that type is yet!).
(In fact, as the function ends here, the type checker would give an
error at this point, since the element types of `t` and `u` are still
not yet known, even though they are known to be the same.)

224
src/traits-canonicalization.md Normal file
View File

@ -0,0 +1,224 @@
# Canonicalization
Canonicalization is the process of **isolating** an inference value
from its context. It is a key part of implementing
[canonical queries][cq], and you may wish to read the parent chapter
to get more context.
Canonicalization is really based on a very simple concept: every
[inference variable](./type-inference.html#vars) is always in one of
two states: either it is **unbound**, in which case we don't know yet
what type it is, or it is **bound**, in which case we do. So to
isolate some data-structure T that contains types/regions from its
environment, we just walk down and find the unbound variables that
appear in T; those variables get replaced with "canonical variables",
starting from zero and numbered in a fixed order (left to right, for
the most part, but really it doesn't matter as long as it is
consistent).
[cq]: ./traits-canonical-queries.html
So, for example, if we have the type `X = (?T, ?U)`, where `?T` and
`?U` are distinct, unbound inference variables, then the canonical
form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these
**canonical placeholders**. Note that the type `Y = (?U, ?T)` also
canonicalizes to `(?0, ?1)`. But the type `Z = (?T, ?T)` would
canonicalize to `(?0, ?0)` (as would `(?U, ?U)`). In other words, the
exact identity of the inference variables is not important -- unless
they are repeated.
We use this to improve caching as well as to detect cycles and other
things during trait resolution. Roughly speaking, the idea is that if
two trait queries have the same canonicalize form, then they will get
the same answer. That answer will be expressed in terms of the
canonical variables (`?0`, `?1`), which we can then map back to the
original variables (`?T`, `?U`).
## Canonicalizing the query
To see how it works, imagine that we are asking to solve the following
trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound.
This query contains two unbound variables, but it also contains the
lifetime `'static`. The trait system generally ignores all lifetimes
and treats them equally, so when canonicalizing, we will *also*
replace any [free lifetime](./background.html#free-vs-bound) with a
canonical variable. Therefore, we get the following result:
?0: Foo<'?1, ?2>
Sometimes we write this differently, like so:
for<T,L,T> { ?0: Foo<'?1, ?2> }
This `for<>` gives some information about each of the canonical
variables within. In this case, each `T` indicates a type variable,
so `?0` and `?2` are types; the `L` indicates a lifetime varibale, so
`?1` is a lifetime. The `canonicalize` method *also* gives back a
`CanonicalVarValues` array OV with the "original values" for each
canonicalized variable:
[?A, 'static, ?B]
We'll need this vector OV later, when we process the query response.
## Executing the query
Once we've constructed the canonical query, we can try to solve it.
To do so, we will wind up creating a fresh inference context and
**instantiating** the canonical query in that context. The idea is that
we create a substitution S from the canonical form containing a fresh
inference variable (of suitable kind) for each canonical variable.
So, for our example query:
for<T,L,T> { ?0: Foo<'?1, ?2> }
the substitution S might be:
S = [?A, '?B, ?C]
We can then replace the bound canonical variables (`?0`, etc) with
these inference variables, yielding the following fully instantiated
query:
?A: Foo<'?B, ?C>
Remember that substitution S though! We're going to need it later.
OK, now that we have a fresh inference context and an instantiated
query, we can go ahead and try to solve it. The trait solver itself is
explained in more detail in [another section](./traits-slg.html), but
suffice to say that it will compute a [certainty value][cqqr] (`Proven` or
`Ambiguous`) and have side-effects on the inference variables we've
created. For example, if there were only one impl of `Foo`, like so:
[cqqr]: ./traits-canonical-queries.html#query-response
```
impl<'a, X> Foo<'a, X> for Vec<X>
where X: 'a
{ ... }
```
then we might wind up with a certainty value of `Proven`, as well as
creating fresh inference variables `'?D` and `?E` (to represent the
parameters on the impl) and unifying as follows:
- `'?B = '?D`
- `?A = Vec<?E>`
- `?C = ?E`
We would also accumulate the region constraint `?E: '?D`, due to the
where clause.
In order to create our final query result, we have to "lift" these
values out of the query's inference context and into something that
can be reapplied in our original inference context. We do that by
**re-applying canonicalization**, but to the **query result**.
## Canonicalizing the query result
As discussed in [the parent section][cqqr], most trait queries wind up
with a result that brings together a "certainty value" `certainty`, a
result substitution `var_values`, and some region constraints. To
create this, we wind up re-using the substitution S that we created
when first instantiating our query. To refresh your memory, we had a query
for<T,L,T> { ?0: Foo<'?1, ?2> }
for which we made a substutition S:
S = [?A, '?B, ?C]
We then did some work which unified some of those variables with other things. If we
"refresh" S with the latest results, we get:
S = [Vec<?E>, '?D, ?E]
These are precisely the new values for the three input variables from
our original query. Note though that they include some new variables
(like `?E`). We can make those go away by canonicalizing again! We don't
just canonicalize S, though, we canonicalize the whole query response QR:
QR = {
certainty: Proven, // or whatever
var_values: [Vec<?E>, '?D, ?E] // this is S
region_constraints: [?E: '?D], // from the impl
value: (), // for our purposes, just (), but
// in some cases this might have
// a type or other info
}
The result would be as follows:
Canonical(QR) = for<T, L> {
certainty: Proven,
var_values: [Vec<?0>, '?1, ?2]
region_constraints: [?2: '?1],
value: (),
}
(One subtle point: when we canonicalize the query **result**, we do not
use any special treatment for free lifetimes. Note that both
references to `'?D`, for example, were converted into the same
canonical variable (`?1`). This is in contrast to the original query,
where we canonicalized every free lifetime into a fresh canonical
variable.)
Now, this result must be reapplied in each context where needed.
## Processing the canonicalized query result
In the previous section we produced a canonical query result. We now have
to apply that result in our original context. If you recall, way back in the
beginning, we were trying to prove this query:
?A: Foo<'static, ?B>
We canonicalized that into this:
for<T,L,T> { ?0: Foo<'?1, ?2> }
and now we got back a canonical response:
for<T, L> {
certainty: Proven,
var_values: [Vec<?0>, '?1, ?2]
region_constraints: [?2: '?1],
value: (),
}
We now want to apply that response to our context. Conceptually, how
we do that is to (a) instantiate each of the canonical variables in
the result with a fresh inference variable, (b) unify the values in
the result with the original values, and then (c) record the region
constraints for later. Doing step (a) would yield a result of
```
{
certainty: Proven,
var_values: [Vec<?C>, '?D, ?C]
^^ ^^^ fresh inference variables
region_constraints: [?C: '?D],
value: (),
}
```
Step (b) would then unify:
```
?A with Vec<?C>
'static with '?D
?B with ?C
```
And finally the region constraint of `?C: 'static` would be recorded
for later verification.
(What we *actually* do is a mildly optimized variant of that: Rather
than eagerly instantiating all of the canonical values in the result
with variables, we instead walk the vector of values, looking for
cases where the value is just a canonical variable. In our example,
`values[2]` is `?C`, so that we means we can deduce that `?C := ?B and
`'?D := 'static`. This gives us a partial set of values. Anything for
which we do not find a value, we create an inference variable.)

158
src/traits-goals-and-clauses.md Normal file
View File

@ -0,0 +1,158 @@
# Goals and clauses
In logic programming terms, a **goal** is something that you must
prove and a **clause** is something that you know is true. As
described in the [lowering to logic](./traits-lowering-to-logic.html)
chapter, Rust's trait solver is based on an extension of hereditary
harrop (HH) clauses, which extend traditional Prolog Horn clauses with
a few new superpowers.
## Goals and clauses meta structure
In Rust's solver, **goals** and **clauses** have the following forms
(note that the two definitions reference one another):
Goal = DomainGoal // defined in the section below
| Goal && Goal
| Goal || Goal
| exists<K> { Goal } // existential quantification
| forall<K> { Goal } // universal quantification
| if (Clause) { Goal } // implication
| true // something that's trivially true
| ambiguous // something that's never provable
Clause = DomainGoal
| Clause :- Goal // if can prove Goal, then Clause is true
| Clause && Clause
| forall<K> { Clause }
K = <type> // a "kind"
| <lifetime>
The proof procedure for these sorts of goals is actually quite
straightforward. Essentially, it's a form of depth-first search. The
paper
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
gives the details.
[pphhf]: ./traits-bibliography.html#pphhf
<a name="domain-goals">
## Domain goals
<a name=trait-ref>
To define the set of *domain goals* in our system, we need to first
introduce a few simple formulations. A **trait reference** consists of
the name of a trait along with a suitable set of inputs P0..Pn:
TraitRef = P0: TraitName<P1..Pn>
So, for example, `u32: Display` is a trait reference, as is `Vec<T>:
IntoIterator`. Note that Rust surface syntax also permits some extra
things, like associated type bindings (`Vec<T>: IntoIterator<Item =
T>`), that are not part of a trait reference.
<a name=projection>
A **projection** consists of an associated item reference along with
its inputs P0..Pm:
Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
Given that, we can define a `DomainGoal` as follows:
DomainGoal = Implemented(TraitRef)
| ProjectionEq(Projection = Type)
| Normalize(Projection -> Type)
| FromEnv(TraitRef)
| FromEnv(Projection = Type)
| WellFormed(Type)
| WellFormed(TraitRef)
| WellFormed(Projection = Type)
| Outlives(Type, Region)
| Outlives(Region, Region)
- `Implemented(TraitRef)` -- true if the given trait is
implemented for the given input types and lifetimes
- `FromEnv(TraitEnv)` -- true if the given trait is *assumed* to be implemented;
that is, if it can be derived from the in-scope where clauses
- as we'll see in the section on lowering, `FromEnv(X)` implies
`Implemented(X)` but not vice versa. This distinction is crucial
to [implied bounds].
- `ProjectionEq(Projection = Type)` -- the given associated type `Projection` is equal
to `Type`; see [the section on associated types](./traits-associated-types.html)
- in general, proving `ProjectionEq(TraitRef::Item = Type)` also
requires proving `Implemented(TraitRef)`
- `Normalize(Projection -> Type)` -- the given associated type `Projection` can be [normalized][n]
to `Type`
- as discussed in [the section on associated types](./traits-associated-types.html),
`Normalize` implies `ProjectionEq` but not vice versa
- `WellFormed(..)` -- these goals imply that the given item is
*well-formed*
- well-formedness is important to [implied bounds].
[n]: ./traits-associated-types.html#normalize
<a name=coinductive>
## Coinductive goals
Most goals in our system are "inductive". In an inductive goal,
circular reasoning is disallowed. Consider this example clause:
Implemented(Foo: Bar) :-
Implemented(Foo: Bar).
Considered inductively, this clause is useless: if we are trying to
prove `Implemented(Foo: Bar)`, we would then recursively have to prove
`Implemented(Foo: Bar)`, and that cycle would continue ad infinitum
(the trait solver will terminate here, it would just consider that
`Implemented(Foo: Bar)` is not known to be true).
However, some goals are *co-inductive*. Simply put, this means that
cycles are OK. So, if `Bar` were a co-inductive trait, then the rule
above would be perfectly valid, and it would indicate that
`Implemented(Foo: Bar)` is true.
*Auto traits* are one example in Rust where co-inductive goals are used.
Consider the `Send` trait, and imagine that we have this struct:
```rust
struct Foo {
next: Option<Box<Foo>>
}
```
The default rules for auto traits say that `Foo` is `Send` if the
types of its fields are `Send`. Therefore, we would have a rule like
Implemented(Foo: Send) :-
Implemented(Option<Box<Foo>>: Send).
As you can probably imagine, proving that `Option<Box<Foo>>: Send` is
going to wind up circularly requiring us to prove that `Foo: Send`
again. So this would be an example where we wind up in a cycle -- but
that's ok, we *do* consider `Foo: Send` to hold, even though it
references itself.
In general, co-inductive traits are used in Rust trait solving when we
want to enumerate a fixed set of possibilities. In the case of auto
traits, we are enumerating the set of reachable types from a given
starting point (i.e., `Foo` can reach values of type
`Option<Box<Foo>>`, which implies it can reach values of type
`Box<Foo>`, and then of type `Foo`, and then the cycle is complete).
In addition to auto traits, `WellFormed` predicates are co-inductive.
These are used to achieve a similar "enumerate all the cases" pattern,
as described in the section on [implied bounds].
[implied bounds]: ./traits-lowering-rules.html#implied-bounds
## Incomplete chapter
Some topics yet to be written:
- Elaborate on the proof procedure
- SLG solving -- introduce negative reasoning

9
src/traits-implied-bounds.md Normal file
View File

@ -0,0 +1,9 @@
# Implied Bounds
*to be written*
Cover:
- Why the `FromEnv` setup etc is the way it is
- Perhaps move some of the material from 'lowering rules' in to here
- Show various examples where you could go wrong

268
src/traits-lowering-rules.md Normal file
View File

@ -0,0 +1,268 @@
# Lowering rules
This section gives the complete lowering rules for Rust traits into
[program clauses][pc]. It is a kind of reference. These rules
reference the [domain goals][dg] defined in an earlier section.
[pc]: ./traits-goals-and-clauses.html
[dg]: ./traits-goals-and-clauses.html#domain-goals
## Notation
The nonterminal `Pi` is used to mean some generic *parameter*, either a
named lifetime like `'a` or a type paramter like `A`.
The nonterminal `Ai` is used to mean some generic *argument*, which
might be a lifetime like `'a` or a type like `Vec<A>`.
When defining the lowering rules, we will give goals and clauses in
the [notation given in this section](./traits-goals-and-clauses.html).
We sometimes insert "macros" like `LowerWhereClause!` into these
definitions; these macros reference other sections within this chapter.
## Lowering where clauses
When used in a goal position, where clauses can be mapped directly to
[domain goals][dg], as follows:
- `A0: Foo<A1..An>` maps to `Implemented(A0: Foo<A1..An>)`.
- `A0: Foo<A1..An, Item = T>` maps to `ProjectionEq(<A0 as Foo<A1..An>>::Item = T)`
- `T: 'r` maps to `Outlives(T, 'r)`
- `'a: 'b` maps to `Outlives('a, 'b)`
In the rules below, we will use `WC` to indicate where clauses that
appear in Rust syntax; we will then use the same `WC` to indicate
where those where clauses appear as goals in the program clauses that
we are producing. In that case, the mapping above is used to convert
from the Rust syntax into goals.
### Transforming the lowered where clauses
In addition, in the rules below, we sometimes do some transformations
on the lowered where clauses, as defined here:
- `FromEnv(WC)` -- this indicates that:
- `Implemented(TraitRef)` becomes `FromEnv(TraitRef)`
- `ProjectionEq(Projection = Ty)` becomes `FromEnv(Projection = Ty)`
- other where-clauses are left intact
- `WellFormed(WC)` -- this indicates that:
- `Implemented(TraitRef)` becomes `WellFormed(TraitRef)`
- `ProjectionEq(Projection = Ty)` becomes `WellFormed(Projection = Ty)`
*TODO*: I suspect that we want to alter the outlives relations too,
but Chalk isn't modeling those right now.
## Lowering traits
Given a trait definition
```rust
trait Trait<P1..Pn> // P0 == Self
where WC
{
// trait items
}
```
we will produce a number of declarations. This section is focused on
the program clauses for the trait header (i.e., the stuff outside the
`{}`); the [section on trait items](#trait-items) covers the stuff
inside the `{}`.
### Trait header
From the trait itself we mostly make "meta" rules that setup the
relationships between different kinds of domain goals. The first such
rule from the trait header creates the mapping between the `FromEnv`
and `Implemented` predicates:
forall<Self, P1..Pn> {
Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
}
<a name="implied-bounds">
#### Implied bounds
The next few clauses have to do with implied bounds (see also
[RFC 2089]). For each trait, we produce two clauses:
[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html
// For each where clause WC:
forall<Self, P1..Pn> {
FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
}
This clause says that if we are assuming that the trait holds, then we can also
assume that it's where-clauses hold. It's perhaps useful to see an example:
```rust
trait Eq: PartialEq { ... }
```
In this case, the `PartialEq` supertrait is equivalent to a `where
Self: PartialEq` where clause, in our simplified model. The program
clause above therefore states that if we can prove `FromEnv(T: Eq)` --
e.g., if we are in some function with `T: Eq` in its where clauses --
then we also know that `FromEnv(T: PartialEq)`. Thus the set of things
that follow from the environment are not only the **direct where
clauses** but also things that follow from them.
The next rule is related; it defines what it means for a trait reference
to be **well-formed**:
// For each where clause WC:
forall<Self, P1..Pn> {
WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
}
This `WellFormed` rule states that `T: Trait` is well-formed if (a)
`T: Trait` is implemented and (b) all the where-clauses declared on
`Trait` are well-formed (and hence they are implemented). Remember
that the `WellFormed` predicate is
[coinductive](./traits-goals-and-clauses.html#coinductive); in this
case, it is serving as a kind of "carrier" that allows us to enumerate
all the where clauses that are transitively implied by `T: Trait`.
An example:
```rust
trait Foo: A + Bar { }
trait Bar: B + Foo { }
trait A { }
trait B { }
```
Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and `T: B`.
And indeed if we were to try to prove `WellFormed(T: Foo)`, we would have to prove each
one of those:
- `WellFormed(T: Foo)`
- `Implemented(T: Foo)`
- `WellFormed(T: A)`
- `Implemented(T: A)`
- `WellFormed(T: Bar)`
- `Implemented(T: Bar)`
- `WellFormed(T: B)`
- `Implemented(T: Bar)`
- `WellFormed(T: Foo)` -- cycle, true coinductively
This `WellFormed` predicate is only used when proving that impls are
well-formed -- basically, for each impl of some trait ref `TraitRef`,
we must show that `WellFormed(TraitRef)`. This in turn justifies the
implied bounds rules that allow us to extend the set of `FromEnv`
items.
<a name=trait-items>
## Lowering trait items
### Associated type declarations
Given a trait that declares a (possibly generic) associated type:
```rust
trait Trait<P1..Pn> // P0 == Self
where WC
{
type AssocType<Pn+1..Pm>: Bounds where WC1;
}
```
We will produce a number of program clauses. The first two define
the rules by which `ProjectionEq` can succeed; these two clauses are discussed
in detail in the [section on associated types](./traits-associated-types.html),,
but reproduced here for reference:
// ProjectionEq can succeed by normalizing:
forall<Self, P1..Pn, Pn+1..Pm, U> {
ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :-
Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U)
}
// ProjectionEq can succeed by skolemizing, see "associated type"
// chapter for more:
forall<Self, P1..Pn, Pn+1..Pm> {
ProjectionEq(
<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
(Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>
) :-
// But only if the trait is implemented, and the conditions from
// the associated type are met as well:
Implemented(Self: Trait<P1..Pn>)
&& WC1
}
The next rule covers implied bounds for the projection. In particular,
the `Bounds` declared on the associated type must be proven to hold to
show that the impl is well-formed, and hence we can rely on them
elsewhere.
// XXX how exactly should we set this up? Have to be careful;
// presumably this has to be a kind of `FromEnv` setup.
### Lowering function and constant declarations
Chalk didn't model functions and constants, but I would eventually
like to treat them exactly like normalization. See [the section on function/constant
values below](#constant-vals) for more details.
## Lowering impls
Given an impl of a trait:
```rust
impl<P0..Pn> Trait<A1..An> for A0
where WC
{
// zero or more impl items
}
```
Let `TraitRef` be the trait reference `A0: Trait<A1..An>`. Then we
will create the following rules:
forall<P0..Pn> {
Implemented(TraitRef) :- WC
}
In addition, we will lower all of the *impl items*.
## Lowering impl items
### Associated type values
Given an impl that contains:
```rust
impl<P0..Pn> Trait<A1..An> for A0
where WC
{
type AssocType<Pn+1..Pm> where WC1 = T;
}
```
We produce the following rule:
forall<P0..Pm> {
forall<Pn+1..Pm> {
Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
WC && WC1
}
}
Note that `WC` and `WC1` both encode where-clauses that the impl can
rely on.
<a name=constant-vals>
### Function and constant values
Chalk didn't model functions and constants, but I would eventually
like to treat them exactly like normalization. This presumably
involves adding a new kind of parameter (constant), and then having a
`NormalizeValue` domain goal. This is *to be written* because the
details are a bit up in the air.

185
src/traits-lowering-to-logic.md Normal file
View File

@ -0,0 +1,185 @@
# Lowering to logic
The key observation here is that the Rust trait system is basically a
kind of logic, and it can be mapped onto standard logical inference
rules. We can then look for solutions to those inference rules in a
very similar fashion to how e.g. a [Prolog] solver works. It turns out
that we can't *quite* use Prolog rules (also called Horn clauses) but
rather need a somewhat more expressive variant.
[Prolog]: https://en.wikipedia.org/wiki/Prolog
## Rust traits and logic
One of the first observations is that the Rust trait system is
basically a kind of logic. As such, we can map our struct, trait, and
impl declarations into logical inference rules. For the most part,
these are basically Horn clauses, though we'll see that to capture the
full richness of Rust -- and in particular to support generic
programming -- we have to go a bit further than standard Horn clauses.
To see how this mapping works, let's start with an example. Imagine
we declare a trait and a few impls, like so:
```rust
trait Clone { }
impl Clone for usize { }
impl<T> Clone for Vec<T> where T: Clone { }
```
We could map these declarations to some Horn clauses, written in a
Prolog-like notation, as follows:
```
Clone(usize).
Clone(Vec<?T>) :- Clone(?T).
// The notation `A :- B` means "A is true if B is true".
// Or, put another way, B implies A.
```
In Prolog terms, we might say that `Clone(Foo)` -- where `Foo` is some
Rust type -- is a *predicate* that represents the idea that the type
`Foo` implements `Clone`. These rules are **program clauses**; they
state the conditions under which that predicate can be proven (i.e.,
considered true). So the first rule just says "Clone is implemented
for `usize`". The next rule says "for any type `?T`, Clone is
implemented for `Vec<?T>` if clone is implemented for `?T`". So
e.g. if we wanted to prove that `Clone(Vec<Vec<usize>>)`, we would do
so by applying the rules recursively:
- `Clone(Vec<Vec<usize>>)` is provable if:
- `Clone(Vec<usize>)` is provable if:
- `Clone(usize)` is provable. (Which is is, so we're all good.)
But now suppose we tried to prove that `Clone(Vec<Bar>)`. This would
fail (after all, I didn't give an impl of `Clone` for `Bar`):
- `Clone(Vec<Bar>)` is provable if:
- `Clone(Bar)` is provable. (But it is not, as there are no applicable rules.)
We can easily extend the example above to cover generic traits with
more than one input type. So imagine the `Eq<T>` trait, which declares
that `Self` is equatable with a value of type `T`:
```rust
trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
```
That could be mapped as follows:
```
Eq(usize, usize).
Eq(Vec<?T>, Vec<?U>) :- Eq(?T, ?U).
```
So far so good.
## Type-checking normal functions
OK, now that we have defined some logical rules that are able to
express when traits are implemented and to handle associated types,
let's turn our focus a bit towards **type-checking**. Type-checking is
interesting because it is what gives us the goals that we need to
prove. That is, everything we've seen so far has been about how we
derive the rules by which we can prove goals from the traits and impls
in the program; but we are also interested in how to derive the goals
that we need to prove, and those come from type-checking.
Consider type-checking the function `foo()` here:
```rust
fn foo() { bar::<usize>() }
fn bar<U: Eq<U>>() { }
```
This function is very simple, of course: all it does is to call
`bar::<usize>()`. Now, looking at the definition of `bar()`, we can see
that it has one where-clause `U: Eq<U>`. So, that means that `foo()` will
have to prove that `usize: Eq<usize>` in order to show that it can call `bar()`
with `usize` as the type argument.
If we wanted, we could write a Prolog predicate that defines the
conditions under which `bar()` can be called. We'll say that those
conditions are called being "well-formed":
```
barWellFormed(?U) :- Eq(?U, ?U).
```
Then we can say that `foo()` type-checks if the reference to
`bar::<usize>` (that is, `bar()` applied to the type `usize`) is
well-formed:
```
fooTypeChecks :- barWellFormed(usize).
```
If we try to prove the goal `fooTypeChecks`, it will succeed:
- `fooTypeChecks` is provable if:
- `barWellFormed(usize)`, which is provable if:
- `Eq(usize, usize)`, which is provable because of an impl.
Ok, so far so good. Let's move on to type-checking a more complex function.
## Type-checking generic functions: beyond Horn clauses
In the last section, we used standard Prolog horn-clauses (augmented with Rust's
notion of type equality) to type-check some simple Rust functions. But that only
works when we are type-checking non-generic functions. If we want to type-check
a generic function, it turns out we need a stronger notion of goal than Prolog
can be provide. To see what I'm talking about, let's revamp our previous
example to make `foo` generic:
```rust
fn foo<T: Eq<T>>() { bar::<T>() }
fn bar<U: Eq<U>>() { }
```
To type-check the body of `foo`, we need to be able to hold the type
`T` "abstract". That is, we need to check that the body of `foo` is
type-safe *for all types `T`*, not just for some specific type. We might express
this like so:
```
fooTypeChecks :-
// for all types T...
forall<T> {
// ...if we assume that Eq(T, T) is provable...
if (Eq(T, T)) {
// ...then we can prove that `barWellFormed(T)` holds.
barWellFormed(T)
}
}.
```
This notation I'm using here is the notation I've been using in my
prototype implementation; it's similar to standard mathematical
notation but a bit Rustified. Anyway, the problem is that standard
Horn clauses don't allow universal quantification (`forall`) or
implication (`if`) in goals (though many Prolog engines do support
them, as an extension). For this reason, we need to accept something
called "first-order hereditary harrop" (FOHH) clauses -- this long
name basically means "standard Horn clauses with `forall` and `if` in
the body". But it's nice to know the proper name, because there is a
lot of work describing how to efficiently handle FOHH clauses; see for
example Gopalan Nadathur's excellent
["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf]
in [the bibliography].
[the bibliography]: ./traits-bibliography.html
[pphhf]: ./traits-bibliography.html#pphhf
It turns out that supporting FOHH is not really all that hard. And
once we are able to do that, we can easily describe the type-checking
rule for generic functions like `foo` in our logic.
## Source
This page is a lightly adapted version of a
[blog post by Nicholas Matsakis][lrtl].
[lrtl]: http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/

3
src/traits-regions.md Normal file
View File

@ -0,0 +1,3 @@
# Region constraints
*to be written*

1
src/traits-slg.md Normal file
View File

@ -0,0 +1 @@
# The SLG solver

11
src/traits-wf.md Normal file
View File

@ -0,0 +1,11 @@
# Well-formedness checking
This chapter is mostly *to be written*. WF checking, in short, has the
job of checking that the various declarations in a Rust program are
well-formed. This is the basis for implied bounds, and partly for that
reason, this checking can be surprisingly subtle! (For example, we
have to be sure that each impl proves the WF conditions declared on
the trait.)

35
src/traits.md Normal file
View File

@ -0,0 +1,35 @@
# 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](./trait-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:
- [Lowering to logic](./traits-lowering-to-logic.html), which expresses
Rust traits in terms of standard logical terms.
- The [goals and clauses](./traits-goals-and-clauses.html) chapter
describes the precise form of rules we use, and
[lowering rules](./traits-lowering-rules.html) gives the complete set of
lowering rules in a more reference-like form.
- [Canonical queries](./traits-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](./traits-associated-types.html), which is the
technique we use to accommodate associated types when figuring out
whether types are equal.
- [Region constraints](./traits-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.

2
src/type-inference.md
View File

@ -43,6 +43,8 @@ The `tcx.infer_ctxt` method actually returns a builder, which means
there are some kinds of configuration you can do before the `infcx` is
created. See `InferCtxtBuilder` for more information.
<a name=vars>
## Inference variables
The main purpose of the inference context is to house a bunch of