Error, Higher Kinded types Scala: type arguments do not conform. type T's bounds are stricter than type T's declared bounds

Question

Here is a simple experiment in Scala REPL:

scala> trait A; trait B extends A; trait C extends B
defined trait A
defined trait B
defined trait C

scala> trait TC[T]
defined trait TC

scala> trait TC2[T <: B]
defined trait TC2

scala> class Test[TC[T]]
warning: there was one feature warning; re-run with -feature for details
defined class Test

scala> new Test[TC]
res1: Test[TC] = Test@6f195bc3

scala> new Test[TC2]



<console>:11: error: kinds of the type arguments (TC2) do not conform to the expected kinds of the type parameters (type TC) in class Test.
TC2's type parameters do not match type TC's expected parameters:
type T (in trait TC2)'s bounds <: B are stricter than type T's declared bounds >: Nothing <: Any
       val res2 =
           ^
<console>:12: error: kinds of the type arguments (TC2) do not conform to the expected kinds of the type parameters (type TC) in class Test.
TC2's type parameters do not match type TC's expected parameters:
type T (in trait TC2)'s bounds <: B are stricter than type T's declared bounds >: Nothing <: Any
              new Test[TC2]
                  ^

Question 1:

How can these error messages be explained based on the Scala Language Specification ?

In other words, which sections of the SLS explain these error messages ?

Question 2:, how can these error messages be explained in simple terms (not based on SLS) ?

Phrasing the previous question in the compiler's words:

why is it a problem that TC2's type parameters do not match type TC's expected parameters, i.e. type T (in trait TC2)'s bounds <: B are stricter than type T's declared bounds >: Nothing ?

Is there any book or article where the reasoning behind this error message is explained ?

Perhaps somewhere in Pierce's TAPL book ?

Answer 1

As I note in a comment above, the TC in the type parameter list of Test (and in the error message) is not the TC that you defined a couple of lines earlier—it's a new type constructor parameter that shadows the trait TC.

(As a side note, I'd strongly suggest not shadowing type parameters. Shadowing variables at the value level can be confusing enough, but shadowing type parameters is almost always a recipe for confusion.)

Type constructor parameters are discussed in section 4.4 of the spec. From that section:

A type constructor parameter adds a nested type parameter clause to the type parameter... The above scoping restrictions are generalized to the case of nested type parameter clauses, which declare higher-order type parameters. Higher-order type parameters (the type parameters of a type parameter t) are only visible in their immediately surrounding parameter clause (possibly including clauses at a deeper nesting level) and in the bounds of t.

Your T here is one of these higher-order type parameters. It can be bounded (like any other type parameter), but it's not. This is what causes the error: you're trying to provide a type constructor that constrains its type parameter (TC2) as the value of a type constructor parameter that doesn't share the constraint (that in fact doesn't have any constraints at all).

To get an intuitive sense of why this is a problem, consider the following trait:

trait Foo[X[_]] {
  def create[A]: X[A]
}

This is a perfectly reasonable thing to write—I could create an instance for example like this:

object ListFoo extends Foo[List] {
  def create[A]: List[A] = Nil
}

Now suppose I have a type constructor with a constraint:

trait MyIntOptionThingy[A <: Option[Int]]

The compiler prohibits me from instantiating a Foo[MyIntOptionThingy] because the type parameter of MyIntOptionThingy is constrained more strictly than the type parameter of the X in Foo's type parameter list. If you think about it this makes sense: how would I be able to define create for any A, when the only As that would work for MyIntOptionThingy are Some[Int], None.type, and Option[Int]?