|
1 | 1 | # Well-formedness checking
|
2 | 2 |
|
3 |
| -This chapter is mostly *to be written*. WF checking, in short, has the |
4 |
| -job of checking that the various declarations in a Rust program are |
5 |
| -well-formed. This is the basis for implied bounds, and partly for that |
6 |
| -reason, this checking can be surprisingly subtle! (For example, we |
| 3 | +WF checking has the job of checking that the various declarations in a Rust |
| 4 | +program are well-formed. This is the basis for implied bounds, and partly for |
| 5 | +that reason, this checking can be surprisingly subtle! For example, we |
7 | 6 | have to be sure that each impl proves the WF conditions declared on
|
8 |
| -the trait.) |
| 7 | +the trait. |
9 | 8 |
|
| 9 | +For each declaration in a Rust program, we will generate a logical goal and try |
| 10 | +to prove it using the lowered rules we described in the |
| 11 | +[lowering rules](./lowering-rules.md) chapter. If we are able to prove it, we |
| 12 | +say that the construct is well-formed. If not, we report an error to the user. |
10 | 13 |
|
| 14 | +Well-formedness checking happens in the [`src/rules/wf.rs`][wf] module in |
| 15 | +chalk. After you have read this chapter, you may find useful to see an |
| 16 | +extended set of examples in the [`src/rules/wf/test.rs`][wf_test] submodule. |
11 | 17 |
|
| 18 | +The new-style WF checking has not been implemented in rustc yet. |
| 19 | + |
| 20 | +[wf]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf.rs |
| 21 | +[wf_test]: https://github.com/rust-lang-nursery/chalk/blob/master/src/rules/wf/test.rs |
| 22 | + |
| 23 | +We give here a complete reference of the generated goals for each Rust |
| 24 | +declaration. |
| 25 | + |
| 26 | +In addition with the notations introduced in the chapter about |
| 27 | +lowering rules, we'll introduce another notation: when WF checking a |
| 28 | +declaration, we'll often have to prove that all types that appear are |
| 29 | +well-formed, except type parameters that we always assume to be WF. Hence, |
| 30 | +we'll use the following notation: for a type `SomeType<...>`, we denote |
| 31 | +`InputTypes(SomeType<...>)` the set of all non-parameter types appearing in |
| 32 | +`SomeType<...>`, including `SomeType<...>` itself. |
| 33 | + |
| 34 | +Examples: |
| 35 | +* `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]` |
| 36 | +* `InputTypes(Box<T>) = [Box<T>]` |
| 37 | +* `InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]` |
| 38 | + |
| 39 | +We may naturally extend the `InputTypes` notation to where clauses, for example |
| 40 | +`InputTypes(A0: Trait<A1,...,An>)` is the union of `InputTypes(A0)`, |
| 41 | +`InputTypes(A1)`, ..., `InputTypes(An)`. |
| 42 | + |
| 43 | +# Type definitions |
| 44 | + |
| 45 | +Given a general type definition: |
| 46 | +```rust,ignore |
| 47 | +struct Type<P...> where WC_type { |
| 48 | + field1: A1, |
| 49 | + ... |
| 50 | + fieldn: An, |
| 51 | +} |
| 52 | +``` |
| 53 | + |
| 54 | +we generate the following goal: |
| 55 | +``` |
| 56 | +forall<P...> { |
| 57 | + if (FromEnv(WC_type)) { |
| 58 | + WellFormed(InputTypes(WC_type)) && |
| 59 | + WellFormed(InputTypes(A1)) && |
| 60 | + ... |
| 61 | + WellFormed(InputTypes(An)) |
| 62 | + } |
| 63 | +} |
| 64 | +``` |
| 65 | + |
| 66 | +which in English gives: assuming that the where clauses defined on the type |
| 67 | +hold, prove that every type appearing in the type definition is well-formed. |
| 68 | + |
| 69 | +Some examples: |
| 70 | +```rust,ignore |
| 71 | +struct OnlyClone<T> where T: Clone { |
| 72 | + clonable: T, |
| 73 | +} |
| 74 | +// The only types appearing are type parameters: we have nothing to check, |
| 75 | +// the type definition is well-formed. |
| 76 | +
|
| 77 | +struct Foo<T> where T: Clone { |
| 78 | + foo: OnlyClone<T>, |
| 79 | +} |
| 80 | +// The only non-parameter type which appears in this definition is |
| 81 | +// `OnlyClone<T>`. The generated goal is the following: |
| 82 | +// ``` |
| 83 | +// forall<T> { |
| 84 | +// if (FromEnv(T: Clone)) { |
| 85 | +// WellFormed(OnlyClone<T>) |
| 86 | +// } |
| 87 | +// } |
| 88 | +// ``` |
| 89 | +// which is provable. |
| 90 | +
|
| 91 | +struct Bar<T> where OnlyClone<T>: Debug { |
| 92 | + bar: i32, |
| 93 | +} |
| 94 | +// The only non-parameter type which appears in this definition is |
| 95 | +// `OnlyClone<T>`. The generated goal is the following: |
| 96 | +// ``` |
| 97 | +// forall<T> { |
| 98 | +// if (FromEnv(OnlyClone<T>: Debug)) { |
| 99 | +// WellFormed(OnlyClone<T>) |
| 100 | +// } |
| 101 | +// } |
| 102 | +// ``` |
| 103 | +// which is not provable since `WellFormed(OnlyClone<T>)` requires proving |
| 104 | +// `Implemented(T: Clone)`, and we are unable to prove that for an unknown `T`. |
| 105 | +// Hence, this type definition is considered illegal. An additional |
| 106 | +// `where T: Clone` would make it legal. |
| 107 | +``` |
| 108 | + |
| 109 | +# Trait definitions |
| 110 | + |
| 111 | +Given a general trait definition: |
| 112 | +```rust,ignore |
| 113 | +trait Trait<P1...> where WC_trait { |
| 114 | + type Assoc<P2...>: Bounds_assoc where WC_assoc; |
| 115 | +} |
| 116 | +``` |
| 117 | + |
| 118 | +we generate the following goal: |
| 119 | +```text |
| 120 | +forall<P1...> { |
| 121 | + if (FromEnv(WC_trait)) { |
| 122 | + WellFormed(InputTypes(WC_trait)) && |
| 123 | +
|
| 124 | + forall<P2...> { |
| 125 | + if (FromEnv(WC_assoc)) { |
| 126 | + WellFormed(InputTypes(Bounds_assoc)) && |
| 127 | + WellFormed(InputTypes(WC_assoc)) |
| 128 | + } |
| 129 | + } |
| 130 | + } |
| 131 | +} |
| 132 | +``` |
| 133 | + |
| 134 | +There is not much to verify in a trait definition. We just want |
| 135 | +to prove that the types appearing in the trait definition are well-formed, |
| 136 | +under the assumption that the different where clauses hold. |
| 137 | + |
| 138 | +Some examples: |
| 139 | +```rust,ignore |
| 140 | +struct OnlyClone<T: Clone> { ... } |
| 141 | +
|
| 142 | +trait Foo<T> where T: Clone, OnlyClone<T>: Debug { |
| 143 | + ... |
| 144 | +} |
| 145 | +// The only non-parameter type which appears in this definition is |
| 146 | +// `OnlyClone<T>`. The generated goal is the following: |
| 147 | +// ``` |
| 148 | +// forall<T> { |
| 149 | +// if (FromEnv(T: Clone), FromEnv(OnlyClone<T>: Debug)) { |
| 150 | +// WellFormed(OnlyClone<T>) |
| 151 | +// } |
| 152 | +// } |
| 153 | +// ``` |
| 154 | +// which is provable thanks to the `FromEnv(T: Clone)` assumption. |
| 155 | +
|
| 156 | +trait Bar { |
| 157 | + type Assoc<T>: From<OnlyClone<T>>; |
| 158 | +} |
| 159 | +// The only non-parameter type which appears in this definition is |
| 160 | +// `OnlyClone<T>`. The generated goal is the following: |
| 161 | +// forall<T> { |
| 162 | +// WellFormed(OnlyClone<T>) |
| 163 | +// } |
| 164 | +// which is not provable, hence the trait definition is considered illegal. |
| 165 | +
|
| 166 | +trait Baz { |
| 167 | + type Assoc<T>: From<OnlyClone<T>> where T: Clone; |
| 168 | +} |
| 169 | +// The generated goal is now: |
| 170 | +// forall<T> { |
| 171 | +// if (FromEnv(T: Clone)) { |
| 172 | +// WellFormed(OnlyClone<T>) |
| 173 | +// } |
| 174 | +// } |
| 175 | +// which is now provable. |
| 176 | +``` |
| 177 | + |
| 178 | +# Impls |
| 179 | + |
| 180 | +Now we give ourselves a general impl for the trait defined above: |
| 181 | +```rust,ignore |
| 182 | +impl<P1...> Trait<A1...> for SomeType<A2...> where WC_impl { |
| 183 | + type Assoc<P2...> = SomeValue<A3...> where WC_assoc; |
| 184 | +} |
| 185 | +``` |
| 186 | + |
| 187 | +Note that here, `WC_assoc` are the same where clauses as those defined on the |
| 188 | +associated type definition in the trait declaration, *except* that type |
| 189 | +parameters from the trait are substituted with values provided by the impl |
| 190 | +(see example below). You cannot add new where clauses. You may omit to write |
| 191 | +the where clauses if you want to emphasize the fact that you are actually not |
| 192 | +relying on them. |
| 193 | + |
| 194 | +Some examples to illustrate that: |
| 195 | +```rust,ignore |
| 196 | +trait Foo<T> { |
| 197 | + type Assoc where T: Clone; |
| 198 | +} |
| 199 | +
|
| 200 | +struct OnlyClone<T: Clone> { ... } |
| 201 | +
|
| 202 | +impl<T> Foo<Option<T>> for () { |
| 203 | + // We substitute type parameters from the trait by the ones provided |
| 204 | + // by the impl, that is instead of having a `T: Clone` where clause, |
| 205 | + // we have an `Option<T>: Clone` one. |
| 206 | + type Assoc = OnlyClone<Option<T>> where Option<T>: Clone; |
| 207 | +} |
| 208 | +
|
| 209 | +impl<T> Foo<T> for i32 { |
| 210 | + // I'm not using the `T: Clone` where clause from the trait, so I can |
| 211 | + // omit it. |
| 212 | + type Assoc = u32; |
| 213 | +} |
| 214 | +
|
| 215 | +impl<T> Foo<T> for f32 { |
| 216 | + type Assoc = OnlyClone<Option<T>> where Option<T>: Clone; |
| 217 | + // ^^^^^^^^^^^^^^^^^^^^^^ |
| 218 | + // this where clause does not exist |
| 219 | + // on the original trait decl: illegal |
| 220 | +} |
| 221 | +``` |
| 222 | + |
| 223 | +So where clauses on associated types work *exactly* like where clauses on |
| 224 | +trait methods: in an impl, we must substitute the parameters from the traits |
| 225 | +with values provided by the impl, we may omit them if we don't need them, and |
| 226 | +we cannot add new where clauses. |
| 227 | + |
| 228 | +Now let's see the generated goal for this general impl: |
| 229 | +``` |
| 230 | +forall<P1...> { |
| 231 | + if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>))) { |
| 232 | + WellFormed(SomeType<A2...>: Trait<A1...>) && |
| 233 | + WellFormed(InputTypes(WC_impl)) && |
| 234 | +
|
| 235 | + forall<P2...> { |
| 236 | + if (FromEnv(WC_assoc)) { |
| 237 | + WellFormed(SomeValue<A3...>: Bounds_assoc) && |
| 238 | + WellFormed(InputTypes(SomeValue<A3...>)) |
| 239 | + } |
| 240 | + } |
| 241 | + } |
| 242 | +} |
| 243 | +``` |
| 244 | + |
| 245 | +Here is the most complex goal. As always, a first thing is that assuming that |
| 246 | +the various where clauses hold, we prove that every type appearing in the impl |
| 247 | +is well-formed, ***except*** types appearing in the receiver type |
| 248 | +`SomeType<A2...>`. Instead, we *assume* that those types are well-formed |
| 249 | +(hence the `if (FromEnv(InputTypes(SomeType<A2...>)))` condition). This is |
| 250 | +part of the implied bounds proposal, so that we can rely on the bounds |
| 251 | +written on the definition of the `SomeType<A2...>` type (and that we don't |
| 252 | +need to repeat those bounds). |
| 253 | + |
| 254 | +Next, assuming that the where clauses on the impl `WC_impl` hold and that the |
| 255 | +input types of `SomeType<A2...>` are well-formed, we prove that |
| 256 | +`WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove |
| 257 | +that `SomeType<A2...>` verify all the where clauses that might transitively |
| 258 | +come from the `Trait` definition (see |
| 259 | +[this subsection](./implied-bounds#co-inductiveness-of-wellformed)). |
| 260 | + |
| 261 | +Lastly, assuming that the where clauses on the associated type `WC_assoc` hold, |
| 262 | +we prove that `WellFormed(SomeValue<A3...>: Bounds_assoc)` hold. Again, we are |
| 263 | +not only proving `Implemented(SomeValue<A3...>: Bounds_assoc)`, but also |
| 264 | +all the facts that might transitively come from `Bounds_assoc`. This is because |
| 265 | +we allow the use of implied bounds on associated types: if we have |
| 266 | +`FromEnv(SomeType: Trait)` in our environment, the lowering rules |
| 267 | +chapter indicates that we are able to deduce |
| 268 | +`FromEnv(<SomeType as Trait>::Assoc: Bounds_assoc)` without knowing what the |
| 269 | +precise value of `<SomeType as Trait>::Assoc` is. |
0 commit comments