forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Rollup merge of rust-lang#108033 - lcnr:coinductive-attr, r=compiler-…
…errors add an unstable `#[rustc_coinductive]` attribute useful to test coinduction, especially in the new solver. as this attribute should remain permanently unstable I don't think this needs any official approval. cc `@rust-lang/types` had to weaken the check for stable query results in the solver to prevent an ICE if there's a coinductive cycle with constraints. r? `@compiler-errors`
- Loading branch information
Showing
10 changed files
with
130 additions
and
37 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,54 @@ | ||
// check-pass | ||
// revisions: old new | ||
//[new] compile-flags: -Ztrait-solver=next | ||
|
||
// If we use canonical goals during trait solving we have to reevaluate | ||
// the root goal of a cycle until we hit a fixpoint. | ||
// | ||
// Here `main` has a goal `(?0, ?1): Trait` which is canonicalized to | ||
// `exists<^0, ^1> (^0, ^1): Trait`. | ||
// | ||
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait` | ||
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait` | ||
// - COINDUCTIVE CYCLE OK (no constraints) | ||
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>` | ||
// - OK (^0 = u32 -apply-> ?0 = u32) | ||
// - OK (?0 = u32 -canonicalize-> ^0 = u32) | ||
// - coinductive cycle with provisional result != final result, rerun | ||
// | ||
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait` | ||
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait` | ||
// - COINDUCTIVE CYCLE OK (^0 = u32 -apply-> ?1 = u32) | ||
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>` | ||
// - OK (^0 = u32 -apply-> ?1 = u32) | ||
// - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32) | ||
// - coinductive cycle with provisional result != final result, rerun | ||
// | ||
// - `exists<^0, ^1> (^0, ^1): Trait` -instantiate-> `(?0, ?1): Trait` | ||
// -`(?1, ?0): Trait` -canonicalize-> `exists<^0, ^1> (^0, ^1): Trait` | ||
// - COINDUCTIVE CYCLE OK (^0 = u32, ^1 = u32 -apply-> ?1 = u32, ?0 = u32) | ||
// - `(): ConstrainToU32<?0>` -canonicalize-> `exists<^0> (): ConstrainToU32<^0>` | ||
// - OK (^0 = u32 -apply-> ?1 = u32) | ||
// - OK (?0 = u32, ?1 = u32 -canonicalize-> ^0 = u32, ^1 = u32) | ||
// - coinductive cycle with provisional result == final result, DONE | ||
#![feature(rustc_attrs)] | ||
#[rustc_coinductive] | ||
trait Trait {} | ||
|
||
impl<T, U> Trait for (T, U) | ||
where | ||
(U, T): Trait, | ||
(): ConstrainToU32<T>, | ||
{} | ||
|
||
trait ConstrainToU32<T> {} | ||
impl ConstrainToU32<u32> for () {} | ||
|
||
fn impls_trait<T, U>() | ||
where | ||
(T, U): Trait, | ||
{} | ||
|
||
fn main() { | ||
impls_trait::<_, _>(); | ||
} |