1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
//@ 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::<()>();
}
|
