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 the identical variables. 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.