Match type reduction of nested type constructors does not propagate contravariance

[sjrd]

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 Any

Output

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)?

[odersky]

I agree that the behavior is not according to spec and needs to be changed. I should not be the one charged with doing this, though. Maybe @Decel or @mbovel could take a look at it?

[odersky]

I believe the problem and the fix will be either in matchtype reduction or iun GADT constraint solving.

[Decel]

This isn't supposed to work, right?

class C[-T]

type F[X] = X match
  case C[C[t]] => t

def x: F[C[Any]] = ???

But it works and we have

==> normalize F[C[Any]]?
  ==> reduce match type C[Any] match {
  case C[C[t]] => t
} 1269408193?
  <== reduce match type C[Any] match {
  case C[C[t]] => t
} 1269408193 = Nothing
<== normalize F[C[Any]] = Nothing

[dwijnand]

Well C[Any] <: C[C[Nothing]], so it seems right.

[Decel]

Well C[Any] <: C[C[Nothing]], so it seems right.

Well, then it is not a bug. It's supposed to widen the type resulting from matching, not the original one. So in REPL cases, it widens the match, not the whole type. In the case of Any it widens what's left of the match. So for something like:

class C[-T]

type F[X] = X match
  case C[C[C[C[t]]]] => t // 4 C

def x: F[C[C[C[Any]]]] = ??? // 3 C

You get Nothing because C[Any] <: C[Nothing].

If we change this to fit the original example pattern, then in

type F[X] = X match
  case List[t] => t

def x: F[List[Nothing]] = ???

we would get Any instead of Nothing since it would widen the t, which is pretty bad...

[sjrd]

It's supposed to widen the type resulting from matching, not the original one.

What is your definition of "the type resulting from matching"? The only reasonable interpretation I can come up with is the right-hand-side of the =>. That would mean that we should always widen t in this case, and that therefore we should always get t = Any. That does not seem reasonable to me.

[Decel]

For

class C[-T]

type F[X] = X match
  case C[C[t]] => t

def x: F[C[C[_]]] = ???

It widens t, not C[C[t]], so we get Nothing.

In case of

class C[-T]

type F[X] = X match
  case C[C[t]] => t

def x: F[C[Any]] = ???

It widens C[t], not C[C[t]], and since its upper bound is C[Nothing], we get Nothing.

For Any case It's a bit counterintuitive since you get C[Nothing] and t = Nothing, but when you notice it, it makes sense.

[sjrd]

You haven't answered my question:

What is your definition of "the type resulting from matching"?

You give me two examples, both for the same match type with the pattern case C[C[t]] => t, but in one case you argue that it must widen t and in the other case you argue that it must widen C[t]. What is the rationale, here? Also, how do you explain the inconsistency with covariant type constructors, clearly illustrated in the first post?

[Decel]

I thought illustrating with examples was better, I am very sorry.

The type resulting from matching is the type we get after we unify scrutinee with the pattern. This type for C[C[t]] => t and C[C[_] is t, for C[C[t]] => t and C[Any] is C[t]. For case C[C[C[C[t]]]] => t and C[C[C[Any]]] it's C[t]

I don't understand the inconsistency with covariance, it seems to work correctly -- if you want to have a widening of C[C[t] with C[C[t]] => t and C[C[_]] then you should type instead C[C[C[t]]] => t and C[Any]. Otherwise, you get a widening of t to Nothing, since it's covariant, because that's what we get after unification.

(Also, it's very useful to think of t as _, when t is not inferred from def)

[Decel]

Although it's pretty counterintuitive, I agree!

But trying to change this is a recipe for disaster. The problem is -- what do you widen even?

If we widen the pattern we may run into the problem I have described above.
If we widen the scrutinee we can't really infer t.

And you can't really unify them so that you have the desired behavior.