Motivation
Currently, match type reduction stalls once a case is encountered that doesn’t match but cannot be shown to be disjoint either.
This prevents multiple base cases to be accessible. Consider the following code.
// Typelevel natural numbers
sealed trait Nat
case class Zero() extends Nat
case class Succ[N <: Nat](n: N) extends Nat
// Typelevel sum of natural numbers
type Sum[M <: Nat, N <: Nat] <: Nat = (M, N) match
case (Zero, _) => N
case (_, Zero) => M
case (Succ[predM], _) => Succ[Sum[predM, N]]
case (_, Succ[predN]) => Succ[Sum[M, predN]]
Sum
has two base cases. However, the second cannot apply as generally. For M
, N
<:
Nat
:

Sum[Zero, N]
reduces toN
. 
Sum[M, Zero]
is stuck and doesn’t reduce, as it is not known whetherM
isZero
.
Below is an example illustrating how this limitation impacts expressivity.
// Uniform tuple with length encoded as part of the type
sealed trait Uniform[Length <: Nat, T]:
def reversed: Uniform[Length, T] = reversedOnAcc(Empty())
def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[Sum[Length, M], T]
// Empy uniform tuple
case class Empty[T]() extends Uniform[Zero, T]:
def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[M, T] = acc
// Nonempty uniform tuple
case class Cons[PredL <: Nat, T](head: T, tail: Uniform[PredL, T]) extends Uniform[Succ[PredL], T]:
def reversedOnAcc[M <: Nat](acc: Uniform[M, T]): Uniform[Succ[Sum[PredL, M]], T] =
tail.reversedOnAcc(Cons(head, acc))
There doesn’t seem to be any way to rewrite Sum
that can make this code compile, as the reduction of both base cases is needed.
Proposal
In order to remedy this, the addition of a new reduction rule for match types is proposed.
Here are the objectives:
 Reduction should remain sound (and deterministic).
 Enhanced reduction should be compatible with current match type reduction.
 Expressivity should be enhanced (by allowing code like the example above to compile).
Here is an elaboration of objective 2: for any current match type reduction M
→ N
, either

N
is fully reduced. In that case, the new rule should not change the reduction. 
N
is not fully reduced. In that case, ifM
→R
with the new rule, thenN
also has to reduce toR
with the new rule.
If the two first objectives are satisfied, disruption should be minimized. Code that currently compiles should still compile and keep the same semantics.
The new rule is currently expressed as an additional subtyping rule for System FM (as defined in the paper TypeLevel Programming with Match Types). It is presented in the draft linked here, as I couldn’t find a way to include math directly here.
Concerns
One concern is how this would affect compiletime complexity. I do not think this is a fundamental issue for the proposal, as match types can already lead to arbitrary compiletime complexity for a project (family), including nonterminating.
To mitigate this concern further, a way could be added for the user to bound
the number of steps taken by the compiler during the match type reduction phase. This would already be useful now for current match type reduction.