Match types should be subtypes of the union of their case right-hand sides

[LPTK]

A match type is apparently not a subtype of the union of it branches. So this for instance does not work:

def flip: (x: 0 | 1) => x.type match { case 0 => 1 case 1 => 0 } = ???
val n: 0 | 1 = if ??? then 0 else 1
flip(n) // works
flip(flip(n)) // does not work: we don't have flip(n).type <: 0 | 1
val m: n.type match { case 0 => 1 case 1 => 0 } = flip(n)
flip(m) // does not work

-- [E007] Type Mismatch Error: tests/pos/i7807.scala:15:8 --------------------------------------------------------------
15 |   flip(m)
   |        ^
   |        Found:    (Test.m :
   |          (Test.n : (0 : Int) | (1 : Int)) match {
   |            case (0 : Int) => (1 : Int)
   |            case (1 : Int) => (0 : Int)
   |          }
   |        )
   |        Required: (0 : Int) | (1 : Int)

I would have expected it to work.

---

This was originally reported here: https://github.com/lampepfl/dotty/pull/7835#discussion_r361741296.

I think it ought to work, because whatever a match type reduces to, it is always one of its right-hand-sides, given some values for the types extracted from the pattern. Conceptually, the match type would be a subtype of the union of the match right-hand sides with the extracted type variables converted to wildcards (or otherwise avoided); for example we should treat X match { case List[t] => (t, t) } as a subtype of (_, _).

The algorithm could be the following: when solving a subtyping constraint with a match type on the left, try each right-hand side of the match type separately, making the pattern-extracted type variables rigid skolem variables (it looks like this can be done with the typer.ProtoTypes.constrained(_: TypeLambda) method).

I have tried adapting recur in TypeComparer to try the alternatives of a match type:

-        recur(tp1.underlying, tp2) || compareMatch
+        recur(tp1.bound, tp2) || tp1.alternatives.forall(recur(_, tp2)) || compareMatch

But this has problems with recursive match types: indeed, for these we will get into infinite deep subtyping recursions!

I did not find a way to detect if a match type is recursive. However, it should be possible to use the following approximation: if the match type has an explicit bound, assume it may be recursive; otherwise, use the algorithm above. This is sound because a recursive match type without a bound will give a cycle error anyways.

There is currently no way to test if a bound was provided explicitly (currently Any is picked during type assignment if no bound was given), but it could probably be done. An alternative would be to pick the type union as the bound itself when no bound is given.

What do you think?

[odersky]

This should be re-opened a a feature request. I believe it would be not at all easy to implement since it can cause new cycles. What is the upper bound of a recursive match type?

[LPTK]

@odersky my understanding was that a recursive match type requires an explicit user-provided upper bound, otherwise it raises a cyclic error. At least this is the behavior that I have observed.

So unless I am mistaken on that point, I do not see how this can create more cycles.

[OlivierBlanvillain]

An alternative would be to pick the type union as the bound itself when no bound is given.

That sounds like the best solution, it's easy to implement and doesn't affect soundness.