why the old GADT typing rules are wrong

patmat_gadt.scala

class TestPos2 {
  class Base[+T]
  case class C[T](x: T) extends Base[T]
  def foo[T](b: Base[T]): T =
    b match { 
      case C(x) =>
        // since b: Base[T] and Base is covariant in T, b: Base[X forSome {type X <: T}], where we may assume Base to be invariant in its first type parameter
        // thus, since b is actually a C[U], we may assume that U =:= X forSome {type X <: T}
        // hence, x: X forSome {type X <: T}, or, by subsumption, x: T
        x
    }
}

class TestNeg1 {
  case class Foo[T, U](f: T => U)
  def f(x: Any): Any => Any = x match { case Foo(bar) => bar }
  // uh-oh, Any => Any should be Nothing => Any.
}

object TestNeg2 extends App {
  class Wrapped[W](var x: W) // must be invariant (to trigger the bug)
  class AbsWrapperCov[+B] // must be covariant
  case class Wrapper[T](underlying: Wrapped[T]) extends AbsWrapperCov[T]

  def unwrap[A](it: AbsWrapperCov[A]): Wrapped[A] = it match {
    case Wrapper(wrapped) =>
      // since it: AbsWrapperCov[A] and AbsWrapperCov is covariant in A,
      // it: AbsWrapperCov[X forSome {type X <: A}], where we may assume AbsWrapperCov to be invariant in its first type parameter
      // thus, since `it` is actually a Wrapper[W], we may assume that W =:= X forSome {type X <: A}
      // hence, wrapped: Wrapped[X forSome {type X <: A}], which is not a subtype of Wrapped[A] since Wrapped is invariant in its first type parameter
      wrapped

    // -Yvirtpatmat says:
    // matchRes4 = <error: value wrapped>;
    // found   : Test.Wrapped[T] where type T <: A
    // required: Test.Wrapped[A]
    // which is the right thing to do, I'd say (try running this test)
    // however, the plain pattern matcher accepts this program
    // what's worse, the standard library relies on stuff like this type checking... 

      // from JavaConversions:
      //
      // implicit def asJavaIterator[A](it: Iterator[A]): ju.Iterator[A] = it match {
      //   case JIteratorWrapper(wrapped) => wrapped
      //   case _ => IteratorWrapper(it)
      // }

  }  

  class A { def imNotAB = println("notB")}
  class B

  val w = new Wrapped(new A)
  unwrap[Any](Wrapper(w)).x = new B
  w.x.imNotAB
}