Core calculus in scala type system (recursion)

Question

How does the Typer in the scala compiler verify the following:

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

The upper bound D[T] of class D's type parameter must be compatible with E. Type E is not equivalent to D, so its base type D will be checked. Because the type constructors of E's base type and D are equal, the bounds must be checked. And here comes the recursion. The Core Calculus does not handle this.

Answer 1

1) Start with

E extends D[E]

2) Extends implies subtyping in Scala, so

E <: D[E]        

3) Because of the definition "class D[T <: D[T]]", the requirement on T for any D[T] is that T <: D[T]. Step 2 said E must be able to be able to be plugged in to T, so it better match that requirement. Substituting E for T we get the requirement that

E <: D[E]

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

Answer 2

No real answer, just two remarks: This pattern is known as CRTP, and it works in Java, too (see java.lang.Enum)