SI-5189: refined GADT soundness fix

extrapolate GADT skolems: only complicate types when needed
make sure we only deskolemize GADT skolems after typedCase

1 files changed, 18 insertions, 0 deletions

diff --git a/test/files/neg/t5189b.scala b/test/files/neg/t5189b.scala
index 1750f14084..7c1871dc97 100644
--- a/test/files/neg/t5189b.scala
+++ b/test/files/neg/t5189b.scala
@@ -5,8 +5,21 @@ class TestPos {
   def unwrap[T](x: AbsWrapperCov[T]): T = x match {
     case Wrapper/*[_ <: T ]*/(x) => x // _ <: T, which is a subtype of T
   }
+
+  def unwrapOption[T](x: Option[T]): T = x match {
+    case Some(xs) => xs
+  }
+
+
+  case class Down[+T](x: T)
+  case class Up[-T](f: T => Unit)
+
+  def f1[T](x1: Down[T])(x2: Up[T]) = ((x1, x2)) match {
+    case (Down(x), Up(f)) => f(x)
+  }
 }
 
+
 object TestNeg extends App {
   class AbsWrapperCov[+A]
   case class Wrapper[B](x: Wrapped[B]) extends AbsWrapperCov[B]
@@ -33,6 +46,11 @@ object TestNeg extends App {
   // val w = new Wrapped(new A)
   // unwrap[Any](Wrapper(w)).cell = new B
   // w.cell.imNotAB
+
+  def unwrapOption[T](x: Option[T]): T = x match {
+    case Some(xs) => xs.foo // the error message should not refer to a skolem (testing extrapolation)
+  }
+
 }
 
 // class TestPos1 {