Skip to content

Instantly share code, notes, and snippets.

@adriaanm
Created February 27, 2012 17:05
Show Gist options
  • Save adriaanm/1925479 to your computer and use it in GitHub Desktop.
Save adriaanm/1925479 to your computer and use it in GitHub Desktop.
why the old GADT typing rules are wrong
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
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment