Covariant annotation prevents match type 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

trait A[N <: Nat]:
  def bar: PredOrZero[N]

trait B[PredN <: Nat] extends A[Succ[PredN]]:
  override def bar: PredN

def foo[M <: Nat]: Unit =
  summon[PredOrZero[Succ[M]] =:= M]

Output

error overriding method bar in trait A of type => Playground.PredOrZero[Playground.Succ[PredN]];
  method bar of type => PredN has incompatible type

Expectation

The code is expected to compile.

Note that summon[PredOrZero[Succ[M]] =:= M] does compile, so the compiler knows they are equal.

The error goes away if the covariance annotation is removed (Succ[N <: Nat]).