Type inference for GADTs prevents writing type-safe code

[rnd4222]

Given the following code it is not possible to write f() without using asInstanceOf (while code itself is correct and well-typed).
Note that it's not even possible to annotate something without getting "type erasure" warning to guide type inference.

object Example {
  def f[A, E](l1: L1[A, E]) = l1 match {
    case L1L(L2Cons(L2Nil()), l3) =>
      L1L3(L3Cons(L1L3(l3.asInstanceOf))) // removing asInstanceOf here causes compile error
    case _ => ???
  }

  sealed trait L1[+A, +E]
  case class L1L3[A, E](l3: L3[A, E]) extends L1[A, E]
  case class L1L[A, Z, E](l2: L2[A, Z], l3: L3[Z, E]) extends L1[A, E]

  sealed trait L2[+A, +E]
  case class L2Nil[A]() extends L2[A, A]
  case class L2Cons[A, E](tail: L2[List[A], E]) extends L2[A, E]

  sealed trait L3[+A, +E]
  case class L3Cons[A, E](tail: L1[List[A], E]) extends L3[A, E]
}

[rnd4222]

@smarter it is not actually fixed in dotty, see https://scastie.scala-lang.org/NhD0zPOyQvSOxWJ3FCpMxA

[smarter]

@rnd4222 Try it with a local version of dotty for example by running sbt console in https://github.com/lampepfl/dotty-example-project. Scastie is using a really old version of dotty because of scalacenter/scastie#281.

[rnd4222]

@smarter OK, got it.
Any chances it would be fixed in Scala 2.x?

[smarter]

Realistically, no. GADTs are a complicated topic and already known to be broken in various ways in Scala 2, so nothing is likely to change unless someone spends significant amount of time to improve things.