Type inference on nested GADTs

[OlivierBlanvillain]

Type inference fails to infer i: Int in the following pattern matching:

case class Pair[A, B](_1: A, _2: B)

trait Cons[+H, +T]

object Cons {
  def apply[H, T](h: H, t: T): Cons[H, T] = ???
  def unapply[H, T](t: Cons[H, T]): Option[Pair[H, T]] = ???
}

object Test {
  def main(args: Array[String]): Unit = {
    Cons(Option(1), None) match {
      case Cons(Some(i), None) =>
        i: Int // error: found: Any(i), requires: Int
        assert(i == 1)
    }
  }
}

-Xprint:frontend shows a union type in the unapply:

case Cons.unapply[Option[Int] | Some[Any], None$](
  Some.unapply[Any](i @ _): Some[Any], None
)

[odersky]

It works if Pair is declared as covariant.