Merge pull request #222 from scalexm/wf

Write well-formedness checking chapter

1 files changed, 463 insertions, 5 deletions

diff --git a/src/doc/rustc-dev-guide/src/traits/wf.md b/src/doc/rustc-dev-guide/src/traits/wf.md
index c002b8cc17b..f0cb03caab2 100644
--- a/src/doc/rustc-dev-guide/src/traits/wf.md
+++ b/src/doc/rustc-dev-guide/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<T>) = [Box<T>]` (assuming that `T` is a type parameter)
+* `InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]`
+
+We also extend the `InputTypes` notation to where clauses in the natural way.
+So, for example `InputTypes(A0: Trait<A1,...,An>)` is the union of
+`InputTypes(A0)`, `InputTypes(A1)`, ..., `InputTypes(An)`.
+
+# Type definitions
+
+Given a general type definition:
+```rust,ignore
+struct Type<P...> where WC_type {
+    field1: A1,
+    ...
+    fieldn: An,
+}
+```
+
+we generate the following goal, which represents its well-formedness condition:
+```text
+forall<P...> {
+    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<T> 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<T> where T: Clone {
+    foo: OnlyClone<T>,
+}
+// The only non-parameter type which appears in this definition is
+// `OnlyClone<T>`. The generated goal is the following:
+// ```
+// forall<T> {
+//     if (FromEnv(T: Clone)) {
+//          WellFormed(OnlyClone<T>)
+//     }
+// }
+// ```
+// which is provable.
+```
+
+```rust,ignore
+struct Bar<T> where <T as Iterator>::Item: Debug {
+    bar: i32,
+}
+// The only non-parameter types which appear in this definition are
+// `<T as Iterator>::Item` and `i32`. The generated goal is the following:
+// ```
+// forall<T> {
+//     if (FromEnv(<T as Iterator>::Item: Debug)) {
+//          WellFormed(<T as Iterator>::Item) &&
+//               WellFormed(i32)
+//     }
+// }
+// ```
+// which is not provable since `WellFormed(<T as Iterator>::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<P1...> where WC_trait {
+    type Assoc<P2...>: Bounds_assoc where WC_assoc;
+}
+```
+
+we generate the following goal:
+```text
+forall<P1...> {
+    if (FromEnv(WC_trait)) {
+        WellFormed(InputTypes(WC_trait)) &&
+
+            forall<P2...> {
+                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<T> where T: Iterator, <T as Iterator>::Item: Debug {
+    ...
+}
+// The only non-parameter type which appears in this definition is
+// `<T as Iterator>::Item`. The generated goal is the following:
+// ```
+// forall<T> {
+//     if (FromEnv(T: Iterator), FromEnv(<T as Iterator>::Item: Debug)) {
+//         WellFormed(<T as Iterator>::Item)
+//     }
+// }
+// ```
+// which is provable thanks to the `FromEnv(T: Iterator)` assumption.
+```
+
+```rust,ignore
+trait Bar {
+    type Assoc<T>: From<<T as Iterator>::Item>;
+}
+// The only non-parameter type which appears in this definition is
+// `<T as Iterator>::Item`. The generated goal is the following:
+// ```
+// forall<T> {
+//     WellFormed(<T as Iterator>::Item)
+// }
+// ```
+// which is not provable, hence the trait definition is considered illegal.
+```
+
+```rust,ignore
+trait Baz {
+    type Assoc<T>: From<<T as Iterator>::Item> where T: Iterator;
+}
+// The generated goal is now:
+// ```
+// forall<T> {
+//     if (FromEnv(T: Iterator)) {
+//         WellFormed(<T as Iterator>::Item)
+//     }
+// }
+// ```
+// which is now provable.
+```
+
+# Impls
+
+Now we give ourselves a general impl for the trait defined above:
+```rust,ignore
+impl<P1...> Trait<A1...> for SomeType<A2...> where WC_impl {
+    type Assoc<P2...> = SomeValue<A3...> 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<T> {
+    type Assoc where T: Clone;
+}
+
+struct OnlyClone<T: Clone> { ... }
+
+impl<U> Foo<Option<U>> 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<U>: Clone` one.
+    type Assoc = OnlyClone<Option<U>> where Option<U>: Clone;
+}
+
+impl<T> Foo<T> for i32 {
+    // I'm not using the `T: Clone` where clause from the trait, so I can
+    // omit it.
+    type Assoc = u32;
+}
+
+impl<T> Foo<T> for f32 {
+    type Assoc = OnlyClone<Option<T>> where Option<T>: 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<P1...> {
+    // Well-formedness of types appearing in the impl
+    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
+        WellFormed(InputTypes(WC_impl)) &&
+
+            forall<P2...> {
+                if (FromEnv(WC_assoc)) {
+                        WellFormed(InputTypes(SomeValue<A3...>))
+                }
+            }
+    }
+
+    // Implied bounds checking
+    if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) {
+        WellFormed(SomeType<A2...>: Trait<A1...>) &&
+
+            forall<P2...> {
+                if (FromEnv(WC_assoc)) {
+                    WellFormed(SomeValue<A3...>: 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<A2...>: Trait<A1...>`. Instead, we *assume* that those types are
+well-formed
+(hence the `if (FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>)))`
+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<A2...>` 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<A2...>` are well-formed, we prove that
+`WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove
+that `SomeType<A2...>` 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<A3...>: Bounds_assoc)` hold. Again, we are
+not only proving `Implemented(SomeValue<A3...>: 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(<SomeType as Trait>::Assoc: Bounds_assoc)` without knowing what the
+precise value of `<SomeType as Trait>::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<T> Partial for T where T: Complete { }
+// The generated goal is:
+// ```
+// forall<T> {
+//     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<T> Complete for T { }
+// The generated goal is:
+// ```
+// forall<T> {
+//     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<T> Complete for T` blanket impl.
+//
+// `Implemented(T: Partial)` can be proved thanks to the
+// `impl<T> 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<T> Bar for T where <T as Iterator>::Item: Bar { }
+// We have a non-parameter type appearing in the where clauses:
+// `<T as Iterator>::Item`. The generated goal is:
+// ```
+// forall<T> {
+//     if (FromEnv(<T as Iterator>::Item: Bar)) {
+//         WellFormed(T: Bar) &&
+//             WellFormed(<T as Iterator>::Item: Bar)
+//     }
+// }
+// ```
+// And `WellFormed(<T as Iterator>::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<T> { }
+
+impl<T> Bar for Stuff<T> where T: Foo {
+    type Item = T;
+}
+// The generated goal is:
+// ```
+// forall<T> {
+//     if (FromEnv(T: Foo)) {
+//         WellFormed(T: Foo).
+//     }
+// }
+// ```
+// which is provable.
+```
+
+```rust,ignore
+trait Debug { ... }
+// `WellFormed(Self: Debug) :- Implemented(Self: Debug).`
+
+struct Box<T> { ... }
+impl<T> Debug for Box<T> where T: Debug { ... }
+
+trait PointerFamily {
+    type Pointer<T>: Debug where T: Debug;
+}
+// `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).`
+
+struct BoxFamily;
+
+impl PointerFamily for BoxFamily {
+    type Pointer<T> = Box<T> where T: Debug;
+}
+// The generated goal is:
+// ```
+// forall<T> {
+//     WellFormed(BoxFamily: PointerFamily) &&
+//
+//     if (FromEnv(T: Debug)) {
+//         WellFormed(Box<T>: Debug) &&
+//             WellFormed(Box<T>)
+//     }
+// }
+// ```
+// `WellFormed(BoxFamily: PointerFamily)` amounts to proving
+// `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl.
+//
+// `WellFormed(Box<T>)` is always true (there are no where clauses on the
+// `Box` type definition).
+//
+// Moreover, we have an `impl<T: Debug> Debug for Box<T>`, hence
+// we can prove `WellFormed(Box<T>: Debug)` and the impl is indeed legal.
+```
+
+```rust,ignore
+trait Foo {
+    type Assoc<T>;
+}
+
+struct OnlyClone<T: Clone> { ... }
+
+impl Foo for i32 {
+    type Assoc<T> = OnlyClone<T>;
+}
+// The generated goal is:
+// ```
+// forall<T> {
+//     WellFormed(i32: Foo) &&
+//        WellFormed(OnlyClone<T>)
+// }
+// ```
+// however `WellFormed(OnlyClone<T>)` 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.
+```