| // compile-flags: -Znext-solver |
| // check-pass |
| #![feature(rustc_attrs)] |
| |
| // A test showcasing that using a provisional cache can differ |
| // from only tracking stack entries. |
| // |
| // Without a provisional cache, we have the following proof tree: |
| // |
| // - (): A |
| // - (): B |
| // - (): A (coinductive cycle) |
| // - (): C |
| // - (): B (coinductive cycle) |
| // - (): C |
| // - (): B |
| // - (): A (coinductive cycle) |
| // - (): C (coinductive cycle) |
| // |
| // While with the current provisional cache implementation we get: |
| // |
| // - (): A |
| // - (): B |
| // - (): A (coinductive cycle) |
| // - (): C |
| // - (): B (coinductive cycle) |
| // - (): C |
| // - (): B (provisional cache hit) |
| // |
| // Note that if even if we were to expand the provisional cache hit, |
| // the proof tree would still be different: |
| // |
| // - (): A |
| // - (): B |
| // - (): A (coinductive cycle) |
| // - (): C |
| // - (): B (coinductive cycle) |
| // - (): C |
| // - (): B (provisional cache hit, expanded) |
| // - (): A (coinductive cycle) |
| // - (): C |
| // - (): B (coinductive cycle) |
| // |
| // Theoretically, this can result in observable behavior differences |
| // due to incompleteness. However, this would require a very convoluted |
| // example and would still be sound. The difference is determinstic |
| // and can not be observed outside of the cycle itself as we don't move |
| // non-root cycle participants into the global cache. |
| // |
| // For an example of how incompleteness could impact the observable behavior here, see |
| // |
| // tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.rs |
| #[rustc_coinductive] |
| trait A {} |
| |
| #[rustc_coinductive] |
| trait B {} |
| |
| #[rustc_coinductive] |
| trait C {} |
| |
| impl<T: ?Sized + B + C> A for T {} |
| impl<T: ?Sized + A + C> B for T {} |
| impl<T: ?Sized + B> C for T {} |
| |
| fn impls_a<T: A>() {} |
| |
| fn main() { |
| impls_a::<()>(); |
| } |