Hide associated types equality constraints

[Nadrieril]

The following is unsupported because we don't handle the equality constraint:

trait Iterator {
    type Item;
}

fn f<I, J>(x: I::Item) -> J::Item
where
    I: Iterator,
    J: Iterator<Item=I::Item>,
{ x }

The solution proposed by @sonmarcho would be to transform associated types into type parameters. Type equalities would then only apply to free type variables, which we can handle by merging any two variables that are equated. We would therefore generate:

trait Iterator<Item> {}

fn f<I, J, Item>(x: Item) -> Item
where
    I: Iterator<Item>,
    J: Iterator<Item>,
{ x }

[sonmarcho]

Rephrasing a bit: we can extract the code above with Charon, and it's actually handled by Aeneas (which has a normalization mechanism) but the generated pure model doesn't type-check.

[Nadrieril]

Copying over the current limitation I wrote about in #532:

This has 4 know limitations today:

• Bug: type aliases don't work with --remove-associated-types #531;
• Bug: incorrect generics when implemented method has more specific signature #513;
• Doesn't yet work with dyn Trait (Add support for dyn Trait #123);
• We erase some lifetimes in quantified clauses like T: for<'a> Trait<'a, Type = &'a ()> (Bug: --remove-associated-types doesn't track quantified lifetimes #534).

This also has 3 fundamental limitations that we can't work around:

• We can't handle GATs, as this would require passing type-level functions as type parameters;
• We can't handle for<'a> clauses with unconstrained associated types, for the same reason;
• We can't add parameters to self-recursive traits, as this would require an infinite list of parameters.