chalk design meeting 2019-12-16 normalization

The problem

See chalk#234 for some details. Essentially, the way Chalk handles projections can lead to ambiguity, because there is both a "placeholder type" (Trait::Item)<T> as well as the normalized type <T as Trait>::Item -> U (where U is the normalized type). This leads to two separate answers that are "equal", but the aggregator treats them as unequal currently, so the final answer is ambiguous.

Thoughts on potential solutions

  • Improve the uniqueness checker Essentially, don't modify the engine or solver at all with regards to the existing answers. Instead, modify the aggregator to check if the two types normalize to each other. source
  • Don't search all options Here, instead of having two answers (placeholdero and normalized type), we have some way to try the normalized type first; then, if that fails, use the placeholder type. source
  • Using a different approach to normalization There has been previous work that applies normalization in Haskell. source
  • Remove unnormalized types. This is somewhat of a stepping stone. The idea here is to "desugar" projection types into explicit goals when lowering, so there is no longer "unnormalized projections", only normalized projections and placeholder types. source 2
  • Merge placeholder and projection types This is somewhat different to the previous thought. Here, our idea of "unnormalized projections" is instead replaced by "normalized projections to placeholders" where placeholders can act like inference variables.
  • Only add the placeholder clause when no impls exist This extends upon the second "Don't search all options" thought. Currently, the placeholder clause is added separately to the normalized values (from impls). Perhaps we could instead only add the placeholder clauses if no impls exist. This has implications for well-formed goals, since they rely on the placeholder type right now.

Cases to consider

Simple case

See chalk#234.

program {
    trait Trait1 { type Type; }
    trait Trait2<T> { }
    impl<T, U> Trait2<T> for U where U: Trait1<Type = T> {}

    struct u32 {}
    struct S {}
    impl Trait1 for S { type Type = u32; }
}

goal {
    exists<U> { S: Trait2<U> }
} yields {
    "Unique"
}

Here, there really is only one solution: U = u32 (because <S as Trait1>::Type = u32). However, because of the placeholder type (Trait1::Type)<S>, the actual answer returned is ambiguous.

With inference variables

program {
    trait Trait1 { type Type; }
    trait Trait2<T> { }
    impl<T, U> Trait2<T> for U where U: Trait1<Type = T> {}

    struct u32 {}
    struct S {}
    impl Trait1 for S { type Type = u32; }
    struct i32 {}
    struct X {}
    impl Trait1 for X { type Type = i32; }
}

goal {
    exists<T, U> { T: Trait2<U> }
} first 3 with max 10 {
    ...
}

Here, the best answer we could give would be ?0 = ^0, ?1 = <?0 as Trait1>::Type. But, maybe also "ambiguous" is okay here, because ?0 = S, ?1 = u32 and ?0 = X, ?1 = i32 are both distinct answers.

Mapping

If the projection type to be normalized contains inference variables, what do we use to figure out their values?

Here is one simple case:

trait Id { type Output; }

impl Id for i32 {
    type Output = i32;
}

impl Id for u32 {
    type Output = u32;
}

Given ProjectionEq(<?X as Id>::Output = i32), can we infer that ?X = i32?

rustc cannot, but chalk can.

Other relevant questions

  • Do we need both ProjectionEq and Normalize? Relevant for conditionally adding placeholder type if no impls.
  • What benefit do we get by having a separate projection type and associated type?
  • rust analyzer infinite loop The core problem with this was an inference variable was getting normalized to a projection with an inference variable, which got truncated and a cycle happened. The accepted solution didn't necessarily fix the "root" cause. A proposed solution touched projections irt. unification with inference variables.

Previous work or progress

Some work towards thoughts 5/6

Branch 1
Branch 2
Branch 3

The core approach with these approaches revolve around not storing the answer to a ProjectionEq/Normalize as a simple type, but instead as a "normalized projection". E.g. from the simple case about, the answer would be <S as Trait1>::Type as u32. If there are no impls it would instead be <S as Trait1>::Type as (Trait1::Type)<?0> or just <S as Trait1>::Type as ?0.

Some thoughts from this:

  • Mostly there. Each branch has a slightly different approach. Probably don't need both ProjectionEq and Normalize. Probably don't need both the projection type and placeholder type.
  • Need to think about how well-formed goals interact with projection.
Select a repo