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() {
173173 }
174174}
175175
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+
176244#[ test]
177245fn normalize_gat1 ( ) {
178246 test ! {
You can’t perform that action at this time.
0 commit comments