add test for inductive cycle hangs

This commit is contained in:
lcnr 2023-12-09 09:47:14 +00:00
parent 608f32435a
commit ef796db5f0
4 changed files with 57 additions and 4 deletions

View File

@ -3,8 +3,12 @@
// Proving `W<?0>: Trait` instantiates `?0` with `(W<?1>, W<?2>)` and then
// proves `W<?1>: Trait` and `W<?2>: Trait`, resulting in a coinductive cycle.
//
// Proving coinductive cycles runs until we reach a fixpoint. This fixpoint is
// never reached here and each step doubles the amount of nested obligations.
// Proving coinductive cycles runs until we reach a fixpoint. However, after
// computing `try_evaluate_added_goals` in the second fixpoint iteration, the
// self type already has a depth equal to the number of steps. This results
// in enormous constraints, causing the canonicalizer to hang without ever
// reaching the recursion limit. We currently avoid that by erasing the constraints
// from overflow.
//
// This previously caused a hang in the trait solver, see
// https://github.com/rust-lang/trait-system-refactor-initiative/issues/13.

View File

@ -1,12 +1,12 @@
error[E0275]: overflow evaluating the requirement `W<_>: Trait`
--> $DIR/fixpoint-exponential-growth.rs:29:13
--> $DIR/fixpoint-exponential-growth.rs:33:13
|
LL | impls::<W<_>>();
| ^^^^
|
= help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`fixpoint_exponential_growth`)
note: required by a bound in `impls`
--> $DIR/fixpoint-exponential-growth.rs:26:13
--> $DIR/fixpoint-exponential-growth.rs:30:13
|
LL | fn impls<T: Trait>() {}
| ^^^^^ required by this bound in `impls`

View File

@ -0,0 +1,33 @@
// compile-flags: -Ztrait-solver=next
// This currently hangs if we do not erase constraints from
// overflow.
//
// We set the provisional result of `W<?0>` to `?0 := W<_>`.
// The next iteration does not simply result in a `?0 := W<W<_>` constraint as
// one might expect, but instead each time we evaluate the nested `W<T>` goal we
// apply the previously returned constraints: the first fixpoint iteration goes
// as follows: `W<?1>: Trait` constrains `?1` to `W<?2>`, we then evaluate
// `W<W<?2>>: Trait` the next time we try to prove the nested goal. This results
// inn `W<W<W<?3>>>` and so on. This goes on until we reach overflow in
// `try_evaluate_added_goals`. This means the provisional result after the
// second fixpoint iteration is already `W<W<W<...>>>` with a size proportional
// to the number of steps in `try_evaluate_added_goals`. The size then continues
// to grow. The exponential blowup from having 2 nested goals per impl causes
// the solver to hang without hitting the recursion limit.
trait Trait {}
struct W<T: ?Sized>(*const T);
impl<T: ?Sized> Trait for W<W<T>>
where
W<T>: Trait,
W<T>: Trait,
{}
fn impls_trait<T: Trait>() {}
fn main() {
impls_trait::<W<_>>();
//~^ ERROR overflow evaluating the requirement
}

View File

@ -0,0 +1,16 @@
error[E0275]: overflow evaluating the requirement `W<_>: Trait`
--> $DIR/inductive-fixpoint-hang.rs:31:19
|
LL | impls_trait::<W<_>>();
| ^^^^
|
= help: consider increasing the recursion limit by adding a `#![recursion_limit = "256"]` attribute to your crate (`inductive_fixpoint_hang`)
note: required by a bound in `impls_trait`
--> $DIR/inductive-fixpoint-hang.rs:28:19
|
LL | fn impls_trait<T: Trait>() {}
| ^^^^^ required by this bound in `impls_trait`
error: aborting due to 1 previous error
For more information about this error, try `rustc --explain E0275`.