Description
Compiler version
3.3.0-RC2
Minimized code
As a REPL session:
scala> class Consumer[-T]
// defined class Consumer
scala> type F[X] = X match { case List[t] => t }
scala> def x: F[List[_]] = 5
def x: Any // OK
scala> type F[X] = X match { case Consumer[t] => t }
scala> def x: F[Consumer[_]] = ???
def x: Nothing // OK
scala> type F[X] = X match { case Consumer[List[t]] => t }
scala> def x: F[Consumer[List[_]]] = 5
def x: Any // KO. Expected Nothing
scala> type F[X] = X match { case Consumer[Consumer[t]] => t }
scala> def x: F[Consumer[Consumer[_]]] = ???
def x: Nothing // KO. Expected Any
scala> type F[X] = X match { case Consumer[Consumer[Consumer[t]]] => t }
scala> def x: F[Consumer[Consumer[Consumer[_]]]] = ???
def x: Nothing // OK, but it looks like chance
scala> type F[X] = X match { case Consumer[List[Consumer[t]]] => t }
scala> def x: F[Consumer[List[Consumer[_]]]] = ???
def x: Nothing // KO. Expected AnyOutput
In every case, t is instantiated to Any when the innermost type constructor is covariant, and to Nothing when the innermost type constructor is contravariant. The instantiation completely disregards any contravariant type constructor on the "path" from the top scrutinee down to the type parameter.
Expectation
The spec says:
Type parameters in patterns are minimally instantiated when computing S <: Pi. An instantiation Is is minimal for Xs if all type variables in Xs that appear covariantly and nonvariantly in Is are as small as possible and all type variables in Xs that appear contravariantly in Is are as large as possible. Here, "small" and "large" are understood with respect to <:.
I expect "that appear contravariantly" to actually take the whole path into account. So I expected the results shown in comments in the above REPL session.
Perhaps nesting type constructors in contravariant position of type match patterns should not even be allowed in the first place? It's very unclear to me how to specify that. Indeed, it means that we need to reverse the whole type match logic when we get in those situations. Normally, we unify a scrutinee S with a pattern P in a way that makes S <: P. It is quite clear what that means even when P is an applied type Pc[...Pi], because we can take the baseType(S, Pc) and extract the arguments from that. But now we should unify in a way that makes Pc[...Pi] <: S. What does that mean in general (without resorting to type inference and constraints, which do not exist after typer anymore)?