Trait bounds on other traits AKA type class inheritance/composition

[yannbolliger]

Currently, trait bounds on traits are extracted as an inheritance relationship of the extracted abstract classes:

trait A { fn a(); }
trait B { fn b(); }
trait AB: A + B { ... } 

results in

 abstract class A[T] { def a(): () }
 abstract class B[T] { def b(): () }
 abstract class AB[T] extends A[T] with B[T]

However, inheritance is not very compatible with Rust's way of defining implementations of traits, as the following example shows. If one wants to generally implement the trait AB in Rust, one can do:

impl<T: A + B> AB for T { ... } 

which currently results in:

case class Implementation[T]((ev0: A[T]) @evidence, (ev1: B[T]) @evidence) extends AB[T]

But, that is not accepted by Stainless with the following error:

abstract methods A.a, B.b were not overridden by a method, a lazy val, or a constructor parameter.

Therefore, it would be more practical to handle trait bounds on traits with composition:

 abstract class AB[T] {
  def ev0: A[T]
  def ev1: B[T]
  @inline def a():() = ev0.a()
  @inline def b():() = ev1.b()
  ...
}