@@ -233,56 +233,79 @@ impl<T> Foo<T> for f32 {
233
233
}
234
234
```
235
235
236
- So where clauses on associated types work * exactly* like where clauses on
237
- trait methods: in an impl, we must substitute the parameters from the traits
238
- with values provided by the impl, we may omit them if we don't need them, but
239
- we cannot add new where clauses.
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
240
241
241
Now let's see the generated goal for this general impl:
242
242
``` text
243
243
forall<P1...> {
244
- if (FromEnv(WC_impl), FromEnv(InputTypes(SomeType<A2...>))) {
245
- WellFormed( SomeType<A2...>: Trait<A1...>) &&
246
- WellFormed(InputTypes(WC_impl)) &&
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
247
248
248
forall<P2...> {
249
249
if (FromEnv(WC_assoc)) {
250
- WellFormed(SomeValue<A3...>: Bounds_assoc) &&
251
250
WellFormed(InputTypes(SomeValue<A3...>))
252
251
}
253
252
}
254
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
+ }
255
265
}
256
266
```
257
267
258
268
Here is the most complex goal. As always, first, assuming that
259
269
the various where clauses hold, we prove that every type appearing in the impl
260
- is well-formed, *** except*** types appearing in the receiver type
261
- ` SomeType<A2...> ` . Instead, we * assume* that those types are well-formed
262
- (hence the ` if (FromEnv(InputTypes(SomeType<A2...>))) ` condition). This is
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
263
275
part of the implied bounds proposal, so that we can rely on the bounds
264
- written on the definition of the ` SomeType<A2...> ` type (and that we don't
276
+ written on the definition of e.g. the ` SomeType<A2...> ` type (and that we don't
265
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)
266
282
267
- Next, assuming that the where clauses on the impl ` WC_impl ` hold and that the
268
- input types of ` SomeType<A2...> ` are well-formed, we prove that
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
269
285
` WellFormed(SomeType<A2...>: Trait<A1...>) ` hold. That is, we want to prove
270
286
that ` SomeType<A2...> ` verify all the where clauses that might transitively
271
287
come from the ` Trait ` definition (see
272
288
[ this subsection] ( ./implied-bounds.md#co-inductiveness-of-wellformed ) ).
273
289
274
- Lastly, assuming that the where clauses on the associated type ` WC_assoc ` hold,
290
+ Lastly, assuming in addition that the where clauses on the associated type
291
+ ` WC_assoc ` hold,
275
292
we prove that ` WellFormed(SomeValue<A3...>: Bounds_assoc) ` hold. Again, we are
276
293
not only proving ` Implemented(SomeValue<A3...>: Bounds_assoc) ` , but also
277
- all the facts that might transitively come from ` Bounds_assoc ` . This is because
278
- we allow the use of implied bounds on associated types: if we have
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
279
296
` FromEnv(SomeType: Trait) ` in our environment, the lowering rules
280
297
chapter indicates that we are able to deduce
281
298
` FromEnv(<SomeType as Trait>::Assoc: Bounds_assoc) ` without knowing what the
282
299
precise value of ` <SomeType as Trait>::Assoc ` is.
283
300
284
301
Some examples for the generated goal:
285
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
+
286
309
trait Copy { }
287
310
// This is a program clause that comes from the trait definition above
288
311
// and that the trait solver can use for its reasonings. I'm just restating
@@ -304,6 +327,8 @@ trait Complete where Self: Partial { }
304
327
// WellFormed(Self: Partial).
305
328
// ```
306
329
330
+ // Impl WF Goals
331
+
307
332
impl<T> Partial for T where T: Complete { }
308
333
// The generated goal is:
309
334
// ```
0 commit comments