-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Closed
Labels
itype:bugitype:soundnessSoundness bug (it lets us compile code that crashes at runtime with a ClassCastException)Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)stat:fixed in nextThe issue was fixed in Next and only still applies to LTS.The issue was fixed in Next and only still applies to LTS.
Description
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.
Metadata
Metadata
Assignees
Labels
itype:bugitype:soundnessSoundness bug (it lets us compile code that crashes at runtime with a ClassCastException)Soundness bug (it lets us compile code that crashes at runtime with a ClassCastException)stat:fixed in nextThe issue was fixed in Next and only still applies to LTS.The issue was fixed in Next and only still applies to LTS.