From 51671cd435a9b24bcbe9a3b3e3c7e98b1832dfea Mon Sep 17 00:00:00 2001 From: lcnr Date: Tue, 14 Feb 2023 10:53:25 +0100 Subject: [PATCH] add test for coinduction in new solver --- .../rustc_trait_selection/src/solve/mod.rs | 10 +++- .../src/solve/search_graph/mod.rs | 18 +++++++ .../ui/coinduction/canonicalization-rerun.rs | 54 +++++++++++++++++++ 3 files changed, 80 insertions(+), 2 deletions(-) create mode 100644 tests/ui/coinduction/canonicalization-rerun.rs diff --git a/compiler/rustc_trait_selection/src/solve/mod.rs b/compiler/rustc_trait_selection/src/solve/mod.rs index e56588c58bd..38a86d55a2c 100644 --- a/compiler/rustc_trait_selection/src/solve/mod.rs +++ b/compiler/rustc_trait_selection/src/solve/mod.rs @@ -265,12 +265,18 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> { // call `exists ::Assoc == U` to enable better caching. This goal // could constrain `U` to `u32` which would cause this check to result in a // solver cycle. - if cfg!(debug_assertions) && has_changed && !self.in_projection_eq_hack { + if cfg!(debug_assertions) + && has_changed + && !self.in_projection_eq_hack + && !self.search_graph.in_cycle() + { let mut orig_values = OriginalQueryValues::default(); let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values); let canonical_response = EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?; - assert!(canonical_response.value.var_values.is_identity()); + if !canonical_response.value.var_values.is_identity() { + bug!("unstable result: {goal:?} {canonical_goal:?} {canonical_response:?}"); + } assert_eq!(certainty, canonical_response.value.certainty); } diff --git a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs index a2ca4bc189c..e989c9145d1 100644 --- a/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs +++ b/compiler/rustc_trait_selection/src/solve/search_graph/mod.rs @@ -42,6 +42,24 @@ impl<'tcx> SearchGraph<'tcx> { && !self.overflow_data.did_overflow() } + /// Whether we're currently in a cycle. This should only be used + /// for debug assertions. + pub(super) fn in_cycle(&self) -> bool { + if let Some(stack_depth) = self.stack.last() { + // Either the current goal on the stack is the root of a cycle... + if self.stack[stack_depth].has_been_used { + return true; + } + + // ...or it depends on a goal with a lower depth. + let current_goal = self.stack[stack_depth].goal; + let entry_index = self.provisional_cache.lookup_table[¤t_goal]; + self.provisional_cache.entries[entry_index].depth != stack_depth + } else { + false + } + } + /// Tries putting the new goal on the stack, returning an error if it is already cached. /// /// This correctly updates the provisional cache if there is a cycle. diff --git a/tests/ui/coinduction/canonicalization-rerun.rs b/tests/ui/coinduction/canonicalization-rerun.rs new file mode 100644 index 00000000000..b10ba3a810f --- /dev/null +++ b/tests/ui/coinduction/canonicalization-rerun.rs @@ -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` -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` -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` -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 Trait for (T, U) +where + (U, T): Trait, + (): ConstrainToU32, +{} + +trait ConstrainToU32 {} +impl ConstrainToU32 for () {} + +fn impls_trait() +where + (T, U): Trait, +{} + +fn main() { + impls_trait::<_, _>(); +}