From c009f4805921cca91b13a0aec8f9c4bfa952054a Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Sun, 19 Apr 2020 22:48:45 +0800 Subject: [PATCH 1/5] Remove details about chalk and point to Chalk Book instead. --- src/SUMMARY.md | 19 +- src/traits/associated-types.md | 168 ----------- src/traits/bibliography.md | 27 -- src/traits/canonical-queries.md | 252 ---------------- src/traits/canonicalization.md | 256 ---------------- src/traits/chalk-overview.md | 256 ---------------- src/traits/chalk.md | 43 +++ src/traits/goals-and-clauses.md | 270 ----------------- src/traits/implied-bounds.md | 502 -------------------------------- src/traits/index.md | 64 ---- src/traits/lowering-rules.md | 416 -------------------------- src/traits/lowering-to-logic.md | 185 ------------ src/traits/resolution.md | 2 +- src/traits/slg.md | 302 ------------------- src/traits/wf.md | 469 ----------------------------- 15 files changed, 48 insertions(+), 3183 deletions(-) delete mode 100644 src/traits/associated-types.md delete mode 100644 src/traits/bibliography.md delete mode 100644 src/traits/canonical-queries.md delete mode 100644 src/traits/canonicalization.md delete mode 100644 src/traits/chalk-overview.md create mode 100644 src/traits/chalk.md delete mode 100644 src/traits/goals-and-clauses.md delete mode 100644 src/traits/implied-bounds.md delete mode 100644 src/traits/index.md delete mode 100644 src/traits/lowering-rules.md delete mode 100644 src/traits/lowering-to-logic.md delete mode 100644 src/traits/slg.md delete mode 100644 src/traits/wf.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 28abd8d65..38634e26a 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -72,24 +72,13 @@ - [`TypeFolder` and `TypeFoldable`](./ty-fold.md) - [Generic arguments](./generic_arguments.md) - [Type inference](./type-inference.md) - - [Trait solving (old-style)](./traits/resolution.md) + - [Trait solving](./traits/resolution.md) - [Higher-ranked trait bounds](./traits/hrtb.md) - [Caching subtleties](./traits/caching.md) - [Specialization](./traits/specialization.md) - - [Trait solving (new-style)](./traits/index.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) - - [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) - - [The SLG solver](./traits/slg.md) - - [An Overview of Chalk](./traits/chalk-overview.md) - - [Bibliography](./traits/bibliography.md) + - [Chalk-based trait solving](./traits/chalk.md) + - [Region constraints](./traits/regions.md) + - [Chalk-oriented lowering module in rustc](./traits/lowering-module.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) - [Variance](./variance.md) diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md deleted file mode 100644 index 41ce5ac9e..000000000 --- a/src/traits/associated-types.md +++ /dev/null @@ -1,168 +0,0 @@ -# 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 -- Placeholder associated type projections -- 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 ` 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 - - - -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` -declares (among other things) that `Item = T`: - -```rust,ignore -impl IntoIterator for Option { - type Item = T; - ... -} -``` - -This means we can normalize the projection ` 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. - -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 -impls. For example, the `impl` of `IntoIterator` for `Option` that -we saw above would be lowered to a program clause like so: - -```text -forall { - Normalize( as IntoIterator>::Item -> T) :- - Implemented(Option: IntoIterator) -} -``` - -where in this case, the one `Implemented` condition is always true. - -> 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. - -## Placeholder associated types - -Sometimes however we want to work with associated types that cannot be -normalized. For example, consider this function: - -```rust,ignore -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. - -Placeholder associated types are never written directly by the user. -They are used internally by the trait system only, as we will see -shortly. - -In rustc, they correspond to the `TyKind::UnnormalizedProjectionTy` enum -variant, declared in [`librustc_middle/ty/sty.rs`][sty]. In chalk, we use an -`ApplicationTy` with a name living in a special namespace dedicated to -placeholder associated types (see the `TypeName` enum declared in -[`chalk-ir/src/lib.rs`][chalk_type_name]). - -[sty]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/ty/sty.rs -[chalk_type_name]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs - -## 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 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: - -```text -ProjectionEq(::Item = U) -``` - -and we will see that it can be proven *either* via normalization or -via the placeholder type. As part of lowering an associated type declaration from -some trait, we create two program clauses for `ProjectionEq`: - -```text -forall { - ProjectionEq(::Item = U) :- - Normalize(::Item -> U) -} - -forall { - ProjectionEq(::Item = (IntoIterator::Item)) -} -``` - -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: - -```text -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 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) diff --git a/src/traits/bibliography.md b/src/traits/bibliography.md deleted file mode 100644 index a0242d4c4..000000000 --- a/src/traits/bibliography.md +++ /dev/null @@ -1,27 +0,0 @@ -# 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 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 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 diff --git a/src/traits/canonical-queries.md b/src/traits/canonical-queries.md deleted file mode 100644 index e15bdaae2..000000000 --- a/src/traits/canonical-queries.md +++ /dev/null @@ -1,252 +0,0 @@ -# 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: AsRef -``` - -The solver might answer: - -```text -Vec: 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: AsRef> - continue? (y/n) -``` - -This answer derives from the fact that there is a reflexive impl -(`impl AsRef 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: 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: Clone - Vec: Clone - continue? (y/n) - Vec>: Clone - continue? (y/n) - Vec>>: Clone - continue? (y/n) - Vec>>>: 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: Clone -``` - -might produce the answer: - -```text -Rc: Clone - continue? (y/n) -``` - -After all, `Rc` 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 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, 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: 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: Clone`, - say, or `Rc: 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: 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 Borrow for T where T: ?Sized -impl Borrow<[T]> for Vec where T: Sized -``` - -**Example 1.** Imagine we are type-checking this (rather artificial) -bit of code: - -```rust,ignore -fn foo(a: A, vec_b: Option) where A: Borrow { } - -fn main() { - let mut t: Vec<_> = vec![]; // Type: Vec - let mut u: Option<_> = None; // Type: Option - foo(t, u); // Example 1: requires `Vec: Borrow` - ... -} -``` - -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` and -`B = ?U`. Therefore, the where clause on `foo` requires that `Vec: -Borrow`. This is thus our first example trait query. - -There are many possible solutions to the query `Vec: Borrow`; -for example: - -- `?U = Vec`, -- `?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: Borrow`) 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: A, vec_b: Option) where A: Borrow { } - -fn main() { - // What we saw before: - let mut t: Vec<_> = vec![]; // Type: Vec - let mut u: Option<_> = None; // Type: Option - foo(t, u); // `Vec: Borrow` => ambiguous - - // New stuff: - u = Some(vec![]); // ?U = Vec -} -``` - -As a result of this assignment, the type of `u` is forced to be -`Option>`, where `?V` represents the element type of the -vector. This in turn implies that `?U` is [unified] to `Vec`. - -[unified]: ../type-checking.html - -Let's suppose that the type checker decides to revisit the -"as-yet-unproven" trait obligation we saw before, `Vec: -Borrow`. `?U` is no longer an unbound inference variable; it now -has a value, `Vec`. So, if we "refresh" the query with that value, we get: - -```text -Vec: Borrow> -``` - -This time, there is only one impl that applies, the reflexive impl: - -```text -impl Borrow 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.) - - diff --git a/src/traits/canonicalization.md b/src/traits/canonicalization.md deleted file mode 100644 index d6d57d785..000000000 --- a/src/traits/canonicalization.md +++ /dev/null @@ -1,256 +0,0 @@ -# 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]: ./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 canonical 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](../appendix/background.html#free-vs-bound) with a -canonical variable (Note that `'static` is actually a _free_ lifetime -variable here. We are not considering it in the typing context of the whole -program but only in the context of this trait reference. Mathematically, we -are not quantifying over the whole program, but only this obligation). -Therefore, we get the following result: - -```text -?0: Foo<'?1, ?2> -``` - -Sometimes we write this differently, like so: - -```text -for { ?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 variable, so -`?1` is a lifetime. The `canonicalize` method *also* gives back a -`CanonicalVarValues` array OV with the "original values" for each -canonicalized variable: - -```text -[?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: - -```text -for { ?0: Foo<'?1, ?2> } -``` - -the substitution S might be: - -```text -S = [?A, '?B, ?C] -``` - -We can then replace the bound canonical variables (`?0`, etc) with -these inference variables, yielding the following fully instantiated -query: - -```text -?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](./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]: ./canonical-queries.html#query-response - -```rust,ignore -impl<'a, X> Foo<'a, X> for Vec -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` -- `?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 - -```text -for { ?0: Foo<'?1, ?2> } -``` - -for which we made a substutition S: - -```text -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: - -```text -S = [Vec, '?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: - -```text -QR = { - certainty: Proven, // or whatever - var_values: [Vec, '?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: - -```text -Canonical(QR) = for { - certainty: Proven, - var_values: [Vec, '?1, ?0] - region_constraints: [?0: '?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: - -```text -?A: Foo<'static, ?B> -``` - -We canonicalized that into this: - -```text -for { ?0: Foo<'?1, ?2> } -``` - -and now we got back a canonical response: - -```text -for { - certainty: Proven, - var_values: [Vec, '?1, ?0] - region_constraints: [?0: '?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 - -```text -{ - certainty: Proven, - var_values: [Vec, '?D, ?C] - ^^ ^^^ fresh inference variables - region_constraints: [?C: '?D], - value: (), -} -``` - -Step (b) would then unify: - -```text -?A with Vec -'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 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.) - diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md deleted file mode 100644 index 64cb589c1..000000000 --- a/src/traits/chalk-overview.md +++ /dev/null @@ -1,256 +0,0 @@ -# An Overview of Chalk - -> Chalk is under heavy development, so if any of these links are broken or if -> any of the information is inconsistent with the code or outdated, please -> [open an issue][rustc-issues] so we can fix it. If you are able to fix the -> issue yourself, we would love your contribution! - -[Chalk][chalk] recasts Rust's trait system explicitly in terms of logic -programming by "lowering" Rust code into a kind of logic program we can then -execute queries against (see [*Lowering to Logic*][lowering-to-logic] and -[*Lowering Rules*][lowering-rules]). Its goal is to be an executable, highly -readable specification of the Rust trait system. - -There are many expected benefits from this work. It will consolidate our -existing, somewhat ad-hoc implementation into something far more principled and -expressive, which should behave better in corner cases, and be much easier to -extend. - -## Chalk Structure - -Chalk has two main "products". The first of these is the -[`chalk_engine`][chalk_engine] crate, which defines the core [SLG -solver][slg]. This is the part rustc uses. - -The rest of chalk can be considered an elaborate testing harness. Chalk is -capable of parsing Rust-like "programs", lowering them to logic, and -performing queries on them. - -Here's a sample session in the chalk repl, chalki. After feeding it our -program, we perform some queries on it. - -```rust,ignore -?- program -Enter a program; press Ctrl-D when finished -| struct Foo { } -| struct Bar { } -| struct Vec { } -| trait Clone { } -| impl Clone for Vec where T: Clone { } -| impl Clone for Foo { } - -?- Vec: Clone -Unique; substitution [], lifetime constraints [] - -?- Vec: Clone -No possible solution. - -?- exists { Vec: Clone } -Ambiguous; no inference guidance -``` - -You can see more examples of programs and queries in the [unit -tests][chalk-test-example]. - -Next we'll go through each stage required to produce the output above. - -### Parsing ([chalk_parse]) - -Chalk is designed to be incorporated with the Rust compiler, so the syntax and -concepts it deals with heavily borrow from Rust. It is convenient for the sake -of testing to be able to run chalk on its own, so chalk includes a parser for a -Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is -not intended to look exactly like it or support the exact same syntax. - -The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. -You can find the [complete definition of the AST][chalk-ast] in the source code. - -The syntax contains things from Rust that we know and love, for example: traits, -impls, and struct definitions. Parsing is often the first "phase" of -transformation that a program goes through in order to become a format that -chalk can understand. - -### Rust Intermediate Representation ([chalk_rust_ir]) - -After getting the AST we convert it to a more convenient intermediate -representation called [`chalk_rust_ir`][chalk_rust_ir]. This is sort of -analogous to the [HIR] in Rust. The process of converting to IR is called -*lowering*. - -The [`chalk::program::Program`][chalk-program] struct contains some "rust things" -but indexed and accessible in a different way. For example, if you have a -type like `Foo`, we would represent `Foo` as a string in the AST but in -`chalk::program::Program`, we use numeric indices (`ItemId`). - -The [IR source code][ir-code] contains the complete definition. - -### Chalk Intermediate Representation ([chalk_ir]) - -Once we have Rust IR it is time to convert it to "program clauses". A -[`ProgramClause`] is essentially one of the following: - -* A [clause] of the form `consequence :- conditions` where `:-` is read as - "if" and `conditions = cond1 && cond2 && ...` -* A universally quantified clause of the form - `forall { consequence :- conditions }` - * `forall { ... }` is used to represent [universal quantification]. See the - section on [Lowering to logic][lowering-forall] for more information. - * A key thing to note about `forall` is that we don't allow you to "quantify" - over traits, only types and regions (lifetimes). That is, you can't make a - rule like `forall { u32: Trait }` which would say "`u32` implements - all traits". You can however say `forall { T: Trait }` meaning "`Trait` - is implemented by all types". - * `forall { ... }` is represented in the code using the [`Binders` - struct][binders-struct]. - -*See also: [Goals and Clauses][goals-and-clauses]* - -This is where we encode the rules of the trait system into logic. For -example, if we have the following Rust: - -```rust,ignore -impl Clone for Vec {} -``` - -We generate the following program clause: - -```rust,ignore -forall { (Vec: Clone) :- (T: Clone) } -``` - -This rule dictates that `Vec: Clone` is only satisfied if `T: Clone` is also -satisfied (i.e. "provable"). - -Similar to [`chalk::program::Program`][chalk-program] which has "rust-like -things", chalk_ir defines [`ProgramEnvironment`] which is "pure logic". -The main field in that struct is `program_clauses`, which contains the -[`ProgramClause`]s generated by the rules module. - -### Rules ([chalk_solve]) - -The `chalk_solve` crate ([source code][chalk_solve]) defines the logic rules we -use for each item in the Rust IR. It works by iterating over every trait, impl, -etc. and emitting the rules that come from each one. - -*See also: [Lowering Rules][lowering-rules]* - -#### Well-formedness checks - -As part of lowering to logic, we also do some "well formedness" checks. See -the [`chalk_solve::wf` source code][solve-wf-src] for where those are done. - -*See also: [Well-formedness checking][wf-checking]* - -#### Coherence - -The method `CoherenceSolver::specialization_priorities` in the `coherence` module -([source code][coherence-src]) checks "coherence", which means that it -ensures that two impls of the same trait for the same type cannot exist. - -### Solver ([chalk_solve]) - -Finally, when we've collected all the program clauses we care about, we want -to perform queries on it. The component that finds the answer to these -queries is called the *solver*. - -*See also: [The SLG Solver][slg]* - -## Crates - -Chalk's functionality is broken up into the following crates: -- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg]. -- [**chalk_rust_ir**][chalk_rust_ir], containing the "HIR-like" form of the AST -- [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of - types, lifetimes, and goals. -- [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`, - effectively, which implements logic rules converting `chalk_rust_ir` to - `chalk_ir` - - Defines the `coherence` module, which implements coherence rules - - [`chalk_engine::context`][engine-context] provides the necessary hooks. -- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser. -- [**chalk**][doc-chalk]: Brings everything together. Defines the following - modules: - - `chalk::lowering`, which converts AST to `chalk_rust_ir` - - Also includes [chalki][chalki], chalk's REPL. - -[Browse source code on GitHub](https://github.com/rust-lang/chalk) - -## Testing - -chalk has a test framework for lowering programs to logic, checking the -lowered logic, and performing queries on it. This is how we test the -implementation of chalk itself, and the viability of the [lowering -rules][lowering-rules]. - -The main kind of tests in chalk are **goal tests**. They contain a program, -which is expected to lower to logic successfully, and a set of queries -(goals) along with the expected output. Here's an -[example][chalk-test-example]. Since chalk's output can be quite long, goal -tests support specifying only a prefix of the output. - -**Lowering tests** check the stages that occur before we can issue queries -to the solver: the [lowering to chalk_rust_ir][chalk-test-lowering], and the -[well-formedness checks][chalk-test-wf] that occur after that. - -### Testing internals - -Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like -syntax and runs it through the full pipeline described above. The macro -ultimately calls the [`solve_goal` function][solve_goal]. - -Likewise, lowering tests use the [`lowering_success!` and -`lowering_error!` macros][test-lowering-macros]. - -## More Resources - -* [Chalk Source Code](https://github.com/rust-lang/chalk) -* [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md) - -### Blog Posts - -* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/) -* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/) -* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/) -* [Negative reasoning in Chalk](https://aturon.github.io/blog/2017/04/24/negative-chalk/) -* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/) -* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/) -* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/) - -[goals-and-clauses]: ./goals-and-clauses.html -[HIR]: ../hir.html -[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses -[lowering-rules]: ./lowering-rules.html -[lowering-to-logic]: ./lowering-to-logic.html -[slg]: ./slg.html -[wf-checking]: ./wf.html - -[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree -[chalk]: https://github.com/rust-lang/chalk -[rustc-issues]: https://github.com/rust-lang/rustc-dev-guide/issues -[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification - -[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause.html -[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/chalk_integration/program_environment/struct.ProgramEnvironment.html -[chalk_engine]: https://rust-lang.github.io/chalk/chalk_engine -[chalk_ir]: https://rust-lang.github.io/chalk/chalk_ir/index.html -[chalk_parse]: https://rust-lang.github.io/chalk/chalk_parse/index.html -[chalk_solve]: https://rust-lang.github.io/chalk/chalk_solve/index.html -[chalk_rust_ir]: https://rust-lang.github.io/chalk/chalk_rust_ir/index.html -[doc-chalk]: https://rust-lang.github.io/chalk/chalk/index.html -[engine-context]: https://rust-lang.github.io/chalk/chalk_engine/context/index.html -[chalk-program]: https://rust-lang.github.io/chalk/chalk_integration/program/struct.Program.html - -[binders-struct]: https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html -[chalk-ast]: https://rust-lang.github.io/chalk/chalk_parse/ast/index.html -[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 -[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31 -[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs -[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1 -[chalki]: https://github.com/rust-lang/chalk/blob/master/src/main.rs -[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause -[coherence-src]: https://rust-lang.github.io/chalk/chalk_solve/coherence/index.html -[ir-code]: https://rust-lang.github.io/chalk/chalk_rust_ir/ -[solve-wf-src]: https://rust-lang.github.io/chalk/chalk_solve/wf/index.html -[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85 -[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54 -[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33 diff --git a/src/traits/chalk.md b/src/traits/chalk.md new file mode 100644 index 000000000..dcb0a244f --- /dev/null +++ b/src/traits/chalk.md @@ -0,0 +1,43 @@ +# Chalk-based 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 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]! + +[wg]: https://github.com/rust-lang/rust/issues/48416 + +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. + +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 + +You can read more about chalk itself in the +[Chalk book](https://rust-lang.github.io/chalk/book/) section. + +## Ongoing work +The design of the new-style trait solving currently happens in two places: + +**chalk**. The [chalk][chalk] repository is where we experiment with new ideas +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 into logical inference rules in the [lowering module in rustc](./lowering-module.md). + +[chalk]: https://github.com/rust-lang/chalk +[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md deleted file mode 100644 index ecd2ce145..000000000 --- a/src/traits/goals-and-clauses.md +++ /dev/null @@ -1,270 +0,0 @@ -# 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 { Goal } // existential quantification - | forall { 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 { Clause } - -K = // a "kind" - | -``` - -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 - - - -## 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 { 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. - - - -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 -``` - -So, for example, `u32: Display` is a trait reference, as is `Vec: -IntoIterator`. Note that Rust surface syntax also permits some extra -things, like associated type bindings (`Vec: IntoIterator`), that are not part of a trait reference. - - - -A **projection** consists of an associated item reference along with -its inputs P0..Pm: - -```text -Projection = >::AssocItem -``` - -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::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::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(::Item -> U)` -also requires proving `Implemented(T: Trait)`. - -[n]: ./associated-types.html#normalize -[at]: ./associated-types.html - -#### FromEnv(TraitRef) -e.g. `FromEnv(Self: Add)` - -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(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)` - -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 where K: Hash { ... } - -fn loud_insert(set: &mut HashSet, item: K) { - println!("inserting!"); - set.insert(item); -} -``` - -`HashSet` is an input type of the `loud_insert` function. Hence, we assume it -to be well-formed, so we would have `FromEnv(HashSet)` inside the body of our -function. As we'll see in the section on lowering, `FromEnv(HashSet)` 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)`, which is true in Rust, or - `WellFormed(Vec)`, which is not (because `str` is not `Sized`.) - -* *TraitRefs*, like `WellFormed(Vec: 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)` in the `loud_insert` -example because we will verify `WellFormed(HashSet)` 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. - - - -## 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> -} -``` - -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>: Send). -``` - -As you can probably imagine, proving that `Option>: 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>`, which implies it can reach values of type -`Box`, 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 diff --git a/src/traits/implied-bounds.md b/src/traits/implied-bounds.md deleted file mode 100644 index 5876f3b62..000000000 --- a/src/traits/implied-bounds.md +++ /dev/null @@ -1,502 +0,0 @@ -# Implied Bounds - -Implied bounds remove the need to repeat where clauses written on -a type declaration or a trait declaration. For example, say we have the -following type declaration: -```rust,ignore -struct HashSet { - ... -} -``` - -then everywhere we use `HashSet` as an "input" type, that is appearing in -the receiver type of an `impl` or in the arguments of a function, we don't -want to have to repeat the `where K: Hash` bound, as in: - -```rust,ignore -// I don't want to have to repeat `where K: Hash` here. -impl HashSet { - ... -} - -// Same here. -fn loud_insert(set: &mut HashSet, item: K) { - println!("inserting!"); - set.insert(item); -} -``` - -Note that in the `loud_insert` example, `HashSet` is not the type -of the `set` argument of `loud_insert`, it only *appears* in the -argument type `&mut HashSet`: we care about every type appearing -in the function's header (the header is the signature without the return type), -not only types of the function's arguments. - -The rationale for applying implied bounds to input types is that, for example, -in order to call the `loud_insert` function above, the programmer must have -*produced* the type `HashSet` already, hence the compiler already verified -that `HashSet` was well-formed, i.e. that `K` effectively implemented -`Hash`, as in the following example: - -```rust,ignore -fn main() { - // I am producing a value of type `HashSet`. - // If `i32` was not `Hash`, the compiler would report an error here. - let set: HashSet = HashSet::new(); - loud_insert(&mut set, 5); -} -``` - -Hence, we don't want to repeat where clauses for input types because that would -sort of duplicate the work of the programmer, having to verify that their types -are well-formed both when calling the function and when using them in the -arguments of their function. The same reasoning applies when using an `impl`. - -Similarly, given the following trait declaration: -```rust,ignore -trait Copy where Self: Clone { // desugared version of `Copy: Clone` - ... -} -``` - -then everywhere we bound over `SomeType: Copy`, we would like to be able to -use the fact that `SomeType: Clone` without having to write it explicitly, -as in: -```rust,ignore -fn loud_clone(x: T) { - println!("cloning!"); - x.clone(); -} - -fn fun_with_copy(x: T) { - println!("will clone a `Copy` type soon..."); - - // I'm using `loud_clone` with `T: Copy`, I know this - // implies `T: Clone` so I don't want to have to write it explicitly. - loud_clone(x); -} -``` - -The rationale for implied bounds for traits is that if a type implements -`Copy`, that is, if there exists an `impl Copy` for that type, there *ought* -to exist an `impl Clone` for that type, otherwise the compiler would have -reported an error in the first place. So again, if we were forced to repeat the -additional `where SomeType: Clone` everywhere whereas we already know that -`SomeType: Copy` hold, we would kind of duplicate the verification work. - -Implied bounds are not yet completely enforced in rustc, at the moment it only -works for outlive requirements, super trait bounds, and bounds on associated -types. The full RFC can be found [here][RFC]. We'll give here a brief view -of how implied bounds work and why we chose to implement it that way. The -complete set of lowering rules can be found in the corresponding -[chapter](./lowering-rules.md). - -[RFC]: https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md - -## Implied bounds and lowering rules - -Now we need to express implied bounds in terms of logical rules. We will start -with exposing a naive way to do it. Suppose that we have the following traits: -```rust,ignore -trait Foo { - ... -} - -trait Bar where Self: Foo { } { - ... -} -``` - -So we would like to say that if a type implements `Bar`, then necessarily -it must also implement `Foo`. We might think that a clause like this would -work: -```text -forall { - Implemented(Type: Foo) :- Implemented(Type: Bar). -} -``` - -Now suppose that we just write this impl: -```rust,ignore -struct X; - -impl Bar for X { } -``` - -Clearly this should not be allowed: indeed, we wrote a `Bar` impl for `X`, but -the `Bar` trait requires that we also implement `Foo` for `X`, which we never -did. In terms of what the compiler does, this would look like this: -```rust,ignore -struct X; - -impl Bar for X { - // We are in a `Bar` impl for the type `X`. - // There is a `where Self: Foo` bound on the `Bar` trait declaration. - // Hence I need to prove that `X` also implements `Foo` for that impl - // to be legal. -} -``` -So the compiler would try to prove `Implemented(X: Foo)`. Of course it will -not find any `impl Foo for X` since we did not write any. However, it -will see our implied bound clause: -```text -forall { - Implemented(Type: Foo) :- Implemented(Type: Bar). -} -``` - -so that it may be able to prove `Implemented(X: Foo)` if `Implemented(X: Bar)` -holds. And it turns out that `Implemented(X: Bar)` does hold since we wrote -a `Bar` impl for `X`! Hence the compiler will accept the `Bar` impl while it -should not. - -## Implied bounds coming from the environment - -So the naive approach does not work. What we need to do is to somehow decouple -implied bounds from impls. Suppose we know that a type `SomeType<...>` -implements `Bar` and we want to deduce that `SomeType<...>` must also implement -`Foo`. - -There are two possibilities: first, we have enough information about -`SomeType<...>` to see that there exists a `Bar` impl in the program which -covers `SomeType<...>`, for example a plain `impl<...> Bar for SomeType<...>`. -Then if the compiler has done its job correctly, there *must* exist a `Foo` -impl which covers `SomeType<...>`, e.g. another plain -`impl<...> Foo for SomeType<...>`. In that case then, we can just use this -impl and we do not need implied bounds at all. - -Second possibility: we do not know enough about `SomeType<...>` in order to -find a `Bar` impl which covers it, for example if `SomeType<...>` is just -a type parameter in a function: -```rust,ignore -fn foo() { - // We'd like to deduce `Implemented(T: Foo)`. -} -``` - -That is, the information that `T` implements `Bar` here comes from the -*environment*. The environment is the set of things that we assume to be true -when we type check some Rust declaration. In that case, what we assume is that -`T: Bar`. Then at that point, we might authorize ourselves to have some kind -of "local" implied bound reasoning which would say -`Implemented(T: Foo) :- Implemented(T: Bar)`. This reasoning would -only be done within our `foo` function in order to avoid the earlier -problem where we had a global clause. - -We can apply these local reasonings everywhere we can have an environment --- i.e. when we can write where clauses -- that is, inside impls, -trait declarations, and type declarations. - -## Computing implied bounds with `FromEnv` - -The previous subsection showed that it was only useful to compute implied -bounds for facts coming from the environment. -We talked about "local" rules, but there are multiple possible strategies to -indeed implement the locality of implied bounds. - -In rustc, the current strategy is to *elaborate* bounds: that is, each time -we have a fact in the environment, we recursively derive all the other things -that are implied by this fact until we reach a fixed point. For example, if -we have the following declarations: -```rust,ignore -trait A { } -trait B where Self: A { } -trait C where Self: B { } - -fn foo() { - ... -} -``` -then inside the `foo` function, we start with an environment containing only -`Implemented(T: C)`. Then because of implied bounds for the `C` trait, we -elaborate `Implemented(T: B)` and add it to our environment. Because of -implied bounds for the `B` trait, we elaborate `Implemented(T: A)`and add it -to our environment as well. We cannot elaborate anything else, so we conclude -that our final environment consists of `Implemented(T: A + B + C)`. - -In the new-style trait system, we like to encode as many things as possible -with logical rules. So rather than "elaborating", we have a set of *global* -program clauses defined like so: -```text -forall { Implemented(T: A) :- FromEnv(T: A). } - -forall { Implemented(T: B) :- FromEnv(T: B). } -forall { FromEnv(T: A) :- FromEnv(T: B). } - -forall { Implemented(T: C) :- FromEnv(T: C). } -forall { FromEnv(T: C) :- FromEnv(T: C). } -``` -So these clauses are defined globally (that is, they are available from -everywhere in the program) but they cannot be used because the hypothesis -is always of the form `FromEnv(...)` which is a bit special. Indeed, as -indicated by the name, `FromEnv(...)` facts can **only** come from the -environment. -How it works is that in the `foo` function, instead of having an environment -containing `Implemented(T: C)`, we replace this environment with -`FromEnv(T: C)`. From here and thanks to the above clauses, we see that we -are able to reach any of `Implemented(T: A)`, `Implemented(T: B)` or -`Implemented(T: C)`, which is what we wanted. - -## Implied bounds and well-formedness checking - -Implied bounds are tightly related with well-formedness checking. -Well-formedness checking is the process of checking that the impls the -programmer wrote are legal, what we referred to earlier as "the compiler doing -its job correctly". - -We already saw examples of illegal and legal impls: -```rust,ignore -trait Foo { } -trait Bar where Self: Foo { } - -struct X; -struct Y; - -impl Bar for X { - // This impl is not legal: the `Bar` trait requires that we also - // implement `Foo`, and we didn't. -} - -impl Foo for Y { - // This impl is legal: there is nothing to check as there are no where - // clauses on the `Foo` trait. -} - -impl Bar for Y { - // This impl is legal: we have a `Foo` impl for `Y`. -} -``` -We must define what "legal" and "illegal" mean. For this, we introduce another -predicate: `WellFormed(Type: Trait)`. We say that the trait reference -`Type: Trait` is well-formed if `Type` meets the bounds written on the -`Trait` declaration. For each impl we write, assuming that the where clauses -declared on the impl hold, the compiler tries to prove that the corresponding -trait reference is well-formed. The impl is legal if the compiler manages to do -so. - -Coming to the definition of `WellFormed(Type: Trait)`, it would be tempting -to define it as: -```rust,ignore -trait Trait where WC1, WC2, ..., WCn { - ... -} -``` - -```text -forall { - WellFormed(Type: Trait) :- WC1 && WC2 && .. && WCn. -} -``` -and indeed this was basically what was done in rustc until it was noticed that -this mixed badly with implied bounds. The key thing is that implied bounds -allows someone to derive all bounds implied by a fact in the environment, and -this *transitively* as we've seen with the `A + B + C` traits example. -However, the `WellFormed` predicate as defined above only checks that the -*direct* superbounds hold. That is, if we come back to our `A + B + C` -example: -```rust,ignore -trait A { } -// No where clauses, always well-formed. -// forall { WellFormed(Type: A). } - -trait B where Self: A { } -// We only check the direct superbound `Self: A`. -// forall { WellFormed(Type: B) :- Implemented(Type: A). } - -trait C where Self: B { } -// We only check the direct superbound `Self: B`. We do not check -// the `Self: A` implied bound coming from the `Self: B` superbound. -// forall { WellFormed(Type: C) :- Implemented(Type: B). } -``` -There is an asymmetry between the recursive power of implied bounds and -the shallow checking of `WellFormed`. It turns out that this asymmetry -can be [exploited][bug]. Indeed, suppose that we define the following -traits: -```rust,ignore -trait Partial where Self: Copy { } -// WellFormed(Self: Partial) :- Implemented(Self: Copy). - -trait Complete where Self: Partial { } -// WellFormed(Self: Complete) :- Implemented(Self: Partial). - -impl Partial for T where T: Complete { } - -impl Complete for T { } -``` - -For the `Partial` impl, what the compiler must prove is: -```text -forall { - if (T: Complete) { // assume that the where clauses hold - WellFormed(T: Partial) // show that the trait reference is well-formed - } -} -``` -Proving `WellFormed(T: Partial)` amounts to proving `Implemented(T: Copy)`. -However, we have `Implemented(T: Complete)` in our environment: thanks to -implied bounds, we can deduce `Implemented(T: Partial)`. Using implied bounds -one level deeper, we can deduce `Implemented(T: Copy)`. Finally, the `Partial` -impl is legal. - -For the `Complete` impl, what the compiler must prove is: -```text -forall { - WellFormed(T: Complete) // show that the trait reference is well-formed -} -``` -Proving `WellFormed(T: Complete)` amounts to proving `Implemented(T: Partial)`. -We see that the `impl Partial for T` applies if we can prove -`Implemented(T: Complete)`, and it turns out we can prove this fact since our -`impl Complete for T` is a blanket impl without any where clauses. - -So both impls are legal and the compiler accepts the program. Moreover, thanks -to the `Complete` blanket impl, all types implement `Complete`. So we could -now use this impl like so: -```rust,ignore -fn eat(x: T) { } - -fn copy_everything(x: T) { - eat(x); - eat(x); -} - -fn main() { - let not_copiable = vec![1, 2, 3, 4]; - copy_everything(not_copiable); -} -``` -In this program, we use the fact that `Vec` implements `Complete`, as any -other type. Hence we can call `copy_everything` with an argument of type -`Vec`. Inside the `copy_everything` function, we have the -`Implemented(T: Complete)` bound in our environment. Thanks to implied bounds, -we can deduce `Implemented(T: Partial)`. Using implied bounds again, we deduce -`Implemented(T: Copy)` and we can indeed call the `eat` function which moves -the argument twice since its argument is `Copy`. Problem: the `T` type was -in fact `Vec` which is not copy at all, hence we will double-free the -underlying vec storage so we have a memory unsoundness in safe Rust. - -Of course, disregarding the asymmetry between `WellFormed` and implied bounds, -this bug was possible only because we had some kind of self-referencing impls. -But self-referencing impls are very useful in practice and are not the real -culprits in this affair. - -[bug]: https://github.com/rust-lang/rust/pull/43786 - -## Co-inductiveness of `WellFormed` - -So the solution is to fix this asymmetry between `WellFormed` and implied -bounds. For that, we need for the `WellFormed` predicate to not only require -that the direct superbounds hold, but also all the bounds transitively implied -by the superbounds. What we can do is to have the following rules for the -`WellFormed` predicate: -```rust,ignore -trait A { } -// WellFormed(Self: A) :- Implemented(Self: A). - -trait B where Self: A { } -// WellFormed(Self: B) :- Implemented(Self: B) && WellFormed(Self: A). - -trait C where Self: B { } -// WellFormed(Self: C) :- Implemented(Self: C) && WellFormed(Self: B). -``` - -Notice that we are now also requiring `Implemented(Self: Trait)` for -`WellFormed(Self: Trait)` to be true: this is to simplify the process of -traversing all the implied bounds transitively. This does not change anything -when checking whether impls are legal, because since we assume -that the where clauses hold inside the impl, we know that the corresponding -trait reference do hold. Thanks to this setup, you can see that we indeed -require to prove the set of all bounds transitively implied by the where -clauses. - -However there is still a catch. Suppose that we have the following trait -definition: -```rust,ignore -trait Foo where ::Item: Foo { - type Item; -} -``` - -so this definition is a bit more involved than the ones we've seen already -because it defines an associated item. However, the well-formedness rule -would not be more complicated: -```text -WellFormed(Self: Foo) :- - Implemented(Self: Foo) && - WellFormed(::Item: Foo). -``` - -Now we would like to write the following impl: -```rust,ignore -impl Foo for i32 { - type Item = i32; -} -``` -The `Foo` trait definition and the `impl Foo for i32` are perfectly valid -Rust: we're kind of recursively using our `Foo` impl in order to show that -the associated value indeed implements `Foo`, but that's ok. But if we -translate this to our well-formedness setting, the compiler proof process -inside the `Foo` impl is the following: it starts with proving that the -well-formedness goal `WellFormed(i32: Foo)` is true. In order to do that, -it must prove the following goals: `Implemented(i32: Foo)` and -`WellFormed(::Item: Foo)`. `Implemented(i32: Foo)` holds because -there is our impl and there are no where clauses on it so it's always true. -However, because of the associated type value we used, -`WellFormed(::Item: Foo)` simplifies to just -`WellFormed(i32: Foo)`. So in order to prove its original goal -`WellFormed(i32: Foo)`, the compiler needs to prove `WellFormed(i32: Foo)`: -this clearly is a cycle and cycles are usually rejected by the trait solver, -unless... if the `WellFormed` predicate was made to be co-inductive. - -A co-inductive predicate, as discussed in the chapter on -[goals and clauses](./goals-and-clauses.md#coinductive-goals), are predicates -for which the -trait solver accepts cycles. In our setting, this would be a valid thing to do: -indeed, the `WellFormed` predicate just serves as a way of enumerating all -the implied bounds. Hence, it's like a fixed point algorithm: it tries to grow -the set of implied bounds until there is nothing more to add. Here, a cycle -in the chain of `WellFormed` predicates just means that there is no more bounds -to add in that direction, so we can just accept this cycle and focus on other -directions. It's easy to prove that under these co-inductive semantics, we -are effectively visiting all the transitive implied bounds, and only these. - -## Implied bounds on types - -We mainly talked about implied bounds for traits because this was the most -subtle regarding implementation. Implied bounds on types are simpler, -especially because if we assume that a type is well-formed, we don't use that -fact to deduce that other types are well-formed, we only use it to deduce -that e.g. some trait bounds hold. - -For types, we just use rules like these ones: -```rust,ignore -struct Type<...> where WC1, ..., WCn { - ... -} -``` - -```text -forall<...> { - WellFormed(Type<...>) :- WC1, ..., WCn. -} - -forall<...> { - FromEnv(WC1) :- FromEnv(Type<...>). - ... - FromEnv(WCn) :- FromEnv(Type<...>). -} -``` -We can see that we have this asymmetry between well-formedness check, -which only verifies that the direct superbounds hold, and implied bounds which -gives access to all bounds transitively implied by the where clauses. In that -case this is ok because as we said, we don't use `FromEnv(Type<...>)` to deduce -other `FromEnv(OtherType<...>)` things, nor do we use `FromEnv(Type: Trait)` to -deduce `FromEnv(OtherType<...>)` things. So in that sense type definitions are -"less recursive" than traits, and we saw in a previous subsection that -it was the combination of asymmetry and recursive trait / impls that led to -unsoundness. As such, the `WellFormed(Type<...>)` predicate does not need -to be co-inductive. - -This asymmetry optimization is useful because in a real Rust program, we have -to check the well-formedness of types very often (e.g. for each type which -appears in the body of a function). diff --git a/src/traits/index.md b/src/traits/index.md deleted file mode 100644 index 5544ce513..000000000 --- a/src/traits/index.md +++ /dev/null @@ -1,64 +0,0 @@ -# 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]! - -[wg]: https://github.com/rust-lang/rust/issues/48416 - -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. - - The [goals and clauses](./goals-and-clauses.html) chapter - 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. - -> 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: - -**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/chalk -[chalk_engine]: https://github.com/rust-lang/chalk/tree/master/chalk-engine -[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits diff --git a/src/traits/lowering-rules.md b/src/traits/lowering-rules.md deleted file mode 100644 index c780e7cf5..000000000 --- a/src/traits/lowering-rules.md +++ /dev/null @@ -1,416 +0,0 @@ -# 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]: ./goals-and-clauses.html -[dg]: ./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 parameter like `A`. - -The nonterminal `Ai` is used to mean some generic *argument*, which -might be a lifetime like `'a` or a type like `Vec`. - -When defining the lowering rules, we will give goals and clauses in -the [notation given in this section](./goals-and-clauses.html). -We sometimes insert "macros" like `LowerWhereClause!` into these -definitions; these macros reference other sections within this chapter. - -## Rule names and cross-references - -Each of these lowering rules is given a name, documented with a -comment like so: - - // Rule Foo-Bar-Baz - -The reference implementation of these rules is to be found in -[`chalk/chalk-solve/src/clauses.rs`][chalk_rules]. They are also ported in -rustc in the [`librustc_traits`][librustc_traits] crate. - -[chalk_rules]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses.rs -[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits - -## Lowering where clauses - -When used in a goal position, where clauses can be mapped directly to -the `Holds` variant of [domain goals][dg], as follows: - -- `A0: Foo` maps to `Implemented(A0: Foo)` -- `T: 'r` maps to `Outlives(T, 'r)` -- `'a: 'b` maps to `Outlives('a, 'b)` -- `A0: Foo` is a bit special and expands to two distinct - goals, namely `Implemented(A0: Foo)` and - `ProjectionEq(>::Item = T)` - -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)` - - other where-clauses are left intact -- `WellFormed(WC)` – this indicates that: - - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)` - - other where-clauses are left intact - -*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,ignore -trait Trait // 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: - -```text -// Rule Implemented-From-Env -forall { - Implemented(Self: Trait) :- FromEnv(Self: Trait) -} -``` - - - -#### Implied bounds - -The next few clauses have to do with implied bounds (see also -[RFC 2089] and the [implied bounds][implied_bounds] chapter for a more in depth -cover). For each trait, we produce two clauses: - -[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html -[implied_bounds]: ./implied-bounds.md - -```text -// Rule Implied-Bound-From-Trait -// -// For each where clause WC: -forall { - FromEnv(WC) :- FromEnv(Self: Trait) -} -``` - -This clause says that if we are assuming that the trait holds, then we can also -assume that its where-clauses hold. It's perhaps useful to see an example: - -```rust,ignore -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**: - -```text -// Rule WellFormed-TraitRef -forall { - WellFormed(Self: Trait) :- Implemented(Self: Trait) && 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](./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,ignore -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. - -## Lowering type definitions - -We also want to have some rules which define when a type is well-formed. -For example, given this type: - -```rust,ignore -struct Set where K: Hash { ... } -``` - -then `Set` is well-formed because `i32` implements `Hash`, but -`Set` would not be well-formed. Basically, a type is well-formed -if its parameters verify the where clauses written on the type definition. - -Hence, for every type definition: - -```rust, ignore -struct Type where WC { ... } -``` - -we produce the following rule: - -```text -// Rule WellFormed-Type -forall { - WellFormed(Type) :- WC -} -``` - -Note that we use `struct` for defining a type, but this should be understood -as a general type definition (it could be e.g. a generic `enum`). - -Conversely, we define rules which say that if we assume that a type is -well-formed, we can also assume that its where clauses hold. That is, -we produce the following family of rules: - -```text -// Rule Implied-Bound-From-Type -// -// For each where clause `WC` -forall { - FromEnv(WC) :- FromEnv(Type) -} -``` - -As for the implied bounds RFC, functions will *assume* that their arguments -are well-formed. For example, suppose we have the following bit of code: - -```rust,ignore -trait Hash: Eq { } -struct Set { ... } - -fn foo(collection: Set, x: K, y: K) { - // `x` and `y` can be equalized even if we did not explicitly write - // `where K: Eq` - if x == y { - ... - } -} -``` - -In the `foo` function, we assume that `Set` is well-formed, i.e. we have -`FromEnv(Set)` in our environment. Because of the previous rule, we get - `FromEnv(K: Hash)` without needing an explicit where clause. And because -of the `Hash` trait definition, there also exists a rule which says: - -```text -forall { - FromEnv(K: Eq) :- FromEnv(K: Hash) -} -``` - -which means that we finally get `FromEnv(K: Eq)` and then can compare `x` -and `y` without needing an explicit where clause. - - - -## Lowering trait items - -### Associated type declarations - -Given a trait that declares a (possibly generic) associated type: - -```rust,ignore -trait Trait // P0 == Self -where WC -{ - type AssocType: 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](./associated-types.html), -but reproduced here for reference: - -```text -// Rule ProjectionEq-Normalize -// -// ProjectionEq can succeed by normalizing: -forall { - ProjectionEq(>::AssocType = U) :- - Normalize(>::AssocType -> U) -} -``` - -```text -// Rule ProjectionEq-Placeholder -// -// ProjectionEq can succeed through the placeholder associated type, -// see "associated type" chapter for more: -forall { - ProjectionEq( - >::AssocType = - (Trait::AssocType) - ) -} -``` - -The next rule covers implied bounds for the projection. In particular, -the `Bounds` declared on the associated type must have been proven to hold -to show that the impl is well-formed, and hence we can rely on them -elsewhere. - -```text -// Rule Implied-Bound-From-AssocTy -// -// For each `Bound` in `Bounds`: -forall { - FromEnv(>::AssocType>: Bound) :- - FromEnv(Self: Trait) && WC1 -} -``` - -Next, we define the requirements for an instantiation of our associated -type to be well-formed... - -```text -// Rule WellFormed-AssocTy -forall { - WellFormed((Trait::AssocType)) :- - Implemented(Self: Trait) && WC1 -} -``` - -...along with the reverse implications, when we can assume that it is -well-formed. - -```text -// Rule Implied-WC-From-AssocTy -// -// For each where clause WC1: -forall { - FromEnv(WC1) :- FromEnv((Trait::AssocType)) -} -``` - -```text -// Rule Implied-Trait-From-AssocTy -forall { - FromEnv(Self: Trait) :- - FromEnv((Trait::AssocType)) -} -``` - -### 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,ignore -impl Trait for A0 -where WC -{ - // zero or more impl items -} -``` - -Let `TraitRef` be the trait reference `A0: Trait`. Then we -will create the following rules: - -```text -// Rule Implemented-From-Impl -forall { - 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,ignore -impl Trait for P0 -where WC_impl -{ - type AssocType = T; -} -``` - -and our where clause `WC1` on the trait associated type from above, we -produce the following rule: - -```text -// Rule Normalize-From-Impl -forall { - forall { - Normalize(>::AssocType -> T) :- - Implemented(P0 as Trait) && WC1 - } -} -``` - -Note that `WC_impl` and `WC1` both encode where-clauses that the impl can -rely on. (`WC_impl` is not used here, because it is implied by -`Implemented(P0 as Trait)`.) - - - -### 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. diff --git a/src/traits/lowering-to-logic.md b/src/traits/lowering-to-logic.md deleted file mode 100644 index e1a6c1361..000000000 --- a/src/traits/lowering-to-logic.md +++ /dev/null @@ -1,185 +0,0 @@ -# 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 Clone for Vec 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) :- 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` if clone is implemented for `?T`". So -e.g. if we wanted to prove that `Clone(Vec>)`, we would do -so by applying the rules recursively: - -- `Clone(Vec>)` is provable if: - - `Clone(Vec)` 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)`. This would -fail (after all, I didn't give an impl of `Clone` for `Bar`): - -- `Clone(Vec)` 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` trait, which declares -that `Self` is equatable with a value of type `T`: - -```rust,ignore -trait Eq { ... } -impl Eq for usize { } -impl> Eq> for Vec { } -``` - -That could be mapped as follows: - -```text -Eq(usize, usize). -Eq(Vec, Vec) :- 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::() } -fn bar>() { } -``` - -This function is very simple, of course: all it does is to call -`bar::()`. Now, looking at the definition of `bar()`, we can see -that it has one where-clause `U: Eq`. So, that means that `foo()` will -have to prove that `usize: Eq` 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::` (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>() { bar::() } -fn bar>() { } -``` - -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 { - // ...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/ diff --git a/src/traits/resolution.md b/src/traits/resolution.md index 2ba451677..7f73bfe4f 100644 --- a/src/traits/resolution.md +++ b/src/traits/resolution.md @@ -6,7 +6,7 @@ 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](./index.html). +see [*this* subchapter](./chalk.html). ## Major concepts diff --git a/src/traits/slg.md b/src/traits/slg.md deleted file mode 100644 index 74ec89fa0..000000000 --- a/src/traits/slg.md +++ /dev/null @@ -1,302 +0,0 @@ -# The On-Demand SLG solver - -Given a set of program clauses (provided by our [lowering rules][lowering]) -and a query, we need to return the result of the query and the value of any -type variables we can determine. This is the job of the solver. - -For example, `exists { Vec: FromIterator }` has one solution, so -its result is `Unique; substitution [?T := u32]`. A solution also comes with -a set of region constraints, which we'll ignore in this introduction. - -[lowering]: ./lowering-rules.html - -## Goals of the Solver - -### On demand - -There are often many, or even infinitely many, solutions to a query. For -example, say we want to prove that `exists { Vec: Debug }` for _some_ -type `?T`. Our solver should be capable of yielding one answer at a time, say -`?T = u32`, then `?T = i32`, and so on, rather than iterating over every type -in the type system. If we need more answers, we can request more until we are -done. This is similar to how Prolog works. - -*See also: [The traditional, interactive Prolog query][pq]* - -[pq]: ./canonical-queries.html#the-traditional-interactive-prolog-query - -### Breadth-first - -`Vec: Debug` is true if `?T: Debug`. This leads to a cycle: `[Vec, -Vec>, Vec>>]`, and so on all implement `Debug`. Our -solver ought to be breadth first and consider answers like `[Vec: Debug, -Vec: Debug, ...]` before it recurses, or we may never find the answer -we're looking for. - -### Cachable - -To speed up compilation, we need to cache results, including partial results -left over from past solver queries. - -## Description of how it works - -The basis of the solver is the [`Forest`] type. A *forest* stores a -collection of *tables* as well as a *stack*. Each *table* represents -the stored results of a particular query that is being performed, as -well as the various *strands*, which are basically suspended -computations that may be used to find more answers. Tables are -interdependent: solving one query may require solving others. - -[`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html - -### Walkthrough - -Perhaps the easiest way to explain how the solver works is to walk -through an example. Let's imagine that we have the following program: - -```rust,ignore -trait Debug { } - -struct u32 { } -impl Debug for u32 { } - -struct Rc { } -impl Debug for Rc { } - -struct Vec { } -impl Debug for Vec { } -``` - -Now imagine that we want to find answers for the query `exists { Rc: -Debug }`. The first step would be to u-canonicalize this query; this is the -act of giving canonical names to all the unbound inference variables based on -the order of their left-most appearance, as well as canonicalizing the -universes of any universally bound names (e.g., the `T` in `forall { ... -}`). In this case, there are no universally bound names, but the canonical -form Q of the query might look something like: - -```text -Rc: Debug -``` - -where `?0` is a variable in the root universe U0. We would then go and -look for a table with this canonical query as the key: since the forest is -empty, this lookup will fail, and we will create a new table T0, -corresponding to the u-canonical goal Q. - -**Ignoring negative reasoning and regions.** To start, we'll ignore -the possibility of negative goals like `not { Foo }`. We'll phase them -in later, as they bring several complications. - -**Creating a table.** When we first create a table, we also initialize -it with a set of *initial strands*. A "strand" is kind of like a -"thread" for the solver: it contains a particular way to produce an -answer. The initial set of strands for a goal like `Rc: Debug` -(i.e., a "domain goal") is determined by looking for *clauses* in the -environment. In Rust, these clauses derive from impls, but also from -where-clauses that are in scope. In the case of our example, there -would be three clauses, each coming from the program. Using a -Prolog-like notation, these look like: - -```text -(u32: Debug). -(Rc: Debug) :- (T: Debug). -(Vec: Debug) :- (T: Debug). -``` - -To create our initial strands, then, we will try to apply each of -these clauses to our goal of `Rc: Debug`. The first and third -clauses are inapplicable because `u32` and `Vec` cannot be unified -with `Rc`. The second clause, however, will work. - -**What is a strand?** Let's talk a bit more about what a strand *is*. In the code, a strand -is the combination of an inference table, an _X-clause_, and (possibly) -a selected subgoal from that X-clause. But what is an X-clause -([`ExClause`], in the code)? An X-clause pulls together a few things: - -- The current state of the goal we are trying to prove; -- A set of subgoals that have yet to be proven; -- There are also a few things we're ignoring for now: - - delayed literals, region constraints - -The general form of an X-clause is written much like a Prolog clause, -but with somewhat different semantics. Since we're ignoring delayed -literals and region constraints, an X-clause just looks like this: - -```text -G :- L -``` - -where G is a goal and L is a set of subgoals that must be proven. -(The L stands for *literal* -- when we address negative reasoning, a -literal will be either a positive or negative subgoal.) The idea is -that if we are able to prove L then the goal G can be considered true. - -In the case of our example, we would wind up creating one strand, with -an X-clause like so: - -```text -(Rc: Debug) :- (?T: Debug) -``` - -Here, the `?T` refers to one of the inference variables created in the -inference table that accompanies the strand. (I'll use named variables -to refer to inference variables, and numbered variables like `?0` to -refer to variables in a canonicalized goal; in the code, however, they -are both represented with an index.) - -For each strand, we also optionally store a *selected subgoal*. This -is the subgoal after the turnstile (`:-`) that we are currently trying -to prove in this strand. Initially, when a strand is first created, -there is no selected subgoal. - -[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html - -**Activating a strand.** Now that we have created the table T0 and -initialized it with strands, we have to actually try and produce an answer. -We do this by invoking the [`ensure_root_answer`] operation on the table: -specifically, we say `ensure_root_answer(T0, A0)`, meaning "ensure that there -is a 0th answer A0 to query T0". - -Remember that tables store not only strands, but also a vector of cached -answers. The first thing that [`ensure_root_answer`] does is to check whether -answer A0 is in this vector. If so, we can just return immediately. In this -case, the vector will be empty, and hence that does not apply (this becomes -important for cyclic checks later on). - -When there is no cached answer, [`ensure_root_answer`] will try to produce one. -It does this by selecting a strand from the set of active strands -- the -strands are stored in a `VecDeque` and hence processed in a round-robin -fashion. Right now, we have only one strand, storing the following X-clause -with no selected subgoal: - -```text -(Rc: Debug) :- (?T: Debug) -``` - -When we activate the strand, we see that we have no selected subgoal, -and so we first pick one of the subgoals to process. Here, there is only -one (`?T: Debug`), so that becomes the selected subgoal, changing -the state of the strand to: - -```text -(Rc: Debug) :- selected(?T: Debug, A0) -``` - -Here, we write `selected(L, An)` to indicate that (a) the literal `L` -is the selected subgoal and (b) which answer `An` we are looking for. We -start out looking for `A0`. - -[`ensure_root_answer`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer - -**Processing the selected subgoal.** Next, we have to try and find an -answer to this selected goal. To do that, we will u-canonicalize it -and try to find an associated table. In this case, the u-canonical -form of the subgoal is `?0: Debug`: we don't have a table yet for -that, so we can create a new one, T1. As before, we'll initialize T1 -with strands. In this case, there will be three strands, because all -the program clauses are potentially applicable. Those three strands -will be: - -- `(u32: Debug) :-`, derived from the program clause `(u32: Debug).`. - - Note: This strand has no subgoals. -- `(Vec: Debug) :- (?U: Debug)`, derived from the `Vec` impl. -- `(Rc: Debug) :- (?U: Debug)`, derived from the `Rc` impl. - -We can thus summarize the state of the whole forest at this point as -follows: - -```text -Table T0 [Rc: Debug] - Strands: - (Rc: Debug) :- selected(?T: Debug, A0) - -Table T1 [?0: Debug] - Strands: - (u32: Debug) :- - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -**Delegation between tables.** Now that the active strand from T0 has -created the table T1, it can try to extract an answer. It does this -via that same `ensure_answer` operation we saw before. In this case, -the strand would invoke `ensure_answer(T1, A0)`, since we will start -with the first answer. This will cause T1 to activate its first -strand, `u32: Debug :-`. - -This strand is somewhat special: it has no subgoals at all. This means -that the goal is proven. We can therefore add `u32: Debug` to the set -of *answers* for our table, calling it answer A0 (it is the first -answer). The strand is then removed from the list of strands. - -The state of table T1 is therefore: - -```text -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -Note that I am writing out the answer A0 as a substitution that can be -applied to the table goal; actually, in the code, the goals for each -X-clause are also represented as substitutions, but in this exposition -I've chosen to write them as full goals, following [NFTD]. - -[NFTD]: ./bibliography.html#slg - -Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok` -to the table T0, indicating that answer A0 is available. T0 now has -the job of incorporating that result into its active strand. It does -this in two ways. First, it creates a new strand that is looking for -the next possible answer of T1. Next, it incorpoates the answer from -A0 and removes the subgoal. The resulting state of table T0 is: - -```text -Table T0 [Rc: Debug] - Strands: - (Rc: Debug) :- selected(?T: Debug, A1) - (Rc: Debug) :- -``` - -We then immediately activate the strand that incorporated the answer -(the `Rc: Debug` one). In this case, that strand has no further -subgoals, so it becomes an answer to the table T0. This answer can -then be returned up to our caller, and the whole forest goes quiescent -at this point (remember, we only do enough work to generate *one* -answer). The ending state of the forest at this point will be: - -```text -Table T0 [Rc: Debug] - Answer: - A0 = [?0 = u32] - Strands: - (Rc: Debug) :- selected(?T: Debug, A1) - -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -Here you can see how the forest captures both the answers we have -created thus far *and* the strands that will let us try to produce -more answers later on. - -## See also - -- [chalk_solve README][readme], which contains links to papers used and - acronyms referenced in the code -- This section is a lightly adapted version of the blog post [An on-demand - SLG solver for chalk][slg-blog] -- [Negative Reasoning in Chalk][negative-reasoning-blog] explains the need - for negative reasoning, but not how the SLG solver does it - -[readme]: https://github.com/rust-lang/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md -[slg-blog]: http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/ -[negative-reasoning-blog]: https://aturon.github.io/blog/2017/04/24/negative-chalk/ diff --git a/src/traits/wf.md b/src/traits/wf.md deleted file mode 100644 index aa17f8c2c..000000000 --- a/src/traits/wf.md +++ /dev/null @@ -1,469 +0,0 @@ -# Well-formedness checking - -WF checking 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. - -For each declaration in a Rust program, we will generate a logical goal and try -to prove it using the lowered rules we described in the -[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we -say that the construct is well-formed. If not, we report an error to the user. - -Well-formedness checking happens in the [`chalk/chalk-solve/src/wf.rs`][wf] -module in chalk. After you have read this chapter, you may find useful to see -an extended set of examples in the [`chalk/tests/test/wf_lowering.rs`][wf_test] submodule. - -The new-style WF checking has not been implemented in rustc yet. - -[wf]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/wf.rs -[wf_test]: https://github.com/rust-lang/chalk/blob/master/tests/test/wf_lowering.rs - -We give here a complete reference of the generated goals for each Rust -declaration. - -In addition to the notations introduced in the chapter about -lowering rules, we'll introduce another notation: when checking WF of a -declaration, we'll often have to prove that all types that appear are -well-formed, except type parameters that we always assume to be WF. Hence, -we'll use the following notation: for a type `SomeType<...>`, we define -`InputTypes(SomeType<...>)` to be the set of all non-parameter types appearing -in `SomeType<...>`, including `SomeType<...>` itself. - -Examples: -* `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]` -* `InputTypes(Box) = [Box]` (assuming that `T` is a type parameter) -* `InputTypes(Box>) = [Box, Box>]` - -We also extend the `InputTypes` notation to where clauses in the natural way. -So, for example `InputTypes(A0: Trait)` is the union of -`InputTypes(A0)`, `InputTypes(A1)`, ..., `InputTypes(An)`. - -# Type definitions - -Given a general type definition: -```rust,ignore -struct Type where WC_type { - field1: A1, - ... - fieldn: An, -} -``` - -we generate the following goal, which represents its well-formedness condition: -```text -forall { - if (FromEnv(WC_type)) { - WellFormed(InputTypes(WC_type)) && - WellFormed(InputTypes(A1)) && - ... - WellFormed(InputTypes(An)) - } -} -``` - -which in English states: assuming that the where clauses defined on the type -hold, prove that every type appearing in the type definition is well-formed. - -Some examples: -```rust,ignore -struct OnlyClone where T: Clone { - clonable: T, -} -// The only types appearing are type parameters: we have nothing to check, -// the type definition is well-formed. -``` - -```rust,ignore -struct Foo where T: Clone { - foo: OnlyClone, -} -// The only non-parameter type which appears in this definition is -// `OnlyClone`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(T: Clone)) { -// WellFormed(OnlyClone) -// } -// } -// ``` -// which is provable. -``` - -```rust,ignore -struct Bar where ::Item: Debug { - bar: i32, -} -// The only non-parameter types which appear in this definition are -// `::Item` and `i32`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(::Item: Debug)) { -// WellFormed(::Item) && -// WellFormed(i32) -// } -// } -// ``` -// which is not provable since `WellFormed(::Item)` requires -// proving `Implemented(T: Iterator)`, and we are unable to prove that for an -// unknown `T`. -// -// Hence, this type definition is considered illegal. An additional -// `where T: Iterator` would make it legal. -``` - -# Trait definitions - -Given a general trait definition: -```rust,ignore -trait Trait where WC_trait { - type Assoc: Bounds_assoc where WC_assoc; -} -``` - -we generate the following goal: -```text -forall { - if (FromEnv(WC_trait)) { - WellFormed(InputTypes(WC_trait)) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(InputTypes(Bounds_assoc)) && - WellFormed(InputTypes(WC_assoc)) - } - } - } -} -``` - -There is not much to verify in a trait definition. We just want -to prove that the types appearing in the trait definition are well-formed, -under the assumption that the different where clauses hold. - -Some examples: -```rust,ignore -trait Foo where T: Iterator, ::Item: Debug { - ... -} -// The only non-parameter type which appears in this definition is -// `::Item`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(T: Iterator), FromEnv(::Item: Debug)) { -// WellFormed(::Item) -// } -// } -// ``` -// which is provable thanks to the `FromEnv(T: Iterator)` assumption. -``` - -```rust,ignore -trait Bar { - type Assoc: From<::Item>; -} -// The only non-parameter type which appears in this definition is -// `::Item`. The generated goal is the following: -// ``` -// forall { -// WellFormed(::Item) -// } -// ``` -// which is not provable, hence the trait definition is considered illegal. -``` - -```rust,ignore -trait Baz { - type Assoc: From<::Item> where T: Iterator; -} -// The generated goal is now: -// ``` -// forall { -// if (FromEnv(T: Iterator)) { -// WellFormed(::Item) -// } -// } -// ``` -// which is now provable. -``` - -# Impls - -Now we give ourselves a general impl for the trait defined above: -```rust,ignore -impl Trait for SomeType where WC_impl { - type Assoc = SomeValue where WC_assoc; -} -``` - -Note that here, `WC_assoc` are the same where clauses as those defined on the -associated type definition in the trait declaration, *except* that type -parameters from the trait are substituted with values provided by the impl -(see example below). You cannot add new where clauses. You may omit to write -the where clauses if you want to emphasize the fact that you are actually not -relying on them. - -Some examples to illustrate that: -```rust,ignore -trait Foo { - type Assoc where T: Clone; -} - -struct OnlyClone { ... } - -impl Foo> for () { - // We substitute type parameters from the trait by the ones provided - // by the impl, that is instead of having a `T: Clone` where clause, - // we have an `Option: Clone` one. - type Assoc = OnlyClone> where Option: Clone; -} - -impl Foo for i32 { - // I'm not using the `T: Clone` where clause from the trait, so I can - // omit it. - type Assoc = u32; -} - -impl Foo for f32 { - type Assoc = OnlyClone> where Option: Clone; - // ^^^^^^^^^^^^^^^^^^^^^^ - // this where clause does not exist - // on the original trait decl: illegal -} -``` - -> So in Rust, where clauses on associated types work *exactly* like where -> clauses on trait methods: in an impl, we must substitute the parameters from -> the traits with values provided by the impl, we may omit them if we don't -> need them, but we cannot add new where clauses. - -Now let's see the generated goal for this general impl: -```text -forall { - // Well-formedness of types appearing in the impl - if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType: Trait))) { - WellFormed(InputTypes(WC_impl)) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(InputTypes(SomeValue)) - } - } - } - - // Implied bounds checking - if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType: Trait))) { - WellFormed(SomeType: Trait) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(SomeValue: Bounds_assoc) - } - } - } -} -``` - -Here is the most complex goal. As always, first, assuming that -the various where clauses hold, we prove that every type appearing in the impl -is well-formed, ***except*** types appearing in the impl header -`SomeType: Trait`. Instead, we *assume* that those types are -well-formed -(hence the `if (FromEnv(InputTypes(SomeType: Trait)))` -conditions). This is -part of the implied bounds proposal, so that we can rely on the bounds -written on the definition of e.g. the `SomeType` type (and that we don't -need to repeat those bounds). -> Note that we don't need to check well-formedness of types appearing in -> `WC_assoc` because we already did that in the trait decl (they are just -> repeated with some substitutions of values which we already assume to be -> well-formed) - -Next, still assuming that the where clauses on the impl `WC_impl` hold and that -the input types of `SomeType` are well-formed, we prove that -`WellFormed(SomeType: Trait)` hold. That is, we want to prove -that `SomeType` verify all the where clauses that might transitively -be required by the `Trait` definition (see -[this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)). - -Lastly, assuming in addition that the where clauses on the associated type -`WC_assoc` hold, -we prove that `WellFormed(SomeValue: Bounds_assoc)` hold. Again, we are -not only proving `Implemented(SomeValue: Bounds_assoc)`, but also -all the facts that might transitively come from `Bounds_assoc`. We must do this -because we allow the use of implied bounds on associated types: if we have -`FromEnv(SomeType: Trait)` in our environment, the lowering rules -chapter indicates that we are able to deduce -`FromEnv(::Assoc: Bounds_assoc)` without knowing what the -precise value of `::Assoc` is. - -Some examples for the generated goal: -```rust,ignore -// Trait Program Clauses - -// These are program clauses that come from the trait definitions below -// and that the trait solver can use for its reasonings. I'm just restating -// them here so that we have them in mind. - -trait Copy { } -// This is a program clause that comes from the trait definition above -// and that the trait solver can use for its reasonings. I'm just restating -// it here (and also the few other ones coming just after) so that we have -// them in mind. -// `WellFormed(Self: Copy) :- Implemented(Self: Copy).` - -trait Partial where Self: Copy { } -// ``` -// WellFormed(Self: Partial) :- -// Implemented(Self: Partial) && -// WellFormed(Self: Copy). -// ``` - -trait Complete where Self: Partial { } -// ``` -// WellFormed(Self: Complete) :- -// Implemented(Self: Complete) && -// WellFormed(Self: Partial). -// ``` - -// Impl WF Goals - -impl Partial for T where T: Complete { } -// The generated goal is: -// ``` -// forall { -// if (FromEnv(T: Complete)) { -// WellFormed(T: Partial) -// } -// } -// ``` -// Then proving `WellFormed(T: Partial)` amounts to proving -// `Implemented(T: Partial)` and `Implemented(T: Copy)`. -// Both those facts can be deduced from the `FromEnv(T: Complete)` in our -// environment: this impl is legal. - -impl Complete for T { } -// The generated goal is: -// ``` -// forall { -// WellFormed(T: Complete) -// } -// ``` -// Then proving `WellFormed(T: Complete)` amounts to proving -// `Implemented(T: Complete)`, `Implemented(T: Partial)` and -// `Implemented(T: Copy)`. -// -// `Implemented(T: Complete)` can be proved thanks to the -// `impl Complete for T` blanket impl. -// -// `Implemented(T: Partial)` can be proved thanks to the -// `impl Partial for T where T: Complete` impl and because we know -// `T: Complete` holds. - -// However, `Implemented(T: Copy)` cannot be proved: the impl is illegal. -// An additional `where T: Copy` bound would be sufficient to make that impl -// legal. -``` - -```rust,ignore -trait Bar { } - -impl Bar for T where ::Item: Bar { } -// We have a non-parameter type appearing in the where clauses: -// `::Item`. The generated goal is: -// ``` -// forall { -// if (FromEnv(::Item: Bar)) { -// WellFormed(T: Bar) && -// WellFormed(::Item: Bar) -// } -// } -// ``` -// And `WellFormed(::Item: Bar)` is not provable: we'd need -// an additional `where T: Iterator` for example. -``` - -```rust,ignore -trait Foo { } - -trait Bar { - type Item: Foo; -} - -struct Stuff { } - -impl Bar for Stuff where T: Foo { - type Item = T; -} -// The generated goal is: -// ``` -// forall { -// if (FromEnv(T: Foo)) { -// WellFormed(T: Foo). -// } -// } -// ``` -// which is provable. -``` - -```rust,ignore -trait Debug { ... } -// `WellFormed(Self: Debug) :- Implemented(Self: Debug).` - -struct Box { ... } -impl Debug for Box where T: Debug { ... } - -trait PointerFamily { - type Pointer: Debug where T: Debug; -} -// `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).` - -struct BoxFamily; - -impl PointerFamily for BoxFamily { - type Pointer = Box where T: Debug; -} -// The generated goal is: -// ``` -// forall { -// WellFormed(BoxFamily: PointerFamily) && -// -// if (FromEnv(T: Debug)) { -// WellFormed(Box: Debug) && -// WellFormed(Box) -// } -// } -// ``` -// `WellFormed(BoxFamily: PointerFamily)` amounts to proving -// `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl. -// -// `WellFormed(Box)` is always true (there are no where clauses on the -// `Box` type definition). -// -// Moreover, we have an `impl Debug for Box`, hence -// we can prove `WellFormed(Box: Debug)` and the impl is indeed legal. -``` - -```rust,ignore -trait Foo { - type Assoc; -} - -struct OnlyClone { ... } - -impl Foo for i32 { - type Assoc = OnlyClone; -} -// The generated goal is: -// ``` -// forall { -// WellFormed(i32: Foo) && -// WellFormed(OnlyClone) -// } -// ``` -// however `WellFormed(OnlyClone)` is not provable because it requires -// `Implemented(T: Clone)`. It would be tempting to just add a `where T: Clone` -// bound inside the `impl Foo for i32` block, however we saw that it was -// illegal to add where clauses that didn't come from the trait definition. -``` From 38beffaf0cf30aa57523947760a12e19d8d906d2 Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Sun, 19 Apr 2020 23:06:05 +0800 Subject: [PATCH 2/5] Fix links and CI error. --- src/appendix/code-index.md | 6 +++--- src/appendix/glossary.md | 6 +++--- src/traits/chalk.md | 3 ++- src/traits/lowering-module.md | 4 ++-- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/appendix/code-index.md b/src/appendix/code-index.md index a4b18ecc0..327709c31 100644 --- a/src/appendix/code-index.md +++ b/src/appendix/code-index.md @@ -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`) | [Trait Solving: Goals and Clauses], [Trait Solving: 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`) | [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) `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,5 @@ Item | Kind | Short description | Chapter | [Macro expansion]: ../macro-expansion.html [Name resolution]: ../name-resolution.html [Parameter Environment]: ../param_env.html -[Trait Solving: Goals and Clauses]: ../traits/goals-and-clauses.html#domain-goals -[Trait Solving: Lowering impls]: ../traits/lowering-rules.html#lowering-impls +[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 diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index 5dc8f3801..ded31485b 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -49,7 +49,7 @@ memoization
| The process of storing the results o MIR
| The Mid-level IR that is created after type-checking for use by borrowck and codegen. ([see more](../mir/index.html)) miri
| An interpreter for MIR used for constant evaluation. ([see more](../miri.html)) monomorphization
| 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`, 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`, a copy for `Vec`, etc). -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). +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). 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
| 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
| 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
| Something that must be proven by the 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
| 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
| An optimization that avoids unnecessary monomorphisation. ([see more](../backend/monomorph.md#polymorphization)) -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). +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). promoted constants
| Constants extracted from a function and lifted to static scope; see [this section](../mir/index.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). @@ -74,7 +74,7 @@ tcx
| The "typing context", main data stru 'tcx
| The lifetime of the allocation arena. ([see more](../ty.html)) 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. -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)) +trait reference
| 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)) trans
| The code to translate MIR into LLVM IR. Renamed to codegen. ty
| The internal representation of a type. ([see more](../ty.html)) UFCS
| Short for Universal Function Call Syntax, this is an unambiguous syntax for calling a method. ([see more](../type-checking.html)) diff --git a/src/traits/chalk.md b/src/traits/chalk.md index dcb0a244f..dceb04354 100644 --- a/src/traits/chalk.md +++ b/src/traits/chalk.md @@ -37,7 +37,8 @@ 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 into logical inference rules in the [lowering module in rustc](./lowering-module.md). +[`librustc_traits`][librustc_traits]. 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 [librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits diff --git a/src/traits/lowering-module.md b/src/traits/lowering-module.md index 3c5bd7be5..0efc82c3e 100644 --- a/src/traits/lowering-module.md +++ b/src/traits/lowering-module.md @@ -1,8 +1,8 @@ # The lowering module in rustc The program clauses described in the -[lowering rules](./lowering-rules.html) section are actually -created in the [`rustc_traits::lowering`][lowering] module. +[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/ From 5afa182171be78f7b332c08c472862d4c63e1927 Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Mon, 20 Apr 2020 22:24:38 +0800 Subject: [PATCH 3/5] Address review comments. --- src/SUMMARY.md | 6 +- src/appendix/code-index.md | 5 +- src/appendix/glossary.md | 6 +- src/traits/canonical-queries.md | 252 +++++++++++++++++++++++++++++ src/traits/chalk.md | 23 ++- src/traits/goals-and-clauses.md | 270 ++++++++++++++++++++++++++++++++ src/traits/lowering-module.md | 55 ------- src/traits/lowering-to-logic.md | 185 ++++++++++++++++++++++ src/traits/regions.md | 9 -- 9 files changed, 726 insertions(+), 85 deletions(-) create mode 100644 src/traits/canonical-queries.md create mode 100644 src/traits/goals-and-clauses.md create mode 100644 src/traits/lowering-to-logic.md delete mode 100644 src/traits/regions.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 38634e26a..ee4d7e3f2 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -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) diff --git a/src/appendix/code-index.md b/src/appendix/code-index.md index 327709c31..76f4609cc 100644 --- a/src/appendix/code-index.md +++ b/src/appendix/code-index.md @@ -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`) | [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`) | [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 diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index ded31485b..a3b3826ea 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -49,7 +49,7 @@ memoization
| The process of storing the results o MIR
| The Mid-level IR that is created after type-checking for use by borrowck and codegen. ([see more](../mir/index.html)) miri
| An interpreter for MIR used for constant evaluation. ([see more](../miri.html)) monomorphization
| 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`, 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`, a copy for `Vec`, etc). -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
| 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
| 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
| 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
| 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
| Something that must be proven by the 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
| 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
| An optimization that avoids unnecessary monomorphisation. ([see more](../backend/monomorph.md#polymorphization)) -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
| 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/index.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). @@ -74,7 +74,7 @@ tcx
| The "typing context", main data stru 'tcx
| The lifetime of the allocation arena. ([see more](../ty.html)) 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. -trait reference
| 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
| The name of a trait along with a suitable set of input type/lifetimes. ([see more](../traits/goals-and-clauses.html#trait-ref)) trans
| The code to translate MIR into LLVM IR. Renamed to codegen. ty
| The internal representation of a type. ([see more](../ty.html)) UFCS
| Short for Universal Function Call Syntax, this is an unambiguous syntax for calling a method. ([see more](../type-checking.html)) diff --git a/src/traits/canonical-queries.md b/src/traits/canonical-queries.md new file mode 100644 index 000000000..e15bdaae2 --- /dev/null +++ b/src/traits/canonical-queries.md @@ -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: AsRef +``` + +The solver might answer: + +```text +Vec: 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: AsRef> + continue? (y/n) +``` + +This answer derives from the fact that there is a reflexive impl +(`impl AsRef 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: 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: Clone + Vec: Clone + continue? (y/n) + Vec>: Clone + continue? (y/n) + Vec>>: Clone + continue? (y/n) + Vec>>>: 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: Clone +``` + +might produce the answer: + +```text +Rc: Clone + continue? (y/n) +``` + +After all, `Rc` 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 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, 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: 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: Clone`, + say, or `Rc: 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: 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 Borrow for T where T: ?Sized +impl Borrow<[T]> for Vec where T: Sized +``` + +**Example 1.** Imagine we are type-checking this (rather artificial) +bit of code: + +```rust,ignore +fn foo(a: A, vec_b: Option) where A: Borrow { } + +fn main() { + let mut t: Vec<_> = vec![]; // Type: Vec + let mut u: Option<_> = None; // Type: Option + foo(t, u); // Example 1: requires `Vec: Borrow` + ... +} +``` + +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` and +`B = ?U`. Therefore, the where clause on `foo` requires that `Vec: +Borrow`. This is thus our first example trait query. + +There are many possible solutions to the query `Vec: Borrow`; +for example: + +- `?U = Vec`, +- `?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: Borrow`) 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: A, vec_b: Option) where A: Borrow { } + +fn main() { + // What we saw before: + let mut t: Vec<_> = vec![]; // Type: Vec + let mut u: Option<_> = None; // Type: Option + foo(t, u); // `Vec: Borrow` => ambiguous + + // New stuff: + u = Some(vec![]); // ?U = Vec +} +``` + +As a result of this assignment, the type of `u` is forced to be +`Option>`, where `?V` represents the element type of the +vector. This in turn implies that `?U` is [unified] to `Vec`. + +[unified]: ../type-checking.html + +Let's suppose that the type checker decides to revisit the +"as-yet-unproven" trait obligation we saw before, `Vec: +Borrow`. `?U` is no longer an unbound inference variable; it now +has a value, `Vec`. So, if we "refresh" the query with that value, we get: + +```text +Vec: Borrow> +``` + +This time, there is only one impl that applies, the reflexive impl: + +```text +impl Borrow 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.) + + diff --git a/src/traits/chalk.md b/src/traits/chalk.md index dceb04354..70af2a1f5 100644 --- a/src/traits/chalk.md +++ b/src/traits/chalk.md @@ -1,14 +1,12 @@ -# Chalk-based 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 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-based trait solving + +[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 diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md new file mode 100644 index 000000000..ecd2ce145 --- /dev/null +++ b/src/traits/goals-and-clauses.md @@ -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 { Goal } // existential quantification + | forall { 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 { Clause } + +K = // a "kind" + | +``` + +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 + + + +## 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 { 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. + + + +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 +``` + +So, for example, `u32: Display` is a trait reference, as is `Vec: +IntoIterator`. Note that Rust surface syntax also permits some extra +things, like associated type bindings (`Vec: IntoIterator`), that are not part of a trait reference. + + + +A **projection** consists of an associated item reference along with +its inputs P0..Pm: + +```text +Projection = >::AssocItem +``` + +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::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::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(::Item -> U)` +also requires proving `Implemented(T: Trait)`. + +[n]: ./associated-types.html#normalize +[at]: ./associated-types.html + +#### FromEnv(TraitRef) +e.g. `FromEnv(Self: Add)` + +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(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)` + +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 where K: Hash { ... } + +fn loud_insert(set: &mut HashSet, item: K) { + println!("inserting!"); + set.insert(item); +} +``` + +`HashSet` is an input type of the `loud_insert` function. Hence, we assume it +to be well-formed, so we would have `FromEnv(HashSet)` inside the body of our +function. As we'll see in the section on lowering, `FromEnv(HashSet)` 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)`, which is true in Rust, or + `WellFormed(Vec)`, which is not (because `str` is not `Sized`.) + +* *TraitRefs*, like `WellFormed(Vec: 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)` in the `loud_insert` +example because we will verify `WellFormed(HashSet)` 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. + + + +## 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> +} +``` + +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>: Send). +``` + +As you can probably imagine, proving that `Option>: 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>`, which implies it can reach values of type +`Box`, 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 diff --git a/src/traits/lowering-module.md b/src/traits/lowering-module.md index 0efc82c3e..1efdcafb7 100644 --- a/src/traits/lowering-module.md +++ b/src/traits/lowering-module.md @@ -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 Foo for T where T: Iterator { } - -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 { Implemented(T: Foo) :- ProjectionEq(::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 diff --git a/src/traits/lowering-to-logic.md b/src/traits/lowering-to-logic.md new file mode 100644 index 000000000..e1a6c1361 --- /dev/null +++ b/src/traits/lowering-to-logic.md @@ -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 Clone for Vec 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) :- 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` if clone is implemented for `?T`". So +e.g. if we wanted to prove that `Clone(Vec>)`, we would do +so by applying the rules recursively: + +- `Clone(Vec>)` is provable if: + - `Clone(Vec)` 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)`. This would +fail (after all, I didn't give an impl of `Clone` for `Bar`): + +- `Clone(Vec)` 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` trait, which declares +that `Self` is equatable with a value of type `T`: + +```rust,ignore +trait Eq { ... } +impl Eq for usize { } +impl> Eq> for Vec { } +``` + +That could be mapped as follows: + +```text +Eq(usize, usize). +Eq(Vec, Vec) :- 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::() } +fn bar>() { } +``` + +This function is very simple, of course: all it does is to call +`bar::()`. Now, looking at the definition of `bar()`, we can see +that it has one where-clause `U: Eq`. So, that means that `foo()` will +have to prove that `usize: Eq` 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::` (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>() { bar::() } +fn bar>() { } +``` + +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 { + // ...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/ diff --git a/src/traits/regions.md b/src/traits/regions.md deleted file mode 100644 index 4657529dc..000000000 --- a/src/traits/regions.md +++ /dev/null @@ -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. From 28abc904edc17bf78e0969e66bf01cc0f219685d Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Mon, 20 Apr 2020 22:36:05 +0800 Subject: [PATCH 4/5] Fix links. --- src/traits/canonical-queries.md | 11 +++-------- src/traits/goals-and-clauses.md | 12 ++++++------ src/traits/lowering-to-logic.md | 6 +++--- 3 files changed, 12 insertions(+), 17 deletions(-) diff --git a/src/traits/canonical-queries.md b/src/traits/canonical-queries.md index e15bdaae2..5ba450d4e 100644 --- a/src/traits/canonical-queries.md +++ b/src/traits/canonical-queries.md @@ -7,7 +7,7 @@ would like to know the answer to – and in the 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). +normalize some associated type. This section covers queries at a fairly high level of abstraction. The subsections look a bit more closely at how these ideas are implemented @@ -104,9 +104,7 @@ 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.) +where-clauses, that would be provable. The response to a trait query in rustc is typically a `Result, NoSolution>` (where the `T` will vary a bit @@ -130,10 +128,7 @@ we did find. It consists of four parts: - 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. + the lifetimes that you supplied as inputs. We'll ignore these here. - **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 diff --git a/src/traits/goals-and-clauses.md b/src/traits/goals-and-clauses.md index ecd2ce145..f4ceb99a0 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -41,7 +41,7 @@ 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 +[pphhf]: https://rust-lang.github.io/chalk/book/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 @@ -118,7 +118,7 @@ e.g. `ProjectionEq::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). +[the section on associated types in Chalk Book][at]. #### Normalize(Projection -> Type) e.g. `ProjectionEq::Item -> u8` @@ -126,12 +126,12 @@ e.g. `ProjectionEq::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`, +types in Chalk Book][at], `Normalize` implies `ProjectionEq`, but not vice versa. In general, proving `Normalize(::Item -> U)` also requires proving `Implemented(T: Trait)`. -[n]: ./associated-types.html#normalize -[at]: ./associated-types.html +[n]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html#normalize +[at]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html #### FromEnv(TraitRef) e.g. `FromEnv(Self: Add)` @@ -260,7 +260,7 @@ 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 +[implied bounds]: https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html#implied-bounds ## Incomplete chapter diff --git a/src/traits/lowering-to-logic.md b/src/traits/lowering-to-logic.md index e1a6c1361..cc8b3bf80 100644 --- a/src/traits/lowering-to-logic.md +++ b/src/traits/lowering-to-logic.md @@ -168,10 +168,10 @@ 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]. +in [the bibliography of Chalk Book][bibliography]. -[the bibliography]: ./bibliography.html -[pphhf]: ./bibliography.html#pphhf +[bibliography]: https://rust-lang.github.io/chalk/book/bibliography.html +[pphhf]: https://rust-lang.github.io/chalk/book/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 From 215645a651ec0334b2395cbf044bb19ec947ac75 Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Sat, 25 Apr 2020 09:17:48 +0800 Subject: [PATCH 5/5] Address review comments. Co-Authored-By: Who? Me?! --- src/SUMMARY.md | 8 ++++---- src/traits/lowering-module.md | 2 ++ 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/SUMMARY.md b/src/SUMMARY.md index ee4d7e3f2..fe040d9e2 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -77,10 +77,10 @@ - [Caching subtleties](./traits/caching.md) - [Specialization](./traits/specialization.md) - [Chalk-based trait solving](./traits/chalk.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) + - [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) diff --git a/src/traits/lowering-module.md b/src/traits/lowering-module.md index 1efdcafb7..8795cb79c 100644 --- a/src/traits/lowering-module.md +++ b/src/traits/lowering-module.md @@ -1 +1,3 @@ # The lowering module in rustc + +This work is ongoing. This section will be filled in once some of it has landed in `rustc`.