From 462b7c3558c3ba85dd001e8c1239cfdcd4165b42 Mon Sep 17 00:00:00 2001 From: scalexm Date: Wed, 17 Oct 2018 20:15:19 +0200 Subject: [PATCH 1/6] Write well-formedness checking chapter --- src/traits/wf.md | 268 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 263 insertions(+), 5 deletions(-) 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. From b5dff2ed5fc7ba2d7966ffd3c9275fd690a50236 Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 29 Oct 2018 15:54:37 +0100 Subject: [PATCH 2/6] Add some examples for impls --- src/traits/wf.md | 213 ++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 192 insertions(+), 21 deletions(-) diff --git a/src/traits/wf.md b/src/traits/wf.md index cd0fb556..bd1188d8 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -73,7 +73,9 @@ struct OnlyClone where T: Clone { } // 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, } @@ -87,23 +89,28 @@ struct Foo where T: Clone { // } // ``` // which is provable. +``` -struct Bar where OnlyClone: Debug { +```rust,ignore +struct Bar where ::Item: Debug { bar: i32, } -// The only non-parameter type which appears in this definition is -// `OnlyClone`. The generated goal is the following: +// The only non-parameter types which appear in this definition are +// `::Item` and `i32`. The generated goal is the following: // ``` // forall { -// if (FromEnv(OnlyClone: Debug)) { -// WellFormed(OnlyClone) +// if (FromEnv(::Item: Debug)) { +// WellFormed(::Item) && +// WellFormed(i32) // } // } // ``` -// which is not provable since `WellFormed(OnlyClone)` requires proving -// `Implemented(T: Clone)`, and we are unable to prove that for an unknown `T`. +// 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: Clone` would make it legal. +// `where T: Iterator` would make it legal. ``` # Trait definitions @@ -137,41 +144,47 @@ under the assumption that the different where clauses hold. Some examples: ```rust,ignore -struct OnlyClone { ... } - -trait Foo where T: Clone, OnlyClone: Debug { +trait Foo where T: Iterator, ::Item: Debug { ... } // The only non-parameter type which appears in this definition is -// `OnlyClone`. The generated goal is the following: +// `::Item`. The generated goal is the following: // ``` // forall { -// if (FromEnv(T: Clone), FromEnv(OnlyClone: Debug)) { -// WellFormed(OnlyClone) +// if (FromEnv(T: Iterator), FromEnv(::Item: Debug)) { +// WellFormed(::Item) // } // } // ``` -// which is provable thanks to the `FromEnv(T: Clone)` assumption. +// which is provable thanks to the `FromEnv(T: Iterator)` assumption. +``` +```rust,ignore trait Bar { - type Assoc: From>; + type Assoc: From<::Item>; } // The only non-parameter type which appears in this definition is -// `OnlyClone`. The generated goal is the following: +// `::Item`. The generated goal is the following: +// ``` // forall { -// WellFormed(OnlyClone) +// WellFormed(::Item) // } +// ``` // which is not provable, hence the trait definition is considered illegal. +``` +```rust,ignore trait Baz { - type Assoc: From> where T: Clone; + type Assoc: From<::Item> where T: Iterator; } // The generated goal is now: +// ``` // forall { -// if (FromEnv(T: Clone)) { -// WellFormed(OnlyClone) +// if (FromEnv(T: Iterator)) { +// WellFormed(::Item) // } // } +// ``` // which is now provable. ``` @@ -267,3 +280,161 @@ we allow the use of implied bounds on associated types: if we have 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 Copy { } +// `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 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 CowFamily { + type Pointer = Box where T: Debug; +} +// The generated goal is: +// ``` +// forall { +// WellFormed(CowFamily: PointerFamily) && +// +// if (FromEnv(T: Debug)) { +// WellFormed(Box: Debug) && +// WellFormed(Box) +// } +// } +// ``` +// `WellFormed(CowFamily: PointerFamily)` amounts to proving +// `Implemented(CowFamily: 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. +``` From 83652097f3f39c007318939355bf45b3fc6671de Mon Sep 17 00:00:00 2001 From: scalexm Date: Mon, 29 Oct 2018 18:58:13 +0100 Subject: [PATCH 3/6] Fix code blocks --- src/traits/wf.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/traits/wf.md b/src/traits/wf.md index bd1188d8..4cef9ec8 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -52,7 +52,7 @@ struct Type where WC_type { ``` we generate the following goal: -``` +```text forall { if (FromEnv(WC_type)) { WellFormed(InputTypes(WC_type)) && @@ -239,7 +239,7 @@ 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: -``` +```text forall { if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType))) { WellFormed(SomeType: Trait) && From e20f283a1e44d3616f80dea2fa5a67282664ed72 Mon Sep 17 00:00:00 2001 From: Who? Me?! Date: Mon, 29 Oct 2018 22:20:26 +0100 Subject: [PATCH 4/6] Fix a few things Co-Authored-By: scalexm --- src/traits/wf.md | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/src/traits/wf.md b/src/traits/wf.md index 4cef9ec8..ec391924 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -23,8 +23,8 @@ The new-style WF checking has not been implemented in rustc yet. 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 +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 denote @@ -212,11 +212,11 @@ trait Foo { struct OnlyClone { ... } -impl Foo> for () { +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; + // we have an `Option: Clone` one. + type Assoc = OnlyClone> where Option: Clone; } impl Foo for i32 { @@ -235,7 +235,7 @@ impl Foo for f32 { 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 +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: @@ -255,7 +255,7 @@ forall { } ``` -Here is the most complex goal. As always, a first thing is that assuming that +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 receiver type `SomeType`. Instead, we *assume* that those types are well-formed @@ -269,7 +269,7 @@ 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)). +[this subsection](./implied-bounds.md#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 @@ -284,6 +284,10 @@ precise value of `::Assoc` is. Some examples for the generated goal: ```rust,ignore 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 { } @@ -392,13 +396,13 @@ trait PointerFamily { struct BoxFamily; -impl PointerFamily for CowFamily { +impl PointerFamily for BoxFamily { type Pointer = Box where T: Debug; } // The generated goal is: // ``` // forall { -// WellFormed(CowFamily: PointerFamily) && +// WellFormed(BoxFamily: PointerFamily) && // // if (FromEnv(T: Debug)) { // WellFormed(Box: Debug) && @@ -406,8 +410,8 @@ impl PointerFamily for CowFamily { // } // } // ``` -// `WellFormed(CowFamily: PointerFamily)` amounts to proving -// `Implemented(CowFamily: PointerFamily)`, which is ok thanks to our impl. +// `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). From fe9dc61b8935742d40727af66e2ae110701f84fd Mon Sep 17 00:00:00 2001 From: Tyler Mandry Date: Tue, 30 Oct 2018 21:06:07 +0100 Subject: [PATCH 5/6] Fix a few more things Co-Authored-By: scalexm --- src/traits/wf.md | 59 ++++++++++++++++++++++++++++++++++-------------- 1 file changed, 42 insertions(+), 17 deletions(-) diff --git a/src/traits/wf.md b/src/traits/wf.md index ec391924..8c4938d3 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -233,49 +233,66 @@ impl Foo for f32 { } ``` -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, but -we cannot add new where clauses. +> 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 { - if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType))) { - WellFormed(SomeType: Trait) && - WellFormed(InputTypes(WC_impl)) && + // 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(SomeValue: Bounds_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 receiver type -`SomeType`. Instead, we *assume* that those types are well-formed -(hence the `if (FromEnv(InputTypes(SomeType)))` condition). This is +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 the `SomeType` type (and that we don't +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, assuming that the where clauses on the impl `WC_impl` hold and that the -input types of `SomeType` are well-formed, we prove that +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 come from the `Trait` definition (see [this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)). -Lastly, assuming that the where clauses on the associated type `WC_assoc` hold, +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`. This is because -we allow the use of implied bounds on associated types: if we have +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 @@ -283,6 +300,12 @@ 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 @@ -304,6 +327,8 @@ trait Complete where Self: Partial { } // WellFormed(Self: Partial). // ``` +// Impl WF Goals + impl Partial for T where T: Complete { } // The generated goal is: // ``` From cbb021e93f31d2b4c7f153232df03a7dd2859c14 Mon Sep 17 00:00:00 2001 From: scalexm Date: Fri, 2 Nov 2018 21:50:36 +0100 Subject: [PATCH 6/6] Fix nits --- src/traits/wf.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/traits/wf.md b/src/traits/wf.md index 8c4938d3..f0cb03ca 100644 --- a/src/traits/wf.md +++ b/src/traits/wf.md @@ -27,18 +27,18 @@ 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 denote -`InputTypes(SomeType<...>)` the set of all non-parameter types appearing in -`SomeType<...>`, including `SomeType<...>` itself. +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]` +* `InputTypes(Box) = [Box]` (assuming that `T` is a type parameter) * `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)`. +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 @@ -51,7 +51,7 @@ struct Type where WC_type { } ``` -we generate the following goal: +we generate the following goal, which represents its well-formedness condition: ```text forall { if (FromEnv(WC_type)) { @@ -63,7 +63,7 @@ forall { } ``` -which in English gives: assuming that the where clauses defined on the type +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: @@ -284,7 +284,7 @@ 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 -come from the `Trait` definition (see +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