Make all match types invariant

[OlivierBlanvillain]

Covariant match types should be removed as they can lead to contractions. For example:

type Id[+X] = X match {
  case Int => Int
  case String => String
}

• Int & String <: String
• Id[Int & String] reduces to Int, Id[String] reduces to String
• By covariance of Id we can deduce that Int <: String, which is wrong.

[odersky]

I think the right approach is to make occurrences of type variables in scrutinee and patterns non-variant and to leave occurrences in the right-hand sides co-variant.

[OlivierBlanvillain]

I'm not sure I'm following. The issue I'm raising is about the match type itself being covariant. Currently, by writing a + in type Id[+X] the user can clam that forall A, B, A <: B implies M[A] <: M[B], but that can lead to inconsistencies.

Having variance in the type variable of scrutinee and patterns should be fine: that simply denotes a larger set of value. The algorithm implemented in #5996 accounts for those.

[odersky]

The way variance checkin works is that you traverse the type and characterize positions as non-variant, covariant or invariant. A type parameter declared co-variant may only occur in covariant positions, and so on.

Here's an example:

type F[+X, Y] = Y match {
  case Int => X
  case String => Int
}

That one is OK. So it depends where a type variable occurs.

Unfortunately, even this refined criterion breaks Tuple.scala in 5 locations. E.g.

  type Tail[+X <: NonEmptyTuple] <: Tuple = X match {
    case _ *: xs => xs
  }

  type Concat[+X <: Tuple, +Y <: Tuple] <: Tuple = X match {
    case Unit => Y
    case x1 *: xs1 => x1 *: Concat[xs1, Y]
  }

Both cases would be rejected, but they are not real errors, since the types are covariant.

[odersky]

Let's analyze why Concat is covariant in X (semantically):

• We know the match is exhaustive, since Unit and *: are the only two subclasses of Tuple.
• We know the patterns are non-overlapping

So that means, if X <: X1 <: Tuple, then Concat[X, Y] <: Concat[X1, Y] and it's safe to take X as covariant. I also have the feeling that it will be important not to lose this information.

But it's very subtle. We need both static reducibility (i.e. the bound of a type guarantees that the match always succeeds) and non-overlapping patterns (guaranteeing that the same case is chosen for X and X1.

[OlivierBlanvillain]

What about this proof that Unit is a subtype of Tuple2:?

Unit & (Int *: Unit) <: (Int *: Unit)

=> (by covariance of Concat on its first type parameter)
Concat[Unit & (Int *: Unit), Unit] <: Concat[(Int *: Unit), Unit]

=> (by match type reduction)
Unit <: (Int *: Unit)

[odersky]

Touche. I did not think about empty types. Yes, they ruin the argument.

But then how do we formulate a useful version of Tuple?

[OlivierBlanvillain]

What's the use case for variance here? The invariant Concat looks perfectly fine to me 😄

[LPTK]

When reducing a covariant match type Id[+T] applied to some A, as in Id[A], we should consider that A may only be a supertype of the type Id was originally applied on. So subtype patterns must necessarily be inconclusive! We shouldn't be able to reduce such covariant match types to anything, as is.

Wouldn't it be cleaner if match types used exact type patterns? As in, case Int => matches exactly Int and none of its subtypes. We could still of course bind type variables inside patterns, so it would still work for tuples. Subtype and supertype patterns could be recovered via the syntaxes _ <: Int and _ >: Int.

This would allow tuples to be covariant, because when matching S *: T with case Unit => we would be able to discard the case, as there can be no subtype of Unit that is exactly of the shape S *: T (since *: does not inherit form Unit.

[OlivierBlanvillain]

Wouldn't it be cleaner if match types used exact type patterns?

I think that would be problematic as soon as we try to type values with match types. For example, it would be nice to be able to type check the following:

def foo[X](x: X)
  : X match {
      case Int => 1
      case _   => 2
    }
  = x match {
      case _: Int => 1
      case _      => 2
  }

[LPTK]

@OlivierBlanvillain I don't see how that would work anyway.
Consider your function called as foo[Any](0), which would have type 2 but would return 1.

EDIT: I guess you meant something like this, which I wrote using a _ <: Int pattern to show that it's not that bad and actually better mirrors the value pattern:

def foo(x: Any)
  : x.type match {
      case _ <: Int => 1
      case _   => 2
    }
  = x match {
      case _: Int => 1
      case _      => 2
  }

[odersky]

**What's the use case for variance here? The invariant Concat looks perfectly fine to me 😄

To start, here are some cases from the tuples1.scala test that fail to compile:

  def concat[X <: Tuple, Y <: Tuple](x: X, y: Y): Tuple.Concat[X, Y] = x ++ y
  def head[X <: NonEmptyTuple](x: X): Tuple.Head[X] = x.head

I believe most people would expect these cases to work.

What one has to do is the following:

  def concat(x: Tuple, y: Tuple): Tuple.Concat[x.type, y.type] = x ++ y
  def head(x: NonEmptyTuple): Tuple.Head[x.type] = x.head

That works to some degree, but lacks a generalization capability. I.e. all the types we compute are forever tied to concrete singleton types. I don't think this is good enough.

[odersky]

Another approach that avoids the problem of empty types might be to add the rule:

• If S is empty, then S match { ... } reduces to Nothing

With that rule we might take scrutinee occurrences of type variables to be covariant, provided patterns are non-overlapping. That would let us leave Tuple.scala in the form it is.

There's still a tricky question to answer. Say you have a match alias

F[X] = X match {
  case Int => String
  case String => Int
}

Then F[Int] = String, but F[Any] does not reduce. However, String !<: F[Any]. Is that a violation of variance? Given the direct definition, sure. But can we construct an unsoundness example for this? I believe not, and would be really interested to see one.

Maybe we could equate a match type

  S match { ... }

semantically with the union of all reduced types of SS match {...} where SS is a subtype of S. Then
F[Any] would be equated with String | Int and variance would hold.

[odersky]

Interestingly, the union of all reduced types of SS match {...} where SS is a subtype of S is the dual of parallel reduction. Parallel reduction means we can fire more than one rule and intersect the results. The new rule would mean we take a non-deterministic choice of all rules that might match.

I am seeing more and more similarities with our understanding of GADTs. Here's an attempt at new match type reduction rules that bridge the gap:

A match type

    S match {
       case P_1 => B_1
       ...
       case P_n => B_n
    }

reduces to

  A_1 | ... | A_k

where As = A_1, .., A_k is the largest set of types such that:

• given a fresh variable x: S, if S is nonempty and x.type <: P_i is satisfiable with bindings s_i for the type variables in P_i then s_i B_i is in As

This aligns with our approach to GADTs and gives a justification for our handling of empty types. Indeed, if S is empty then As is empty, and the empty union is Nothing.

/cc @AleksanderBG

[odersky]

My intuition is that it's better not to have sequential reduction on the type level, so the "union of all cases that could possibly match" approach is attractive. True, at runtime match reduction is sequential. But that's relevant for the type system only insofar that the type we compute from a match expression or match type must be a supertype of the type we reduce to at runtime. And the union approach delivers oin that.

[OlivierBlanvillain]

To start, here are some cases from the tuples1.scala test that fail to compile:
[...]
I believe most people would expect these cases to work.

To me this looks like type inference and inlining working poorly together. In the following, dotty will happily infer both ++[X, Y] and ++[x.type, y.type] despite ++ being invariant:

type ++[x <: Tuple, y <: Tuple] <: Tuple =
  x match {
    case x *: xs => x *: ++[xs, y]
    case Unit    => y
  }

def ++[X <: Tuple, Y <: Tuple](x: X, y: Y): ++[X, Y] =
  (x match {
    case x *: xs => x *: ++(xs, y)
    case ()      => ()
  }).asInstanceOf[++[X, Y]]

def concat1[X <: Tuple, Y <: Tuple](x: X, y: Y): ++[X, Y] = ++(x, y)
def concat2[X <: Tuple, Y <: Tuple](x: X, y: Y): ++[x.type, y.type] = ++(x, y)
def concat3(x: Tuple, y: Tuple): ++[x.type, y.type] = ++(x, y)

My gut feeling is that at this point all the focus should be on correlating match types with expressions. Anything related HKT, variance, inlining, kind polymorphism is just less important than being able to use match types in programs without casts... Which is why I'm suggesting Plan A: make all match types invariant.

[odersky]

I think the fact that current tuples are "stuck to singleton types" under nonvariance has to with the fact that their implementation uses this.type extensively. But we have not yet shown that a different implementation is feasible. The proof is in the pudding where the pudding would be a new implementation of Tuple with updated tests.

My gut feeling is that at this point all the focus should be on correlating match types with expressions. Anything related HKT, variance, inlining, kind polymorphism is just less important than being able to use match types in programs without casts...

Agreed on that! Plus: keep tuples working.

Which is why I'm suggesting Plan A: make all match types invariant.

I am not sure that follows 😉

[odersky]

Good news: Tuples could be adapted to live in a non-variant world. #6050 implements variance checking rules for match types and adapts Tuple.scala to conform to them.

I believe we should still investigate the match-reduction with union-types idea.