diff --git a/tests/test/cycle.rs b/tests/test/cycle.rs index f552fb4fcc3..fab9e7de3fc 100644 --- a/tests/test/cycle.rs +++ b/tests/test/cycle.rs @@ -302,3 +302,83 @@ fn inductive_canonical_cycle() { } } } + +#[test] +fn mixed_cycle_detection_not_on_stack1() { + test! { + program { + #[coinductive] + trait A {} + #[coinductive] + trait B {} + trait C {} + + impl A for () + where + (): B, + (): C, + {} + + impl B for () + where + (): A, + {} + + impl C for () + where + (): B, + {} + } + + goal { + exists { + (): A + } + } yields[SolverChoice::slg(10, None)] { + expect![["No possible solution"]] + } yields[SolverChoice::recursive_default()] { + expect![["No possible solution"]] + } + } +} + +#[test] +fn mixed_cycle_detection_not_on_stack2() { + test! { + program { + #[coinductive] + trait A {} + #[coinductive] + trait B {} + trait C {} + + impl A for () + where + (): C, + (): B, + {} + + impl B for () + where + (): A, + {} + + impl C for () + where + (): B, + {} + } + + goal { + exists { + (): A + } + } yields[SolverChoice::slg(10, None)] { + // FIXME: this should be no solution as `C` is inductive + expect![["Unique; for { substitution [?0 := ^0.0] }"]] + } yields[SolverChoice::recursive_default()] { + // FIXME: this should be no solution as `C` is inductive + expect![["Unique; for { substitution [?0 := ^0.0] }"]] + } + } +}