Match type upper bounds lead to unexpected compiler behavior

[Bersier]

Compiler version

3.1.3

Minimized code

sealed trait IntT
sealed trait NatT extends IntT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT
final case class Minus[+N <: Succ[NatT]](n: N) extends IntT

type NatDif[X <: NatT, Y <: NatT] <: IntT = Y match
  case _0 => X
  case Succ[y] => X match
    case _0 => Minus[Y]
    case Succ[x] => NatDif[x, y]

type NatDivH[X <: NatT, Y <: Succ[NatT], Z <: NatT] <: (NatT, NatT) = NatDif[X, Y] match
  case Minus[_] => (Z, X)
  case _0 => (Succ[Z], _0)
  case Succ[x] => NatDivH[Succ[x], Y, Succ[Z]]

type NatDiv[X <: NatT, Y <: Succ[NatT]] <: (NatT, NatT) = Y match
  case _1 => (X, _0)
  case _ => NatDivH[X, Y, _0]

type Second[P] = P match
  case (_, y) => y

type NatRem[X <: NatT, Y <: Succ[NatT]] = Second[NatDiv[X, Y]]

type NatRem2[X <: NatT, Y <: Succ[NatT]] <: NatT = NatDiv[X, Y] match
  case (_, y) => y

@main def main(): Unit =
  _1: Second[NatDiv[_3, _2]] // No error, as expected.
  _1: Second[NatDiv[_3, _1]] // Error, as expected.
  _1: NatRem[_3, _1] // No error, unexpected.
  _1: NatRem2[_3, _2] // Error, unexpected.

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]

val _0: _0 = Zero()
val _1: _1 = Succ(_0)

Output

See here.

The unexpected error for _1: NatRem2[_3, _2]:

Match type reduction failed since selector  (Succ[_0], Succ[Zero])
matches none of the cases

    case (_, y) => y

Expectation

Removing the type bounds from the match type definitions fixes the unexpected errors or lack thereof. It is unexpected that the behavior of the code should change based on redundant type bounds. Moreover, the error messages seem misleading at best. See this thread.

[Bersier]

I managed to minimize the code further (it should also be easier to follow):

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT

type ZeroAndSecondNat[X <: NatT, Y <: Succ[NatT]] <: (NatT, NatT) = Y match
  case Succ[_] => (_0, Y)

type Second[P] = P match
  case (_, y) => y

type SecondNat[X <: NatT, Y <: Succ[NatT]] = Second[ZeroAndSecondNat[X, Y]]

type SecondNat2[X <: NatT, Y <: Succ[NatT]] <: NatT = ZeroAndSecondNat[X, Y] match
  case (_, y) => y

@main def main(): Unit =
  _2: Second[ZeroAndSecondNat[_1, _2]] // No error, as expected.
  _2: Second[ZeroAndSecondNat[_1, _1]] // Error, as expected.
  _2: SecondNat[_1, _1]                // No error, unexpected.
  _2: SecondNat2[_1, _2]               // Error, unexpected.

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]

val _0: _0 = Zero()
val _1: _1 = Succ(_0)
val _2: _2 = Succ(_1)

@dwijnand Is that small enough?

[dwijnand]

Yep, thank you.

[dwijnand]

Likely the same cause as #15926.

[Bersier]

I tried this with Scala 3.4.0-RC4, and the minimized code now behaves as expected. However, the original code still behaves oddly. Here is some new minimized code:

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT

type NatDiv[X <: NatT, Y <: Succ[NatT]] <: (NatT, NatT) = Y match
  case _1 => (X, _0)
  case _ => (_1, _1)

type NatRem2[X <: NatT, Y <: Succ[NatT]] = NatDiv[X, Y] match
  case (_, y) => y

@main def main(): Unit =
  _1: NatRem2[_3, _2] // Error, unexpected.

type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]

val _0: _0 = Zero()
val _1: _1 = Succ(_0)

The compiler error:

Found:    (_1 : _1)
Required: NatRem2[_3, _2]

Note: a match type could not be fully reduced:

  trying to reduce  NatRem2[_3, _2]
  failed since selector (_1, _1)
  is uninhabited (there are no values of that type).

@sjrd