The core idea is that all traits are mapped to dependent types - their dictionary - with fields for their super predicates and their associated items. The dictionary for item bounds are stored together with the associated type itself. Let's look at a few such mappings by converting them into lean4 code.

trait Foo {}

/- The dictionary for `Foo` does not have any fields -/
inductive Foo (self : Type) : Type where
| mk : Foo self

trait Bar<T>: Foo {}

/- The dictionary has the dictionary for the super trait `Foo` as a field -/
inductive Bar (self : Type) (t : Type) : Type where
| mk : Foo self -> Bar self t 

trait Baz<T> {
    type Assoc<U: Bar<T>>: Foo;
}

/- We've got a separate dictionary for associated types, containing both
the underlying type and dictionaries for the item bounds of that type -/
inductive BazAssoc (self : Type) (t : Type) (u : Type) : Type where
| mk : (assoc_type: Type) -> Foo assoc_type -> BazAssoc self t u
/- The dictionary for `Baz` contains a function taking the type parameter
`U`, a proof that `U: Bar<T>` holds and then returns the dictionary for the
associated type -/
inductive Baz (self : Type) (t : Type) : Type where
| mk : (assoc: (u : Type) -> Bar u t -> BazAssoc self t u) -> Baz self t

Implementations of these traits then get mapped to functions taking their where-clauses as arguments and returning a dictionary:

impl Foo for u32 {}

def impl_Foo_for_u32 : Foo Nat := Foo.mk

impl<T: Foo> Bar<T> for T {}

def impl_Bar_T_for_T (t : Type) (dict : Foo t) : Bar t t := Bar.mk dict

impl Baz<u32> for u32 {
    type Assoc<U: Bar<u32>> = U;
}

def impl_Baz_u32_for_u32 : Baz Nat Nat :=
  let assoc := fun (u : Type) (dictB : Bar u Nat) => 
    let (Bar.mk dictF) := dictB /- access the super trait dictionary -/
    BazAssoc.mk u dictF
  Baz.mk assoc

We then lower the proof tree created by the trait solver to a function. Let's go through all the ways a trait goal can be proven by the trait solver:

• we've already seen the way impls get lowered; applying an impl simply corresponds to calling the corresponding function
• applying a where-bound simply uses the function argument representing this bound
• applying an elaborated where-bound corresponds to a field access of a function argument
• applying an item bound corresponds to a field access of the associated type dictionary
• a coinductive cycle gets lowered to a recursive call

We do not need the resulting function to terminate. It only has to be a well-formed corecursive function. A corecursive function may not necessarily terminate itself, but matching on the returned value has to be guaranteed to terminate in finite amount of time. Lets look at a few examples:

// pseudo-Rust
enum Stream<T> {
   Nil,
   Cons(T, Stream<T>),
}
// Well-formed: guaranteed to fully terminate
fn repeat_n<T>(elem: T, count: usize) -> Stream<T> {
   match count {
       0 => Stream::Nil,
       n + 1 => Stream::Cons(elem, repeat_n(elem, n)), 
   }
}
// Well-formed: while it doesn't terminate, matching on its return value
// will, leaving an infinitely expanding lazily evaluated tail.
fn repeat<T>(elem: T) -> Stream<T> {
    Stream::Cons(elem, repeat(elem))
}
// Not well-formed: unlike `fn repeat` we never make progress while computing
// the return value of this function.
fn loop<T>() -> Stream<T> {
    loop()
}

The functions corresponding to proof trees are not guaranteed to be well-formed by construction. This is due to multiple reasons. Lets quickly go through issues which don't affect the changes in this PR them before looking at our requirements for coinductive cycles.

We need to both introduce and check Type universes to avoid Girard's paradox. Even the above example doesn't actually compile in lean, we need to explicitly provide universe information at places, which may restrict the way the trait dictionaries can be used:

inductive Foo (self : Type 0) : Type 1 where
| mk : Foo self

def impl_Foo_for_u32 : Foo Nat := Foo.mk

inductive Bar (self : Type 0) (t : Type 0) : Type 1 where
| mk : Foo self -> Bar self t
def impl_Bar_u32_for_u32 : Bar Nat Nat := Bar.mk impl_Foo_for_u32

inductive BazAssoc (self : Type 0) (t : Type 0) (u : Type 0) : Type 1 where
| mk : (assoc_type: Type 0) -> Foo assoc_type -> BazAssoc self t u
inductive Baz (self : Type 0) (t : Type 0) : Type 1 where
| mk : (assoc: (u : Type) -> Bar u t -> BazAssoc self t u) -> Baz self t
def impl_Baz_u32_for_u32 : Baz Nat Nat :=
  let assoc := fun (u : Type) (dictB : Bar u Nat) => 
    let (Bar.mk dictF) := dictB
    BazAssoc.mk u dictF
  Baz.mk assoc

I am not convinced this is an actual be an issue as we're never generic over dictionary kinds; we do not have "associated traits".

We allow potentially diverging associated types. Using these definitely does not terminate, see rust-lang/rust#135011.

These are forbidden in lean and coq. They can be used to get non-terminating functions. I am unsure whether this is an issue affected us, given the fairly limited complexity of the functions representing proof trees.

trait Magic {
    type Assoc<T: Magic>: Copy;
}

inductive Copy (self : Type 0) : Type 1 where
| mk : Copy self
inductive MagicAssoc (self : Type 0) (t : Type 0) : Type 1 where
| mk : (assoc_type : Type 0) -> Copy assoc_type -> MagicAssoc self t
inductive Magic : (self : Type 0) -> Type 1 where
| mk : (assoc : (t : Type) -> Magic t -> MagicAssoc self t) -> Magic self

(kernel) arg #2 of 'Magic.mk' has a non positive occurrence of the datatypes being declared

For a corecursive function to be accepted, the recursive calls must be guarded. It must be inside of at least one constructor, as seen in the fn repeat example above. This guarantees that evaluating the function is always able to make at least one step progress per recursive call.

However, this is not yet sufficient as we may project out of this constructor again. This is what would be happening in the following example:

trait Magic: Copy {}
impl<T: Magic> Magic for T {}
fn magic_copy<T: Magic>(x: T) -> (T, T) { (x, x) }

We would map this to the following:

inductive Copy (self : Type) : Type where
| mk : Copy self

inductive Magic (self : Type) : Type where
| mk : Copy self -> Magic self

def impl_Magic_for_T (t : Type) (dict: Magic t) : Magic t :=
  let (Magic.mk dictC) := dict
  Magic.mk dictC

/- To call `fn magic_copy`, we need to prove `T: Magic` -/
def call_magic_copy (t: Type) : Magic t :=
  impl_Magic_for_T t (call_magic_copy t)

We could expand the body of call_magic_copy to only call itself inside of a constructor. However, the field access discards that constructor regardless.

def impl_Magic_for_T_inline (t : Type) (dict: Magic t) : Magic t :=
  Magic.mk (
    let (Magic.mk dictC) := dict
    dictC
  )

def call_magic_copy (t: Type) : Magic t :=
  Magic.mk (
    let (Magic.mk dictC) := (call_magic_copy t)
    dictC
  )

Citing from "Certified Programming with Dependent Types" by Adam Chlipala we can see how this is handled in Coq:

Coq’s complete rule for co-recursive definitions includes not just the basic guardedness condition, but also a requirement about where co-recursive calls may occur. In particular, a co-recursive call must be a direct argument to a constructor, nested only inside of other constructor calls or fun or match expressions.

Enforcing this (or a similar condition) for our proof trees is somewhat difficult to reason about. However, let's look at the ways proof trees get lowered to functions. The only ways to project out of a constructor are the following:

• accessing an associated item, either its type or its item bounds
• accessing super predicates

Both of these things are not possible for auto traits. We can therefore freely allow cycles guarded by an auto trait constructor, as this constructor can never be projected out of!