diff --git a/src/traits/wf.md b/src/traits/wf.md index c002b8cc..f0cb03ca 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -1,11 +1,469 @@ # Well-formedness checking -This chapter is mostly *to be written*. WF checking, in short, 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 +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.) +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 [`src/rules/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 [`src/rules/wf/test.rs`][wf_test] submodule. +The new-style WF checking has not been implemented in rustc yet. + +[wf]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf.rs +[wf_test]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf/test.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. +```