rust/compiler/rustc_next_trait_solver/src
Matthias Krüger ae92125a75
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`
2024-07-30 04:31:54 +02:00
..
relate Uplift PredicateEmittingRelation first 2024-07-06 10:05:49 -04:00
solve Rollup merge of #127574 - lcnr:coherence-check-supertrait, r=compiler-errors 2024-07-30 04:31:54 +02:00
canonicalizer.rs Split SolverDelegate back out from InferCtxtLike 2024-07-05 16:39:39 -04:00
coherence.rs rustc_next_trait_solver: derivative -> derive-where 2024-07-12 21:48:16 +03:00
delegate.rs Rollup merge of #127439 - compiler-errors:uplift-elaborate, r=lcnr 2024-07-08 13:04:33 +08:00
lib.rs Uplift trait_ref_is_knowable and friends 2024-07-07 11:10:32 -04:00
relate.rs Uplift PredicateEmittingRelation first 2024-07-06 10:05:49 -04:00
resolve.rs Reformat use declarations. 2024-07-29 08:26:52 +10:00