handling incompleteness in the new solver

We sometimes make decisions during type inference which are not strictly necessary, i.e. we constrain inference variables to some specific type even though another type may be equally as valid. For example:

fn impl_trait() -> impl Into<u32> {
    0u16
}

fn main() {
    // There are two possible types for `x`:
    // - `u32` by using the "alias bound" of `impl Into<u32>`
    // - `impl Into<u32>`, i.e. `u16`, by using `impl<T> From<T> for T`
    //
    // We infer the type of `x` to be `u32` here as it is highly likely
    // that this is expected by the user.
    let x = impl_trait().into();
    println!("{}", std::mem::size_of_val(&x));
}

This behavior can result in unexpected errors in case we incorrectly guide inference. It also causes trait solving to be order dependent. It mostly happens in places where we have multiple valid ways - candidates - to prove a given goal and choose a single one of them. The exact way we prefer candidates is deeply intertwined with the inner workings on the trait solver and cannot trivially be emulated in the new solver.

there must not be incompleteness in coherence

Coherence must not have any incompleteness as incompleteness can result in incorrect errors which can be used to allow overlapping impls.

Outside of coherence we rely on incompleteness for things to work™, to match the behavior expected by users, and for backwards compatible reasons.

`select` in the new solver

Unlike the current trait solver, candidate selection is not a fundamental part of the new trait solver. The new trait solver instead tries to merge its different candidates: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L760-L797.

We do however also need something closer to the current selection behavior:

get a single candidate (incompletely prefering some over others)
return the nested obligations of that candidate

The most notable place where this behavior is needed is coerce_unsized: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_hir_typeck/src/coercion.rs#L602-L706. This implements its own, completely separate fulfillment loop with special behavior to decide whether or not an unsize coercion should take place. Rewriting this fulfillment loop to not rely on the existing behavior ofselect while mostly being backwards compatible is a difficult issue and I expect it to require a significant time investment.

Because of the above, with the new solver we implemented a select which lives outside of the trait solver and has the same behavior as the old select: https://github.com/rust-lang/rust/blob/1a449dcfd25143f7e1f6b6f5ddf1c12af361e2ff/compiler/rustc_trait_selection/src/solve/assembly/mod.rs#L760-L797

This means that the way incompleteness is handled inside of the solver, e.g. by trait goals, is separate from how it is handled by select (which is used by method probing and coercions).

Incompleteness inside of the trait solver

Outside of select which currently matches the behavior of the old solver, the trait solver itself is currently incomplete in 3 different places. We always first try to merge all options via fn try_merge_responses and only rely on incompleteness if that fails.

merging trait and project candidates

https://github.com/rust-lang/trait-system-refactor-initiative/issues/45

We prefer candidates from the environment, the exact rules for this are still undecided, see https://github.com/rust-lang/rust/pull/113445 which has the minimal amount of incompleteness here.

Case Study: the order of where clauses

trait Left<T> {}
impl<T, U> Left<U> for T {}

trait Right<T> {}
impl<T, U> Right<U> for T {}

trait Join<U> {
    fn test();
}

// With the reordering,
//   impl<T, U> Join<U> for T where T: Right<U>, T: Left<U> {
// you'll get a different output
impl<T, U> Join<U> for T where T: Left<U>, T: Right<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_join<T: Join<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Left<bool>, T: Right<()> {
    // Both entering the trait solver via select and
    // ordinary trait solving have the same result, as
    // a nested goal is resposible for the incompleteness.
    <T as Join<_>>::test();
    impls_join::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

https://rust.godbolt.org/z/rajs4seb5

We have the following proof tree for this example:

goal: T: Join<?U> where T: Left<bool>, T: Right<()>
- impl: impl<T, U> Join<U>
  - nested goal: T: Left<?U>
    - proven via impl: AMBIG, no constraints (?U: Sized bound)
    - proven via param env: OK, ?U == bool
    - a complete solver would return AMBIG
    - prefering param env candidates and constrains ?U to bool
  - nested goal: T: Right<bool> (after incomplete previous goal)
    - proven via impl: OK
    - param env candidate T: Right<()> does not apply

If we instead first check T: Right<?U> we would incompletely constrain ?U to ().

alias-relate bidrectional normalization

https://github.com/rust-lang/trait-system-refactor-initiative/issues/25

If we have an AliasRelate goal with normalizeable aliases on both sides it's often possible to prove it by both first normalize the lhs and then the rhs or the other way around. These two candidates end up having subtly different responses, e.g. they can differ in whether a type is normalized in the inference constraints.

trait Trait {
    type Assoc;
    fn assoc(&self) -> &Self::Assoc;
}

struct Foo<'a>(&'a str);
impl<'a> Trait for Foo<'a> {
    type Assoc = Foo<'a>;
    fn assoc(&self) -> &Self::Assoc {
        self
    }
}

fn main() {
    let origin = Foo("hi");
    let target = if false {
        origin.assoc()
    } else {
        origin.assoc()
    };
}

would result in

error[E0284]: type annotations needed: cannot satisfy `<Foo<'_> as Trait>::Assoc <: <Foo<'_> as Trait>::Assoc`
  --> src/main.rs:16:18
   |
16 |       let target = if false {
   |  __________________^
17 | |         origin.assoc()
18 | |     } else {
19 | |         origin.assoc()
20 | |     };
   | |_____^ cannot satisfy `<Foo<'_> as Trait>::Assoc <: <Foo<'_> as Trait>::Assoc`

It might be possible to avoid this issue (at least in some cases), by converting the returned region constraints into some "normal form" wrt to the query input which should allow us to merge these responses. I am not sure whether this is possible in the general case.

This is also frequently an issue with opaque types. Given an alias relate goal AliasRelate(impl Trait, <iter::Empty<i32> as Iterator>::Item), should the hidden type of impl Trait be <iter::Empty<i32> as Iterator>::Item or i32? To handle this we add a fourth option to prove alias-relate goals: bidirectional-normalizes-to https://github.com/rust-lang/rust/blob/55e8df2b0e3c4494b77f2431b912c51e6fe733ba/compiler/rustc_trait_selection/src/solve/alias_relate.rs#L170-L194

This goal is lhs normalizes-to rhs AND rhs normalizes-to lhs. If we add keep the requirement of the type system that normalization does not add additional bounds apart from the WF-conditions of the alias, then this shouldn't even be incomplete.

We currently also prefer the substs-relate candidate in alias-relate over any normalizes-to, but afaict this one is unnecessary if we have bidirectional-normalizes-to.

a stack of questions

how do I ask a question while reading?

when do we WANT this behavior?

nikomatsakis: the doc didn't go into cases where env preference is required.

lcnr: doc https://github.com/rust-lang/trait-system-refactor-initiative/issues/45

what is behavior of solver for the case study?

Case Study: the order of where clauses

nikomatsakis: It's not spelled out very clearly, or at least I was unsure. I believe the new trait solver does exhibit order dependency here, right?

lcnr: yes, but it is not strictly necessary and I have an open PR which changes this and afaict doesn't break anything "important" that I know of https://github.com/rust-lang/rust/pull/113445

use std::fmt::Display;
fn test<T: Display + Into<String>>(t: T) -> String {
    let x = t.into();
    format!("{x}")
}

fn main() {
    test(22)
}

use std::fmt::Display;
fn test<T: Display + Into<String>>(t: T) {
    let x = t.into();
    println!("{x}");
}

fn main() {
    test("test")
}

another version

use std::fmt::Debug;

fn test<T: Debug + Into<String>>(t: T) -> String {
    let x = t.into();
    format!("{x}")
}

#[derive(Debug)]
struct Foo;

impl From<Foo> for String { 
    fn from(x: Foo) -> String { format!("{x:?}") }
}

fn main() {
    test(Foo);
}

what about moving the "arbitrary choice" into type check? This is what chalk was trying to do.

Example: blanket

preference only at the "top level" feels bad, e.g. moving stuff into extension traits can break type inference:

trait Nested<T> {}
impl<T, U> Nested<U> for T {}

trait Root<U> {
    fn test();
}

impl<T, U> Root<U> for T where T: Nested<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_root<T: Root<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Nested<bool> {
    // Both entering the trait solver via select and
    // ordinary trait solving have the same result, as
    // a nested goal is resposible for the incompleteness.
    <T as Root<_>>::test();
    impls_root::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant
}

trait Left<T> {}
impl<T, U> Left<U> for T {}

trait Right<T> {}
impl<T, U> Right<U> for T {}

trait Join<U> {
    fn test();
}

// With the reordering,
//   impl<T, U> Join<U> for T where T: Right<U>, T: Left<U> {
// you'll get a different output
impl<T, U> Join<U> for T where T: Left<U>, T: Right<U> {
    fn test() {
        println!("{}", std::any::type_name::<U>());
    }
}

fn impls_join<T: Left<U> + Right<U>, U>() {
    println!("{}", std::any::type_name::<U>());
}

fn try_it<T>() where T: Left<bool>, T: Right<()> {
    impls_join::<T, _>();
}

fn main() {
    try_it::<u8>() // the type here is irrelevant

normalization behavior

nikomatsakis: In the section …

alias-relate bidrectional normalization

it states that normalization can result in subtle errors and gives an example, but I don't understand what is causing this error to arise. When we invoke origin.assoc() we get back a return type of &'x <Foo<'y> as Trait>::Assoc, and we invoke it twice, once for each branch of the if, so they are getting equated… this presumably attempts to normalize… which I would assume succeeds…?

lcnr: for <Foo<'0> as Trait>::Assoc <: <Foo<'1> as Trait>::Assoc

normalizing Foo<'a> as Trait>::Assoc results in some region constraint on 'a which gets put into an ordered list. So by normalizing with different orders the lists have the same content, but different orders

Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })
Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })
Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: QueryRegionConstraints { outlives: [(OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation), (OutlivesPredicate(ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) }), ReLateBound(DebruijnIndex(0), BoundRegion { var: 0, kind: BrAnon(None) })), BoringNoLocation)], member_constraints: [] }, opaque_types: [] }) }, max_universe: U0, variables: [CanonicalVarInfo { kind: Region(U0) }] })

"add-keep"

nikomatsakis: from the text:

If we add keep the requirement of the type system that normalization does not add additional bounds apart from the WF-conditions of the alias, then this shouldn’t even be incomplete.

We don't have this requrement today, right? So presumably it is add, and I don't think it's possible to add, because it would narrow down the set of impls we can accept rather dramatically?

lcnr: projections are wf if they implement their trait and the gat where bounds hold. this is exactly what we use to normalize. This stops being the case with https://github.com/rust-lang/trait-system-refactor-initiative/issues/12

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`	在筆記中貼入程式碼
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.

there must not be incompleteness in coherence

select in the new solver

Incompleteness inside of the trait solver

merging trait and project candidates

Case Study: the order of where clauses

alias-relate bidrectional normalization

a stack of questions

how do I ask a question while reading?

when do we WANT this behavior?

what is behavior of solver for the case study?

normalization behavior

"add-keep"

`select` in the new solver