In Scala 3, why is it sometimes possible to do impredicative type assignment?

Question

Scala 3 is an impredicative language, it is generally impossible to assign higher kind to normal type (at the risk of triggering Girard's paradox), but in reality, some type assignment appears to be able to bypass this rule:

      trait Vec[T]

      type VV1 = Vec // paradox!

      type VV2 = [T] =>> Vec[T] // no paradox?

What are the differences between the last 2 lines? Why is the second one possible?

Answer 1

The second line is possible because language authors decided that type alias can contain type constructor for consistency. If List is a type despite not being a proper type, so can be a type alias if we want to be consistent. And if functions can be curried, partially applied or passed over, so can be types.

trait Vec[T]

type VV1 = Vec // not! a paradox, but shorthand for type VV1 = [T] =>> Vec[T]

Second line is equal to third line:

A parameterized type definition

type T[X] = R

is regarded as a shorthand for an unparameterized definition with a type lambda as right-hand side:

type T = [X] =>> R

A partially applied type constructor such as List is assumed to be equivalent to its eta expansion. I.e, List = [X] =>> List[X]. This allows type constructors to be compared with type lambdas.

See specification for more details.

Answer 2

Found the cause: In Scala, higher-kind orders cannot be correlated with the syntax of the type name, a 0-type and 2-type can both be assigned to a type name. They only differs in behaviour when being consumed:

      type VV2 = [T <: AnyVal] =>> Vec[T] // no paradox?

      type NN = List[VV2] // still paradox!
      // : Type argument VV2 does not have the same kind as its bound 

Regarding the first definition type VV = Vec, it is probably prohibited by the compiler due to some parsing ambiguity