update test for inductive canonical cycles
This commit is contained in:
parent
89e0576bd3
commit
31099ee384
2 changed files with 58 additions and 43 deletions
|
@ -1,28 +1,69 @@
|
|||
// known-bug
|
||||
// check-pass
|
||||
|
||||
// This test checks that we're correctly dealing with inductive cycles
|
||||
// with canonical inference variables.
|
||||
|
||||
// This should compile but fails with the current solver.
|
||||
//
|
||||
// This checks that the new solver uses `Ambiguous` when hitting the
|
||||
// inductive cycle here when proving `exists<^0, ^1> (): Trait<^0, ^1>`
|
||||
// which requires proving `Trait<?1, ?0>` but that has the same
|
||||
// canonical representation.
|
||||
trait Trait<T, U> {}
|
||||
|
||||
impl<T, U> Trait<T, U> for ()
|
||||
trait IsNotU32 {}
|
||||
impl IsNotU32 for i32 {}
|
||||
impl<T: IsNotU32, U> Trait<T, U> for () // impl 1
|
||||
where
|
||||
(): Trait<U, T>,
|
||||
T: OtherTrait,
|
||||
(): Trait<U, T>
|
||||
{}
|
||||
|
||||
trait OtherTrait {}
|
||||
impl OtherTrait for u32 {}
|
||||
impl<T> Trait<u32, T> for () {} // impl 2
|
||||
|
||||
fn require_trait<T, U>()
|
||||
// If we now check whether `(): Trait<?0, ?1>` holds this has to
|
||||
// result in ambiguity as both `for<T> (): Trait<u32, T>` and `(): Trait<i32, u32>`
|
||||
// applies. The remainder of this test asserts that.
|
||||
|
||||
// If we were to error on inductive cycles with canonical inference variables
|
||||
// this would be wrong:
|
||||
|
||||
// (): Trait<?0, ?1>
|
||||
// - impl 1
|
||||
// - ?0: IsNotU32 // ambig
|
||||
// - (): Trait<?1, ?0> // canonical cycle -> err
|
||||
// - ERR
|
||||
// - impl 2
|
||||
// - OK ?0 == u32
|
||||
//
|
||||
// Result: OK ?0 == u32.
|
||||
|
||||
// (): Trait<i32, u32>
|
||||
// - impl 1
|
||||
// - i32: IsNotU32 // ok
|
||||
// - (): Trait<u32, i32>
|
||||
// - impl 1
|
||||
// - u32: IsNotU32 // err
|
||||
// - ERR
|
||||
// - impl 2
|
||||
// - OK
|
||||
// - OK
|
||||
// - impl 2 (trivial ERR)
|
||||
//
|
||||
// Result OK
|
||||
|
||||
// This would mean that `(): Trait<?0, ?1>` is not complete,
|
||||
// which is unsound if we're in coherence.
|
||||
|
||||
fn implements_trait<T, U>() -> (T, U)
|
||||
where
|
||||
(): Trait<T, U>
|
||||
{}
|
||||
(): Trait<T, U>,
|
||||
{
|
||||
todo!()
|
||||
}
|
||||
|
||||
// A hack to only constrain the infer vars after first checking
|
||||
// the `(): Trait<_, _>`.
|
||||
trait Constrain<T> {}
|
||||
impl<T> Constrain<T> for T {}
|
||||
fn constrain<T: Constrain<U>, U>(_: U) {}
|
||||
|
||||
fn main() {
|
||||
require_trait::<_, _>();
|
||||
//~^ ERROR overflow evaluating
|
||||
let (x, y) = implements_trait::<_, _>();
|
||||
|
||||
constrain::<i32, _>(x);
|
||||
constrain::<u32, _>(y);
|
||||
}
|
||||
|
|
|
@ -1,26 +0,0 @@
|
|||
error[E0275]: overflow evaluating the requirement `_: Sized`
|
||||
--> $DIR/inductive-canonical-cycle.rs:26:5
|
||||
|
|
||||
LL | require_trait::<_, _>();
|
||||
| ^^^^^^^^^^^^^^^^^^^^^
|
||||
|
|
||||
= help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`inductive_canonical_cycle`)
|
||||
note: required for `()` to implement `Trait<_, _>`
|
||||
--> $DIR/inductive-canonical-cycle.rs:11:12
|
||||
|
|
||||
LL | impl<T, U> Trait<T, U> for ()
|
||||
| ^^^^^^^^^^^ ^^
|
||||
= note: 128 redundant requirements hidden
|
||||
= note: required for `()` to implement `Trait<_, _>`
|
||||
note: required by a bound in `require_trait`
|
||||
--> $DIR/inductive-canonical-cycle.rs:22:9
|
||||
|
|
||||
LL | fn require_trait<T, U>()
|
||||
| ------------- required by a bound in this
|
||||
LL | where
|
||||
LL | (): Trait<T, U>
|
||||
| ^^^^^^^^^^^ required by this bound in `require_trait`
|
||||
|
||||
error: aborting due to previous error
|
||||
|
||||
For more information about this error, try `rustc --explain E0275`.
|
Loading…
Add table
Reference in a new issue