---
# System prepended metadata

title: Rust for non-Rustacean math-y types

---

# Rust for non-Rustacean math-y types

*This hackmd is prepared for the purposes of discussion with folks familiar with PL/proof/logic/etc but not so much with Rust.*

## Overarching goals for today

* We have some practical problems
    * Want to extend our semantics to be coinductive but not sure how to handle 
    * How to best describe associated types ("beyond syntactic equality")
* We have some more abstract problems
    * We want to map Rust's trait system to logical concepts so we can reason about it better
    * Building an (executable) model of the Rust type system to serve as a "spec" ([a-mir-formality](https://github.com/rust-lang/a-mir-formality))

## Simple Rust program

```rust
trait Clone {
    fn clone(&self) -> Self;
}

impl Clone for u32 {
    fn clone(&self) -> Self {
        *self
    }
}

impl<T> Clone for Option<T>
where
    T: Clone,
{
    fn clone(&self) {
        match self {
            Some(x) => x.clone(),
            None => (),
        }
    }
}

fn foo<T: Clone>(t: T) {
    t.clone();
}

fn main() {
    foo(22);
    foo(Some(22));
}
```

## Supertraits

```rust
trait Eq: PartialEq {} // supertrait

trait PartialEq {
    fn partial_eq(self, other: Self) -> bool;
}

fn foo<T: Eq>(a: T, b: T) {
    //    ^^
    a.partial_eq(b)
}
```

## Associated types

```rust
trait Iterator {
    type Item: Clone;
    
    fn next(&mut self) -> Option<Self::Item>;
}

fn clone_all<I: Iterator>(i: I) {
    while let Some(elem) = i.next() {
        // elem has type `I::Item`...
        
        elem.clone(); // ...and we know that impl `Clone`
    }
}
```

## Rust 0

Grammar

```
Program := (TraitDefn | StructDefn | Implementation)*

TraitDefn := trait Tr {}

Ty := S < {Ty} >
    | X

StructDefn := struct S < {X} >

Implementation := impl<{X}> Tr for Ty where WC {}

WC := (Ty : Tr)
    | WC, WC

X := identifier of a generic parameter
```

## Defining Rust trait solver

So given a `Program`, when can we judge a given trait to be implemented?

We'll define a judgment `WC_a |- WC_g`. This means that, given the assumptions `WC_a`, `WC_g` is provable.

So far WC is just `(Ty: Tr)`, so e.g. `|- (u32: Clone)` says that `Clone` is implemented for `u32`.


```
substituted impl Tr for Ty_t where WC
Ty_t = Ty_s
A |- WC
------------------------------- impl
A |- (Ty_s: Tr)
```


```
impl<{X}> Tr for Ty_t where WC
let S be some substitution for {X}
S Ty_t = Ty_s
A |- S WC
------------------------------- impl
A |- (Ty_s: Tr)
```

```rust
impl Clone for u32 where true

impl<T> Clone for Option<T>
where
    T: Clone,
```


```
impl<T> Clone for Option<T> where (T: Clone)
S = { T => u32 }          -- inferred by the compiler via unification
S Option<T> = Option<u32> --after-substitution--> Option<u32> = Option<u32>
A |- S (T: Clone)         --after-substitution-->  A |- (u32: Clone)
------------------------------- impl
A |- (Option<u32>: Clone)
```

And we can define some basic connectives:

```
------------------------------- environment
..., WC_i, ... |- WC_i
```

```
A |- WC_0
A |- WC_1
------------------------------- and
A |- WC_0 && WC_1
```

...and some basic things like weakening, reordering, which I won't bother to list.

## Defining Rust trait solver

Now we can use this to prove interesting things like `Option<u32>: Clone`:

* `Option<u32>: Clone`, from `impl<T> Clone for Option<T> where T: Clone` with substitution `[u32 / T]`
    * `u32: Clone`, from `impl Clone for u32`

## Extending to higher-ranked stuff

More interestingly, we can extend WC to include higher-ranked things and implications:

```
WC = (WC && WC)
   | (T: Trait)
   | forall<X> WC
   | (WC => WC)
```
 
with rules like

```
X not free in A, Program
A |- WC
------------------------------- forall-introduction
A |- forall<X> WC
```

and

```
(A, WC_0) |- WC_1
------------------------------- implication-introduction
A |- (WC_0 => WC_1)
```

and

```
A |- (forall<X> WC_0)
------------------------------- forall-elimination
A |- { Ty / X } WC_0
```

```
A |- (WC_0 => WC_1)
A |- WC_0
------------------------------- implies-left
A |- WC_1
```

Why would we do this? As it happens, Rust includes "higher-ranked trait bounds",
but we also need to be able to do forall and implication just to do basic type checking. 
For example, consider this function:

```rust
fn clone_t<T>(t: T)
where
   T: Clone,
{
    let o: Option<T> = Some(t);
    o.clone();                   // valid if `Option<T>: Clone`
}
```

To prove that `o.clone()` is valid, the type-checker wants to judge that `Option<T>: Clone`.
We can express that as

```
|- forall<T> ((T: Clone) => (Option<T>: Clone))
```

and we can prove this via the above rules

* `|- forall<T> ((T: Clone) => (Option<T>: Clone))`, then by rule "forall-introduction"..
    * `|- ((T: Clone) => (Option<T>: Clone))`, by rule "implication-introduction"...
        * `(T: Clone) |- (Option<T>: Clone)`, by rule "impl"...
            * `(T: Clone) |- (T: Clone)`, by rule environment.

### ill-typed program


```rust
fn clone_t<T>(t: T)
{
    let o: Option<T> = Some(t);
    o.clone();                   // valid if `Option<T>: Clone`
}
```

* `|- forall<T> (Option<T>: Clone)`, then by rule "forall-introduction"..
    * `|- (Option<T>: Clone)`, by rule "impl"...
        * `|- (T: Clone)` cannot be proven


### Supertrait declarations

Extend grammar

```
TraitDefn = trait Tr: Tr {}
```

so that e.g.

```rust
trait Eq: PartialEq {} // supertrait
trait PartialEq {}
```

can be permitted by a rule

```
trait Trait2: Trait1 {}
A |- (T: Trait2)
------------------------- supertrait v1
A |- (T: Trait1)
```

## More ill-typed

```rust
trait Clone { fn clone(&self) -> Self; }

struct S { }

fn main() {
    let s = S { };
    s.clone(); // ERROR -- if this were to execute, we would have no method definition to use
    // "goes wrong"
}
```

## What does soundness mean?

What does proving

```
|- WC
```

*mean*? We are trying to maintain an invariant here, that `WC` is *truly true*, meaning...

* When `WC = (T: Trait)`, then
    * `T` is a struct in the program
    * and there exists a (substituted) impl such that `Self = T` and all WC are *truly true*
* When `WC = forall<{X}> WC_0`, then
    * for any well-defined substitution `S` such that `S WC_0` is *truly true*
        * where well-defined means that it only refers to structs declared in the program
* When `WC = WC_0 => WC_1`, then
    * if `WC_0` is *truly true*, then `WC_1` is *truly true*
        * (or *provable* implies *truly true*?)
* When `WC = WC_0 && WC_1`, then
    * both `WC_0` and `WC_1` are *truly true*

We would like to guarantee that

* If `|- WC` then `WC` is *truly true*. 

The rule system we developed so far does not meet this property -- because of supertraits.

## But

```rust
trait Eq
where
    Self: PartialEq,
{ }

trait PartialEq {
    fn partial_eq(&self);
}

impl Eq for u32 { }

// This is missing:
//
// impl PartialEq for u32 { fn partial_eq(&self) { X } }

fn main() {
    let t: u32 = 22;
    t.partial_eq(); // Provable, but should it be?
}
```

* `|- (u32: PartialEq)`, via supertrait rule (which says that `Eq=>PartialEq`)
    * `|- (u32: Eq)`, via impl (`impl Eq for u32`)
        * ok!

## Possible solutions

### Validate the impl

```
trait Tr: Tr1 {}
|- forall<{X}> (WC => Ty: Tr1)
----------------------------
|- impl<{X}> Tr for Ty where WC { } OK
```

But what about

```rust
trait Clone {  fn clone(&self) -> Self; }

trait Magic: Clone
impl<T: Magic> Magic for T {
    /* ok on its own */
}

fn main() {
    let t: u32 = 22;
    t.clone()
    // "almost" provable, even though there is no `impl Clone for u32`
}
```

* `|- u32: Clone`, via supertrait (MAgic => Clone)
    * `|- u32: Magic`, via impl
        * `|- u32: Magic`, via impl
            * `|- u32: Magic`, via impl
                * ...never get a finite proof tree...
                    * today we are inductive, but we want to be coinductive

This impl appears well-formed. Using it will cause an infinite proof, however (but see coinduction notes later).

#### Forbid blanket impls like this?

Also forbids useful patterns that we rely on everywhere, most obviously...

```rust
trait Extension: BaseTrait {
    fn new_method(&self);
}
impl<T: BaseTrait> Extension for T {
//   ^^^^^^^^^^^^ "syntactically" the same
    fn new_method(&self) {
        /* just use methods from the base trait */
    }
}
```

...in general enforcing ordering etc gets tricky.

### Check the assumptions when you use the impl

Our solution:

```
impl<{X}> Tr for Ty_t where WC {}
trait Tr: Tr1 {}       // <-- changed
let S be some substitution for {X}
S Ty_t = Ty_s
A |- S WC
A |- (Ty_s: Tr1)       // <-- changed
------------------------------- impl v2
A |- (Ty_s: Tr)
```

## Desired change to Rust: coinductive semantics

We allow people to write `#[derive(Clone)]`. This will autogenerate the code for cloning. Given a struct like this

```rust
#[derive(Clone)]
struct Tree<T> {
    data: T,
    children: Vec<Tree<T>>,
}

// impl<T> Clone for Vec<T> where T: Clone { .. }
```

it could for example generate

```rust
impl<T> Clone for Tree<T>
where
    T: Clone,
    Vec<Tree<T>>: Clone,
{
    fn clone(&self) -> Self {
        Tree {
            data: self.data.clone(),
            children: self.children.clone(),
        }
    }
}
```

OK, so far so good. But now you go to prove, say, that `Tree<u32>: Clone` and you get...

* `Tree<u32>: Clone` if
    * `u32: Clone` -- true
    * `Vec<Tree<u32>>: Clone` if
        * `Tree<u32>: Clone`
            * cycle -- in an inductive semantics, this is an error

We would like to shift to coinductive semantics. In fact, we already have it for some traits (e.g., `Send`, which indicates a thread-safe data structure).

### BUT: implications

We can't just take the rules we've been using and interpret them coinductively.
It will break with supertraits.

```rust
trait Eq: PartialEq
```

then we had the equivalent of a rule like

```
A |- T: Eq
-------------
A |- T: PartialEq
```

which is clearly not productive. This can be "weaponized":

```rust
trait Haha: Clone { }
impl<T: Haha> Haha for T { }
```

would result in

```
A |- T: Haha
--------- "supertrait"
A |- T: Clone
```

```
A |- T: Haha
--------- "impl"
A |- T: Haha
```

given these traits and impls, you can prove `X: Clone` for any type `X`
(not just those types that have impls).

How?

* `X: Clone`, using "supertrait"
    * `X: Haha`, using "impl"
        * ... (ad infinitum)
            * `X: Haha`, using "impl"

### How we are handling it in our model today

Don't permit "general" coinduction. Instead, only allow coinductive reasoning when proving impl where clauses:

```
trait Tr: Tr1 {}
impl<{X}> Tr for Ty_t where WC {}
let S be some substitution for {X}
S Ty_t = Ty_s
A, (Ty_s: Tr) |- S WC  // <-- changed
// ~~~~~~~~~~ permit cycles
A |- (Ty_s: Tr1)
------------------------------- impl v3
A |- (Ty_s: Tr)
```

Simplified


```
trait Trait: TrSuper {}
substituted impl Trait for Ty_self where WC {}
A, (Ty_self: Trait) |- WC                        // <-- coinductive
A |- (Ty_self: TrSuper)
------------------------------- impl v3
A |- (Ty_self: Trait)
```


```
trait Trait: TrSuper {}
A, later (Ty_self: Trait) |- (Ty_self: Trait) implemented
A, later (Ty_self: Trait) |- (Ty_self: TrSuper)
-------------------------------
A |- (Ty_self: Trait)
```

```
substituted impl Trait for Ty_self where WC {}
A0, (Ty_self: Trait) |- WC
------------------------------- impl
A0, later (Ty_self: Trait) |- (Ty_self: Trait) implemented
```

Now if we have a "cyclic" impl like so

```rust
trait Magic: Clone { }
impl<T: Magic> Magic for T { }
```

* `|- u32: Clone`, via supertrait rule
    * `|- u32: Magic`, via impl
        * `(u32: Magic) |- (u32: Magic)` (impl where clauses) -- OK!
            * via assumption
        * `|- u32: Clone` (because `trait Magic: Clone`)
            * cycle (rules are inductive --> error)

you can still try to prove `T: Clone` by first proving `T: Magic` but then you just have to prove `T: Clone` again (without the benefit of the cyclic assumption).

## What does soundness mean... coinductively?

Let's say a WC `WC` is *truly true* if

* When `WC = (T: Trait)`, then there exists a (substituted) impl such that `Self = T` and all WC are *truly true*
* When `WC = forall<{X}> WC_0`, then for any substitution `S` such that `S WC_0` is *truly true*
* When `WC = WC_0 => WC_1`, then if `WC_0` is *truly true*, then `WC_1` is *truly true*
    * (or *provable* implies *truly true*?)
* When `WC = WC_0, WC_1`, then both `WC_0` and `WC_1` are *truly true*

We would like to guarantee that

* If `|- WC` then `WC` is *truly true*. 

## Challenges and questions so far

* How do we define *soundness*?
    * We can show that whenever you can prove `|- Ty: Foo`, there wll always be an `impl` rather trivially by induction
* But can we relate that to an approximation of an underlying "logic"?
    * e.g., translate `impl<T> Clone for Option<T> where T: Clone` to `(Option<T>: Clone) :- (T: Clone)` and interpret coinductively
    * show that our solver is an approximation of that
        * for example `impl<T> Trait for T where Option<T>: Trait` is coinductively true (infinite proof tree) but it is not provable in our system
    * but then what about `forall` and implication, and how do we take into account supertraits?
        * e.g. `forall<T> ((T: Eq) => (T: PartialEq))` should be a provable WC, but we can't translate `trait Eq: PartialEq` to `(T: PartialEq) :- (T: Eq)` and still interpret coinductively
    * what precedent is there here to look at?

### Sidenote: Elaborating assumptions?

```
(Ty: Eq) in A
A, (Ty: PartialEq) |- WC
------------------------ "supertrait(Eq/PartialEq)"
A |- WC
```

## Associated types (or "aliases")

Grammar

```
Program := (TraitDefn | StructDefn | Implementation)*

TraitDefn := trait Tr where WC { AssocTypeDefn }
//                               ~~~~~~~~~~~~~ new

AssocTypeDefn := type Assoc : {Tr}     // <-- new

Ty := S < {Ty} >
    | X
    | Ty::Assoc                        // <-- new 
    

StructDefn := struct S < {X} >

Implementation := impl<{X}> Tr for Ty where WC { AssocTypeValue }
//                                               ~~~~~~~~~~~~~~ new

AssocTypeValue := type Assoc = Ty     // <-- new

WC := (Ty : Tr)
    | Ty: Tr<Assoc = Ty>              // <-- new
    | WC, WC

X := identifier of a generic parameter
```

```rust!
trait Clone { }
impl Clone for u32 { }

trait Iterator {
    type Item: Clone; // <-- associated type
    
    fn next(&mut self) -> Option<Self::Item>;
}

impl<T> Iterator for Vec<T>
where
    T: Clone,
{
    type Item = T;

    fn next(&mut self) -> Option<Self::Item> {
        ..
    }
}

fn foo<I>(iter: &mut I)
where
    I: Iterator,
{
    let v: Option<I::Item> = iter.next();
    v.clone();
}

fn main() {
    let v: Vec<u32> = Vec::new();
    
    let i: Option< u32                           > = v.next();
    let j: Option< <Vec<u32> as Iterator>::Item  > = v.next();
}
```

## What does soundness mean... for associated types

Let's say a WC `WC` is *truly true* if

* When `WC = Ty0: Tr<Assoc = Ty1>`, then
    * there exists exactly one (substituted) impl `I` such that
        * `Self = Ty0`,
        * all its WC are *truly true*,
        * `I` defines `Assoc` as `Ty1` (after subst).
    * (exactly one = job of coherence, out of scope?)

and, as before, unchanged

* When `WC = (T: Trait)`, then there exists a (substituted) impl such that `Self = T` and all WC are *truly true*
* When `WC = forall<{X}> WC_0`, then for any substitution `S` such that `S WC_0` is *truly true*
* When `WC = WC_0 => WC_1`, then if `WC_0` is *truly true*, then `WC_1` is *truly true*
    * (or *provable* implies *truly true*?)
* When `WC = WC_0, WC_1`, then both `WC_0` and `WC_1` are *truly true*

We would like to guarantee that

* If `|- WC` then `WC` is *truly true*. 

## 

* `Vec<X> = Vec<u32>` => `X = u32`
* `X::Item = u32::Item` => ?
    * just as `f(x) = f(y)` does not tell me that `x = y` for an arbitrary function `f`


```rust
fn foo<X: Iterator<Item = u32>>(x: X) {
    X::Item ==> u32
}
```


```rust!
fn foo<U, X: Iterator<Item = U>>(x: X) {
    X::Item ==> U
}
```

## 

```
WC = T: Trait<Assoc = U> 
```

```
A |- U = T::Assoc
------------------------------- fallback
A |- T: Trait<Assoc = U>
```

```
substituted impl Tr for T where WC { type Assoc = S<U>; }
A, T: Trait<Assoc = S<U>> |- WC
------------------------------- normalize-via-impl
A, later(T: Trait<Assoc = S<U>>) |- T: Trait<Assoc = S<U>>
```

```
trait Trait0 { type Assoc: Trait1 }
------------------------------- fallback
A |- T::Assoc: Trait1
```

```
---------------------------
A |- T = T
```


```
A |- T: Trait<Assoc = U1>
A |- U1 = U2
---------------------------
A |- (T::Assoc) = U2
```

### cyclic normalization impl

```rust
trait Trait {
    type Assoc;
}

impl Trait for i32 {
    type Assoc = <u32 as Trait>::Assoc;
}

impl Trait for u32
where
    i32: Trait<Assoc = ()>,
{
    type Assoc = ();
}
```

- `|- i32: Trait<Assoc = ()>` normalize via impl
    - (no where clause, output = `<u32 as Trait>::Assoc`)
    - `|- <u32 as Trait>::Assoc = ()` eq-via-normalize
        - `|- u32: Trait<Assoc = ()>` normalize via impl <-- productive
            - in where-clause `|- i32: Trait<Assoc = ()>` cycle
            - `|- () = ()`, ok because "duh"

```rust=
trait OtherTrait {
    type OtherAssoc;
}

trait Trait<U> {
    type Assoc;
}

impl<U: OtherTrait> Trait<U> for i32 {
    type Assoc = <u32 as Trait<U>>::Assoc;
}

impl<U: OtherTrait> Trait<U> for u32
where
    i32: Trait<U, Assoc = U::OtherAssoc>,
{
    type Assoc = U::OtherAssoc;
}

impl OtherTrait for i32 {
    type OtherAssoc = <i32 as Trait<i32>>::Assoc;
} // forall<T> { i32: Trait<i32, Assoc = T> }
```

- `|- i32: Trait<U, Assoc = U::OtherAssoc>` normalize via impl
    - (no where clause, output = `<u32 as Trait<U>>::Assoc`)
    - `|- <u32 as Trait<U>>::Assoc = U::OtherAssoc` eq-via-normalize
        - `|- u32: Trait<U, Assoc = U::OtherAssoc>` normalize via impl
            - `|- i32: Trait<Assoc = U::OtherAssoc>` cycle

- `|- i32: Trait<i32, Assoc = T>` normalize-via-impl
    - no where clauses
    - `|- <u32 as Trait<i32>>::Assoc == T` eq-via-norm
        - `|- u32: Trait<i32, Assoc = T>` normalize via impl
            - where-clause `|- i32: Trait<i32, Assoc = <i32 as OtherTrait>::OtherAssoc>`, normalize-via-impl
                - no where-clauses
                - `|- <u32 as Trait<i32>>::Assoc = <i32 as OtherTrait>::OtherAssoc`, eq-via-norm
                    - `|- u32: Trait<i32, Assoc = <i32 as OtherTrait>::OtherAssoc>`, normalize-via-impl
                        - `|- i32: Trait<i32, Assoc = ...>`
            - normalized type eq `|- <i32 as OtherTrait>::OtherAssoc = T` eq-via-nom
                - `|- i32: OtherTrait<OtherAssoc = T>` norm-via-impl
                    - no where-clauses
                    - `|- <i32 as Trait<i32>>::Assoc = T`, eq-via-norm
                        - `|- i32: Trait<i32, Assoc = T>` -- cycle (at the top)

### failure mode 1: normalize to anything

```rust
trait Trait {
    type Assoc;
}

impl Trait for u32 {
    type Assoc = u32::Assoc;
}
```

With naive rules we can prove...

* `|- forall<T> { u32::Assoc = T }`, via whatevr:
    * `|- u32::Assoc = T`, via alias-norm:
        * `|- u32: Trait<Assoc = u32::Assoc>`, via normalize-fallback
            * `|- u32::Assoc = T`, cycle (coinductively ok?)

...this seems bad.

### associated type bounds cyclic reasoning

```rust
trait Trait {
    type Assoc: Copy;
}

impl<T: Trait> Trait for T {
    type Assoc = String;
      // <T as Trait>::Assoc: Copy
}


impl<T: Trait> Trait for T {
    type Assoc = String;
      // <T as Trait>::Assoc: Copy
}

fn foo<T: Trait>(y: T::Assoc) -> (T::Assoc, T::Assoc) {
    (y, y)
}

fn main() {
    foo::<u32>(String::from("hello, world")); // double free!!
    // (u32: Trait) but `(String: Copy)` doesn't hold.
}
```

currently proves the following when checking that the impl is correct

(proving that the impl is valid)
- `|- forall<T> (T: Trait => T::Assoc: Copy)`
    - `|- T: Trait => T::Assoc: Copy`
could this be
- `|- forall<T> (T: Trait => String: Copy)`
    - TODO


we also try to prove `T::Assoc: Copy` in `foo`

we also prove `u32: Trait` when you call `foo` in `main`



```
trait Tr { type Assoc: Tr_a }
substituted impl Tr for T where WC { type Assoc = U1; }
A, (T: Trait<Assoc = U>) |- WC
A |- U1 = U2
A |- (U1: Tr_a)
------------------------------- normalize-via-impl
A |- T: Trait<Assoc = U2>
```


## "implied bounds"

```
A |- (Ty : Tr_a)
trait Tr_a { .. type Assoc : Tr .. }
-------------------------------
A |- (Ty::Assoc: Tr)
```

## "normalization"

```
trait Tr: Tr1 { .. type Assoc : {Tr_a} .. }
impl<{X}> Tr for Ty_t where WC { .. type Assoc = Ty_i .. }
let S be some substitution for {X}
S Ty_t = Ty_s
S Ty_i = Ty_a               // <-- new
A, (Ty_s: Tr) |- S WC
A |- (Ty_s: Tr1)
A |- (Ty_a: Tr_a)           // <-- new
------------------------------- normalize-impl
A |- (Ty_s: Tr<Assoc = Ty_a>)
```

## "normalization fallback"

```
------------------------------- normalize-fallback
A |- (Ty: Tr<Assoc = Ty::Assoc>)
```

## "equality"

### "reflexive"

```
A |- (Ty_1 = Ty_0)
------------------------------- fallback
A |- (Ty_0 = Ty_1)
```

*this can't be interpreted coinductively...*

### "rigid equality"

```
{Ty_0} = {Ty_1}
------------------------------- rigid
A |- (S<{Ty_0}> = S<{Ty_1}>)
```

### "alias equality, base case"

```
A |- T_0 = T_1
------------------------------- alias-opaque
A |- (T_0::Assoc = T_1::Assoc)
```

### "alias equality, normalized case"

```
A |- (T_0: Tr<Assoc = U0>)
A |- U0 = U1
------------------------------- alias-norm
A |- (T_0::Assoc = U1)
```


## some "fun" examples

from [lcnr's notes](https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view)

### ex0

```rust
trait Trait {
    type Assoc;
}

impl Trait for () {
    type Assoc = <()>::Assoc;
}
```

With naive rules we can prove...



* `|- forall<T> { <u32>::Assoc = T }`
    * `|- u32::Assoc = T`, via alias-norm:
        * `|- u32: Trait<Assoc = u32::Assoc>`, via normalize-fallback
        * `|- u32::Assoc = T`, cycle (coinductively ok?)

...this seems bad.

## Random links

* https://hackmd.io/cnX6oA28RwOPfRCTeyLw4Q?view
* https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view

#### stuff


```rust
trait CloneIterator {
    type Item: Clone;
}

fn foo<T: CloneIterator<Item = U>, U>(u: U) {
    u.clone();
}
```