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

Address review comments.

This commit is contained in:
Charles Lew 2020-04-20 22:24:38 +08:00 committed by Who? Me?!
parent 4b1b22464f
commit 37ffada957
9 changed files with 725 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/SUMMARY.md
View File

@ -77,8 +77,10 @@
- [Caching subtleties](./traits/caching.md)
- [Specialization](./traits/specialization.md)
- [Chalk-based trait solving](./traits/chalk.md)
- [Region constraints](./traits/regions.md)
- [Chalk-oriented lowering module in rustc](./traits/lowering-module.md)
- [Lowering to logic](./traits/lowering-to-logic.md)
- [Goals and clauses](./traits/goals-and-clauses.md)
- [Canonical queries](./traits/canonical-queries.md)
- [Lowering module in rustc](./traits/lowering-module.md)
- [Type checking](./type-checking.md)
- [Method Lookup](./method-lookup.md)
- [Variance](./variance.md)

5
src/appendix/code-index.md
View File

@ -27,7 +27,7 @@ Item | Kind | Short description | Chapter |
`StringReader` | struct | This is the lexer used during parsing. It consumes characters from the raw source code being compiled and produces a series of tokens for use by the rest of the parser | [The parser] | [src/librustc_parse/lexer/mod.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_parse/lexer/struct.StringReader.html)
`rustc_ast::token_stream::TokenStream` | struct | An abstract sequence of tokens, organized into `TokenTree`s | [The parser], [Macro expansion] | [src/librustc_ast/tokenstream.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_ast/tokenstream/struct.TokenStream.html)
`TraitDef` | struct | This struct contains a trait's definition with type information | [The `ty` modules] | [src/librustc_middle/ty/trait_def.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/trait_def/struct.TraitDef.html)
`TraitRef` | struct | The combination of a trait and its input types (e.g. `P0: Trait<P1...Pn>`) | [Chalk Book: Goals and Clauses], [Chalk Book: Lowering impls] | [src/librustc_middle/ty/sty.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TraitRef.html)
`TraitRef` | struct | The combination of a trait and its input types (e.g. `P0: Trait<P1...Pn>`) | [Trait Solving: Goals and Clauses] | [src/librustc_middle/ty/sty.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TraitRef.html)
`Ty<'tcx>` | struct | This is the internal representation of a type used for type checking | [Type checking] | [src/librustc_middle/ty/mod.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/type.Ty.html)
`TyCtxt<'tcx>` | struct | The "typing context". This is the central data structure in the compiler. It is the context that you use to perform all manner of queries | [The `ty` modules] | [src/librustc_middle/ty/context.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html)
@ -42,5 +42,4 @@ Item | Kind | Short description | Chapter |
[Macro expansion]: ../macro-expansion.html
[Name resolution]: ../name-resolution.html
[Parameter Environment]: ../param_env.html
[Chalk Book: Goals and Clauses]: https://rust-lang.github.io/chalk/book/clauses/goals_and_clauses.html#domain-goals
[Chalk Book: Lowering impls]: https://rust-lang.github.io/chalk/book/clauses/lowering_rules.html#lowering-impls
[Trait Solving: Goals and Clauses]: ../traits/goals-and-clauses.html#domain-goals

6
src/appendix/glossary.md
View File

@ -49,7 +49,7 @@ memoization <div id="memoization"/> | The process of storing the results o
MIR <div id="mir"/> | The Mid-level IR that is created after type-checking for use by borrowck and codegen. ([see more](../mir/index.html))
miri <div id="miri"/> | An interpreter for MIR used for constant evaluation. ([see more](../miri.html))
monomorphization <div id="mono"/> | The process of taking generic implementations of types and functions and instantiating them with concrete types. For example, in the code we might have `Vec<T>`, but in the final executable, we will have a copy of the `Vec` code for every concrete type used in the program (e.g. a copy for `Vec<usize>`, a copy for `Vec<MyStruct>`, etc).
normalize <div id="normalize"/> | A general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](https://rust-lang.github.io/chalk/book/clauses/type_equality.html#normalize).
normalize <div id="normalize"/> | A general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](../traits/goals-and-clauses.html#normalizeprojection---type).
newtype <div id="newtype"/> | 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 <div id="nll"/> | Short for [non-lexical lifetimes](../borrow_check/region_inference.html), this is an extension to Rust's borrowing system to make it be based on the control-flow graph.
node-id or NodeId <div id="node-id"/> | An index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`. See [the HIR chapter for more](../hir.html#identifiers-in-the-hir).
@ -57,7 +57,7 @@ obligation <div id="obligation"/> | Something that must be proven by the
placeholder <div id="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/placeholders_and_universes.md) for more details.
point <div id="point"/> | Used in the NLL analysis to refer to some particular location in the MIR; typically used to refer to a node in the control-flow graph.
polymorphize <div id="polymorphize"/> | An optimization that avoids unnecessary monomorphisation. ([see more](../backend/monomorph.md#polymorphization))
projection <div id="projection"/> | A general term for a "relative path", e.g. `x.f` is a "field projection", and `T::Item` is an ["associated type projection"](https://rust-lang.github.io/chalk/book/clauses/goals_and_clauses.html#trait-ref).
projection <div id="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 <div id="pc"/> | Constants extracted from a function and lifted to static scope; see [this section](../mir/index.html#promoted) for more details.
provider <div id="provider"/> | The function that executes a query. ([see more](../query.html))
quantified <div id="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).
@ -74,7 +74,7 @@ tcx <div id="tcx"/> | The "typing context", main data stru
'tcx <div id="lifetime-tcx"/> | The lifetime of the allocation arena. ([see more](../ty.html))
token <div id="token"/> | The smallest unit of parsing. Tokens are produced after lexing ([see more](../the-parser.html)).
[TLS] <div id="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.
trait reference <div id="trait-ref"/> | The name of a trait along with a suitable set of input type/lifetimes. ([see more](https://rust-lang.github.io/chalk/book/clauses/goals_and_clauses.html#trait-ref))
trait reference <div id="trait-ref"/> | The name of a trait along with a suitable set of input type/lifetimes. ([see more](../traits/goals-and-clauses.html#trait-ref))
trans <div id="trans"/> | The code to translate MIR into LLVM IR. Renamed to codegen.
ty <div id="ty"/> | The internal representation of a type. ([see more](../ty.html))
UFCS <div id="ufcs"/> | Short for Universal Function Call Syntax, this is an unambiguous syntax for calling a method. ([see more](../type-checking.html))

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

@ -0,0 +1,252 @@
# 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](./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:
```text
?- Vec<i32>: AsRef<?U>
```
The solver might answer:
```text
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:
```text
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:
```text
no
```
Naturally, in some cases, there may be no possible answers, and hence
the solver will just give me back `no` right away:
```text
?- 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:
```text
?- 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:
```text
?- Rc<?T>: Clone
```
might produce the answer:
```text
Rc<?T>: Clone
continue? (y/n)
```
After all, `Rc<?T>` is true **no matter what type `?T` is**.
<a name="query-response"></a>
## 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 tell 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](./slg.html) for details.)
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](./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 clarity, I've written the
`Sized` bounds explicitly):
[borrow]: https://doc.rust-lang.org/std/borrow/trait.Borrow.html
```rust,ignore
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,ignore
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,ignore
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, `Vec<?V>`. So, if we "refresh" the query with that value, we get:
```text
Vec<?T>: Borrow<Vec<?V>>
```
This time, there is only one impl that applies, the reflexive impl:
```text
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.)

21
src/traits/chalk.md
View File

@ -1,14 +1,12 @@
# Chalk-based trait solving (new-style)
# Chalk-based trait solving
> 🚧 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 subchapter](./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]!
[Chalk][chalk] is an experimental trait solver for rust that is currently
under development by the [Traits Working Group][wg]. Its goal is
to enable a lot of trait system features and bug fixes that are
currently hard to implement (e.g. GATs or specialization). 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
@ -36,8 +34,7 @@ The design of the new-style trait solving currently happens in two places:
and designs for the trait system.
**rustc**. Once we are happy with the logical rules, we proceed to
implementing them in rustc. This mainly happens in
[`librustc_traits`][librustc_traits]. We map our struct, trait, and impl declarations
implementing them in rustc. We map our struct, trait, and impl declarations
into logical inference rules in the [lowering module in rustc](./lowering-module.md).
[chalk]: https://github.com/rust-lang/chalk

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

@ -0,0 +1,270 @@
# 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](./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):
```text
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.
In terms of code, these types are defined in
[`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in
[`chalk-ir/src/lib.rs`][chalk_ir] in chalk.
[pphhf]: ./bibliography.html#pphhf
[traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/traits/mod.rs
[chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs
<a name="domain-goals"></a>
## Domain goals
*Domain goals* are the atoms of the trait logic. As can be seen in the
definitions given above, general goals basically consist in a combination of
domain goals.
Moreover, flattening a bit the definition of clauses given previously, one can
see that clauses are always of the form:
```text
forall<K1, ..., Kn> { DomainGoal :- Goal }
```
hence domain goals are in fact clauses' LHS. That is, at the most granular level,
domain goals are what the trait solver will end up trying to prove.
<a name="trait-ref"></a>
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:
```text
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>
A **projection** consists of an associated item reference along with
its inputs P0..Pm:
```text
Projection = <P0 as TraitName<P1..Pn>>::AssocItem<Pn+1..Pm>
```
Given these, we can define a `DomainGoal` as follows:
```text
DomainGoal = Holds(WhereClause)
| FromEnv(TraitRef)
| FromEnv(Type)
| WellFormed(TraitRef)
| WellFormed(Type)
| Normalize(Projection -> Type)
WhereClause = Implemented(TraitRef)
| ProjectionEq(Projection = Type)
| Outlives(Type: Region)
| Outlives(Region: Region)
```
`WhereClause` refers to a `where` clause that a Rust user would actually be able
to write in a Rust program. This abstraction exists only as a convenience as we
sometimes want to only deal with domain goals that are effectively writable in
Rust.
Let's break down each one of these, one-by-one.
#### Implemented(TraitRef)
e.g. `Implemented(i32: Copy)`
True if the given trait is implemented for the given input types and lifetimes.
#### ProjectionEq(Projection = Type)
e.g. `ProjectionEq<T as Iterator>::Item = u8`
The given associated type `Projection` is equal to `Type`; this can be proved
with either normalization or using placeholder associated types. See
[the section on associated types](./associated-types.html).
#### Normalize(Projection -> Type)
e.g. `ProjectionEq<T as Iterator>::Item -> u8`
The given associated type `Projection` can be [normalized][n] to `Type`.
As discussed in [the section on associated
types](./associated-types.html), `Normalize` implies `ProjectionEq`,
but not vice versa. In general, proving `Normalize(<T as Trait>::Item -> U)`
also requires proving `Implemented(T: Trait)`.
[n]: ./associated-types.html#normalize
[at]: ./associated-types.html
#### FromEnv(TraitRef)
e.g. `FromEnv(Self: Add<i32>)`
True if the inner `TraitRef` is *assumed* to be true,
that is, if it can be derived from the in-scope where clauses.
For example, given the following function:
```rust
fn loud_clone<T: Clone>(stuff: &T) -> T {
println!("cloning!");
stuff.clone()
}
```
Inside the body of our function, we would have `FromEnv(T: Clone)`. In-scope
where clauses nest, so a function body inside an impl body inherits the
impl body's where clauses, too.
This and the next rule are used to implement [implied bounds]. As we'll see
in the section on lowering, `FromEnv(TraitRef)` implies `Implemented(TraitRef)`,
but not vice versa. This distinction is crucial to implied bounds.
#### FromEnv(Type)
e.g. `FromEnv(HashSet<K>)`
True if the inner `Type` is *assumed* to be well-formed, that is, if it is an
input type of a function or an impl.
For example, given the following code:
```rust,ignore
struct HashSet<K> where K: Hash { ... }
fn loud_insert<K>(set: &mut HashSet<K>, item: K) {
println!("inserting!");
set.insert(item);
}
```
`HashSet<K>` is an input type of the `loud_insert` function. Hence, we assume it
to be well-formed, so we would have `FromEnv(HashSet<K>)` inside the body of our
function. As we'll see in the section on lowering, `FromEnv(HashSet<K>)` implies
`Implemented(K: Hash)` because the
`HashSet` declaration was written with a `K: Hash` where clause. Hence, we don't
need to repeat that bound on the `loud_insert` function: we rather automatically
assume that it is true.
#### WellFormed(Item)
These goals imply that the given item is *well-formed*.
We can talk about different types of items being well-formed:
* *Types*, like `WellFormed(Vec<i32>)`, which is true in Rust, or
`WellFormed(Vec<str>)`, which is not (because `str` is not `Sized`.)
* *TraitRefs*, like `WellFormed(Vec<i32>: Clone)`.
Well-formedness is important to [implied bounds]. In particular, the reason
it is okay to assume `FromEnv(T: Clone)` in the `loud_clone` example is that we
_also_ verify `WellFormed(T: Clone)` for each call site of `loud_clone`.
Similarly, it is okay to assume `FromEnv(HashSet<K>)` in the `loud_insert`
example because we will verify `WellFormed(HashSet<K>)` for each call site of
`loud_insert`.
#### Outlives(Type: Region), Outlives(Region: Region)
e.g. `Outlives(&'a str: 'b)`, `Outlives('a: 'static)`
True if the given type or region on the left outlives the right-hand region.
<a name="coinductive"></a>
## Coinductive goals
Most goals in our system are "inductive". In an inductive goal,
circular reasoning is disallowed. Consider this example clause:
```text
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
```text
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]: ./lowering-rules.html#implied-bounds
## Incomplete chapter
Some topics yet to be written:
- Elaborate on the proof procedure
- SLG solving – introduce negative reasoning

55
src/traits/lowering-module.md
View File

@ -1,56 +1 @@
# The lowering module in rustc
The program clauses described in the
[lowering rules chapter in Chalk Book](https://rust-lang.github.io/chalk/book/clauses/lowering_rules.html)
are actually created in the [`rustc_traits::lowering`][lowering] module.
[lowering]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_traits/lowering/
## The `program_clauses_for` query
The main entry point is the `program_clauses_for` [query], which –
given a `DefId` – produces a set of Chalk program clauses. The
query is invoked on a `DefId` that identifies something like a trait,
an impl, or an associated item definition. It then produces and
returns a vector of program clauses.
[query]: ../query.html
## Unit tests
**Note: We've removed the Chalk unit tests in [rust-lang/rust#69247].
They will come back once we're ready to integrate next Chalk into rustc.**
Here's a good example test. At the time of
this writing, it looked like this:
```rust,ignore
#![feature(rustc_attrs)]
trait Foo { }
#[rustc_dump_program_clauses] //~ ERROR program clause dump
impl<T: 'static> Foo for T where T: Iterator<Item = i32> { }
fn main() {
println!("hello");
}
```
The `#[rustc_dump_program_clauses]` annotation can be attached to
anything with a `DefId` (It requires the `rustc_attrs` feature). The
compiler will then invoke the `program_clauses_for` query on that
item, and emit compiler errors that dump the clauses produced. These
errors just exist for unit-testing. The stderr will be:
```text
error: program clause dump
--> $DIR/lower_impl.rs:5:1
|
LL | #[rustc_dump_program_clauses]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: forall<T> { Implemented(T: Foo) :- ProjectionEq(<T as std::iter::Iterator>::Item == i32), TypeOutlives(T: 'static), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized). }
```
[rust-lang/rust#69247]: https://github.com/rust-lang/rust/pull/69247

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:
```text
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 it 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,ignore
trait Eq<T> { ... }
impl Eq<usize> for usize { }
impl<T: Eq<U>> Eq<Vec<U>> for Vec<T> { }
```
That could be mapped as follows:
```text
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,ignore
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":
```text
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:
```text
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 what Prolog
can provide. To see what I'm talking about, let's revamp our previous
example to make `foo` generic:
```rust,ignore
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:
```text
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]: ./bibliography.html
[pphhf]: ./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/

9
src/traits/regions.md
View File

@ -1,9 +0,0 @@
# Region constraints
*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.