Currently, match type reduction stalls once a case is encountered that doesn’t match but cannot be shown to be disjoint either.
I often find myself in situations where that prevents my code from type-checking.
For value-level matches, the sequentiality of the matching process is not an issue, since it never stalls on a case. However, at the type level, it significantly reduces expressivity.
I wonder if there is any accessible (backwards-compatible) Scala 3 language change that would allow parallel match types to be expressed (where any case that matches could be used to reduce the match type, regardless of case order).
Here is an example where I think parallel match types would be necessary (and sufficient) to get the code to compile. If there were parallel match types, then
Sum could be written as
type Sum[M <: NatT, N <: NatT] <: NatT = (M, N) parallel match case (_, Zero) => M case (Zero, _) => N case (_, Succ[predN]) => Sum[Succ[M], predN]
Of course, one would have to decide on the semantics of when multiple cases match. But several acceptable solutions seem to exist in that case.