Why do proper types Any and Nothing fit type constructor shape F[_] when they are different kinds?

Viewed 47

Consider the following method which takes type parameter of * -> * kind

def g[F[_]] = ???

Why is the following not a syntax error

g[Any]       // ok
g[Nothing]   // ok

since

scala> :kind -v Any
Any's kind is A
*
This is a proper type.

scala> :kind -v Nothing
Nothing's kind is A
*
This is a proper type.

so Any and Nothing should be of wrong shape?

1 Answers

Quotes from Scala spec:

For every type constructor (with any number of type parameters), scala.Nothing <: <: scala.Any.

https://scala-lang.org/files/archive/spec/2.13/03-types.html#conformance

Say the type parameters have lower bounds 1,…, and upper bounds 1,…,. The parameterized type is well-formed if each actual type parameter conforms to its bounds, i.e. <:<: where is the substitution [1:=1,…,:=].

https://scala-lang.org/files/archive/spec/2.13/03-types.html#parameterized-types

A polymorphic method type is denoted internally as [tps] where [tps] is a type parameter section [1 >: 1 <: 1,…, >: <: ] for some ≥0 and is a (value or method) type. This type represents named methods that take type arguments 1,…, which conform to the lower bounds 1,…, and the upper bounds 1,…, and that yield results of type .

https://scala-lang.org/files/archive/spec/2.13/03-types.html#polymorphic-method-types

So since Any and Nothing conform to upper and lower bounds of F[_] (namely, Any and Nothing correspondingly), g[Any] and g[Nothing] are legal.

Related