diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 360265c0e..24af3bed5 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -117,6 +117,10 @@ - [Lowering to logic](./traits/lowering-to-logic.md) - [Goals and clauses](./traits/goals-and-clauses.md) - [Canonical queries](./traits/canonical-queries.md) + - [Next-gen trait solving](./solve/trait-solving.md) + - [The solver](./solve/the-solver.md) + - [Canonicalization](./solve/canonicalization.md) + - [Coinduction](./solve/coinduction.md) - [Type checking](./type-checking.md) - [Method Lookup](./method-lookup.md) - [Variance](./variance.md) diff --git a/src/solve/canonicalization.md b/src/solve/canonicalization.md new file mode 100644 index 000000000..e34b13bec --- /dev/null +++ b/src/solve/canonicalization.md @@ -0,0 +1,10 @@ +# Canonicalization + +While the exact approach to canonicalization for this solver will differ slightly +wrt to lifetimes, please visit [the relevant chalk chapter][chalk] for now. + + +As of 10 January 2023, canonicalization is not yet fully implemented +in the new solver. + +[chalk]: https://rust-lang.github.io/chalk/book/canonical_queries/canonicalization.html#canonicalization \ No newline at end of file diff --git a/src/solve/coinduction.md b/src/solve/coinduction.md new file mode 100644 index 000000000..c682e002d --- /dev/null +++ b/src/solve/coinduction.md @@ -0,0 +1,250 @@ +# Coinduction + +The trait solver may use coinduction when proving goals. +Coinduction is fairly subtle so we're giving it its own chapter. + +## Coinduction and induction + +With induction, we recursively apply proofs until we end up with a finite proof tree. +Consider the example of `Vec>>: Debug` which results in the following tree. + +- `Vec>>: Debug` + - `Vec>: Debug` + - `Vec: Debug` + - `u32: Debug` + +This tree is finite. But not all goals we would want to hold have finite proof trees, +consider the following example: + +```rust +struct List { + value: T, + next: Option>>, +} +``` + +For `List: Send` to hold all its fields have to recursively implement `Send` as well. +This would result in the following proof tree: + +- `List: Send` + - `T: Send` + - `Option>>: Send` + - `Box>: Send` + - `List: Send` + - `T: Send` + - `Option>>: Send` + - `Box>: Send` + - ... + +This tree would be infinitely large which is exactly what coinduction is about. + +> To **inductively** prove a goal you need to provide a finite proof tree for it. +> To **coinductively** prove a goal the provided proof tree may be infinite. + +## Why is coinduction correct + +When checking whether some trait goals holds, we're asking "does there exist an `impl` +which satisfies this bound". Even if are infinite chains of nested goals, we still have a +unique `impl` which should be used. + +## How to implement coinduction + +While our implementation can not check for coinduction by trying to construct an infinite +tree as that would take infinite resources, it still makes sense to think of coinduction +from this perspective. + +As we cannot check for infinite trees, we instead search for patterns for which we know that +they would result in an infinite proof tree. The currently pattern we detect are (canonical) +cycles. If `T: Send` relies on `T: Send` then it's pretty clear that this will just go on forever. + +With cycles we have to be careful with caching. Because of canonicalization of regions and +inference variables encountering a cycle doesn't mean that we would get an infinite proof tree. +Looking at the following example: +```rust +trait Foo {} +struct Wrapper(T); + +impl Foo for Wrapper> +where + Wrapper: Foo +{} +``` +Proving `Wrapper: Foo` uses the impl `impl Foo for Wrapper>` which constrains +`?0` to `Wrapper` and then requires `Wrapper: Foo`. Due to canonicalization this would be +detected as a cycle. + +The idea to solve is to return a *provisional result* whenever we detect a cycle and repeatedly +retry goals until the *provisional result* is equal to the final result of that goal. We +start out by using `Yes` with no constraints as the result and then update it to the result of +the previous iteration whenever we have to rerun. + +TODO: elaborate here. We use the same approach as chalk for coinductive cycles. +Note that the treatment for inductive cycles currently differs by simply returning `Overflow`. +See [the relevant chapters][chalk] in the chalk book. + +[chalk]: https://rust-lang.github.io/chalk/book/recursive/inductive_cycles.html + + +## Future work + +We currently only consider auto-traits, `Sized`, and `WF`-goals to be coinductive. +In the future we pretty much intend for all goals to be coinductive. +Lets first elaborate on why allowing more coinductive proofs is even desirable. + +### Recursive data types already rely on coinduction... + +...they just tend to avoid them in the trait solver. + +```rust +enum List { + Nil, + Succ(T, Box>), +} + +impl Clone for List { + fn clone(&self) -> Self { + match self { + List::Nil => List::Nil, + List::Succ(head, tail) => List::Succ(head.clone(), tail.clone()), + } + } +} +``` + +We are using `tail.clone()` in this impl. For this we have to prove `Box>: Clone` +which requires `List: Clone` but that relies on the impl which we are currently checking. +By adding that requirement to the `where`-clauses of the impl, which is what we would +do with [perfect derive], we move that cycle into the trait solver and [get an error][ex1]. + +### Recursive data types + +We also need coinduction to reason about recursive types containing projections, +e.g. the following currently fails to compile even though it should be valid. +```rust +use std::borrow::Cow; +pub struct Foo<'a>(Cow<'a, [Foo<'a>]>); +``` +This issue has been known since at least 2015, see +[#23714](https://github.com/rust-lang/rust/issues/23714) if you want to know more. + +### Explicitly checked implied bounds + +When checking an impl, we assume that the types in the impl headers are well-formed. +This means that when using instantiating the impl we have to prove that's actually the case. +[#100051](https://github.com/rust-lang/rust/issues/100051) shows that this is not the case. +To fix this, we have to add `WF` predicates for the types in impl headers. +Without coinduction for all traits, this even breaks `core`. + +```rust +trait FromResidual {} +trait Try: FromResidual<::Residual> { + type Residual; +} + +struct Ready(T); +impl Try for Ready { + type Residual = Ready<()>; +} +impl FromResidual< as Try>::Residual> for Ready {} +``` + +When checking that the impl of `FromResidual` is well formed we get the following cycle: + +The impl is well formed if ` as Try>::Residual` and `Ready` are well formed. +- `wf( as Try>::Residual)` requires +- `Ready: Try`, which requires because of the super trait +- `Ready: FromResidual as Try>::Residual>`, **because of implied bounds on impl** +- `wf( as Try>::Residual)` :tada: **cycle** + +### Issues when extending coinduction to more goals + +There are some additional issues to keep in mind when extending coinduction. +The issues here are not relevant for the current solver. + +#### Implied super trait bounds + +Our trait system currently treats super traits, e.g. `trait Trait: SuperTrait`, +by 1) requiring that `SuperTrait` has to hold for all types which implement `Trait`, +and 2) assuming `SuperTrait` holds if `Trait` holds. + +Relying on 2) while proving 1) is unsound. This can only be observed in case of +coinductive cycles. Without cycles, whenever we rely on 2) we must have also +proven 1) without relying on 2) for the used impl of `Trait`. + +```rust +trait Trait: SuperTrait {} + +impl Trait for T {} + +// Keeping the current setup for coinduction +// would allow this compile. Uff :< +fn sup() {} +fn requires_trait() { sup::() } +fn generic() { requires_trait::() } +``` +This is not really fundamental to coinduction but rather an existing property +which is made unsound because of it. + +##### Possible solutions + +The easiest way to solve this would be to completely remove 2) and always elaborate +`T: Trait` to `T: Trait` and `T: SuperTrait` outside of the trait solver. +This would allow us to also remove 1), but as we still have to prove ordinary +`where`-bounds on traits, that's just additional work. + +While one could imagine ways to disable cyclic uses of 2) when checking 1), +at least the ideas of myself - @lcnr - are all far to complex to be reasonable. + +#### `normalizes_to` goals and progress + +A `normalizes_to` goal represents the requirement that `::Assoc` normalizes +to some `U`. This is achieved by defacto first normalizing `::Assoc` and then +equating the resulting type with `U`. It should be a mapping as each projection should normalize +to exactly one type. By simply allowing infinite proof trees, we would get the following behavior: + +```rust +trait Trait { + type Assoc; +} + +impl Trait for () { + type Assoc = <() as Trait>::Assoc; +} +``` + +If we now compute `normalizes_to(<() as Trait>::Assoc, Vec)`, we would resolve the impl +and get the associated type `<() as Trait>::Assoc`. We then equate that with the expected type, +causing us to check `normalizes_to(<() as Trait>::Assoc, Vec)` again. +This just goes on forever, resulting in an infinite proof tree. + +This means that `<() as Trait>::Assoc` would be equal to any other type which is unsound. + +##### How to solve this + +**WARNING: THIS IS SUBTLE AND MIGHT BE WRONG** + +Unlike trait goals, `normalizes_to` has to be *productive*[^1]. A `normalizes_to` goal +is productive once the projection normalizes to a rigid type constructor, +so `<() as Trait>::Assoc` normalizing to `Vec<<() as Trait>::Assoc>` would be productive. + +A `normalizes_to` goal has two kinds of nested goals. Nested requirements needed to actually +normalize the projection, and the equality between the normalized projection and the +expected type. Only the equality has to be productive. A branch in the proof tree is productive +if it is either finite, or contains at least one `normalizes_to` where the alias is resolved +to a rigid type constructor. + +Alternatively, we could simply always treat the equate branch of `normalizes_to` as inductive. +Any cycles should result in infinite types, which aren't supported anyways and would only +result in overflow when deeply normalizing for codegen. + +experimentation and examples: https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view + +Another attempt at a summary. +- in projection eq, we must make progress with constraining the rhs +- a cycle is only ok if while equating we have a rigid ty on the lhs after norm at least once +- cycles outside of the recursive `eq` call of `normalizes_to` are always fine + +[^1]: related: https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions + +[perfect derive]: https://smallcultfollowing.com/babysteps/blog/2022/04/12/implied-bounds-and-perfect-derive +[ex1]: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0a9c3830b93a2380e6978d6328df8f72 diff --git a/src/solve/the-solver.md b/src/solve/the-solver.md new file mode 100644 index 000000000..38a85358c --- /dev/null +++ b/src/solve/the-solver.md @@ -0,0 +1,17 @@ +# The solver + +Also consider reading the documentation for [the recursive solver in chalk][chalk] +as it is very similar to this implementation and also talks about limitations of this +approach. + +[chalk]: https://rust-lang.github.io/chalk/book/recursive.html + +The basic structure of the solver is a pure function +`fn evaluate_goal(goal: Goal<'tcx>) -> Response`. +While the actual solver is not fully pure to deal with overflow and cycles, we are +going to defer that for now. + +To deal with inference variables and to improve caching, we use +[canonicalization](/canonicalization.html). + +TODO: write the remaining code for this as well. \ No newline at end of file diff --git a/src/solve/trait-solving.md b/src/solve/trait-solving.md new file mode 100644 index 000000000..4b78a21e1 --- /dev/null +++ b/src/solve/trait-solving.md @@ -0,0 +1,114 @@ +# Trait solving (new) + +This chapter describes how trait solving works with the new WIP solver located in +[`rustc_trait_selection/solve`][solve]. Feel free to also look at the docs for +[the current solver](../traits/resolution.hmtl) and [the chalk solver](./chalk.html) +can be found separately. + +## Core concepts + +The goal of the trait system is to check whether a given trait bound is satisfied. +Most notably when typechecking the body of - potentially generic - functions. +For example: + +```rust +fn uses_vec_clone(x: Vec) -> (Vec, Vec) { + (x.clone(), x) +} +``` +Here the call to `x.clone()` requires us to prove that `Vec` implements `Clone` given +the assumption that `T: Clone` is true. We can assume `T: Clone` as that will be proven by +callers of this function. + +The concept of "prove the `Vec: Clone` with the assumption `T: Clone`" is called a [`Goal`]. +Both `Vec: Clone` and `T: Clone` are represented using [`Predicate`]. There are other +predicates, most notably equality bounds on associated items: ` as IntoIterator>::Item == T`. +See the `PredicateKind` enum for an exhaustive list. A `Goal` is represented as the `predicate` we +have to prove and the `param_env` in which this predicate has to hold. + +We prove goals by checking whether each possible [`Candidate`] applies for the given goal by +recursively proving its nested goals. For a list of possible candidates with examples, look at +[`CandidateSource`]. The most important candidates are `Impl` candidates, i.e. trait implementations +written by the user, and `ParamEnv` candidates, i.e. assumptions in our current environment. + +Looking at the above example, to prove `Vec: Clone` we first use +`impl Clone for Vec`. To use this impl we have to prove the nested +goal that `T: Clone` holds. This can use the assumption `T: Clone` from the `ParamEnv` +which does not have any nested goals. Therefore `Vec: Clone` holds. + +The trait solver can either return success, ambiguity or an error as a [`CanonicalResponse`]. +For success and ambiguity it also returns constraints inference and region constraints. + +## Requirements + +Before we dive into the new solver lets first take the time to go through all of our requirements +on the trait system. We can then use these to guide our design later on. + +TODO: elaborate on these rules and get more precise about their meaning. +Also add issues where each of these rules have been broken in the past +(or still are). + +### 1. The trait solver has to be *sound* + +This means that we must never return *success* for goals for which no `impl` exists. That would +simply be unsound by assuming a trait is implemented even though it is not. When using predicates +from the `where`-bounds, the `impl` will be proved by the user of the item. + +### 2. If type checker solves generic goal concrete instantiations of that goal have the same result + +Pretty much: If we successfully typecheck a generic function concrete instantiations +of that function should also typeck. We should not get errors post-monomorphization. +We can however get overflow as in the following snippet: + +```rust +fn foo(x: ) +``` + +### 3. Trait goals in empty environments are proven by a unique impl. + +If a trait goal holds with an empty environment, there is a unique `impl`, +either user-defined or builtin, which is used to prove that goal. + +This is necessary for codegen to select a unique method. +An exception here are *marker traits* which are allowed to overlap. + +### 4. Normalization in empty environments results in a unique type + +Normalization for alias types/consts has a unique result. Otherwise we can easily implement +transmute in safe code. Given the following function, we have to make sure that the input and +output types always get normalized to the same concrete type. +```rust +fn foo( + x: ::Assoc +) -> ::Assoc { + x +} +``` + +### 5. During coherence trait solving has to be complete + +During coherence we never return *error* for goals which can be proven. This allows overlapping +impls which would break rule 3. + +### 6. Trait solving must be (free) lifetime agnostic + +Trait solving during codegen should have the same result as during typeck. As we erase +all free regions during codegen we must not rely on them during typeck. A noteworthy example +is special behavior for `'static`. + +### 7. Removing ambiguity makes strictly more things compile + +We *should* not rely on ambiguity for things to compile. +Not doing that will cause future improvements to be breaking changes. + +### 8. semantic equality implies structural equality + +Two types being equal in the type system must mean that they have the same `TypeId`. + + +[solve]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/index.html +[`Goal`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/struct.Goal.html +[`Predicate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/struct.Predicate.html +[`Candidate`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/assembly/struct.Candidate.html +[`CandidateSource`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/trait_goals/enum.CandidateSource.html +[`CanonicalResponse`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_trait_selection/solve/type.CanonicalResponse.html \ No newline at end of file