diff --git a/src/traits/wf.md b/src/traits/wf.md index c002b8cc..cd0fb556 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -1,11 +1,269 @@ # 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 with the notations introduced in the chapter about +lowering rules, we'll introduce another notation: when WF checking 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 denote +`InputTypes(SomeType<...>)` the set of all non-parameter types appearing in +`SomeType<...>`, including `SomeType<...>` itself. + +Examples: +* `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]` +* `InputTypes(Box) = [Box]` +* `InputTypes(Box>) = [Box, Box>]` + +We may naturally extend the `InputTypes` notation to where clauses, 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: +``` +forall { + if (FromEnv(WC_type)) { + WellFormed(InputTypes(WC_type)) && + WellFormed(InputTypes(A1)) && + ... + WellFormed(InputTypes(An)) + } +} +``` + +which in English gives: 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. + +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. + +struct Bar where OnlyClone: Debug { + bar: i32, +} +// The only non-parameter type which appears in this definition is +// `OnlyClone`. The generated goal is the following: +// ``` +// forall { +// if (FromEnv(OnlyClone: Debug)) { +// WellFormed(OnlyClone) +// } +// } +// ``` +// which is not provable since `WellFormed(OnlyClone)` requires proving +// `Implemented(T: Clone)`, and we are unable to prove that for an unknown `T`. +// Hence, this type definition is considered illegal. An additional +// `where T: Clone` 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 +struct OnlyClone { ... } + +trait Foo where T: Clone, OnlyClone: Debug { + ... +} +// The only non-parameter type which appears in this definition is +// `OnlyClone`. The generated goal is the following: +// ``` +// forall { +// if (FromEnv(T: Clone), FromEnv(OnlyClone: Debug)) { +// WellFormed(OnlyClone) +// } +// } +// ``` +// which is provable thanks to the `FromEnv(T: Clone)` assumption. + +trait Bar { + type Assoc: From>; +} +// The only non-parameter type which appears in this definition is +// `OnlyClone`. The generated goal is the following: +// forall { +// WellFormed(OnlyClone) +// } +// which is not provable, hence the trait definition is considered illegal. + +trait Baz { + type Assoc: From> where T: Clone; +} +// The generated goal is now: +// forall { +// if (FromEnv(T: Clone)) { +// WellFormed(OnlyClone) +// } +// } +// 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 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, and +we cannot add new where clauses. + +Now let's see the generated goal for this general impl: +``` +forall { + if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType))) { + WellFormed(SomeType: Trait) && + WellFormed(InputTypes(WC_impl)) && + + forall { + if (FromEnv(WC_assoc)) { + WellFormed(SomeValue: Bounds_assoc) && + WellFormed(InputTypes(SomeValue)) + } + } + } +} +``` + +Here is the most complex goal. As always, a first thing is that assuming that +the various where clauses hold, we prove that every type appearing in the impl +is well-formed, ***except*** types appearing in the receiver type +`SomeType`. Instead, we *assume* that those types are well-formed +(hence the `if (FromEnv(InputTypes(SomeType)))` condition). This is +part of the implied bounds proposal, so that we can rely on the bounds +written on the definition of the `SomeType` type (and that we don't +need to repeat those bounds). + +Next, 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 +come from the `Trait` definition (see +[this subsection](./implied-bounds#co-inductiveness-of-wellformed)). + +Lastly, assuming 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`. This is 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.