Skip to content

Commit

Permalink
add test for inductive cycle hangs
Browse files Browse the repository at this point in the history
  • Loading branch information
lcnr committed Dec 9, 2023
1 parent 608f324 commit ef796db
Show file tree
Hide file tree
Showing 4 changed files with 57 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Original file line number Diff line number Diff line change
@@ -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`
Expand Down
33 changes: 33 additions & 0 deletions tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs
Original file line number Diff line number Diff line change
@@ -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
}
16 changes: 16 additions & 0 deletions tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr
Original file line number Diff line number Diff line change
@@ -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`.

0 comments on commit ef796db

Please sign in to comment.