@@ -29,6 +29,7 @@ fn dyn_to_dyn_unsizing() {
2929 trait Auto3 { }
3030 }
3131
32+ // Tests with the same principal and auto traits
3233 goal {
3334 forall<' a> {
3435 forall<' b> {
@@ -39,6 +40,17 @@ fn dyn_to_dyn_unsizing() {
3940 "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!2_0 }]"
4041 }
4142
43+ goal {
44+ forall<' a> {
45+ forall<' b> {
46+ dyn Principal + Auto1 + Auto2 + Auto3 + ' a: Unsize <dyn Principal + Auto1 + Auto2 + Auto3 + ' b>
47+ }
48+ }
49+ } yields {
50+ "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!2_0 }]"
51+ }
52+
53+ // Target has a subset of source auto traits
4254 goal {
4355 forall<' a> {
4456 dyn Principal + Auto1 + Auto2 + ' a: Unsize <dyn Principal + Auto1 + ' a>
@@ -47,6 +59,7 @@ fn dyn_to_dyn_unsizing() {
4759 "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"
4860 }
4961
62+ // Both target and source don't have principal as their first trait
5063 goal {
5164 forall<' a> {
5265 dyn Auto1 + Principal + ' a: Unsize <dyn Auto1 + Principal + ' a>
@@ -55,6 +68,7 @@ fn dyn_to_dyn_unsizing() {
5568 "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"
5669 }
5770
71+ // Different order of traits in target and source
5872 // FIXME: this doesn't work because trait object unification
5973 // respects where clause order, which it shouldn't
6074 goal {
@@ -65,7 +79,7 @@ fn dyn_to_dyn_unsizing() {
6579 "No possible solution"
6680 }
6781
68- // Same as above
82+ // See above
6983 goal {
7084 forall<' a> {
7185 dyn Principal + Auto2 + Auto1 + ' a: Unsize <dyn Principal + Auto1 + Auto2 + ' a>
@@ -74,6 +88,7 @@ fn dyn_to_dyn_unsizing() {
7488 "No possible solution"
7589 }
7690
91+ // Source has a subset of auto traits of target
7792 goal {
7893 forall<' a> {
7994 dyn Principal + Auto2 + ' a: Unsize <dyn Principal + Auto1 + Auto2 + ' a>
@@ -82,6 +97,7 @@ fn dyn_to_dyn_unsizing() {
8297 "No possible solution"
8398 }
8499
100+ // Source and target have different set of auto traits
85101 goal {
86102 forall<' a> {
87103 dyn Principal + Auto1 + Auto2 + ' a: Unsize <dyn Principal + Auto1 + Auto3 + ' a>
@@ -90,6 +106,7 @@ fn dyn_to_dyn_unsizing() {
90106 "No possible solution"
91107 }
92108
109+ // Source has a principal trait, while target doesnt, both have the same auto traits.
93110 goal {
94111 forall<' a> {
95112 dyn Principal + Auto1 + ' a: Unsize <dyn Auto1 + ' a>
@@ -98,6 +115,7 @@ fn dyn_to_dyn_unsizing() {
98115 "No possible solution"
99116 }
100117
118+ // Non-matching principal traits
101119 goal {
102120 forall<' a> {
103121 dyn Principal + ' a: Unsize <dyn OtherPrincipal + ' a>
@@ -106,6 +124,7 @@ fn dyn_to_dyn_unsizing() {
106124 "No possible solution"
107125 }
108126
127+ // Matching generic principal traits
109128 goal {
110129 forall<' a> {
111130 dyn GenericPrincipal <u64 , Item = u64 > + ' a: Unsize <dyn GenericPrincipal <u64 , Item = u64 > + ' a>
@@ -114,6 +133,7 @@ fn dyn_to_dyn_unsizing() {
114133 "Unique; substitution [], lifetime constraints [InEnvironment { environment: Env([]), goal: '!1_0: '!1_0 }]"
115134 }
116135
136+ // Non-matching generic principal traits
117137 goal {
118138 forall<' a> {
119139 dyn GenericPrincipal <u32 , Item = u32 > + ' a: Unsize <dyn GenericPrincipal <u32 , Item = u64 > + ' a>
@@ -147,21 +167,21 @@ fn ty_to_dyn_unsizing() {
147167 trait Auto { }
148168
149169 struct Foo { }
170+ struct FooLifetime <' a> { }
150171 struct Bar { }
151172 struct Baz { }
152173 struct FooNotSized <T > {
153174 t: T
154175 }
155176
156177 impl Principal for Foo { }
157- impl Auto for Foo { }
158178 impl UnsafePrincipal for Foo { }
159179
180+ impl <' a> Principal for FooLifetime <' a> { }
181+
160182 impl Principal for Bar { }
161183 impl !Auto for Bar { }
162184
163- impl Auto for Baz { }
164-
165185 impl <T > Principal for FooNotSized <T > { }
166186
167187 impl GenericPrincipal <u32 > for Foo {
@@ -177,6 +197,7 @@ fn ty_to_dyn_unsizing() {
177197 "Unique; substitution [], lifetime constraints []"
178198 }
179199
200+ // Principal is not the first trait
180201 goal {
181202 forall<' a> {
182203 Foo : Unsize <dyn Auto + Principal + ' a>
@@ -185,6 +206,7 @@ fn ty_to_dyn_unsizing() {
185206 "Unique; substitution [], lifetime constraints []"
186207 }
187208
209+ // Auto-only trait object
188210 goal {
189211 forall<' a> {
190212 Foo : Unsize <dyn Auto + ' a>
@@ -193,6 +215,38 @@ fn ty_to_dyn_unsizing() {
193215 "Unique; substitution [], lifetime constraints []"
194216 }
195217
218+ // TypeOutlives tests
219+ goal {
220+ forall<' a> {
221+ FooLifetime <' a>: Unsize <dyn Principal + Auto + ' a>
222+ }
223+ } yields {
224+ "Unique; substitution [], lifetime constraints []"
225+ }
226+
227+ // FIXME: this shouldn't be provable, but currently
228+ // we have no `TypeOutlives` goal to check it
229+ goal {
230+ forall<' a, ' b> {
231+ FooLifetime <' a>: Unsize <dyn Principal + Auto + ' b>
232+ }
233+ } yields {
234+ "Unique; substitution [], lifetime constraints []"
235+ }
236+
237+ // This should produce 'a: 'b constraint, but for the reasons
238+ // above it doesn't
239+ goal {
240+ forall<' a> {
241+ exists<' b> {
242+ FooLifetime <' a>: Unsize <dyn Principal + Auto + ' b>
243+ }
244+ }
245+ } yields {
246+ "Unique; for<?U1> { substitution [?0 := '^0.0], lifetime constraints [] }"
247+ }
248+
249+ // Source does not implement auto trait (with principal)
196250 goal {
197251 forall<' a> {
198252 Bar : Unsize <dyn Principal + Auto + ' a>
@@ -201,6 +255,16 @@ fn ty_to_dyn_unsizing() {
201255 "No possible solution"
202256 }
203257
258+ // Source does not implement auto trait (without principal)
259+ goal {
260+ forall<' a> {
261+ Bar : Unsize <dyn Auto + ' a>
262+ }
263+ } yields {
264+ "No possible solution"
265+ }
266+
267+ // Source does not implement principal
204268 goal {
205269 forall<' a> {
206270 Baz : Unsize <dyn Principal + Auto + ' a>
@@ -209,6 +273,7 @@ fn ty_to_dyn_unsizing() {
209273 "No possible solution"
210274 }
211275
276+ // Implemeted generic principal
212277 goal {
213278 forall<' a> {
214279 Foo : Unsize <dyn GenericPrincipal <u32 , Item = u32 > + ' a>
@@ -217,6 +282,8 @@ fn ty_to_dyn_unsizing() {
217282 "Unique; substitution [], lifetime constraints []"
218283 }
219284
285+
286+ // Non-implemeted generic principal
220287 goal {
221288 forall<' a> {
222289 Foo : Unsize <dyn GenericPrincipal <u32 , Item = u64 > + ' a>
@@ -225,6 +292,7 @@ fn ty_to_dyn_unsizing() {
225292 "No possible solution"
226293 }
227294
295+ // Not object-safe principal trait
228296 goal {
229297 forall<' a> {
230298 Foo : Unsize <dyn UnsafePrincipal + ' a>
@@ -233,6 +301,7 @@ fn ty_to_dyn_unsizing() {
233301 "No possible solution"
234302 }
235303
304+ // Source ty is not Sized
236305 goal {
237306 forall<' a> {
238307 forall<T > {
@@ -243,6 +312,7 @@ fn ty_to_dyn_unsizing() {
243312 "No possible solution"
244313 }
245314
315+ // Sized counterpart for the previous test
246316 goal {
247317 forall<' a> {
248318 forall<T > {
@@ -296,6 +366,7 @@ fn tuple_unsizing() {
296366 "Unique; substitution [], lifetime constraints []"
297367 }
298368
369+ // Last field does not implement `Unsize`
299370 goal {
300371 forall<' a> {
301372 ( u32 , Foo ) : Unsize <( u32 , dyn OtherPrincipal + ' a) >
@@ -304,6 +375,7 @@ fn tuple_unsizing() {
304375 "No possible solution"
305376 }
306377
378+ // Mismatch of head fields
307379 goal {
308380 forall<' a> {
309381 ( u32 , Foo ) : Unsize <( u64 , dyn Principal + ' a) >
@@ -312,6 +384,7 @@ fn tuple_unsizing() {
312384 "No possible solution"
313385 }
314386
387+ // Tuple length mismatch
315388 goal {
316389 forall<' a> {
317390 ( u32 , u32 , Foo ) : Unsize <( u32 , dyn Principal + ' a) >
@@ -320,6 +393,7 @@ fn tuple_unsizing() {
320393 "No possible solution"
321394 }
322395
396+ // Multilevel tuple test
323397 goal {
324398 forall<' a> {
325399 ( u32 , ( u32 , Foo ) ) : Unsize <( u32 , ( u32 , dyn Principal + ' a) ) >
@@ -424,6 +498,7 @@ fn struct_unsizing() {
424498 impl Principal for Foo { }
425499 }
426500
501+ // Single field struct tests
427502 goal {
428503 Foo : Unsize <Foo >
429504 } yields {
@@ -446,6 +521,7 @@ fn struct_unsizing() {
446521 "No possible solution"
447522 }
448523
524+ // Unsizing parameter is used in head fields
449525 goal {
450526 forall<' a> {
451527 SParamsInMultipleFields <Foo >:
@@ -455,6 +531,7 @@ fn struct_unsizing() {
455531 "No possible solution"
456532 }
457533
534+ // Two-field struct test
458535 goal {
459536 forall<' a> {
460537 S12 <Foo , Foo >: Unsize <S12 <Foo , dyn Principal + ' a>>
@@ -463,6 +540,8 @@ fn struct_unsizing() {
463540 "Unique; substitution [], lifetime constraints []"
464541 }
465542
543+ // Test for the unsizing parameters collector
544+ // (checking that it ignores the binder inside `SWithBinders`)
466545 goal {
467546 forall<' a> {
468547 SWithBinders <Foo , Foo >: Unsize <SWithBinders <dyn Principal + ' a, Foo >>
@@ -471,6 +550,7 @@ fn struct_unsizing() {
471550 "Unique; substitution [], lifetime constraints []"
472551 }
473552
553+ // Non-trivial unsizing of the last field
474554 goal {
475555 forall<' a> {
476556 SNested <Foo , Bar <Foo >, Foo >: Unsize <SNested <Foo , Bar <Foo >, dyn Principal + ' a>>
@@ -487,6 +567,7 @@ fn struct_unsizing() {
487567 "No possible solution"
488568 }
489569
570+ // Check that lifetimes can't be used as unsizing parameters
490571 goal {
491572 forall<' a> {
492573 SLifetime <' a, Foo >: Unsize <SLifetime <' a, dyn Principal + ' a>>
@@ -495,18 +576,22 @@ fn struct_unsizing() {
495576 "Unique; substitution [], lifetime constraints []"
496577 }
497578
579+ // Tests with constant as an unsizing parameter
498580 goal {
499581 SGoodConst <5 , [ u32 ; 2 ] >: Unsize <SGoodConst <5 , [ u32 ] >>
500582 } yields {
501583 "Unique; substitution [], lifetime constraints []"
502584 }
503585
586+
587+ // Target does not match source
504588 goal {
505589 SGoodConst <4 , [ u32 ; 2 ] >: Unsize <SGoodConst <5 , [ u32 ] >>
506590 } yields {
507591 "No possible solution"
508592 }
509593
594+ // Unsizing parameter is used in head fields
510595 goal {
511596 SBadConst <5 , [ u32 ; 2 ] >: Unsize <SBadConst <5 , [ u32 ] >>
512597 } yields {
0 commit comments