]>
Commit | Line | Data |
---|---|---|
a1dfa0c6 XL |
1 | # Well-formedness checking |
2 | ||
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 | |
6 | have to be sure that each impl proves the WF conditions declared on | |
7 | the trait. | |
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. | |
13 | ||
48663c56 XL |
14 | Well-formedness checking happens in the [`chalk/chalk-solve/src/wf.rs`][wf] |
15 | module in chalk. After you have read this chapter, you may find useful to see | |
60c5eb7d | 16 | an extended set of examples in the [`chalk/tests/test/wf_lowering.rs`][wf_test] submodule. |
a1dfa0c6 XL |
17 | |
18 | The new-style WF checking has not been implemented in rustc yet. | |
19 | ||
48663c56 | 20 | [wf]: https://github.com/rust-lang/chalk/blob/master/chalk-solve/src/wf.rs |
60c5eb7d | 21 | [wf_test]: https://github.com/rust-lang/chalk/blob/master/tests/test/wf_lowering.rs |
a1dfa0c6 XL |
22 | |
23 | We give here a complete reference of the generated goals for each Rust | |
24 | declaration. | |
25 | ||
26 | In addition to the notations introduced in the chapter about | |
27 | lowering rules, we'll introduce another notation: when checking WF of 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 define | |
31 | `InputTypes(SomeType<...>)` to be the set of all non-parameter types appearing | |
32 | in `SomeType<...>`, including `SomeType<...>` itself. | |
33 | ||
34 | Examples: | |
35 | * `InputTypes((u32, f32)) = [u32, f32, (u32, f32)]` | |
36 | * `InputTypes(Box<T>) = [Box<T>]` (assuming that `T` is a type parameter) | |
37 | * `InputTypes(Box<Box<T>>) = [Box<T>, Box<Box<T>>]` | |
38 | ||
39 | We also extend the `InputTypes` notation to where clauses in the natural way. | |
40 | So, for example `InputTypes(A0: Trait<A1,...,An>)` is the union of | |
41 | `InputTypes(A0)`, `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, which represents its well-formedness condition: | |
55 | ```text | |
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 states: 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 | ||
78 | ```rust,ignore | |
79 | struct Foo<T> where T: Clone { | |
80 | foo: OnlyClone<T>, | |
81 | } | |
82 | // The only non-parameter type which appears in this definition is | |
83 | // `OnlyClone<T>`. The generated goal is the following: | |
84 | // ``` | |
85 | // forall<T> { | |
86 | // if (FromEnv(T: Clone)) { | |
87 | // WellFormed(OnlyClone<T>) | |
88 | // } | |
89 | // } | |
90 | // ``` | |
91 | // which is provable. | |
92 | ``` | |
93 | ||
94 | ```rust,ignore | |
95 | struct Bar<T> where <T as Iterator>::Item: Debug { | |
96 | bar: i32, | |
97 | } | |
98 | // The only non-parameter types which appear in this definition are | |
99 | // `<T as Iterator>::Item` and `i32`. The generated goal is the following: | |
100 | // ``` | |
101 | // forall<T> { | |
102 | // if (FromEnv(<T as Iterator>::Item: Debug)) { | |
103 | // WellFormed(<T as Iterator>::Item) && | |
104 | // WellFormed(i32) | |
105 | // } | |
106 | // } | |
107 | // ``` | |
108 | // which is not provable since `WellFormed(<T as Iterator>::Item)` requires | |
109 | // proving `Implemented(T: Iterator)`, and we are unable to prove that for an | |
110 | // unknown `T`. | |
111 | // | |
112 | // Hence, this type definition is considered illegal. An additional | |
113 | // `where T: Iterator` would make it legal. | |
114 | ``` | |
115 | ||
116 | # Trait definitions | |
117 | ||
118 | Given a general trait definition: | |
119 | ```rust,ignore | |
120 | trait Trait<P1...> where WC_trait { | |
121 | type Assoc<P2...>: Bounds_assoc where WC_assoc; | |
122 | } | |
123 | ``` | |
124 | ||
125 | we generate the following goal: | |
126 | ```text | |
127 | forall<P1...> { | |
128 | if (FromEnv(WC_trait)) { | |
129 | WellFormed(InputTypes(WC_trait)) && | |
130 | ||
131 | forall<P2...> { | |
132 | if (FromEnv(WC_assoc)) { | |
133 | WellFormed(InputTypes(Bounds_assoc)) && | |
134 | WellFormed(InputTypes(WC_assoc)) | |
135 | } | |
136 | } | |
137 | } | |
138 | } | |
139 | ``` | |
140 | ||
141 | There is not much to verify in a trait definition. We just want | |
142 | to prove that the types appearing in the trait definition are well-formed, | |
143 | under the assumption that the different where clauses hold. | |
144 | ||
145 | Some examples: | |
146 | ```rust,ignore | |
147 | trait Foo<T> where T: Iterator, <T as Iterator>::Item: Debug { | |
148 | ... | |
149 | } | |
150 | // The only non-parameter type which appears in this definition is | |
151 | // `<T as Iterator>::Item`. The generated goal is the following: | |
152 | // ``` | |
153 | // forall<T> { | |
154 | // if (FromEnv(T: Iterator), FromEnv(<T as Iterator>::Item: Debug)) { | |
155 | // WellFormed(<T as Iterator>::Item) | |
156 | // } | |
157 | // } | |
158 | // ``` | |
159 | // which is provable thanks to the `FromEnv(T: Iterator)` assumption. | |
160 | ``` | |
161 | ||
162 | ```rust,ignore | |
163 | trait Bar { | |
164 | type Assoc<T>: From<<T as Iterator>::Item>; | |
165 | } | |
166 | // The only non-parameter type which appears in this definition is | |
167 | // `<T as Iterator>::Item`. The generated goal is the following: | |
168 | // ``` | |
169 | // forall<T> { | |
170 | // WellFormed(<T as Iterator>::Item) | |
171 | // } | |
172 | // ``` | |
173 | // which is not provable, hence the trait definition is considered illegal. | |
174 | ``` | |
175 | ||
176 | ```rust,ignore | |
177 | trait Baz { | |
178 | type Assoc<T>: From<<T as Iterator>::Item> where T: Iterator; | |
179 | } | |
180 | // The generated goal is now: | |
181 | // ``` | |
182 | // forall<T> { | |
183 | // if (FromEnv(T: Iterator)) { | |
184 | // WellFormed(<T as Iterator>::Item) | |
185 | // } | |
186 | // } | |
187 | // ``` | |
188 | // which is now provable. | |
189 | ``` | |
190 | ||
191 | # Impls | |
192 | ||
193 | Now we give ourselves a general impl for the trait defined above: | |
194 | ```rust,ignore | |
195 | impl<P1...> Trait<A1...> for SomeType<A2...> where WC_impl { | |
196 | type Assoc<P2...> = SomeValue<A3...> where WC_assoc; | |
197 | } | |
198 | ``` | |
199 | ||
200 | Note that here, `WC_assoc` are the same where clauses as those defined on the | |
201 | associated type definition in the trait declaration, *except* that type | |
202 | parameters from the trait are substituted with values provided by the impl | |
203 | (see example below). You cannot add new where clauses. You may omit to write | |
204 | the where clauses if you want to emphasize the fact that you are actually not | |
205 | relying on them. | |
206 | ||
207 | Some examples to illustrate that: | |
208 | ```rust,ignore | |
209 | trait Foo<T> { | |
210 | type Assoc where T: Clone; | |
211 | } | |
212 | ||
213 | struct OnlyClone<T: Clone> { ... } | |
214 | ||
215 | impl<U> Foo<Option<U>> for () { | |
216 | // We substitute type parameters from the trait by the ones provided | |
217 | // by the impl, that is instead of having a `T: Clone` where clause, | |
218 | // we have an `Option<U>: Clone` one. | |
219 | type Assoc = OnlyClone<Option<U>> where Option<U>: Clone; | |
220 | } | |
221 | ||
222 | impl<T> Foo<T> for i32 { | |
223 | // I'm not using the `T: Clone` where clause from the trait, so I can | |
224 | // omit it. | |
225 | type Assoc = u32; | |
226 | } | |
227 | ||
228 | impl<T> Foo<T> for f32 { | |
229 | type Assoc = OnlyClone<Option<T>> where Option<T>: Clone; | |
230 | // ^^^^^^^^^^^^^^^^^^^^^^ | |
231 | // this where clause does not exist | |
232 | // on the original trait decl: illegal | |
233 | } | |
234 | ``` | |
235 | ||
236 | > So in Rust, where clauses on associated types work *exactly* like where | |
237 | > clauses on trait methods: in an impl, we must substitute the parameters from | |
238 | > the traits with values provided by the impl, we may omit them if we don't | |
239 | > need them, but we cannot add new where clauses. | |
240 | ||
241 | Now let's see the generated goal for this general impl: | |
242 | ```text | |
243 | forall<P1...> { | |
244 | // Well-formedness of types appearing in the impl | |
245 | if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) { | |
246 | WellFormed(InputTypes(WC_impl)) && | |
247 | ||
248 | forall<P2...> { | |
249 | if (FromEnv(WC_assoc)) { | |
250 | WellFormed(InputTypes(SomeValue<A3...>)) | |
251 | } | |
252 | } | |
253 | } | |
254 | ||
255 | // Implied bounds checking | |
256 | if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>))) { | |
257 | WellFormed(SomeType<A2...>: Trait<A1...>) && | |
258 | ||
259 | forall<P2...> { | |
260 | if (FromEnv(WC_assoc)) { | |
261 | WellFormed(SomeValue<A3...>: Bounds_assoc) | |
262 | } | |
263 | } | |
264 | } | |
265 | } | |
266 | ``` | |
267 | ||
268 | Here is the most complex goal. As always, first, assuming that | |
269 | the various where clauses hold, we prove that every type appearing in the impl | |
270 | is well-formed, ***except*** types appearing in the impl header | |
271 | `SomeType<A2...>: Trait<A1...>`. Instead, we *assume* that those types are | |
272 | well-formed | |
273 | (hence the `if (FromEnv(InputTypes(SomeType<A2...>: Trait<A1...>)))` | |
274 | conditions). This is | |
275 | part of the implied bounds proposal, so that we can rely on the bounds | |
276 | written on the definition of e.g. the `SomeType<A2...>` type (and that we don't | |
277 | need to repeat those bounds). | |
278 | > Note that we don't need to check well-formedness of types appearing in | |
279 | > `WC_assoc` because we already did that in the trait decl (they are just | |
280 | > repeated with some substitutions of values which we already assume to be | |
281 | > well-formed) | |
282 | ||
283 | Next, still assuming that the where clauses on the impl `WC_impl` hold and that | |
284 | the input types of `SomeType<A2...>` are well-formed, we prove that | |
285 | `WellFormed(SomeType<A2...>: Trait<A1...>)` hold. That is, we want to prove | |
286 | that `SomeType<A2...>` verify all the where clauses that might transitively | |
287 | be required by the `Trait` definition (see | |
288 | [this subsection](./implied-bounds.md#co-inductiveness-of-wellformed)). | |
289 | ||
290 | Lastly, assuming in addition that the where clauses on the associated type | |
291 | `WC_assoc` hold, | |
292 | we prove that `WellFormed(SomeValue<A3...>: Bounds_assoc)` hold. Again, we are | |
293 | not only proving `Implemented(SomeValue<A3...>: Bounds_assoc)`, but also | |
294 | all the facts that might transitively come from `Bounds_assoc`. We must do this | |
295 | because we allow the use of implied bounds on associated types: if we have | |
296 | `FromEnv(SomeType: Trait)` in our environment, the lowering rules | |
297 | chapter indicates that we are able to deduce | |
298 | `FromEnv(<SomeType as Trait>::Assoc: Bounds_assoc)` without knowing what the | |
299 | precise value of `<SomeType as Trait>::Assoc` is. | |
300 | ||
301 | Some examples for the generated goal: | |
302 | ```rust,ignore | |
303 | // Trait Program Clauses | |
304 | ||
305 | // These are program clauses that come from the trait definitions below | |
306 | // and that the trait solver can use for its reasonings. I'm just restating | |
307 | // them here so that we have them in mind. | |
308 | ||
309 | trait Copy { } | |
310 | // This is a program clause that comes from the trait definition above | |
311 | // and that the trait solver can use for its reasonings. I'm just restating | |
312 | // it here (and also the few other ones coming just after) so that we have | |
313 | // them in mind. | |
314 | // `WellFormed(Self: Copy) :- Implemented(Self: Copy).` | |
315 | ||
316 | trait Partial where Self: Copy { } | |
317 | // ``` | |
318 | // WellFormed(Self: Partial) :- | |
319 | // Implemented(Self: Partial) && | |
320 | // WellFormed(Self: Copy). | |
321 | // ``` | |
322 | ||
323 | trait Complete where Self: Partial { } | |
324 | // ``` | |
325 | // WellFormed(Self: Complete) :- | |
326 | // Implemented(Self: Complete) && | |
327 | // WellFormed(Self: Partial). | |
328 | // ``` | |
329 | ||
330 | // Impl WF Goals | |
331 | ||
332 | impl<T> Partial for T where T: Complete { } | |
333 | // The generated goal is: | |
334 | // ``` | |
335 | // forall<T> { | |
336 | // if (FromEnv(T: Complete)) { | |
337 | // WellFormed(T: Partial) | |
338 | // } | |
339 | // } | |
340 | // ``` | |
341 | // Then proving `WellFormed(T: Partial)` amounts to proving | |
342 | // `Implemented(T: Partial)` and `Implemented(T: Copy)`. | |
343 | // Both those facts can be deduced from the `FromEnv(T: Complete)` in our | |
344 | // environment: this impl is legal. | |
345 | ||
346 | impl<T> Complete for T { } | |
347 | // The generated goal is: | |
348 | // ``` | |
349 | // forall<T> { | |
350 | // WellFormed(T: Complete) | |
351 | // } | |
352 | // ``` | |
353 | // Then proving `WellFormed(T: Complete)` amounts to proving | |
354 | // `Implemented(T: Complete)`, `Implemented(T: Partial)` and | |
355 | // `Implemented(T: Copy)`. | |
356 | // | |
357 | // `Implemented(T: Complete)` can be proved thanks to the | |
358 | // `impl<T> Complete for T` blanket impl. | |
359 | // | |
360 | // `Implemented(T: Partial)` can be proved thanks to the | |
361 | // `impl<T> Partial for T where T: Complete` impl and because we know | |
362 | // `T: Complete` holds. | |
363 | ||
364 | // However, `Implemented(T: Copy)` cannot be proved: the impl is illegal. | |
365 | // An additional `where T: Copy` bound would be sufficient to make that impl | |
366 | // legal. | |
367 | ``` | |
368 | ||
369 | ```rust,ignore | |
370 | trait Bar { } | |
371 | ||
372 | impl<T> Bar for T where <T as Iterator>::Item: Bar { } | |
373 | // We have a non-parameter type appearing in the where clauses: | |
374 | // `<T as Iterator>::Item`. The generated goal is: | |
375 | // ``` | |
376 | // forall<T> { | |
377 | // if (FromEnv(<T as Iterator>::Item: Bar)) { | |
378 | // WellFormed(T: Bar) && | |
379 | // WellFormed(<T as Iterator>::Item: Bar) | |
380 | // } | |
381 | // } | |
382 | // ``` | |
383 | // And `WellFormed(<T as Iterator>::Item: Bar)` is not provable: we'd need | |
384 | // an additional `where T: Iterator` for example. | |
385 | ``` | |
386 | ||
387 | ```rust,ignore | |
388 | trait Foo { } | |
389 | ||
390 | trait Bar { | |
391 | type Item: Foo; | |
392 | } | |
393 | ||
394 | struct Stuff<T> { } | |
395 | ||
396 | impl<T> Bar for Stuff<T> where T: Foo { | |
397 | type Item = T; | |
398 | } | |
399 | // The generated goal is: | |
400 | // ``` | |
401 | // forall<T> { | |
402 | // if (FromEnv(T: Foo)) { | |
403 | // WellFormed(T: Foo). | |
404 | // } | |
405 | // } | |
406 | // ``` | |
407 | // which is provable. | |
408 | ``` | |
409 | ||
410 | ```rust,ignore | |
411 | trait Debug { ... } | |
412 | // `WellFormed(Self: Debug) :- Implemented(Self: Debug).` | |
413 | ||
414 | struct Box<T> { ... } | |
415 | impl<T> Debug for Box<T> where T: Debug { ... } | |
416 | ||
417 | trait PointerFamily { | |
418 | type Pointer<T>: Debug where T: Debug; | |
419 | } | |
420 | // `WellFormed(Self: PointerFamily) :- Implemented(Self: PointerFamily).` | |
421 | ||
422 | struct BoxFamily; | |
423 | ||
424 | impl PointerFamily for BoxFamily { | |
425 | type Pointer<T> = Box<T> where T: Debug; | |
426 | } | |
427 | // The generated goal is: | |
428 | // ``` | |
429 | // forall<T> { | |
430 | // WellFormed(BoxFamily: PointerFamily) && | |
431 | // | |
432 | // if (FromEnv(T: Debug)) { | |
433 | // WellFormed(Box<T>: Debug) && | |
434 | // WellFormed(Box<T>) | |
435 | // } | |
436 | // } | |
437 | // ``` | |
438 | // `WellFormed(BoxFamily: PointerFamily)` amounts to proving | |
439 | // `Implemented(BoxFamily: PointerFamily)`, which is ok thanks to our impl. | |
440 | // | |
441 | // `WellFormed(Box<T>)` is always true (there are no where clauses on the | |
442 | // `Box` type definition). | |
443 | // | |
444 | // Moreover, we have an `impl<T: Debug> Debug for Box<T>`, hence | |
445 | // we can prove `WellFormed(Box<T>: Debug)` and the impl is indeed legal. | |
446 | ``` | |
447 | ||
448 | ```rust,ignore | |
449 | trait Foo { | |
450 | type Assoc<T>; | |
451 | } | |
452 | ||
453 | struct OnlyClone<T: Clone> { ... } | |
454 | ||
455 | impl Foo for i32 { | |
456 | type Assoc<T> = OnlyClone<T>; | |
457 | } | |
458 | // The generated goal is: | |
459 | // ``` | |
460 | // forall<T> { | |
461 | // WellFormed(i32: Foo) && | |
462 | // WellFormed(OnlyClone<T>) | |
463 | // } | |
464 | // ``` | |
465 | // however `WellFormed(OnlyClone<T>)` is not provable because it requires | |
466 | // `Implemented(T: Clone)`. It would be tempting to just add a `where T: Clone` | |
467 | // bound inside the `impl Foo for i32` block, however we saw that it was | |
468 | // illegal to add where clauses that didn't come from the trait definition. | |
469 | ``` |