about summary refs log tree commit diff
path: root/compiler/rustc_next_trait_solver/src
diff options
context:
space:
mode:
authorMatthias Krüger <matthias.krueger@famsik.de>2024-07-30 04:31:54 +0200
committerGitHub <noreply@github.com>2024-07-30 04:31:54 +0200
commitae92125a75e9bab924d2b79703bf3ecec2107bf5 (patch)
tree797993018bc2614c97b10b8ae559f6eb52777c74 /compiler/rustc_next_trait_solver/src
parent368e2fd458a22d0cc133d0c254f2612ee999744f (diff)
parentfe0bd76a8bdb80f4460dd59612076cf91370f7a1 (diff)
Rollup merge of #127574 - lcnr:coherence-check-supertrait, r=compiler-errors
elaborate unknowable goals

A reimplemented version of #124532 affecting only the new solver. Always trying to prove super traits ends up causing a fatal overflow error in diesel, so we cannot land this in the old solver.

The following test currently does not pass coherence:
```rust
trait Super {}
trait Sub<T>: Super {}

trait Overlap<T> {}
impl<T, U: Sub<T>> Overlap<T> for U {}
impl<T> Overlap<T> for () {}

fn main() {}
```

We check whether `(): Sub<?t>` holds. This stalls with ambiguity as downstream crates may add an impl for `(): Sub<Local>`. However, its super trait bound `(): Super` cannot be implemented downstream, so this one is known not to hold.

By trying to prove that all the super bounds of a trait before adding a coherence unknowable candidate, this compiles. This is necessary to prevent breakage from enabling `-Znext-solver=coherence` (#121848), see tests/ui/coherence/super-traits/super-trait-knowable-2.rs for more details. The idea is that while there may be an impl of the trait itself we don't know about, if we're able to prove that a super trait is definitely not implemented, then that impl would also never apply/not be well-formed.

This approach is different from #124532 as it allows tests/ui/coherence/super-traits/super-trait-knowable-3.rs to compile. The approach in #124532 only elaborating the root obligations while this approach tries it for all unknowable trait goals.

r? `@compiler-errors`
Diffstat (limited to 'compiler/rustc_next_trait_solver/src')
-rw-r--r--compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs12
1 files changed, 12 insertions, 0 deletions
diff --git a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
index 4aba7ab5e61..84921e87fb3 100644
--- a/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/assembly/mod.rs
@@ -698,6 +698,18 @@ where
                 if ecx.trait_ref_is_knowable(goal.param_env, trait_ref)? {
                     Err(NoSolution)
                 } else {
+                    // While the trait bound itself may be unknowable, we may be able to
+                    // prove that a super trait is not implemented. For this, we recursively
+                    // prove the super trait bounds of the current goal.
+                    //
+                    // We skip the goal itself as that one would cycle.
+                    let predicate: I::Predicate = trait_ref.upcast(cx);
+                    ecx.add_goals(
+                        GoalSource::Misc,
+                        elaborate::elaborate(cx, [predicate])
+                            .skip(1)
+                            .map(|predicate| goal.with(cx, predicate)),
+                    );
                     ecx.evaluate_added_goals_and_make_canonical_response(Certainty::AMBIGUOUS)
                 }
             },