match types do not support AnyKind

[soronpo]

Not sure if this is a bug, a wanted limitation or just an overlook.
There are two issues with any-kinded types and match types.

1. Inability to match against an any-kinded type.
2. Inability to reduce an any-kinded type, when it "falls-in" the match through the "other" case clause.

Compiler version

Master branch

Minimized code

type Fix1[T <: AnyKind] = T match
  case Option[a] => Option[a]
  case Option    => Option[Int]

type Fix2[T <: AnyKind] = T match
  case Option[a] => Option[a]
  case _         => Option[Int]

Output

[error] 3 |  case Option    => Option[Int]
[error]   |       ^^^^^^
[error]   |       Missing type parameter for Option

[error] 5 |type Fix2[T <: AnyKind] = T match
[error]   |                            ^
[error]   |                            Match type reduction failed since selector  T
[error]   |                            matches none of the cases
[error]   |
[error]   |                                case Option[a] => Option[a]
[error]   |                                case _ => Option[Int]

Expectation

No error.

[sjrd]

I don't think match types were designed to support higher-kinded types. It's unclear how their spec actually behaves in the presence of higher-kinded types, in particular the disjointness criteria. Also, the formalization of match types in Olivier's thesis, which is the ultimate reference for match types, studies them in the context of F<:, which does not have higher-kinded types at all.

I think we should emit an earlier compile error at the level of the definition of those match types, complaining that the scrutinee is not *-kinded (i.e., <: Any).

[LPTK]

Yes, I don't think disjointness makes sense for higher-kinded types. HKTs talk about type functions rather than values, and it's usually possible to find greatest lower bounds between any two similarly-kinded types. For example, regardless of A, B, C, D, the types [X <: A] =>> B[X] and [X <: C] =>> D[X] are never disjoint because the type-level function [X <: Any] =>> Nothing can be assigned both types.

def f[F <: [X <: Int] =>> Int] = ()
def g[F <: [X <: String] =>> List[X]] = ()

f[[X <: Any] =>> Nothing] // compiles
g[[X <: Any] =>> Nothing] // compiles