File tree 1 file changed +80
-0
lines changed
1 file changed +80
-0
lines changed Original file line number Diff line number Diff line change @@ -302,3 +302,83 @@ fn inductive_canonical_cycle() {
302
302
}
303
303
}
304
304
}
305
+
306
+ #[ test]
307
+ fn mixed_cycle_detection_not_on_stack1 ( ) {
308
+ test ! {
309
+ program {
310
+ #[ coinductive]
311
+ trait A <T > { }
312
+ #[ coinductive]
313
+ trait B <T > { }
314
+ trait C <T > { }
315
+
316
+ impl <T > A <T > for ( )
317
+ where
318
+ ( ) : B <T >,
319
+ ( ) : C <T >,
320
+ { }
321
+
322
+ impl <T > B <T > for ( )
323
+ where
324
+ ( ) : A <T >,
325
+ { }
326
+
327
+ impl <T > C <T > for ( )
328
+ where
329
+ ( ) : B <T >,
330
+ { }
331
+ }
332
+
333
+ goal {
334
+ exists<T > {
335
+ ( ) : A <T >
336
+ }
337
+ } yields[ SolverChoice :: slg( 10 , None ) ] {
338
+ expect![ [ "No possible solution" ] ]
339
+ } yields[ SolverChoice :: recursive_default( ) ] {
340
+ expect![ [ "No possible solution" ] ]
341
+ }
342
+ }
343
+ }
344
+
345
+ #[ test]
346
+ fn mixed_cycle_detection_not_on_stack2 ( ) {
347
+ test ! {
348
+ program {
349
+ #[ coinductive]
350
+ trait A <T > { }
351
+ #[ coinductive]
352
+ trait B <T > { }
353
+ trait C <T > { }
354
+
355
+ impl <T > A <T > for ( )
356
+ where
357
+ ( ) : C <T >,
358
+ ( ) : B <T >,
359
+ { }
360
+
361
+ impl <T > B <T > for ( )
362
+ where
363
+ ( ) : A <T >,
364
+ { }
365
+
366
+ impl <T > C <T > for ( )
367
+ where
368
+ ( ) : B <T >,
369
+ { }
370
+ }
371
+
372
+ goal {
373
+ exists<T > {
374
+ ( ) : A <T >
375
+ }
376
+ } yields[ SolverChoice :: slg( 10 , None ) ] {
377
+ // FIXME: this should be no solution as `C` is inductive
378
+ expect![ [ "Unique; for<?U0> { substitution [?0 := ^0.0] }" ] ]
379
+ } yields[ SolverChoice :: recursive_default( ) ] {
380
+ // FIXME: this should be no solution as `C` is inductive
381
+ expect![ [ "Unique; for<?U0> { substitution [?0 := ^0.0] }" ] ]
382
+ }
383
+ }
384
+ }
You can’t perform that action at this time.
0 commit comments