File tree Expand file tree Collapse file tree 1 file changed +68
-0
lines changed Expand file tree Collapse file tree 1 file changed +68
-0
lines changed Original file line number Diff line number Diff line change @@ -173,6 +173,74 @@ fn projection_equality_from_env() {
173
173
}
174
174
}
175
175
176
+ #[ test]
177
+ fn projection_equality_nested ( ) {
178
+ test ! {
179
+ program {
180
+ trait Iterator {
181
+ type Item ;
182
+ }
183
+
184
+ struct u32 { }
185
+ }
186
+
187
+ goal {
188
+ forall<I > {
189
+ if ( I : Iterator ) {
190
+ if ( <I as Iterator >:: Item : Iterator <Item = u32 >) {
191
+ exists<U > {
192
+ <<I as Iterator >:: Item as Iterator >:: Item = U
193
+ }
194
+ }
195
+ }
196
+ }
197
+ } yields[ SolverChoice :: recursive( ) ] {
198
+ "Unique; substitution [?0 := u32]"
199
+ }
200
+ }
201
+ }
202
+
203
+ #[ test]
204
+ fn iterator_flatten ( ) {
205
+ test ! {
206
+ program {
207
+ trait Iterator {
208
+ type Item ;
209
+ }
210
+ #[ non_enumerable]
211
+ trait IntoIterator {
212
+ type Item ;
213
+ type IntoIter : Iterator <Item = <Self as IntoIterator >:: Item >;
214
+ }
215
+ struct Flatten <I > { }
216
+
217
+ impl <I , U > Iterator for Flatten <I >
218
+ where
219
+ I : Iterator ,
220
+ <I as Iterator >:: Item : IntoIterator <IntoIter = U >,
221
+ <I as Iterator >:: Item : IntoIterator <Item = <U as Iterator >:: Item >,
222
+ U : Iterator
223
+ {
224
+ type Item = <U as Iterator >:: Item ;
225
+ }
226
+
227
+ struct u32 { }
228
+ }
229
+
230
+ goal {
231
+ forall<I , U > {
232
+ if ( I : Iterator <Item = U >; U : IntoIterator <Item = u32 >) {
233
+ exists<T > {
234
+ <Flatten <I > as Iterator >:: Item = T
235
+ }
236
+ }
237
+ }
238
+ } yields[ SolverChoice :: recursive( ) ] {
239
+ "Unique; substitution [?0 := u32]"
240
+ }
241
+ }
242
+ }
243
+
176
244
#[ test]
177
245
fn normalize_gat1 ( ) {
178
246
test ! {
You can’t perform that action at this time.
0 commit comments