Dependent typing without no-longer-supported type ascriptions

Question
1

Starting with Scala 3.3,

Type ascriptions after patterns other than:

  • variable pattern, e.g. case x: String =>
  • number literal pattern, e.g. case 10.5: Double =>

are no longer supported. Remove the type ascription or move it to a separate variable pattern.

I relied on such type ascriptions for certain forms of dependent typing. The code below is an example. Is there a way to rewrite it without such type ascriptions?

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match
  case z: Zero => z
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[?]] => dependentlyTypedMod2(predPredN)

type Mod2[N <: NatT] <: NatT = N match
  case Zero => Zero
  case Succ[Zero] => Succ[Zero]
  case Succ[Succ[predPredN]] => Mod2[predPredN]

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

I think I found a solution:

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match
  case _: Zero => Zero()
  case s: Succ[?] => s match
    case Succ(predN) => predN match
      case _: Zero => Succ(Zero())
      case s: Succ[?] => s match
        case Succ(predPredN) => dependentlyTypedMod2(predPredN)

type Mod2[N <: NatT] <: NatT = N match
  case Zero => Zero
  case Succ[predN] => predN match
    case Zero => Succ[Zero]
    case Succ[predPredN] => Mod2[predPredN]

sealed trait NatT
case class Zero() extends NatT
case class Succ[N <: NatT](n: N) extends NatT
1 Like
3

This has quite a bit of boilerplate. It would be nice if type ascriptions were allowed again as syntactic sugar for such nested match expressions.

1 Like