From ef796db5f0d4eecce0dd2ae9fff224542fb88f5b Mon Sep 17 00:00:00 2001 From: lcnr Date: Sat, 9 Dec 2023 09:47:14 +0000 Subject: [PATCH] add test for inductive cycle hangs --- .../fixpoint-exponential-growth.rs | 8 +++-- .../fixpoint-exponential-growth.stderr | 4 +-- .../cycles/inductive-fixpoint-hang.rs | 33 +++++++++++++++++++ .../cycles/inductive-fixpoint-hang.stderr | 16 +++++++++ 4 files changed, 57 insertions(+), 4 deletions(-) create mode 100644 tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs create mode 100644 tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr diff --git a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs index 44e763ef9907d..07c7d4fb29c70 100644 --- a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs +++ b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.rs @@ -3,8 +3,12 @@ // Proving `W: Trait` instantiates `?0` with `(W, W)` and then // proves `W: Trait` and `W: 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. diff --git a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr index 05aaf6108f1da..150100f2c531c 100644 --- a/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr +++ b/tests/ui/traits/new-solver/cycles/coinduction/fixpoint-exponential-growth.stderr @@ -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::>(); | ^^^^ | = 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() {} | ^^^^^ required by this bound in `impls` diff --git a/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs new file mode 100644 index 0000000000000..062c6ae98d56b --- /dev/null +++ b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.rs @@ -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` to `?0 := W<_>`. +// The next iteration does not simply result in a `?0 := W` constraint as +// one might expect, but instead each time we evaluate the nested `W` goal we +// apply the previously returned constraints: the first fixpoint iteration goes +// as follows: `W: Trait` constrains `?1` to `W`, we then evaluate +// `W>: Trait` the next time we try to prove the nested goal. This results +// inn `W>>` 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>>` 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(*const T); + +impl Trait for W> +where + W: Trait, + W: Trait, +{} + +fn impls_trait() {} + +fn main() { + impls_trait::>(); + //~^ ERROR overflow evaluating the requirement +} diff --git a/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr new file mode 100644 index 0000000000000..42451920744b0 --- /dev/null +++ b/tests/ui/traits/new-solver/cycles/inductive-fixpoint-hang.stderr @@ -0,0 +1,16 @@ +error[E0275]: overflow evaluating the requirement `W<_>: Trait` + --> $DIR/inductive-fixpoint-hang.rs:31:19 + | +LL | impls_trait::>(); + | ^^^^ + | + = 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() {} + | ^^^^^ required by this bound in `impls_trait` + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0275`.