# 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.

[chalk#234]: https://github.com/rust-lang/chalk/issues/234

## 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](https://www.microsoft.com/en-us/research/publication/type-checking-with-open-type-functions/) 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.

[source]: https://github.com/rust-lang/chalk/issues/234#issuecomment-528109851
[source 2]: https://github.com/rust-lang/chalk/issues/234#issuecomment-530823193

## 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?**

## Potentially related problems
* **[rust analyzer infinite loop](https://github.com/rust-lang/chalk/issues/280)** 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](https://github.com/rust-lang/chalk/pull/294) didn't necessarily fix the "root" cause. A [proposed solution](https://github.com/rust-lang/chalk/pull/305) touched projections irt. unification with inference variables.

## Previous work or progress

### Some work towards thoughts 5/6

[Branch 1](https://github.com/jackh726/chalk/commits/associated_types)
[Branch 2](https://github.com/jackh726/chalk/commits/associated_types2)
[Branch 3](https://github.com/jackh726/chalk/tree/associated_types3)

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.