File tree Expand file tree Collapse file tree 1 file changed +80
-0
lines changed Expand file tree Collapse file tree 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() {
302302 }
303303 }
304304}
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