diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 28abd8d65..fe040d9e2 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -72,24 +72,15 @@ - [`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) + - [Lowering to logic](./traits/lowering-to-logic.md) + - [Goals and clauses](./traits/goals-and-clauses.md) + - [Canonical queries](./traits/canonical-queries.md) + - [Lowering module in rustc](./traits/lowering-module.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) - [Variance](./variance.md) diff --git a/src/appendix/code-index.md b/src/appendix/code-index.md index a4b18ecc0..76f4609cc 100644 --- a/src/appendix/code-index.md +++ b/src/appendix/code-index.md @@ -27,7 +27,7 @@ Item | Kind | Short description | Chapter | `StringReader` | struct | This is the lexer used during parsing. It consumes characters from the raw source code being compiled and produces a series of tokens for use by the rest of the parser | [The parser] | [src/librustc_parse/lexer/mod.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_parse/lexer/struct.StringReader.html) `rustc_ast::token_stream::TokenStream` | struct | An abstract sequence of tokens, organized into `TokenTree`s | [The parser], [Macro expansion] | [src/librustc_ast/tokenstream.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_ast/tokenstream/struct.TokenStream.html) `TraitDef` | struct | This struct contains a trait's definition with type information | [The `ty` modules] | [src/librustc_middle/ty/trait_def.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/trait_def/struct.TraitDef.html) -`TraitRef` | struct | The combination of a trait and its input types (e.g. `P0: Trait`) | [Trait Solving: Goals and Clauses], [Trait Solving: Lowering impls] | [src/librustc_middle/ty/sty.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TraitRef.html) +`TraitRef` | struct | The combination of a trait and its input types (e.g. `P0: Trait`) | [Trait Solving: Goals and Clauses] | [src/librustc_middle/ty/sty.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TraitRef.html) `Ty<'tcx>` | struct | This is the internal representation of a type used for type checking | [Type checking] | [src/librustc_middle/ty/mod.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/type.Ty.html) `TyCtxt<'tcx>` | struct | The "typing context". This is the central data structure in the compiler. It is the context that you use to perform all manner of queries | [The `ty` modules] | [src/librustc_middle/ty/context.rs](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.TyCtxt.html) @@ -43,4 +43,3 @@ Item | Kind | Short description | Chapter | [Name resolution]: ../name-resolution.html [Parameter Environment]: ../param_env.html [Trait Solving: Goals and Clauses]: ../traits/goals-and-clauses.html#domain-goals -[Trait Solving: Lowering impls]: ../traits/lowering-rules.html#lowering-impls diff --git a/src/appendix/glossary.md b/src/appendix/glossary.md index 5dc8f3801..a3b3826ea 100644 --- a/src/appendix/glossary.md +++ b/src/appendix/glossary.md @@ -49,7 +49,7 @@ memoization
| The process of storing the results o MIR
| The Mid-level IR that is created after type-checking for use by borrowck and codegen. ([see more](../mir/index.html)) miri
| An interpreter for MIR used for constant evaluation. ([see more](../miri.html)) monomorphization
| The process of taking generic implementations of types and functions and instantiating them with concrete types. For example, in the code we might have `Vec`, but in the final executable, we will have a copy of the `Vec` code for every concrete type used in the program (e.g. a copy for `Vec`, a copy for `Vec`, etc). -normalize
| A general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](../traits/associated-types.html#normalize). +normalize
| A general term for converting to a more canonical form, but in the case of rustc typically refers to [associated type normalization](../traits/goals-and-clauses.html#normalizeprojection---type). newtype
| A wrapper around some other type (e.g., `struct Foo(T)` is a "newtype" for `T`). This is commonly used in Rust to give a stronger type for indices. NLL
| Short for [non-lexical lifetimes](../borrow_check/region_inference.html), this is an extension to Rust's borrowing system to make it be based on the control-flow graph. node-id or NodeId
| An index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`. See [the HIR chapter for more](../hir.html#identifiers-in-the-hir). diff --git a/src/traits/associated-types.md b/src/traits/associated-types.md deleted file mode 100644 index 41ce5ac9e..000000000 --- a/src/traits/associated-types.md +++ /dev/null @@ -1,168 +0,0 @@ -# Equality and associated types - -This section covers how the trait system handles equality between -associated types. The full system consists of several moving parts, -which we will introduce one by one: - -- Projection and the `Normalize` predicate -- Placeholder associated type projections -- The `ProjectionEq` predicate -- Integration with unification - -## Associated type projection and normalization - -When a trait defines an associated type (e.g., -[the `Item` type in the `IntoIterator` trait][intoiter-item]), that -type can be referenced by the user using an **associated type -projection** like ` as IntoIterator>::Item`. - -> Often, people will use the shorthand syntax `T::Item`. Presently, that -> syntax is expanded during ["type collection"](../type-checking.html) into the -> explicit form, though that is something we may want to change in the future. - -[intoiter-item]: https://doc.rust-lang.org/nightly/core/iter/trait.IntoIterator.html#associatedtype.Item - - - -In some cases, associated type projections can be **normalized** – -that is, simplified – based on the types given in an impl. So, to -continue with our example, the impl of `IntoIterator` for `Option` -declares (among other things) that `Item = T`: - -```rust,ignore -impl IntoIterator for Option { - type Item = T; - ... -} -``` - -This means we can normalize the projection ` as -IntoIterator>::Item` to just `u32`. - -In this case, the projection was a "monomorphic" one – that is, it -did not have any type parameters. Monomorphic projections are special -because they can **always** be fully normalized. - -Often, we can normalize other associated type projections as well. For -example, ` as IntoIterator>::Item`, where `?T` is an inference -variable, can be normalized to just `?T`. - -In our logic, normalization is defined by a predicate -`Normalize`. The `Normalize` clauses arise only from -impls. For example, the `impl` of `IntoIterator` for `Option` that -we saw above would be lowered to a program clause like so: - -```text -forall { - Normalize( as IntoIterator>::Item -> T) :- - Implemented(Option: IntoIterator) -} -``` - -where in this case, the one `Implemented` condition is always true. - -> Since we do not permit quantification over traits, this is really more like -> a family of program clauses, one for each associated type. - -We could apply that rule to normalize either of the examples that -we've seen so far. - -## Placeholder associated types - -Sometimes however we want to work with associated types that cannot be -normalized. For example, consider this function: - -```rust,ignore -fn foo(...) { ... } -``` - -In this context, how would we normalize the type `T::Item`? - -Without knowing what `T` is, we can't really do so. To represent this case, -we introduce a type called a **placeholder associated type projection**. This -is written like so: `(IntoIterator::Item)`. - -You may note that it looks a lot like a regular type (e.g., `Option`), -except that the "name" of the type is `(IntoIterator::Item)`. This is not an -accident: placeholder associated type projections work just like ordinary -types like `Vec` when it comes to unification. That is, they are only -considered equal if (a) they are both references to the same associated type, -like `IntoIterator::Item` and (b) their type arguments are equal. - -Placeholder associated types are never written directly by the user. -They are used internally by the trait system only, as we will see -shortly. - -In rustc, they correspond to the `TyKind::UnnormalizedProjectionTy` enum -variant, declared in [`librustc_middle/ty/sty.rs`][sty]. In chalk, we use an -`ApplicationTy` with a name living in a special namespace dedicated to -placeholder associated types (see the `TypeName` enum declared in -[`chalk-ir/src/lib.rs`][chalk_type_name]). - -[sty]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/ty/sty.rs -[chalk_type_name]: https://github.com/rust-lang-nursery/chalk/blob/master/chalk-ir/src/lib.rs - -## Projection equality - -So far we have seen two ways to answer the question of "When can we -consider an associated type projection equal to another type?": - -- the `Normalize` predicate could be used to transform projections when we - knew which impl applied; -- **placeholder** associated types can be used when we don't. This is also - known as **lazy normalization**. - -We now introduce the `ProjectionEq` predicate to bring those two cases -together. The `ProjectionEq` predicate looks like so: - -```text -ProjectionEq(::Item = U) -``` - -and we will see that it can be proven *either* via normalization or -via the placeholder type. As part of lowering an associated type declaration from -some trait, we create two program clauses for `ProjectionEq`: - -```text -forall { - ProjectionEq(::Item = U) :- - Normalize(::Item -> U) -} - -forall { - ProjectionEq(::Item = (IntoIterator::Item)) -} -``` - -These are the only two `ProjectionEq` program clauses we ever make for -any given associated item. - -## Integration with unification - -Now we are ready to discuss how associated type equality integrates -with unification. As described in the -[type inference](../type-inference.html) section, unification is -basically a procedure with a signature like this: - -```text -Unify(A, B) = Result<(Subgoals, RegionConstraints), NoSolution> -``` - -In other words, we try to unify two things A and B. That procedure -might just fail, in which case we get back `Err(NoSolution)`. This -would happen, for example, if we tried to unify `u32` and `i32`. - -The key point is that, on success, unification can also give back to -us a set of subgoals that still remain to be proven. (It can also give -back region constraints, but those are not relevant here). - -Whenever unification encounters a non-placeholder associated type -projection P being equated with some other type T, it always succeeds, -but it produces a subgoal `ProjectionEq(P = T)` that is propagated -back up. Thus it falls to the ordinary workings of the trait system -to process that constraint. - -> If we unify two projections P1 and P2, then unification produces a -> variable X and asks us to prove that `ProjectionEq(P1 = X)` and -> `ProjectionEq(P2 = X)`. (That used to be needed in an older system to -> prevent cycles; I rather doubt it still is. -nmatsakis) diff --git a/src/traits/bibliography.md b/src/traits/bibliography.md deleted file mode 100644 index a0242d4c4..000000000 --- a/src/traits/bibliography.md +++ /dev/null @@ -1,27 +0,0 @@ -# Bibliography - -If you'd like to read more background material, here are some -recommended texts and papers: - -[Programming with Higher-order Logic][phl], by Dale Miller and Gopalan -Nadathur, covers the key concepts of Lambda prolog. Although it's a -slim little volume, it's the kind of book where you learn something -new every time you open it. - -[phl]: https://www.amazon.com/Programming-Higher-Order-Logic-Dale-Miller/dp/052187940X - - - -["A proof procedure for the logic of Hereditary Harrop formulas"][pphhf], -by Gopalan Nadathur. This paper covers the basics of universes, -environments, and Lambda Prolog-style proof search. Quite readable. - -[pphhf]: https://dl.acm.org/citation.cfm?id=868380 - - - -["A new formulation of tabled resolution with delay"][nftrd], by -Theresa Swift. This paper gives a kind of abstract treatment of the -SLG formulation that is the basis for our on-demand solver. - -[nftrd]: https://dl.acm.org/citation.cfm?id=651202 diff --git a/src/traits/canonical-queries.md b/src/traits/canonical-queries.md index e15bdaae2..5ba450d4e 100644 --- a/src/traits/canonical-queries.md +++ b/src/traits/canonical-queries.md @@ -7,7 +7,7 @@ would like to know the answer to – and in the checker or other parts of the system, may in the course of doing their thing want to know whether some trait is implemented for some type (e.g., is `u32: Debug` true?). Or they may want to -[normalize some associated type](./associated-types.html). +normalize some associated type. This section covers queries at a fairly high level of abstraction. The subsections look a bit more closely at how these ideas are implemented @@ -104,9 +104,7 @@ trying to enumerate **all possible** answers for you, they are looking for an **unambiguous** answer. In particular, when they tell you the value for a type variable, that means that this is the **only possible instantiation** that you could use, given the current set of impls and -where-clauses, that would be provable. (Internally within the solver, -though, they can potentially enumerate all possible answers. See -[the description of the SLG solver](./slg.html) for details.) +where-clauses, that would be provable. The response to a trait query in rustc is typically a `Result, NoSolution>` (where the `T` will vary a bit @@ -130,10 +128,7 @@ we did find. It consists of four parts: - As we'll see in the example below, we can get back var values even for `Ambiguous` cases. - **Region constraints:** these are relations that must hold between - the lifetimes that you supplied as inputs. We'll ignore these here, - but see the - [section on handling regions in traits](./regions.html) for - more details. + the lifetimes that you supplied as inputs. We'll ignore these here. - **Value:** The query result also comes with a value of type `T`. For some specialized queries – like normalizing associated types – this is used to carry back an extra result, but it's often just diff --git a/src/traits/canonicalization.md b/src/traits/canonicalization.md deleted file mode 100644 index d6d57d785..000000000 --- a/src/traits/canonicalization.md +++ /dev/null @@ -1,256 +0,0 @@ -# Canonicalization - -Canonicalization is the process of **isolating** an inference value -from its context. It is a key part of implementing -[canonical queries][cq], and you may wish to read the parent chapter -to get more context. - -Canonicalization is really based on a very simple concept: every -[inference variable](../type-inference.html#vars) is always in one of -two states: either it is **unbound**, in which case we don't know yet -what type it is, or it is **bound**, in which case we do. So to -isolate some data-structure T that contains types/regions from its -environment, we just walk down and find the unbound variables that -appear in T; those variables get replaced with "canonical variables", -starting from zero and numbered in a fixed order (left to right, for -the most part, but really it doesn't matter as long as it is -consistent). - -[cq]: ./canonical-queries.html - -So, for example, if we have the type `X = (?T, ?U)`, where `?T` and -`?U` are distinct, unbound inference variables, then the canonical -form of `X` would be `(?0, ?1)`, where `?0` and `?1` represent these -**canonical placeholders**. Note that the type `Y = (?U, ?T)` also -canonicalizes to `(?0, ?1)`. But the type `Z = (?T, ?T)` would -canonicalize to `(?0, ?0)` (as would `(?U, ?U)`). In other words, the -exact identity of the inference variables is not important – unless -they are repeated. - -We use this to improve caching as well as to detect cycles and other -things during trait resolution. Roughly speaking, the idea is that if -two trait queries have the same canonical form, then they will get -the same answer. That answer will be expressed in terms of the -canonical variables (`?0`, `?1`), which we can then map back to the -original variables (`?T`, `?U`). - -## Canonicalizing the query - -To see how it works, imagine that we are asking to solve the following -trait query: `?A: Foo<'static, ?B>`, where `?A` and `?B` are unbound. -This query contains two unbound variables, but it also contains the -lifetime `'static`. The trait system generally ignores all lifetimes -and treats them equally, so when canonicalizing, we will *also* -replace any [free lifetime](../appendix/background.html#free-vs-bound) with a -canonical variable (Note that `'static` is actually a _free_ lifetime -variable here. We are not considering it in the typing context of the whole -program but only in the context of this trait reference. Mathematically, we -are not quantifying over the whole program, but only this obligation). -Therefore, we get the following result: - -```text -?0: Foo<'?1, ?2> -``` - -Sometimes we write this differently, like so: - -```text -for { ?0: Foo<'?1, ?2> } -``` - -This `for<>` gives some information about each of the canonical -variables within. In this case, each `T` indicates a type variable, -so `?0` and `?2` are types; the `L` indicates a lifetime variable, so -`?1` is a lifetime. The `canonicalize` method *also* gives back a -`CanonicalVarValues` array OV with the "original values" for each -canonicalized variable: - -```text -[?A, 'static, ?B] -``` - -We'll need this vector OV later, when we process the query response. - -## Executing the query - -Once we've constructed the canonical query, we can try to solve it. -To do so, we will wind up creating a fresh inference context and -**instantiating** the canonical query in that context. The idea is that -we create a substitution S from the canonical form containing a fresh -inference variable (of suitable kind) for each canonical variable. -So, for our example query: - -```text -for { ?0: Foo<'?1, ?2> } -``` - -the substitution S might be: - -```text -S = [?A, '?B, ?C] -``` - -We can then replace the bound canonical variables (`?0`, etc) with -these inference variables, yielding the following fully instantiated -query: - -```text -?A: Foo<'?B, ?C> -``` - -Remember that substitution S though! We're going to need it later. - -OK, now that we have a fresh inference context and an instantiated -query, we can go ahead and try to solve it. The trait solver itself is -explained in more detail in [another section](./slg.html), but -suffice to say that it will compute a [certainty value][cqqr] (`Proven` or -`Ambiguous`) and have side-effects on the inference variables we've -created. For example, if there were only one impl of `Foo`, like so: - -[cqqr]: ./canonical-queries.html#query-response - -```rust,ignore -impl<'a, X> Foo<'a, X> for Vec -where X: 'a -{ ... } -``` - -then we might wind up with a certainty value of `Proven`, as well as -creating fresh inference variables `'?D` and `?E` (to represent the -parameters on the impl) and unifying as follows: - -- `'?B = '?D` -- `?A = Vec` -- `?C = ?E` - -We would also accumulate the region constraint `?E: '?D`, due to the -where clause. - -In order to create our final query result, we have to "lift" these -values out of the query's inference context and into something that -can be reapplied in our original inference context. We do that by -**re-applying canonicalization**, but to the **query result**. - -## Canonicalizing the query result - -As discussed in [the parent section][cqqr], most trait queries wind up -with a result that brings together a "certainty value" `certainty`, a -result substitution `var_values`, and some region constraints. To -create this, we wind up re-using the substitution S that we created -when first instantiating our query. To refresh your memory, we had a query - -```text -for { ?0: Foo<'?1, ?2> } -``` - -for which we made a substutition S: - -```text -S = [?A, '?B, ?C] -``` - -We then did some work which unified some of those variables with other things. -If we "refresh" S with the latest results, we get: - -```text -S = [Vec, '?D, ?E] -``` - -These are precisely the new values for the three input variables from -our original query. Note though that they include some new variables -(like `?E`). We can make those go away by canonicalizing again! We don't -just canonicalize S, though, we canonicalize the whole query response QR: - -```text -QR = { - certainty: Proven, // or whatever - var_values: [Vec, '?D, ?E] // this is S - region_constraints: [?E: '?D], // from the impl - value: (), // for our purposes, just (), but - // in some cases this might have - // a type or other info -} -``` - -The result would be as follows: - -```text -Canonical(QR) = for { - certainty: Proven, - var_values: [Vec, '?1, ?0] - region_constraints: [?0: '?1], - value: (), -} -``` - -(One subtle point: when we canonicalize the query **result**, we do not -use any special treatment for free lifetimes. Note that both -references to `'?D`, for example, were converted into the same -canonical variable (`?1`). This is in contrast to the original query, -where we canonicalized every free lifetime into a fresh canonical -variable.) - -Now, this result must be reapplied in each context where needed. - -## Processing the canonicalized query result - -In the previous section we produced a canonical query result. We now have -to apply that result in our original context. If you recall, way back in the -beginning, we were trying to prove this query: - -```text -?A: Foo<'static, ?B> -``` - -We canonicalized that into this: - -```text -for { ?0: Foo<'?1, ?2> } -``` - -and now we got back a canonical response: - -```text -for { - certainty: Proven, - var_values: [Vec, '?1, ?0] - region_constraints: [?0: '?1], - value: (), -} -``` - -We now want to apply that response to our context. Conceptually, how -we do that is to (a) instantiate each of the canonical variables in -the result with a fresh inference variable, (b) unify the values in -the result with the original values, and then (c) record the region -constraints for later. Doing step (a) would yield a result of - -```text -{ - certainty: Proven, - var_values: [Vec, '?D, ?C] - ^^ ^^^ fresh inference variables - region_constraints: [?C: '?D], - value: (), -} -``` - -Step (b) would then unify: - -```text -?A with Vec -'static with '?D -?B with ?C -``` - -And finally the region constraint of `?C: 'static` would be recorded -for later verification. - -(What we *actually* do is a mildly optimized variant of that: Rather -than eagerly instantiating all of the canonical values in the result -with variables, we instead walk the vector of values, looking for -cases where the value is just a canonical variable. In our example, -`values[2]` is `?C`, so that means we can deduce that `?C := ?B` and -`'?D := 'static`. This gives us a partial set of values. Anything for -which we do not find a value, we create an inference variable.) - diff --git a/src/traits/chalk-overview.md b/src/traits/chalk-overview.md deleted file mode 100644 index 64cb589c1..000000000 --- a/src/traits/chalk-overview.md +++ /dev/null @@ -1,256 +0,0 @@ -# An Overview of Chalk - -> Chalk is under heavy development, so if any of these links are broken or if -> any of the information is inconsistent with the code or outdated, please -> [open an issue][rustc-issues] so we can fix it. If you are able to fix the -> issue yourself, we would love your contribution! - -[Chalk][chalk] recasts Rust's trait system explicitly in terms of logic -programming by "lowering" Rust code into a kind of logic program we can then -execute queries against (see [*Lowering to Logic*][lowering-to-logic] and -[*Lowering Rules*][lowering-rules]). Its goal is to be an executable, highly -readable specification of the Rust trait system. - -There are many expected benefits from this work. It will consolidate our -existing, somewhat ad-hoc implementation into something far more principled and -expressive, which should behave better in corner cases, and be much easier to -extend. - -## Chalk Structure - -Chalk has two main "products". The first of these is the -[`chalk_engine`][chalk_engine] crate, which defines the core [SLG -solver][slg]. This is the part rustc uses. - -The rest of chalk can be considered an elaborate testing harness. Chalk is -capable of parsing Rust-like "programs", lowering them to logic, and -performing queries on them. - -Here's a sample session in the chalk repl, chalki. After feeding it our -program, we perform some queries on it. - -```rust,ignore -?- program -Enter a program; press Ctrl-D when finished -| struct Foo { } -| struct Bar { } -| struct Vec { } -| trait Clone { } -| impl Clone for Vec where T: Clone { } -| impl Clone for Foo { } - -?- Vec: Clone -Unique; substitution [], lifetime constraints [] - -?- Vec: Clone -No possible solution. - -?- exists { Vec: Clone } -Ambiguous; no inference guidance -``` - -You can see more examples of programs and queries in the [unit -tests][chalk-test-example]. - -Next we'll go through each stage required to produce the output above. - -### Parsing ([chalk_parse]) - -Chalk is designed to be incorporated with the Rust compiler, so the syntax and -concepts it deals with heavily borrow from Rust. It is convenient for the sake -of testing to be able to run chalk on its own, so chalk includes a parser for a -Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is -not intended to look exactly like it or support the exact same syntax. - -The parser takes that syntax and produces an [Abstract Syntax Tree (AST)][ast]. -You can find the [complete definition of the AST][chalk-ast] in the source code. - -The syntax contains things from Rust that we know and love, for example: traits, -impls, and struct definitions. Parsing is often the first "phase" of -transformation that a program goes through in order to become a format that -chalk can understand. - -### Rust Intermediate Representation ([chalk_rust_ir]) - -After getting the AST we convert it to a more convenient intermediate -representation called [`chalk_rust_ir`][chalk_rust_ir]. This is sort of -analogous to the [HIR] in Rust. The process of converting to IR is called -*lowering*. - -The [`chalk::program::Program`][chalk-program] struct contains some "rust things" -but indexed and accessible in a different way. For example, if you have a -type like `Foo`, we would represent `Foo` as a string in the AST but in -`chalk::program::Program`, we use numeric indices (`ItemId`). - -The [IR source code][ir-code] contains the complete definition. - -### Chalk Intermediate Representation ([chalk_ir]) - -Once we have Rust IR it is time to convert it to "program clauses". A -[`ProgramClause`] is essentially one of the following: - -* A [clause] of the form `consequence :- conditions` where `:-` is read as - "if" and `conditions = cond1 && cond2 && ...` -* A universally quantified clause of the form - `forall { consequence :- conditions }` - * `forall { ... }` is used to represent [universal quantification]. See the - section on [Lowering to logic][lowering-forall] for more information. - * A key thing to note about `forall` is that we don't allow you to "quantify" - over traits, only types and regions (lifetimes). That is, you can't make a - rule like `forall { u32: Trait }` which would say "`u32` implements - all traits". You can however say `forall { T: Trait }` meaning "`Trait` - is implemented by all types". - * `forall { ... }` is represented in the code using the [`Binders` - struct][binders-struct]. - -*See also: [Goals and Clauses][goals-and-clauses]* - -This is where we encode the rules of the trait system into logic. For -example, if we have the following Rust: - -```rust,ignore -impl Clone for Vec {} -``` - -We generate the following program clause: - -```rust,ignore -forall { (Vec: Clone) :- (T: Clone) } -``` - -This rule dictates that `Vec: Clone` is only satisfied if `T: Clone` is also -satisfied (i.e. "provable"). - -Similar to [`chalk::program::Program`][chalk-program] which has "rust-like -things", chalk_ir defines [`ProgramEnvironment`] which is "pure logic". -The main field in that struct is `program_clauses`, which contains the -[`ProgramClause`]s generated by the rules module. - -### Rules ([chalk_solve]) - -The `chalk_solve` crate ([source code][chalk_solve]) defines the logic rules we -use for each item in the Rust IR. It works by iterating over every trait, impl, -etc. and emitting the rules that come from each one. - -*See also: [Lowering Rules][lowering-rules]* - -#### Well-formedness checks - -As part of lowering to logic, we also do some "well formedness" checks. See -the [`chalk_solve::wf` source code][solve-wf-src] for where those are done. - -*See also: [Well-formedness checking][wf-checking]* - -#### Coherence - -The method `CoherenceSolver::specialization_priorities` in the `coherence` module -([source code][coherence-src]) checks "coherence", which means that it -ensures that two impls of the same trait for the same type cannot exist. - -### Solver ([chalk_solve]) - -Finally, when we've collected all the program clauses we care about, we want -to perform queries on it. The component that finds the answer to these -queries is called the *solver*. - -*See also: [The SLG Solver][slg]* - -## Crates - -Chalk's functionality is broken up into the following crates: -- [**chalk_engine**][chalk_engine]: Defines the core [SLG solver][slg]. -- [**chalk_rust_ir**][chalk_rust_ir], containing the "HIR-like" form of the AST -- [**chalk_ir**][chalk_ir]: Defines chalk's internal representation of - types, lifetimes, and goals. -- [**chalk_solve**][chalk_solve]: Combines `chalk_ir` and `chalk_engine`, - effectively, which implements logic rules converting `chalk_rust_ir` to - `chalk_ir` - - Defines the `coherence` module, which implements coherence rules - - [`chalk_engine::context`][engine-context] provides the necessary hooks. -- [**chalk_parse**][chalk_parse]: Defines the raw AST and a parser. -- [**chalk**][doc-chalk]: Brings everything together. Defines the following - modules: - - `chalk::lowering`, which converts AST to `chalk_rust_ir` - - Also includes [chalki][chalki], chalk's REPL. - -[Browse source code on GitHub](https://github.com/rust-lang/chalk) - -## Testing - -chalk has a test framework for lowering programs to logic, checking the -lowered logic, and performing queries on it. This is how we test the -implementation of chalk itself, and the viability of the [lowering -rules][lowering-rules]. - -The main kind of tests in chalk are **goal tests**. They contain a program, -which is expected to lower to logic successfully, and a set of queries -(goals) along with the expected output. Here's an -[example][chalk-test-example]. Since chalk's output can be quite long, goal -tests support specifying only a prefix of the output. - -**Lowering tests** check the stages that occur before we can issue queries -to the solver: the [lowering to chalk_rust_ir][chalk-test-lowering], and the -[well-formedness checks][chalk-test-wf] that occur after that. - -### Testing internals - -Goal tests use a [`test!` macro][test-macro] that takes chalk's Rust-like -syntax and runs it through the full pipeline described above. The macro -ultimately calls the [`solve_goal` function][solve_goal]. - -Likewise, lowering tests use the [`lowering_success!` and -`lowering_error!` macros][test-lowering-macros]. - -## More Resources - -* [Chalk Source Code](https://github.com/rust-lang/chalk) -* [Chalk Glossary](https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md) - -### Blog Posts - -* [Lowering Rust traits to logic](http://smallcultfollowing.com/babysteps/blog/2017/01/26/lowering-rust-traits-to-logic/) -* [Unification in Chalk, part 1](http://smallcultfollowing.com/babysteps/blog/2017/03/25/unification-in-chalk-part-1/) -* [Unification in Chalk, part 2](http://smallcultfollowing.com/babysteps/blog/2017/04/23/unification-in-chalk-part-2/) -* [Negative reasoning in Chalk](https://aturon.github.io/blog/2017/04/24/negative-chalk/) -* [Query structure in chalk](http://smallcultfollowing.com/babysteps/blog/2017/05/25/query-structure-in-chalk/) -* [Cyclic queries in chalk](http://smallcultfollowing.com/babysteps/blog/2017/09/12/tabling-handling-cyclic-queries-in-chalk/) -* [An on-demand SLG solver for chalk](http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/) - -[goals-and-clauses]: ./goals-and-clauses.html -[HIR]: ../hir.html -[lowering-forall]: ./lowering-to-logic.html#type-checking-generic-functions-beyond-horn-clauses -[lowering-rules]: ./lowering-rules.html -[lowering-to-logic]: ./lowering-to-logic.html -[slg]: ./slg.html -[wf-checking]: ./wf.html - -[ast]: https://en.wikipedia.org/wiki/Abstract_syntax_tree -[chalk]: https://github.com/rust-lang/chalk -[rustc-issues]: https://github.com/rust-lang/rustc-dev-guide/issues -[universal quantification]: https://en.wikipedia.org/wiki/Universal_quantification - -[`ProgramClause`]: https://rust-lang.github.io/chalk/chalk_ir/struct.ProgramClause.html -[`ProgramEnvironment`]: https://rust-lang.github.io/chalk/chalk_integration/program_environment/struct.ProgramEnvironment.html -[chalk_engine]: https://rust-lang.github.io/chalk/chalk_engine -[chalk_ir]: https://rust-lang.github.io/chalk/chalk_ir/index.html -[chalk_parse]: https://rust-lang.github.io/chalk/chalk_parse/index.html -[chalk_solve]: https://rust-lang.github.io/chalk/chalk_solve/index.html -[chalk_rust_ir]: https://rust-lang.github.io/chalk/chalk_rust_ir/index.html -[doc-chalk]: https://rust-lang.github.io/chalk/chalk/index.html -[engine-context]: https://rust-lang.github.io/chalk/chalk_engine/context/index.html -[chalk-program]: https://rust-lang.github.io/chalk/chalk_integration/program/struct.Program.html - -[binders-struct]: https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html -[chalk-ast]: https://rust-lang.github.io/chalk/chalk_parse/ast/index.html -[chalk-test-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L115 -[chalk-test-lowering-example]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs#L8-L31 -[chalk-test-lowering]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rust_ir/lowering/test.rs -[chalk-test-wf]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/rules/wf/test.rs#L1 -[chalki]: https://github.com/rust-lang/chalk/blob/master/src/main.rs -[clause]: https://github.com/rust-lang/chalk/blob/master/GLOSSARY.md#clause -[coherence-src]: https://rust-lang.github.io/chalk/chalk_solve/coherence/index.html -[ir-code]: https://rust-lang.github.io/chalk/chalk_rust_ir/ -[solve-wf-src]: https://rust-lang.github.io/chalk/chalk_solve/wf/index.html -[solve_goal]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L85 -[test-lowering-macros]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test_util.rs#L21-L54 -[test-macro]: https://github.com/rust-lang/chalk/blob/4bce000801de31bf45c02f742a5fce335c9f035f/src/test.rs#L33 diff --git a/src/traits/chalk.md b/src/traits/chalk.md new file mode 100644 index 000000000..70af2a1f5 --- /dev/null +++ b/src/traits/chalk.md @@ -0,0 +1,41 @@ +# Chalk-based trait solving + +[Chalk][chalk] is an experimental trait solver for rust that is currently +under development by the [Traits Working Group][wg]. Its goal is +to enable a lot of trait system features and bug fixes that are +currently hard to implement (e.g. GATs or specialization). if you +would like to help in hacking on the new solver, you will find +instructions for getting involved in the +[Traits Working Group tracking issue][wg]. + +[wg]: https://github.com/rust-lang/rust/issues/48416 + +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. 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 index ecd2ce145..f4ceb99a0 100644 --- a/src/traits/goals-and-clauses.md +++ b/src/traits/goals-and-clauses.md @@ -41,7 +41,7 @@ In terms of code, these types are defined in [`librustc_middle/traits/mod.rs`][traits_mod] in rustc, and in [`chalk-ir/src/lib.rs`][chalk_ir] in chalk. -[pphhf]: ./bibliography.html#pphhf +[pphhf]: https://rust-lang.github.io/chalk/book/bibliography.html#pphhf [traits_mod]: https://github.com/rust-lang/rust/blob/master/src/librustc_middle/traits/mod.rs [chalk_ir]: https://github.com/rust-lang/chalk/blob/master/chalk-ir/src/lib.rs @@ -118,7 +118,7 @@ e.g. `ProjectionEq::Item = u8` The given associated type `Projection` is equal to `Type`; this can be proved with either normalization or using placeholder associated types. See -[the section on associated types](./associated-types.html). +[the section on associated types in Chalk Book][at]. #### Normalize(Projection -> Type) e.g. `ProjectionEq::Item -> u8` @@ -126,12 +126,12 @@ e.g. `ProjectionEq::Item -> u8` The given associated type `Projection` can be [normalized][n] to `Type`. As discussed in [the section on associated -types](./associated-types.html), `Normalize` implies `ProjectionEq`, +types in Chalk Book][at], `Normalize` implies `ProjectionEq`, but not vice versa. In general, proving `Normalize(::Item -> U)` also requires proving `Implemented(T: Trait)`. -[n]: ./associated-types.html#normalize -[at]: ./associated-types.html +[n]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html#normalize +[at]: https://rust-lang.github.io/chalk/book/clauses/type_equality.html #### FromEnv(TraitRef) e.g. `FromEnv(Self: Add)` @@ -260,7 +260,7 @@ In addition to auto traits, `WellFormed` predicates are co-inductive. These are used to achieve a similar "enumerate all the cases" pattern, as described in the section on [implied bounds]. -[implied bounds]: ./lowering-rules.html#implied-bounds +[implied bounds]: https://rust-lang.github.io/chalk/book/clauses/implied_bounds.html#implied-bounds ## Incomplete chapter diff --git a/src/traits/implied-bounds.md b/src/traits/implied-bounds.md deleted file mode 100644 index 5876f3b62..000000000 --- a/src/traits/implied-bounds.md +++ /dev/null @@ -1,502 +0,0 @@ -# Implied Bounds - -Implied bounds remove the need to repeat where clauses written on -a type declaration or a trait declaration. For example, say we have the -following type declaration: -```rust,ignore -struct HashSet { - ... -} -``` - -then everywhere we use `HashSet` as an "input" type, that is appearing in -the receiver type of an `impl` or in the arguments of a function, we don't -want to have to repeat the `where K: Hash` bound, as in: - -```rust,ignore -// I don't want to have to repeat `where K: Hash` here. -impl HashSet { - ... -} - -// Same here. -fn loud_insert(set: &mut HashSet, item: K) { - println!("inserting!"); - set.insert(item); -} -``` - -Note that in the `loud_insert` example, `HashSet` is not the type -of the `set` argument of `loud_insert`, it only *appears* in the -argument type `&mut HashSet`: we care about every type appearing -in the function's header (the header is the signature without the return type), -not only types of the function's arguments. - -The rationale for applying implied bounds to input types is that, for example, -in order to call the `loud_insert` function above, the programmer must have -*produced* the type `HashSet` already, hence the compiler already verified -that `HashSet` was well-formed, i.e. that `K` effectively implemented -`Hash`, as in the following example: - -```rust,ignore -fn main() { - // I am producing a value of type `HashSet`. - // If `i32` was not `Hash`, the compiler would report an error here. - let set: HashSet = HashSet::new(); - loud_insert(&mut set, 5); -} -``` - -Hence, we don't want to repeat where clauses for input types because that would -sort of duplicate the work of the programmer, having to verify that their types -are well-formed both when calling the function and when using them in the -arguments of their function. The same reasoning applies when using an `impl`. - -Similarly, given the following trait declaration: -```rust,ignore -trait Copy where Self: Clone { // desugared version of `Copy: Clone` - ... -} -``` - -then everywhere we bound over `SomeType: Copy`, we would like to be able to -use the fact that `SomeType: Clone` without having to write it explicitly, -as in: -```rust,ignore -fn loud_clone(x: T) { - println!("cloning!"); - x.clone(); -} - -fn fun_with_copy(x: T) { - println!("will clone a `Copy` type soon..."); - - // I'm using `loud_clone` with `T: Copy`, I know this - // implies `T: Clone` so I don't want to have to write it explicitly. - loud_clone(x); -} -``` - -The rationale for implied bounds for traits is that if a type implements -`Copy`, that is, if there exists an `impl Copy` for that type, there *ought* -to exist an `impl Clone` for that type, otherwise the compiler would have -reported an error in the first place. So again, if we were forced to repeat the -additional `where SomeType: Clone` everywhere whereas we already know that -`SomeType: Copy` hold, we would kind of duplicate the verification work. - -Implied bounds are not yet completely enforced in rustc, at the moment it only -works for outlive requirements, super trait bounds, and bounds on associated -types. The full RFC can be found [here][RFC]. We'll give here a brief view -of how implied bounds work and why we chose to implement it that way. The -complete set of lowering rules can be found in the corresponding -[chapter](./lowering-rules.md). - -[RFC]: https://github.com/rust-lang/rfcs/blob/master/text/2089-implied-bounds.md - -## Implied bounds and lowering rules - -Now we need to express implied bounds in terms of logical rules. We will start -with exposing a naive way to do it. Suppose that we have the following traits: -```rust,ignore -trait Foo { - ... -} - -trait Bar where Self: Foo { } { - ... -} -``` - -So we would like to say that if a type implements `Bar`, then necessarily -it must also implement `Foo`. We might think that a clause like this would -work: -```text -forall { - Implemented(Type: Foo) :- Implemented(Type: Bar). -} -``` - -Now suppose that we just write this impl: -```rust,ignore -struct X; - -impl Bar for X { } -``` - -Clearly this should not be allowed: indeed, we wrote a `Bar` impl for `X`, but -the `Bar` trait requires that we also implement `Foo` for `X`, which we never -did. In terms of what the compiler does, this would look like this: -```rust,ignore -struct X; - -impl Bar for X { - // We are in a `Bar` impl for the type `X`. - // There is a `where Self: Foo` bound on the `Bar` trait declaration. - // Hence I need to prove that `X` also implements `Foo` for that impl - // to be legal. -} -``` -So the compiler would try to prove `Implemented(X: Foo)`. Of course it will -not find any `impl Foo for X` since we did not write any. However, it -will see our implied bound clause: -```text -forall { - Implemented(Type: Foo) :- Implemented(Type: Bar). -} -``` - -so that it may be able to prove `Implemented(X: Foo)` if `Implemented(X: Bar)` -holds. And it turns out that `Implemented(X: Bar)` does hold since we wrote -a `Bar` impl for `X`! Hence the compiler will accept the `Bar` impl while it -should not. - -## Implied bounds coming from the environment - -So the naive approach does not work. What we need to do is to somehow decouple -implied bounds from impls. Suppose we know that a type `SomeType<...>` -implements `Bar` and we want to deduce that `SomeType<...>` must also implement -`Foo`. - -There are two possibilities: first, we have enough information about -`SomeType<...>` to see that there exists a `Bar` impl in the program which -covers `SomeType<...>`, for example a plain `impl<...> Bar for SomeType<...>`. -Then if the compiler has done its job correctly, there *must* exist a `Foo` -impl which covers `SomeType<...>`, e.g. another plain -`impl<...> Foo for SomeType<...>`. In that case then, we can just use this -impl and we do not need implied bounds at all. - -Second possibility: we do not know enough about `SomeType<...>` in order to -find a `Bar` impl which covers it, for example if `SomeType<...>` is just -a type parameter in a function: -```rust,ignore -fn foo() { - // We'd like to deduce `Implemented(T: Foo)`. -} -``` - -That is, the information that `T` implements `Bar` here comes from the -*environment*. The environment is the set of things that we assume to be true -when we type check some Rust declaration. In that case, what we assume is that -`T: Bar`. Then at that point, we might authorize ourselves to have some kind -of "local" implied bound reasoning which would say -`Implemented(T: Foo) :- Implemented(T: Bar)`. This reasoning would -only be done within our `foo` function in order to avoid the earlier -problem where we had a global clause. - -We can apply these local reasonings everywhere we can have an environment --- i.e. when we can write where clauses -- that is, inside impls, -trait declarations, and type declarations. - -## Computing implied bounds with `FromEnv` - -The previous subsection showed that it was only useful to compute implied -bounds for facts coming from the environment. -We talked about "local" rules, but there are multiple possible strategies to -indeed implement the locality of implied bounds. - -In rustc, the current strategy is to *elaborate* bounds: that is, each time -we have a fact in the environment, we recursively derive all the other things -that are implied by this fact until we reach a fixed point. For example, if -we have the following declarations: -```rust,ignore -trait A { } -trait B where Self: A { } -trait C where Self: B { } - -fn foo() { - ... -} -``` -then inside the `foo` function, we start with an environment containing only -`Implemented(T: C)`. Then because of implied bounds for the `C` trait, we -elaborate `Implemented(T: B)` and add it to our environment. Because of -implied bounds for the `B` trait, we elaborate `Implemented(T: A)`and add it -to our environment as well. We cannot elaborate anything else, so we conclude -that our final environment consists of `Implemented(T: A + B + C)`. - -In the new-style trait system, we like to encode as many things as possible -with logical rules. So rather than "elaborating", we have a set of *global* -program clauses defined like so: -```text -forall { Implemented(T: A) :- FromEnv(T: A). } - -forall { Implemented(T: B) :- FromEnv(T: B). } -forall { FromEnv(T: A) :- FromEnv(T: B). } - -forall { Implemented(T: C) :- FromEnv(T: C). } -forall { FromEnv(T: C) :- FromEnv(T: C). } -``` -So these clauses are defined globally (that is, they are available from -everywhere in the program) but they cannot be used because the hypothesis -is always of the form `FromEnv(...)` which is a bit special. Indeed, as -indicated by the name, `FromEnv(...)` facts can **only** come from the -environment. -How it works is that in the `foo` function, instead of having an environment -containing `Implemented(T: C)`, we replace this environment with -`FromEnv(T: C)`. From here and thanks to the above clauses, we see that we -are able to reach any of `Implemented(T: A)`, `Implemented(T: B)` or -`Implemented(T: C)`, which is what we wanted. - -## Implied bounds and well-formedness checking - -Implied bounds are tightly related with well-formedness checking. -Well-formedness checking is the process of checking that the impls the -programmer wrote are legal, what we referred to earlier as "the compiler doing -its job correctly". - -We already saw examples of illegal and legal impls: -```rust,ignore -trait Foo { } -trait Bar where Self: Foo { } - -struct X; -struct Y; - -impl Bar for X { - // This impl is not legal: the `Bar` trait requires that we also - // implement `Foo`, and we didn't. -} - -impl Foo for Y { - // This impl is legal: there is nothing to check as there are no where - // clauses on the `Foo` trait. -} - -impl Bar for Y { - // This impl is legal: we have a `Foo` impl for `Y`. -} -``` -We must define what "legal" and "illegal" mean. For this, we introduce another -predicate: `WellFormed(Type: Trait)`. We say that the trait reference -`Type: Trait` is well-formed if `Type` meets the bounds written on the -`Trait` declaration. For each impl we write, assuming that the where clauses -declared on the impl hold, the compiler tries to prove that the corresponding -trait reference is well-formed. The impl is legal if the compiler manages to do -so. - -Coming to the definition of `WellFormed(Type: Trait)`, it would be tempting -to define it as: -```rust,ignore -trait Trait where WC1, WC2, ..., WCn { - ... -} -``` - -```text -forall { - WellFormed(Type: Trait) :- WC1 && WC2 && .. && WCn. -} -``` -and indeed this was basically what was done in rustc until it was noticed that -this mixed badly with implied bounds. The key thing is that implied bounds -allows someone to derive all bounds implied by a fact in the environment, and -this *transitively* as we've seen with the `A + B + C` traits example. -However, the `WellFormed` predicate as defined above only checks that the -*direct* superbounds hold. That is, if we come back to our `A + B + C` -example: -```rust,ignore -trait A { } -// No where clauses, always well-formed. -// forall { WellFormed(Type: A). } - -trait B where Self: A { } -// We only check the direct superbound `Self: A`. -// forall { WellFormed(Type: B) :- Implemented(Type: A). } - -trait C where Self: B { } -// We only check the direct superbound `Self: B`. We do not check -// the `Self: A` implied bound coming from the `Self: B` superbound. -// forall { WellFormed(Type: C) :- Implemented(Type: B). } -``` -There is an asymmetry between the recursive power of implied bounds and -the shallow checking of `WellFormed`. It turns out that this asymmetry -can be [exploited][bug]. Indeed, suppose that we define the following -traits: -```rust,ignore -trait Partial where Self: Copy { } -// WellFormed(Self: Partial) :- Implemented(Self: Copy). - -trait Complete where Self: Partial { } -// WellFormed(Self: Complete) :- Implemented(Self: Partial). - -impl Partial for T where T: Complete { } - -impl Complete for T { } -``` - -For the `Partial` impl, what the compiler must prove is: -```text -forall { - if (T: Complete) { // assume that the where clauses hold - WellFormed(T: Partial) // show that the trait reference is well-formed - } -} -``` -Proving `WellFormed(T: Partial)` amounts to proving `Implemented(T: Copy)`. -However, we have `Implemented(T: Complete)` in our environment: thanks to -implied bounds, we can deduce `Implemented(T: Partial)`. Using implied bounds -one level deeper, we can deduce `Implemented(T: Copy)`. Finally, the `Partial` -impl is legal. - -For the `Complete` impl, what the compiler must prove is: -```text -forall { - WellFormed(T: Complete) // show that the trait reference is well-formed -} -``` -Proving `WellFormed(T: Complete)` amounts to proving `Implemented(T: Partial)`. -We see that the `impl Partial for T` applies if we can prove -`Implemented(T: Complete)`, and it turns out we can prove this fact since our -`impl Complete for T` is a blanket impl without any where clauses. - -So both impls are legal and the compiler accepts the program. Moreover, thanks -to the `Complete` blanket impl, all types implement `Complete`. So we could -now use this impl like so: -```rust,ignore -fn eat(x: T) { } - -fn copy_everything(x: T) { - eat(x); - eat(x); -} - -fn main() { - let not_copiable = vec![1, 2, 3, 4]; - copy_everything(not_copiable); -} -``` -In this program, we use the fact that `Vec` implements `Complete`, as any -other type. Hence we can call `copy_everything` with an argument of type -`Vec`. Inside the `copy_everything` function, we have the -`Implemented(T: Complete)` bound in our environment. Thanks to implied bounds, -we can deduce `Implemented(T: Partial)`. Using implied bounds again, we deduce -`Implemented(T: Copy)` and we can indeed call the `eat` function which moves -the argument twice since its argument is `Copy`. Problem: the `T` type was -in fact `Vec` which is not copy at all, hence we will double-free the -underlying vec storage so we have a memory unsoundness in safe Rust. - -Of course, disregarding the asymmetry between `WellFormed` and implied bounds, -this bug was possible only because we had some kind of self-referencing impls. -But self-referencing impls are very useful in practice and are not the real -culprits in this affair. - -[bug]: https://github.com/rust-lang/rust/pull/43786 - -## Co-inductiveness of `WellFormed` - -So the solution is to fix this asymmetry between `WellFormed` and implied -bounds. For that, we need for the `WellFormed` predicate to not only require -that the direct superbounds hold, but also all the bounds transitively implied -by the superbounds. What we can do is to have the following rules for the -`WellFormed` predicate: -```rust,ignore -trait A { } -// WellFormed(Self: A) :- Implemented(Self: A). - -trait B where Self: A { } -// WellFormed(Self: B) :- Implemented(Self: B) && WellFormed(Self: A). - -trait C where Self: B { } -// WellFormed(Self: C) :- Implemented(Self: C) && WellFormed(Self: B). -``` - -Notice that we are now also requiring `Implemented(Self: Trait)` for -`WellFormed(Self: Trait)` to be true: this is to simplify the process of -traversing all the implied bounds transitively. This does not change anything -when checking whether impls are legal, because since we assume -that the where clauses hold inside the impl, we know that the corresponding -trait reference do hold. Thanks to this setup, you can see that we indeed -require to prove the set of all bounds transitively implied by the where -clauses. - -However there is still a catch. Suppose that we have the following trait -definition: -```rust,ignore -trait Foo where ::Item: Foo { - type Item; -} -``` - -so this definition is a bit more involved than the ones we've seen already -because it defines an associated item. However, the well-formedness rule -would not be more complicated: -```text -WellFormed(Self: Foo) :- - Implemented(Self: Foo) && - WellFormed(::Item: Foo). -``` - -Now we would like to write the following impl: -```rust,ignore -impl Foo for i32 { - type Item = i32; -} -``` -The `Foo` trait definition and the `impl Foo for i32` are perfectly valid -Rust: we're kind of recursively using our `Foo` impl in order to show that -the associated value indeed implements `Foo`, but that's ok. But if we -translate this to our well-formedness setting, the compiler proof process -inside the `Foo` impl is the following: it starts with proving that the -well-formedness goal `WellFormed(i32: Foo)` is true. In order to do that, -it must prove the following goals: `Implemented(i32: Foo)` and -`WellFormed(::Item: Foo)`. `Implemented(i32: Foo)` holds because -there is our impl and there are no where clauses on it so it's always true. -However, because of the associated type value we used, -`WellFormed(::Item: Foo)` simplifies to just -`WellFormed(i32: Foo)`. So in order to prove its original goal -`WellFormed(i32: Foo)`, the compiler needs to prove `WellFormed(i32: Foo)`: -this clearly is a cycle and cycles are usually rejected by the trait solver, -unless... if the `WellFormed` predicate was made to be co-inductive. - -A co-inductive predicate, as discussed in the chapter on -[goals and clauses](./goals-and-clauses.md#coinductive-goals), are predicates -for which the -trait solver accepts cycles. In our setting, this would be a valid thing to do: -indeed, the `WellFormed` predicate just serves as a way of enumerating all -the implied bounds. Hence, it's like a fixed point algorithm: it tries to grow -the set of implied bounds until there is nothing more to add. Here, a cycle -in the chain of `WellFormed` predicates just means that there is no more bounds -to add in that direction, so we can just accept this cycle and focus on other -directions. It's easy to prove that under these co-inductive semantics, we -are effectively visiting all the transitive implied bounds, and only these. - -## Implied bounds on types - -We mainly talked about implied bounds for traits because this was the most -subtle regarding implementation. Implied bounds on types are simpler, -especially because if we assume that a type is well-formed, we don't use that -fact to deduce that other types are well-formed, we only use it to deduce -that e.g. some trait bounds hold. - -For types, we just use rules like these ones: -```rust,ignore -struct Type<...> where WC1, ..., WCn { - ... -} -``` - -```text -forall<...> { - WellFormed(Type<...>) :- WC1, ..., WCn. -} - -forall<...> { - FromEnv(WC1) :- FromEnv(Type<...>). - ... - FromEnv(WCn) :- FromEnv(Type<...>). -} -``` -We can see that we have this asymmetry between well-formedness check, -which only verifies that the direct superbounds hold, and implied bounds which -gives access to all bounds transitively implied by the where clauses. In that -case this is ok because as we said, we don't use `FromEnv(Type<...>)` to deduce -other `FromEnv(OtherType<...>)` things, nor do we use `FromEnv(Type: Trait)` to -deduce `FromEnv(OtherType<...>)` things. So in that sense type definitions are -"less recursive" than traits, and we saw in a previous subsection that -it was the combination of asymmetry and recursive trait / impls that led to -unsoundness. As such, the `WellFormed(Type<...>)` predicate does not need -to be co-inductive. - -This asymmetry optimization is useful because in a real Rust program, we have -to check the well-formedness of types very often (e.g. for each type which -appears in the body of a function). diff --git a/src/traits/index.md b/src/traits/index.md deleted file mode 100644 index 5544ce513..000000000 --- a/src/traits/index.md +++ /dev/null @@ -1,64 +0,0 @@ -# Trait solving (new-style) - -> 🚧 This chapter describes "new-style" trait solving. This is still in the -> [process of being implemented][wg]; this chapter serves as a kind of -> in-progress design document. If you would prefer to read about how the -> current trait solver works, check out -> [this other chapter](./resolution.html). 🚧 -> -> By the way, if you would like to help in hacking on the new solver, you will -> find instructions for getting involved in the -> [Traits Working Group tracking issue][wg]! - -[wg]: https://github.com/rust-lang/rust/issues/48416 - -The new-style trait solver is based on the work done in [chalk][chalk]. Chalk -recasts Rust's trait system explicitly in terms of logic programming. It does -this by "lowering" Rust code into a kind of logic program we can then execute -queries against. - -You can read more about chalk itself in the -[Overview of Chalk](./chalk-overview.md) section. - -Trait solving in rustc is based around a few key ideas: - -- [Lowering to logic](./lowering-to-logic.html), which expresses - Rust traits in terms of standard logical terms. - - The [goals and clauses](./goals-and-clauses.html) chapter - describes the precise form of rules we use, and - [lowering rules](./lowering-rules.html) gives the complete set of - lowering rules in a more reference-like form. - - [Lazy normalization](./associated-types.html), which is the - technique we use to accommodate associated types when figuring out - whether types are equal. - - [Region constraints](./regions.html), which are accumulated - during trait solving but mostly ignored. This means that trait - solving effectively ignores the precise regions involved, always – - but we still remember the constraints on them so that those - constraints can be checked by the type checker. -- [Canonical queries](./canonical-queries.html), which allow us - to solve trait problems (like "is `Foo` implemented for the type - `Bar`?") once, and then apply that same result independently in many - different inference contexts. - -> This is not a complete list of topics. See the sidebar for more. - -## Ongoing work -The design of the new-style trait solving currently happens in two places: - -**chalk**. The [chalk][chalk] repository is where we experiment with new ideas -and designs for the trait system. It primarily consists of two parts: -* a unit testing framework - for the correctness and feasibility of the logical rules defining the - new-style trait system. -* the [`chalk_engine`][chalk_engine] crate, which - defines the new-style trait solver used both in the unit testing framework - and in rustc. - -**rustc**. Once we are happy with the logical rules, we proceed to -implementing them in rustc. This mainly happens in -[`librustc_traits`][librustc_traits]. - -[chalk]: https://github.com/rust-lang/chalk -[chalk_engine]: https://github.com/rust-lang/chalk/tree/master/chalk-engine -[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits diff --git a/src/traits/lowering-module.md b/src/traits/lowering-module.md index 3c5bd7be5..8795cb79c 100644 --- a/src/traits/lowering-module.md +++ b/src/traits/lowering-module.md @@ -1,56 +1,3 @@ # The lowering module in rustc -The program clauses described in the -[lowering rules](./lowering-rules.html) section are actually -created in the [`rustc_traits::lowering`][lowering] module. - -[lowering]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_traits/lowering/ - -## The `program_clauses_for` query - -The main entry point is the `program_clauses_for` [query], which – -given a `DefId` – produces a set of Chalk program clauses. The -query is invoked on a `DefId` that identifies something like a trait, -an impl, or an associated item definition. It then produces and -returns a vector of program clauses. - -[query]: ../query.html - -## Unit tests - -**Note: We've removed the Chalk unit tests in [rust-lang/rust#69247]. -They will come back once we're ready to integrate next Chalk into rustc.** - -Here's a good example test. At the time of -this writing, it looked like this: - -```rust,ignore -#![feature(rustc_attrs)] - -trait Foo { } - -#[rustc_dump_program_clauses] //~ ERROR program clause dump -impl Foo for T where T: Iterator { } - -fn main() { - println!("hello"); -} -``` - -The `#[rustc_dump_program_clauses]` annotation can be attached to -anything with a `DefId` (It requires the `rustc_attrs` feature). The -compiler will then invoke the `program_clauses_for` query on that -item, and emit compiler errors that dump the clauses produced. These -errors just exist for unit-testing. The stderr will be: - -```text -error: program clause dump - --> $DIR/lower_impl.rs:5:1 - | -LL | #[rustc_dump_program_clauses] - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - | - = note: forall { Implemented(T: Foo) :- ProjectionEq(::Item == i32), TypeOutlives(T: 'static), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized). } -``` - -[rust-lang/rust#69247]: https://github.com/rust-lang/rust/pull/69247 +This work is ongoing. This section will be filled in once some of it has landed in `rustc`. diff --git a/src/traits/lowering-rules.md b/src/traits/lowering-rules.md deleted file mode 100644 index c780e7cf5..000000000 --- a/src/traits/lowering-rules.md +++ /dev/null @@ -1,416 +0,0 @@ -# Lowering rules - -This section gives the complete lowering rules for Rust traits into -[program clauses][pc]. It is a kind of reference. These rules -reference the [domain goals][dg] defined in an earlier section. - -[pc]: ./goals-and-clauses.html -[dg]: ./goals-and-clauses.html#domain-goals - -## Notation - -The nonterminal `Pi` is used to mean some generic *parameter*, either a -named lifetime like `'a` or a type parameter like `A`. - -The nonterminal `Ai` is used to mean some generic *argument*, which -might be a lifetime like `'a` or a type like `Vec`. - -When defining the lowering rules, we will give goals and clauses in -the [notation given in this section](./goals-and-clauses.html). -We sometimes insert "macros" like `LowerWhereClause!` into these -definitions; these macros reference other sections within this chapter. - -## Rule names and cross-references - -Each of these lowering rules is given a name, documented with a -comment like so: - - // Rule Foo-Bar-Baz - -The reference implementation of these rules is to be found in -[`chalk/chalk-solve/src/clauses.rs`][chalk_rules]. They are also ported in -rustc in the [`librustc_traits`][librustc_traits] crate. - -[chalk_rules]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/clauses.rs -[librustc_traits]: https://github.com/rust-lang/rust/tree/master/src/librustc_traits - -## Lowering where clauses - -When used in a goal position, where clauses can be mapped directly to -the `Holds` variant of [domain goals][dg], as follows: - -- `A0: Foo` maps to `Implemented(A0: Foo)` -- `T: 'r` maps to `Outlives(T, 'r)` -- `'a: 'b` maps to `Outlives('a, 'b)` -- `A0: Foo` is a bit special and expands to two distinct - goals, namely `Implemented(A0: Foo)` and - `ProjectionEq(>::Item = T)` - -In the rules below, we will use `WC` to indicate where clauses that -appear in Rust syntax; we will then use the same `WC` to indicate -where those where clauses appear as goals in the program clauses that -we are producing. In that case, the mapping above is used to convert -from the Rust syntax into goals. - -### Transforming the lowered where clauses - -In addition, in the rules below, we sometimes do some transformations -on the lowered where clauses, as defined here: - -- `FromEnv(WC)` – this indicates that: - - `Implemented(TraitRef)` becomes `FromEnv(TraitRef)` - - other where-clauses are left intact -- `WellFormed(WC)` – this indicates that: - - `Implemented(TraitRef)` becomes `WellFormed(TraitRef)` - - other where-clauses are left intact - -*TODO*: I suspect that we want to alter the outlives relations too, -but Chalk isn't modeling those right now. - -## Lowering traits - -Given a trait definition - -```rust,ignore -trait Trait // P0 == Self -where WC -{ - // trait items -} -``` - -we will produce a number of declarations. This section is focused on -the program clauses for the trait header (i.e., the stuff outside the -`{}`); the [section on trait items](#trait-items) covers the stuff -inside the `{}`. - -### Trait header - -From the trait itself we mostly make "meta" rules that setup the -relationships between different kinds of domain goals. The first such -rule from the trait header creates the mapping between the `FromEnv` -and `Implemented` predicates: - -```text -// Rule Implemented-From-Env -forall { - Implemented(Self: Trait) :- FromEnv(Self: Trait) -} -``` - - - -#### Implied bounds - -The next few clauses have to do with implied bounds (see also -[RFC 2089] and the [implied bounds][implied_bounds] chapter for a more in depth -cover). For each trait, we produce two clauses: - -[RFC 2089]: https://rust-lang.github.io/rfcs/2089-implied-bounds.html -[implied_bounds]: ./implied-bounds.md - -```text -// Rule Implied-Bound-From-Trait -// -// For each where clause WC: -forall { - FromEnv(WC) :- FromEnv(Self: Trait) -} -``` - -This clause says that if we are assuming that the trait holds, then we can also -assume that its where-clauses hold. It's perhaps useful to see an example: - -```rust,ignore -trait Eq: PartialEq { ... } -``` - -In this case, the `PartialEq` supertrait is equivalent to a `where -Self: PartialEq` where clause, in our simplified model. The program -clause above therefore states that if we can prove `FromEnv(T: Eq)` – -e.g., if we are in some function with `T: Eq` in its where clauses – -then we also know that `FromEnv(T: PartialEq)`. Thus the set of things -that follow from the environment are not only the **direct where -clauses** but also things that follow from them. - -The next rule is related; it defines what it means for a trait reference -to be **well-formed**: - -```text -// Rule WellFormed-TraitRef -forall { - WellFormed(Self: Trait) :- Implemented(Self: Trait) && WellFormed(WC) -} -``` - -This `WellFormed` rule states that `T: Trait` is well-formed if (a) -`T: Trait` is implemented and (b) all the where-clauses declared on -`Trait` are well-formed (and hence they are implemented). Remember -that the `WellFormed` predicate is -[coinductive](./goals-and-clauses.html#coinductive); in this -case, it is serving as a kind of "carrier" that allows us to enumerate -all the where clauses that are transitively implied by `T: Trait`. - -An example: - -```rust,ignore -trait Foo: A + Bar { } -trait Bar: B + Foo { } -trait A { } -trait B { } -``` - -Here, the transitive set of implications for `T: Foo` are `T: A`, `T: Bar`, and -`T: B`. And indeed if we were to try to prove `WellFormed(T: Foo)`, we would -have to prove each one of those: - -- `WellFormed(T: Foo)` - - `Implemented(T: Foo)` - - `WellFormed(T: A)` - - `Implemented(T: A)` - - `WellFormed(T: Bar)` - - `Implemented(T: Bar)` - - `WellFormed(T: B)` - - `Implemented(T: Bar)` - - `WellFormed(T: Foo)` -- cycle, true coinductively - -This `WellFormed` predicate is only used when proving that impls are -well-formed – basically, for each impl of some trait ref `TraitRef`, -we must show that `WellFormed(TraitRef)`. This in turn justifies the -implied bounds rules that allow us to extend the set of `FromEnv` -items. - -## Lowering type definitions - -We also want to have some rules which define when a type is well-formed. -For example, given this type: - -```rust,ignore -struct Set where K: Hash { ... } -``` - -then `Set` is well-formed because `i32` implements `Hash`, but -`Set` would not be well-formed. Basically, a type is well-formed -if its parameters verify the where clauses written on the type definition. - -Hence, for every type definition: - -```rust, ignore -struct Type where WC { ... } -``` - -we produce the following rule: - -```text -// Rule WellFormed-Type -forall { - WellFormed(Type) :- WC -} -``` - -Note that we use `struct` for defining a type, but this should be understood -as a general type definition (it could be e.g. a generic `enum`). - -Conversely, we define rules which say that if we assume that a type is -well-formed, we can also assume that its where clauses hold. That is, -we produce the following family of rules: - -```text -// Rule Implied-Bound-From-Type -// -// For each where clause `WC` -forall { - FromEnv(WC) :- FromEnv(Type) -} -``` - -As for the implied bounds RFC, functions will *assume* that their arguments -are well-formed. For example, suppose we have the following bit of code: - -```rust,ignore -trait Hash: Eq { } -struct Set { ... } - -fn foo(collection: Set, x: K, y: K) { - // `x` and `y` can be equalized even if we did not explicitly write - // `where K: Eq` - if x == y { - ... - } -} -``` - -In the `foo` function, we assume that `Set` is well-formed, i.e. we have -`FromEnv(Set)` in our environment. Because of the previous rule, we get - `FromEnv(K: Hash)` without needing an explicit where clause. And because -of the `Hash` trait definition, there also exists a rule which says: - -```text -forall { - FromEnv(K: Eq) :- FromEnv(K: Hash) -} -``` - -which means that we finally get `FromEnv(K: Eq)` and then can compare `x` -and `y` without needing an explicit where clause. - - - -## Lowering trait items - -### Associated type declarations - -Given a trait that declares a (possibly generic) associated type: - -```rust,ignore -trait Trait // P0 == Self -where WC -{ - type AssocType: Bounds where WC1; -} -``` - -We will produce a number of program clauses. The first two define -the rules by which `ProjectionEq` can succeed; these two clauses are discussed -in detail in the [section on associated types](./associated-types.html), -but reproduced here for reference: - -```text -// Rule ProjectionEq-Normalize -// -// ProjectionEq can succeed by normalizing: -forall { - ProjectionEq(>::AssocType = U) :- - Normalize(>::AssocType -> U) -} -``` - -```text -// Rule ProjectionEq-Placeholder -// -// ProjectionEq can succeed through the placeholder associated type, -// see "associated type" chapter for more: -forall { - ProjectionEq( - >::AssocType = - (Trait::AssocType) - ) -} -``` - -The next rule covers implied bounds for the projection. In particular, -the `Bounds` declared on the associated type must have been proven to hold -to show that the impl is well-formed, and hence we can rely on them -elsewhere. - -```text -// Rule Implied-Bound-From-AssocTy -// -// For each `Bound` in `Bounds`: -forall { - FromEnv(>::AssocType>: Bound) :- - FromEnv(Self: Trait) && WC1 -} -``` - -Next, we define the requirements for an instantiation of our associated -type to be well-formed... - -```text -// Rule WellFormed-AssocTy -forall { - WellFormed((Trait::AssocType)) :- - Implemented(Self: Trait) && WC1 -} -``` - -...along with the reverse implications, when we can assume that it is -well-formed. - -```text -// Rule Implied-WC-From-AssocTy -// -// For each where clause WC1: -forall { - FromEnv(WC1) :- FromEnv((Trait::AssocType)) -} -``` - -```text -// Rule Implied-Trait-From-AssocTy -forall { - FromEnv(Self: Trait) :- - FromEnv((Trait::AssocType)) -} -``` - -### Lowering function and constant declarations - -Chalk didn't model functions and constants, but I would eventually like to -treat them exactly like normalization. See [the section on function/constant -values below](#constant-vals) for more details. - -## Lowering impls - -Given an impl of a trait: - -```rust,ignore -impl Trait for A0 -where WC -{ - // zero or more impl items -} -``` - -Let `TraitRef` be the trait reference `A0: Trait`. Then we -will create the following rules: - -```text -// Rule Implemented-From-Impl -forall { - Implemented(TraitRef) :- WC -} -``` - -In addition, we will lower all of the *impl items*. - -## Lowering impl items - -### Associated type values - -Given an impl that contains: - -```rust,ignore -impl Trait for P0 -where WC_impl -{ - type AssocType = T; -} -``` - -and our where clause `WC1` on the trait associated type from above, we -produce the following rule: - -```text -// Rule Normalize-From-Impl -forall { - forall { - Normalize(>::AssocType -> T) :- - Implemented(P0 as Trait) && WC1 - } -} -``` - -Note that `WC_impl` and `WC1` both encode where-clauses that the impl can -rely on. (`WC_impl` is not used here, because it is implied by -`Implemented(P0 as Trait)`.) - - - -### Function and constant values - -Chalk didn't model functions and constants, but I would eventually -like to treat them exactly like normalization. This presumably -involves adding a new kind of parameter (constant), and then having a -`NormalizeValue` domain goal. This is *to be written* because the -details are a bit up in the air. diff --git a/src/traits/lowering-to-logic.md b/src/traits/lowering-to-logic.md index e1a6c1361..cc8b3bf80 100644 --- a/src/traits/lowering-to-logic.md +++ b/src/traits/lowering-to-logic.md @@ -168,10 +168,10 @@ the body". But it's nice to know the proper name, because there is a lot of work describing how to efficiently handle FOHH clauses; see for example Gopalan Nadathur's excellent ["A Proof Procedure for the Logic of Hereditary Harrop Formulas"][pphhf] -in [the bibliography]. +in [the bibliography of Chalk Book][bibliography]. -[the bibliography]: ./bibliography.html -[pphhf]: ./bibliography.html#pphhf +[bibliography]: https://rust-lang.github.io/chalk/book/bibliography.html +[pphhf]: https://rust-lang.github.io/chalk/book/bibliography.html#pphhf It turns out that supporting FOHH is not really all that hard. And once we are able to do that, we can easily describe the type-checking diff --git a/src/traits/regions.md b/src/traits/regions.md deleted file mode 100644 index 4657529dc..000000000 --- a/src/traits/regions.md +++ /dev/null @@ -1,9 +0,0 @@ -# Region constraints - -*To be written.* - -Chalk does not have the concept of region constraints, and as of this -writing, work on rustc was not far enough to worry about them. - -In the meantime, you can read about region constraints in the -[type inference](../type-inference.html#region-constraints) section. diff --git a/src/traits/resolution.md b/src/traits/resolution.md index 2ba451677..7f73bfe4f 100644 --- a/src/traits/resolution.md +++ b/src/traits/resolution.md @@ -6,7 +6,7 @@ some non-obvious things. **Note:** This chapter (and its subchapters) describe how the trait solver **currently** works. However, we are in the process of designing a new trait solver. If you'd prefer to read about *that*, -see [*this* traits chapter](./index.html). +see [*this* subchapter](./chalk.html). ## Major concepts diff --git a/src/traits/slg.md b/src/traits/slg.md deleted file mode 100644 index 74ec89fa0..000000000 --- a/src/traits/slg.md +++ /dev/null @@ -1,302 +0,0 @@ -# The On-Demand SLG solver - -Given a set of program clauses (provided by our [lowering rules][lowering]) -and a query, we need to return the result of the query and the value of any -type variables we can determine. This is the job of the solver. - -For example, `exists { Vec: FromIterator }` has one solution, so -its result is `Unique; substitution [?T := u32]`. A solution also comes with -a set of region constraints, which we'll ignore in this introduction. - -[lowering]: ./lowering-rules.html - -## Goals of the Solver - -### On demand - -There are often many, or even infinitely many, solutions to a query. For -example, say we want to prove that `exists { Vec: Debug }` for _some_ -type `?T`. Our solver should be capable of yielding one answer at a time, say -`?T = u32`, then `?T = i32`, and so on, rather than iterating over every type -in the type system. If we need more answers, we can request more until we are -done. This is similar to how Prolog works. - -*See also: [The traditional, interactive Prolog query][pq]* - -[pq]: ./canonical-queries.html#the-traditional-interactive-prolog-query - -### Breadth-first - -`Vec: Debug` is true if `?T: Debug`. This leads to a cycle: `[Vec, -Vec>, Vec>>]`, and so on all implement `Debug`. Our -solver ought to be breadth first and consider answers like `[Vec: Debug, -Vec: Debug, ...]` before it recurses, or we may never find the answer -we're looking for. - -### Cachable - -To speed up compilation, we need to cache results, including partial results -left over from past solver queries. - -## Description of how it works - -The basis of the solver is the [`Forest`] type. A *forest* stores a -collection of *tables* as well as a *stack*. Each *table* represents -the stored results of a particular query that is being performed, as -well as the various *strands*, which are basically suspended -computations that may be used to find more answers. Tables are -interdependent: solving one query may require solving others. - -[`Forest`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html - -### Walkthrough - -Perhaps the easiest way to explain how the solver works is to walk -through an example. Let's imagine that we have the following program: - -```rust,ignore -trait Debug { } - -struct u32 { } -impl Debug for u32 { } - -struct Rc { } -impl Debug for Rc { } - -struct Vec { } -impl Debug for Vec { } -``` - -Now imagine that we want to find answers for the query `exists { Rc: -Debug }`. The first step would be to u-canonicalize this query; this is the -act of giving canonical names to all the unbound inference variables based on -the order of their left-most appearance, as well as canonicalizing the -universes of any universally bound names (e.g., the `T` in `forall { ... -}`). In this case, there are no universally bound names, but the canonical -form Q of the query might look something like: - -```text -Rc: Debug -``` - -where `?0` is a variable in the root universe U0. We would then go and -look for a table with this canonical query as the key: since the forest is -empty, this lookup will fail, and we will create a new table T0, -corresponding to the u-canonical goal Q. - -**Ignoring negative reasoning and regions.** To start, we'll ignore -the possibility of negative goals like `not { Foo }`. We'll phase them -in later, as they bring several complications. - -**Creating a table.** When we first create a table, we also initialize -it with a set of *initial strands*. A "strand" is kind of like a -"thread" for the solver: it contains a particular way to produce an -answer. The initial set of strands for a goal like `Rc: Debug` -(i.e., a "domain goal") is determined by looking for *clauses* in the -environment. In Rust, these clauses derive from impls, but also from -where-clauses that are in scope. In the case of our example, there -would be three clauses, each coming from the program. Using a -Prolog-like notation, these look like: - -```text -(u32: Debug). -(Rc: Debug) :- (T: Debug). -(Vec: Debug) :- (T: Debug). -``` - -To create our initial strands, then, we will try to apply each of -these clauses to our goal of `Rc: Debug`. The first and third -clauses are inapplicable because `u32` and `Vec` cannot be unified -with `Rc`. The second clause, however, will work. - -**What is a strand?** Let's talk a bit more about what a strand *is*. In the code, a strand -is the combination of an inference table, an _X-clause_, and (possibly) -a selected subgoal from that X-clause. But what is an X-clause -([`ExClause`], in the code)? An X-clause pulls together a few things: - -- The current state of the goal we are trying to prove; -- A set of subgoals that have yet to be proven; -- There are also a few things we're ignoring for now: - - delayed literals, region constraints - -The general form of an X-clause is written much like a Prolog clause, -but with somewhat different semantics. Since we're ignoring delayed -literals and region constraints, an X-clause just looks like this: - -```text -G :- L -``` - -where G is a goal and L is a set of subgoals that must be proven. -(The L stands for *literal* -- when we address negative reasoning, a -literal will be either a positive or negative subgoal.) The idea is -that if we are able to prove L then the goal G can be considered true. - -In the case of our example, we would wind up creating one strand, with -an X-clause like so: - -```text -(Rc: Debug) :- (?T: Debug) -``` - -Here, the `?T` refers to one of the inference variables created in the -inference table that accompanies the strand. (I'll use named variables -to refer to inference variables, and numbered variables like `?0` to -refer to variables in a canonicalized goal; in the code, however, they -are both represented with an index.) - -For each strand, we also optionally store a *selected subgoal*. This -is the subgoal after the turnstile (`:-`) that we are currently trying -to prove in this strand. Initially, when a strand is first created, -there is no selected subgoal. - -[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html - -**Activating a strand.** Now that we have created the table T0 and -initialized it with strands, we have to actually try and produce an answer. -We do this by invoking the [`ensure_root_answer`] operation on the table: -specifically, we say `ensure_root_answer(T0, A0)`, meaning "ensure that there -is a 0th answer A0 to query T0". - -Remember that tables store not only strands, but also a vector of cached -answers. The first thing that [`ensure_root_answer`] does is to check whether -answer A0 is in this vector. If so, we can just return immediately. In this -case, the vector will be empty, and hence that does not apply (this becomes -important for cyclic checks later on). - -When there is no cached answer, [`ensure_root_answer`] will try to produce one. -It does this by selecting a strand from the set of active strands -- the -strands are stored in a `VecDeque` and hence processed in a round-robin -fashion. Right now, we have only one strand, storing the following X-clause -with no selected subgoal: - -```text -(Rc: Debug) :- (?T: Debug) -``` - -When we activate the strand, we see that we have no selected subgoal, -and so we first pick one of the subgoals to process. Here, there is only -one (`?T: Debug`), so that becomes the selected subgoal, changing -the state of the strand to: - -```text -(Rc: Debug) :- selected(?T: Debug, A0) -``` - -Here, we write `selected(L, An)` to indicate that (a) the literal `L` -is the selected subgoal and (b) which answer `An` we are looking for. We -start out looking for `A0`. - -[`ensure_root_answer`]: https://rust-lang.github.io/chalk/chalk_engine/forest/struct.Forest.html#method.ensure_root_answer - -**Processing the selected subgoal.** Next, we have to try and find an -answer to this selected goal. To do that, we will u-canonicalize it -and try to find an associated table. In this case, the u-canonical -form of the subgoal is `?0: Debug`: we don't have a table yet for -that, so we can create a new one, T1. As before, we'll initialize T1 -with strands. In this case, there will be three strands, because all -the program clauses are potentially applicable. Those three strands -will be: - -- `(u32: Debug) :-`, derived from the program clause `(u32: Debug).`. - - Note: This strand has no subgoals. -- `(Vec: Debug) :- (?U: Debug)`, derived from the `Vec` impl. -- `(Rc: Debug) :- (?U: Debug)`, derived from the `Rc` impl. - -We can thus summarize the state of the whole forest at this point as -follows: - -```text -Table T0 [Rc: Debug] - Strands: - (Rc: Debug) :- selected(?T: Debug, A0) - -Table T1 [?0: Debug] - Strands: - (u32: Debug) :- - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -**Delegation between tables.** Now that the active strand from T0 has -created the table T1, it can try to extract an answer. It does this -via that same `ensure_answer` operation we saw before. In this case, -the strand would invoke `ensure_answer(T1, A0)`, since we will start -with the first answer. This will cause T1 to activate its first -strand, `u32: Debug :-`. - -This strand is somewhat special: it has no subgoals at all. This means -that the goal is proven. We can therefore add `u32: Debug` to the set -of *answers* for our table, calling it answer A0 (it is the first -answer). The strand is then removed from the list of strands. - -The state of table T1 is therefore: - -```text -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -Note that I am writing out the answer A0 as a substitution that can be -applied to the table goal; actually, in the code, the goals for each -X-clause are also represented as substitutions, but in this exposition -I've chosen to write them as full goals, following [NFTD]. - -[NFTD]: ./bibliography.html#slg - -Since we now have an answer, `ensure_answer(T1, A0)` will return `Ok` -to the table T0, indicating that answer A0 is available. T0 now has -the job of incorporating that result into its active strand. It does -this in two ways. First, it creates a new strand that is looking for -the next possible answer of T1. Next, it incorpoates the answer from -A0 and removes the subgoal. The resulting state of table T0 is: - -```text -Table T0 [Rc: Debug] - Strands: - (Rc: Debug) :- selected(?T: Debug, A1) - (Rc: Debug) :- -``` - -We then immediately activate the strand that incorporated the answer -(the `Rc: Debug` one). In this case, that strand has no further -subgoals, so it becomes an answer to the table T0. This answer can -then be returned up to our caller, and the whole forest goes quiescent -at this point (remember, we only do enough work to generate *one* -answer). The ending state of the forest at this point will be: - -```text -Table T0 [Rc: Debug] - Answer: - A0 = [?0 = u32] - Strands: - (Rc: Debug) :- selected(?T: Debug, A1) - -Table T1 [?0: Debug] - Answers: - A0 = [?0 = u32] - Strand: - (Vec: Debug) :- (?U: Debug) - (Rc: Debug) :- (?V: Debug) -``` - -Here you can see how the forest captures both the answers we have -created thus far *and* the strands that will let us try to produce -more answers later on. - -## See also - -- [chalk_solve README][readme], which contains links to papers used and - acronyms referenced in the code -- This section is a lightly adapted version of the blog post [An on-demand - SLG solver for chalk][slg-blog] -- [Negative Reasoning in Chalk][negative-reasoning-blog] explains the need - for negative reasoning, but not how the SLG solver does it - -[readme]: https://github.com/rust-lang/chalk/blob/239e4ae4e69b2785b5f99e0f2b41fc16b0b4e65e/chalk-engine/src/README.md -[slg-blog]: http://smallcultfollowing.com/babysteps/blog/2018/01/31/an-on-demand-slg-solver-for-chalk/ -[negative-reasoning-blog]: https://aturon.github.io/blog/2017/04/24/negative-chalk/ diff --git a/src/traits/wf.md b/src/traits/wf.md deleted file mode 100644 index aa17f8c2c..000000000 --- a/src/traits/wf.md +++ /dev/null @@ -1,469 +0,0 @@ -# Well-formedness checking - -WF checking has the job of checking that the various declarations in a Rust -program are well-formed. This is the basis for implied bounds, and partly for -that reason, this checking can be surprisingly subtle! For example, we -have to be sure that each impl proves the WF conditions declared on -the trait. - -For each declaration in a Rust program, we will generate a logical goal and try -to prove it using the lowered rules we described in the -[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we -say that the construct is well-formed. If not, we report an error to the user. - -Well-formedness checking happens in the [`chalk/chalk-solve/src/wf.rs`][wf] -module in chalk. After you have read this chapter, you may find useful to see -an extended set of examples in the [`chalk/tests/test/wf_lowering.rs`][wf_test] submodule. - -The new-style WF checking has not been implemented in rustc yet. - -[wf]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/wf.rs -[wf_test]: https://github.com/rust-lang/chalk/blob/master/tests/test/wf_lowering.rs - -We give here a complete reference of the generated goals for each Rust -declaration. - -In addition to the notations introduced in the chapter about -lowering rules, we'll introduce another notation: when checking WF of a -declaration, we'll often have to prove that all types that appear are -well-formed, except type parameters that we always assume to be WF. Hence, -we'll use the following notation: for a type `SomeType<...>`, we define -`InputTypes(SomeType<...>)` to be the set of all non-parameter types appearing -in `SomeType<...>`, including `SomeType<...>` itself. - -Examples: -* `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]` -* `InputTypes(Box) = [Box]` (assuming that `T` is a type parameter) -* `InputTypes(Box>) = [Box, Box>]` - -We also extend the `InputTypes` notation to where clauses in the natural way. -So, for example `InputTypes(A0: Trait)` is the union of -`InputTypes(A0)`, `InputTypes(A1)`, ..., `InputTypes(An)`. - -# Type definitions - -Given a general type definition: -```rust,ignore -struct Type where WC_type { - field1: A1, - ... - fieldn: An, -} -``` - -we generate the following goal, which represents its well-formedness condition: -```text -forall { - if (FromEnv(WC_type)) { - WellFormed(InputTypes(WC_type)) && - WellFormed(InputTypes(A1)) && - ... - WellFormed(InputTypes(An)) - } -} -``` - -which in English states: assuming that the where clauses defined on the type -hold, prove that every type appearing in the type definition is well-formed. - -Some examples: -```rust,ignore -struct OnlyClone where T: Clone { - clonable: T, -} -// The only types appearing are type parameters: we have nothing to check, -// the type definition is well-formed. -``` - -```rust,ignore -struct Foo where T: Clone { - foo: OnlyClone, -} -// The only non-parameter type which appears in this definition is -// `OnlyClone`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(T: Clone)) { -// WellFormed(OnlyClone) -// } -// } -// ``` -// which is provable. -``` - -```rust,ignore -struct Bar where ::Item: Debug { - bar: i32, -} -// The only non-parameter types which appear in this definition are -// `::Item` and `i32`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(::Item: Debug)) { -// WellFormed(::Item) && -// WellFormed(i32) -// } -// } -// ``` -// which is not provable since `WellFormed(::Item)` requires -// proving `Implemented(T: Iterator)`, and we are unable to prove that for an -// unknown `T`. -// -// Hence, this type definition is considered illegal. An additional -// `where T: Iterator` would make it legal. -``` - -# Trait definitions - -Given a general trait definition: -```rust,ignore -trait Trait where WC_trait { - type Assoc: Bounds_assoc where WC_assoc; -} -``` - -we generate the following goal: -```text -forall { - if (FromEnv(WC_trait)) { - WellFormed(InputTypes(WC_trait)) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(InputTypes(Bounds_assoc)) && - WellFormed(InputTypes(WC_assoc)) - } - } - } -} -``` - -There is not much to verify in a trait definition. We just want -to prove that the types appearing in the trait definition are well-formed, -under the assumption that the different where clauses hold. - -Some examples: -```rust,ignore -trait Foo where T: Iterator, ::Item: Debug { - ... -} -// The only non-parameter type which appears in this definition is -// `::Item`. The generated goal is the following: -// ``` -// forall { -// if (FromEnv(T: Iterator), FromEnv(::Item: Debug)) { -// WellFormed(::Item) -// } -// } -// ``` -// which is provable thanks to the `FromEnv(T: Iterator)` assumption. -``` - -```rust,ignore -trait Bar { - type Assoc: From<::Item>; -} -// The only non-parameter type which appears in this definition is -// `::Item`. The generated goal is the following: -// ``` -// forall { -// WellFormed(::Item) -// } -// ``` -// which is not provable, hence the trait definition is considered illegal. -``` - -```rust,ignore -trait Baz { - type Assoc: From<::Item> where T: Iterator; -} -// The generated goal is now: -// ``` -// forall { -// if (FromEnv(T: Iterator)) { -// WellFormed(::Item) -// } -// } -// ``` -// which is now provable. -``` - -# Impls - -Now we give ourselves a general impl for the trait defined above: -```rust,ignore -impl Trait for SomeType where WC_impl { - type Assoc = SomeValue where WC_assoc; -} -``` - -Note that here, `WC_assoc` are the same where clauses as those defined on the -associated type definition in the trait declaration, *except* that type -parameters from the trait are substituted with values provided by the impl -(see example below). You cannot add new where clauses. You may omit to write -the where clauses if you want to emphasize the fact that you are actually not -relying on them. - -Some examples to illustrate that: -```rust,ignore -trait Foo { - type Assoc where T: Clone; -} - -struct OnlyClone { ... } - -impl Foo> for () { - // We substitute type parameters from the trait by the ones provided - // by the impl, that is instead of having a `T: Clone` where clause, - // we have an `Option: Clone` one. - type Assoc = OnlyClone> where Option: Clone; -} - -impl Foo for i32 { - // I'm not using the `T: Clone` where clause from the trait, so I can - // omit it. - type Assoc = u32; -} - -impl Foo for f32 { - type Assoc = OnlyClone> where Option: Clone; - // ^^^^^^^^^^^^^^^^^^^^^^ - // this where clause does not exist - // on the original trait decl: illegal -} -``` - -> So in Rust, where clauses on associated types work *exactly* like where -> clauses on trait methods: in an impl, we must substitute the parameters from -> the traits with values provided by the impl, we may omit them if we don't -> need them, but we cannot add new where clauses. - -Now let's see the generated goal for this general impl: -```text -forall { - // Well-formedness of types appearing in the impl - if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType: Trait))) { - WellFormed(InputTypes(WC_impl)) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(InputTypes(SomeValue)) - } - } - } - - // Implied bounds checking - if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType: Trait))) { - WellFormed(SomeType: Trait) && - - forall { - if (FromEnv(WC_assoc)) { - WellFormed(SomeValue: Bounds_assoc) - } - } - } -} -``` - -Here is the most complex goal. As always, first, assuming that -the various where clauses hold, we prove that every type appearing in the impl -is well-formed, ***except*** types appearing in the impl header -`SomeType: Trait`. Instead, we *assume* that those types are -well-formed -(hence the `if (FromEnv(InputTypes(SomeType: Trait)))` -conditions). This is -part of the implied bounds proposal, so that we can rely on the bounds -written on the definition of e.g. the `SomeType` type (and that we don't -need to repeat those bounds). -> Note that we don't need to check well-formedness of types appearing in -> `WC_assoc` because we already did that in the trait decl (they are just -> repeated with some substitutions of values which we already assume to be -> well-formed) - -Next, still assuming that the where clauses on the impl `WC_impl` hold and that -the input types of `SomeType` are well-formed, we prove that -`WellFormed(SomeType: Trait)` hold. That is, we want to prove -that `SomeType` verify all the where clauses that might transitively -be required by the `Trait` definition (see -[this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)). - -Lastly, assuming in addition that the where clauses on the associated type -`WC_assoc` hold, -we prove that `WellFormed(SomeValue: Bounds_assoc)` hold. Again, we are -not only proving `Implemented(SomeValue: Bounds_assoc)`, but also -all the facts that might transitively come from `Bounds_assoc`. We must do this -because we allow the use of implied bounds on associated types: if we have -`FromEnv(SomeType: Trait)` in our environment, the lowering rules -chapter indicates that we are able to deduce -`FromEnv(::Assoc: Bounds_assoc)` without knowing what the -precise value of `::Assoc` is. - -Some examples for the generated goal: -```rust,ignore -// Trait Program Clauses - -// These are program clauses that come from the trait definitions below -// and that the trait solver can use for its reasonings. I'm just restating -// them here so that we have them in mind. - -trait Copy { } -// This is a program clause that comes from the trait definition above -// and that the trait solver can use for its reasonings. I'm just restating -// it here (and also the few other ones coming just after) so that we have -// them in mind. -// `WellFormed(Self: Copy) :- Implemented(Self: Copy).` - -trait Partial where Self: Copy { } -// ``` -// WellFormed(Self: Partial) :- -// Implemented(Self: Partial) && -// WellFormed(Self: Copy). -// ``` - -trait Complete where Self: Partial { } -// ``` -// WellFormed(Self: Complete) :- -// Implemented(Self: Complete) && -// WellFormed(Self: Partial). -// ``` - -// Impl WF Goals - -impl Partial for T where T: Complete { } -// The generated goal is: -// ``` -// forall { -// if (FromEnv(T: Complete)) { -// WellFormed(T: Partial) -// } -// } -// ``` -// Then proving `WellFormed(T: Partial)` amounts to proving -// `Implemented(T: Partial)` and `Implemented(T: Copy)`. -// Both those facts can be deduced from the `FromEnv(T: Complete)` in our -// environment: this impl is legal. - -impl Complete for T { } -// The generated goal is: -// ``` -// forall { -// WellFormed(T: Complete) -// } -// ``` -// Then proving `WellFormed(T: Complete)` amounts to proving -// `Implemented(T: Complete)`, `Implemented(T: Partial)` and -// `Implemented(T: Copy)`. -// -// `Implemented(T: Complete)` can be proved thanks to the -// `impl Complete for T` blanket impl. -// -// `Implemented(T: Partial)` can be proved thanks to the -// `impl Partial for T where T: Complete` impl and because we know -// `T: Complete` holds. - -// However, `Implemented(T: Copy)` cannot be proved: the impl is illegal. -// An additional `where T: Copy` bound would be sufficient to make that impl -// legal. -``` - -```rust,ignore -trait Bar { } - -impl Bar for T where ::Item: Bar { } -// We have a non-parameter type appearing in the where clauses: -// `::Item`. The generated goal is: -// ``` -// forall { -// if (FromEnv(::Item: Bar)) { -// WellFormed(T: Bar) && -// WellFormed(::Item: Bar) -// } -// } -// ``` -// And `WellFormed(::Item: Bar)` is not provable: we'd need -// an additional `where T: Iterator` for example. -``` - -```rust,ignore -trait Foo { } - -trait Bar { - type Item: Foo; -} - -struct Stuff { } - -impl Bar for Stuff where T: Foo { - type Item = T; -} -// The generated goal is: -// ``` -// forall { -// if (FromEnv(T: Foo)) { -// WellFormed(T: Foo). -// } -// } -// ``` -// which is provable. -``` - -```rust,ignore -trait Debug { ... } -// `WellFormed(Self: Debug) :- Implemented(Self: Debug).` - -struct Box { ... } -impl Debug for Box where T: Debug { ... } - -trait PointerFamily { - type Pointer: Debug where T: Debug; -} -// `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).` - -struct BoxFamily; - -impl PointerFamily for BoxFamily { - type Pointer = Box where T: Debug; -} -// The generated goal is: -// ``` -// forall { -// WellFormed(BoxFamily: PointerFamily) && -// -// if (FromEnv(T: Debug)) { -// WellFormed(Box: Debug) && -// WellFormed(Box) -// } -// } -// ``` -// `WellFormed(BoxFamily: PointerFamily)` amounts to proving -// `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl. -// -// `WellFormed(Box)` is always true (there are no where clauses on the -// `Box` type definition). -// -// Moreover, we have an `impl Debug for Box`, hence -// we can prove `WellFormed(Box: Debug)` and the impl is indeed legal. -``` - -```rust,ignore -trait Foo { - type Assoc; -} - -struct OnlyClone { ... } - -impl Foo for i32 { - type Assoc = OnlyClone; -} -// The generated goal is: -// ``` -// forall { -// WellFormed(i32: Foo) && -// WellFormed(OnlyClone) -// } -// ``` -// however `WellFormed(OnlyClone)` is not provable because it requires -// `Implemented(T: Clone)`. It would be tempting to just add a `where T: Clone` -// bound inside the `impl Foo for i32` block, however we saw that it was -// illegal to add where clauses that didn't come from the trait definition. -```