Dotty: Cannot reduce inline match with an enum-based Nat

[biboudis]

minimized code

  enum Nat {
    case Zero
    case Succ[N <: Nat](n: N)
  }
  import Nat._

  inline def toInt(n: => Nat): Int = inline n match {
    case Zero => 0
    case Succ(n1) => toInt(n1) + 1
  }

  val natTwo = toInt(Succ(Succ(Zero)))

results in a compile time error:

inline n match {
   |                                     ^
   |                                     cannot reduce delegate match with
   |                                      scrutinee:  {
   |                                       App.Nat.Succ.apply[App.Nat](App.Nat.Succ.apply[App.Nat](App.Nat$#Zero))
   |                                     } : App.Nat
   |                                      patterns :  case App.Nat$#Zero
   |                                                  case App.Nat.Succ.unapply[N$1 @ N$1](n1 @ _):App.Nat.Succ[N$1]

expectation

To work as the "old" encoding:

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

nitpick: the error message should have been about _inline match_ instead of _delegate_

[nicolasstucki]

@AleksanderBG you had some insight of how the N in case Succ[N <: Nat](n: N) is handled differently than in case class Succ[N <: Nat](n: N) extends Nat

[abgruszecki]

@nicolasstucki inline match AFAIR reduces based on the type of the expression and Succ(x) in the example always returns a Nat, so this just isn't going to work. You can even see in the error message that the type of the scrutinee is App.Nat:

   cannot reduce delegate match with
     scrutinee:  {
       App.Nat.Succ.apply[App.Nat](App.Nat.Succ.apply[App.Nat](App.Nat$#Zero))
     } : App.Nat

[abgruszecki]

Unassigning myself and removing the bug label, since this is more of a design limitation than a bug. We can talk about it during the next monday meeting.

[biboudis]

@odersky wdyt?

[odersky]

I agree it's a spec thing. One more fact that strengthens the case for making cases have the more specific type.