Kernel calculus in a scala system (recursion)

Question

How Typer in the scala compiler checks the following:

class D[T <: D[T]] class E extends D[E] 

The upper bound D [T] of a parameter of class D must be compatible with E. Type E is not equivalent to D, therefore its base type D will be checked. Since the constructors of types of the base type E and D are equal, it is necessary to check the boundaries. And here comes the recursion. Core Calculus can't handle this.

Answer 1

1) Start with

 E extends D[E] 

2) Extensions imply subtyping in Scala, therefore

 E <: D[E] 

3) Due to the definition of "class D [T <: D [T]]", the requirement of T for any D [T] is that T <: D [T]. Step 2 said that E should be able to be connected to T, so it better meets this requirement. Substituting E for T, we obtain the requirement that

 E <: D[E] 

We already showed E <: D [E] in step 2. We are done.

Answer 2

There is no real answer, only two points : this template is known as CRTP , and it also works in Java (see java.lang.Enum )