Lack of match type bound reduction

[Bersier]

Compiler version

3.2.0

Minimized code

sealed trait Nat
case class Zero() extends Nat
case class Succ[N <: Nat](n: N) extends Nat

type PredOrZero[N <: Nat] = N match
  case Zero => Zero
  case Succ[predN] => predN

type PredOrZeroOption[N <: Nat] <: Option[PredOrZero[N]] = N match
  case Zero => None.type
  case Succ[predN] => Some[predN]

Output

Found:    Some[predN]
Required: Option[Playground.PredOrZero[N]]

Expectation

It is expected that any match type within the type bound be reduced with all available information. For the branch case Succ[predN], N is Succ[predN]. In other words, the code is expected to compile.

Note that this is distinct from refining the type bound directly with the available information within a branch, which would be unsound, as in the following example.

type Foo[N <: Nat] <: (N => Unit) = N match
  case Zero => (Zero => Unit)
  case Succ[predN] => (Succ[predN] => Unit)