|
1 |
| -// known-bug |
| 1 | +// check-pass |
| 2 | + |
| 3 | +// This test checks that we're correctly dealing with inductive cycles |
| 4 | +// with canonical inference variables. |
2 | 5 |
|
3 |
| -// This should compile but fails with the current solver. |
4 |
| -// |
5 |
| -// This checks that the new solver uses `Ambiguous` when hitting the |
6 |
| -// inductive cycle here when proving `exists<^0, ^1> (): Trait<^0, ^1>` |
7 |
| -// which requires proving `Trait<?1, ?0>` but that has the same |
8 |
| -// canonical representation. |
9 | 6 | trait Trait<T, U> {}
|
10 | 7 |
|
11 |
| -impl<T, U> Trait<T, U> for () |
| 8 | +trait IsNotU32 {} |
| 9 | +impl IsNotU32 for i32 {} |
| 10 | +impl<T: IsNotU32, U> Trait<T, U> for () // impl 1 |
12 | 11 | where
|
13 |
| - (): Trait<U, T>, |
14 |
| - T: OtherTrait, |
| 12 | + (): Trait<U, T> |
15 | 13 | {}
|
16 | 14 |
|
17 |
| -trait OtherTrait {} |
18 |
| -impl OtherTrait for u32 {} |
| 15 | +impl<T> Trait<u32, T> for () {} // impl 2 |
| 16 | + |
| 17 | +// If we now check whether `(): Trait<?0, ?1>` holds this has to |
| 18 | +// result in ambiguity as both `for<T> (): Trait<u32, T>` and `(): Trait<i32, u32>` |
| 19 | +// applies. The remainder of this test asserts that. |
| 20 | + |
| 21 | +// If we were to error on inductive cycles with canonical inference variables |
| 22 | +// this would be wrong: |
19 | 23 |
|
20 |
| -fn require_trait<T, U>() |
| 24 | +// (): Trait<?0, ?1> |
| 25 | +// - impl 1 |
| 26 | +// - ?0: IsNotU32 // ambig |
| 27 | +// - (): Trait<?1, ?0> // canonical cycle -> err |
| 28 | +// - ERR |
| 29 | +// - impl 2 |
| 30 | +// - OK ?0 == u32 |
| 31 | +// |
| 32 | +// Result: OK ?0 == u32. |
| 33 | + |
| 34 | +// (): Trait<i32, u32> |
| 35 | +// - impl 1 |
| 36 | +// - i32: IsNotU32 // ok |
| 37 | +// - (): Trait<u32, i32> |
| 38 | +// - impl 1 |
| 39 | +// - u32: IsNotU32 // err |
| 40 | +// - ERR |
| 41 | +// - impl 2 |
| 42 | +// - OK |
| 43 | +// - OK |
| 44 | +// - impl 2 (trivial ERR) |
| 45 | +// |
| 46 | +// Result OK |
| 47 | + |
| 48 | +// This would mean that `(): Trait<?0, ?1>` is not complete, |
| 49 | +// which is unsound if we're in coherence. |
| 50 | + |
| 51 | +fn implements_trait<T, U>() -> (T, U) |
21 | 52 | where
|
22 |
| - (): Trait<T, U> |
23 |
| -{} |
| 53 | + (): Trait<T, U>, |
| 54 | +{ |
| 55 | + todo!() |
| 56 | +} |
| 57 | + |
| 58 | +// A hack to only constrain the infer vars after first checking |
| 59 | +// the `(): Trait<_, _>`. |
| 60 | +trait Constrain<T> {} |
| 61 | +impl<T> Constrain<T> for T {} |
| 62 | +fn constrain<T: Constrain<U>, U>(_: U) {} |
24 | 63 |
|
25 | 64 | fn main() {
|
26 |
| - require_trait::<_, _>(); |
27 |
| - //~^ ERROR overflow evaluating |
| 65 | + let (x, y) = implements_trait::<_, _>(); |
| 66 | + |
| 67 | + constrain::<i32, _>(x); |
| 68 | + constrain::<u32, _>(y); |
28 | 69 | }
|
0 commit comments