Unexpected ClassCastException

[Bersier]

Compiler version

3.3.2

Minimized code

dependentlyTypedMod2(Succ(Succ(Succ(Zero()))))

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match
  case Zero(): Zero => Zero()
  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

Output

java.lang.ClassCastException: class Succ cannot be cast to class Zero

Expectation

Succ(Zero())

See this issue.

[sjrd]

This already does not compile on 3.4.0 anymore.

[Bersier]

@sjrd 3.3 is an LTS.

Also, how would you express this without the ascriptions?

[sjrd]

@sjrd 3.3 is an LTS.

True. We can reopen. Although not sure anyone's going to work on this since match types before SIP-56 have been demonstrated to be unsound and depending on the whims of type inference.

Also, how would you express this without the ascriptions?

I don't know about that. I haven't looked into it.