From d596ab2bee4fcbc46cb54d2c8129723e941d444a Mon Sep 17 00:00:00 2001 From: Charles Lew Date: Sun, 19 Apr 2020 22:48:45 +0800 Subject: [PATCH] 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 28abd8d6..38634e26 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 41ce5ac9..00000000 --- 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 a0242d4c..00000000 --- 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 e15bdaae..00000000 --- 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 d6d57d78..00000000 --- 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 64cb589c..00000000 --- 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 00000000..dcb0a244 --- /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 ecd2ce14..00000000 --- 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 5876f3b6..00000000 --- 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 5544ce51..00000000 --- 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 c780e7cf..00000000 --- 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 e1a6c136..00000000 --- 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 2ba45167..7f73bfe4 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 74ec89fa..00000000 --- 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 aa17f8c2..00000000 --- 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. -```