coinduction new normalizes-to solution

normalize to Vec<Alias>

trait Trait {
    type Assoc;
}

type Alias = <() as Trait>::Assoc;
impl Trait for () {
    type Assoc = Vec<Alias>;
}

• normalizes_to(Alias, Vec<Alias>)
  • equate(Vec<Alias>, Vec<Alias>) productive
    • equate(Alias, Alias) trivial identity: OK

While deeply normalizing Alias will result in overflow it won't be unsound.

Even with lazy normalization, we may still want to try to deeply normalize at the end of analysis to catch these cases early where possible. Or we just always treat stuff in the equate branch as inductive.

productive cycle constrain infer

trait Trait {
    type Assoc;
}

type Alias = <() as Trait>::Assoc;
impl Trait for () {
    type Assoc = Vec<Alias>;
}

• normalizes_to(Alias, ?0)
  • equate(Vec<Alias>, ?0) productive: ?0 = Vec<?1>[^2]
    • equate(Alias, ?1)
      • normalizes_to(Alias, ?1) productive cycle: OK

Have to rerun here because normalizes_to constrains an inference var, resulting in overflow at some point.

normalize to Vec<Vec<Alias>>

trait Trait {
    type Assoc;
}

type Alias = <() as Trait>::Assoc;
impl Trait for () {
    type Assoc = Vec<Vec<Alias>>;
}

• normalizes_to(Alias, Vec<Alias>)
  • equate(Vec<Vec<Alias>>, Vec<Alias>) productive
    • equate(Vec<Alias>, Alias)
      • normalizes_to(Alias, Vec<Alias>) productive cycle, OK

As above, we are hiding infinite types which will cause overflow when deeply normalizing but their deeply normalized types would be actually equal.

normalize indirect no cycle

trait Trait {
    type Assoc;
}
type Alias<T: Trait> = <T as Trait>::Assoc;
impl Trait for u8 {
    type Assoc = Alias<i8>;
}
impl Trait for i8 {
    type Assoc = ();
}

• normalizes_to(Alias<u8>, ())
  • equate(Alias<i8>, ()) not productive
    • normalizes_to(Alias<i8>, ())
      • equate((), ()) OK

indirect productive cycle

trait Trait {
    type Assoc;
}
type Alias<T: Trait> = <T as Trait>::Assoc;
impl Trait for u8 {
    type Assoc = Alias<i8>;
}
impl Trait for i8 {
    type Assoc = Vec<Alias<u8>>;
}

• normalizes_to(Alias<u8>, ?0)
  • equate(Alias<i8>, ?0) unproductive
    • normalizes_to(Alias<i8>, ?0)
      • equate(Vec<Alias<u8>>, ?0) productive
        • normalizes_to(Alias<u8>, ?1) productive cycle: OK

indirect unproductive cycle

trait Trait {
    type Assoc;
}
type Alias<T: Trait> = <T as Trait>::Assoc;
impl Trait for u8 {
    type Assoc = Alias<i8>;
}
impl Trait for i8 {
    type Assoc = Alias<u8>;
}

• normalizes_to(Alias<u8>, Vec<()>)
  • equate(Alias<i8>, Vec<()>) not productive
    • normalizes_to(Alias<i8>, Vec<()>)
      • equate(Alias<u8>, Vec<()>) not productive
        • normalizes_to(Alias<u8>, Vec<()>) unproductive cycle ERR

This fails how we expect it to.

cycle outside of eq OK

trait Trait {
    type Assoc;
}

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

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

• normalizes_to(Alias<i32>, ()) (non-rpoductive, normalization)
  • equate(Alias<u32>, ()) (non-productive, eq)
    • normalizes_to(Alias<u32>, ()) (non productive, normalization)
      • equate((), ()) ok
      • trait(i32: Trait) ok
      • normalizes_to(Alias<i32>, ()) (productive, where-clause ~> productive cycle ~> ok)

The cycle here is okay as the recursive normalizes_to(Alias<i32>, ()) is not part of the equate path.

cycle outside eq 2 OK

trait Trait {
  type Assoc;
}

impl<T> Trait for T
where
    u32: Other<Assoc<T> = ()>
{
    type Assoc = u32;
}

trait Other {
  type Assoc<T>
  where
    T: Trait<Assoc = u32>;
}

impl Other for u32 {
  type Assoc<T> = ();
  where
    T: Trait<Assoc = u32>;
}

• normalizes_to(<T as Trait>::Assoc, u32)
  • equate(u32, u32) OK
  • is_implemented(u32: Other) OK
  • normalizes_to(<u32 as Other>::Assoc<T>, ())
    • equate((), ()) OK
    • is_implemented(T: Trait) OK
    • normalizes_to(<T as Trait>::Assoc, u32) cycle: OK

cycle outside eq 3 fun

trait Trait where Self: Trait<Assoc = u32> {
    type Assoc;
}

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

impl WF check:

Environment: is_implemented(T: Trait), normalizes_to(<T as Trait>::Assoc, u32)

• is_implemented(T: Trait) from env: ok
• normalizes_to(<T as Trait>::Assoc, u32) from env: ok

using the impl OK:

• is_implemented(u32: Trait)
  • is_implemented(u32: Trait) cycle OK
  • normalizes_to(<u32 as Trait>::Assoc, u32)
    • equate(u32, u32) OK
    • is_implemented(u32: Trait) cycle OK
    • normalizes_to(<u32 as Trait>::Assoc, u32) cycle OK

using the impl ERR:

• is_implemented(u64: Trait)
  • is_implemented(u64: Trait) cycle OK
  • normalizes_to(<u64 as Trait>::Assoc, u32)
    • equate(u64, u32) ERR
    • is_implemented(u64: Trait) cycle OK
    • normalizes_to(<u64 as Trait>::Assoc, u32) cycle OK