SI-5189: refined GADT soundness fix

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

5 files changed, 30 insertions, 9 deletions

diff --git a/test/files/neg/t3015.check b/test/files/neg/t3015.check
index 53221b7ca0..6948392bb0 100644
--- a/test/files/neg/t3015.check
+++ b/test/files/neg/t3015.check
@@ -1,5 +1,5 @@
 t3015.scala:7: error: scrutinee is incompatible with pattern type;
- found   : _$1 where type +_$1
+ found   : _$1
  required: String
   val b(foo) = "foo" 
        ^
diff --git a/test/files/neg/t3481.check b/test/files/neg/t3481.check
index 48e6ff357b..debe07275b 100644
--- a/test/files/neg/t3481.check
+++ b/test/files/neg/t3481.check
@@ -1,17 +1,17 @@
 t3481.scala:5: error: type mismatch;
  found   : String("hello")
- required: _$1 where type +_$1
+ required: _$1
     f[A[Int]]("hello")
               ^
 t3481.scala:11: error: type mismatch;
- found   : _$2 where type +_$2
+ found   : _$2
  required: b.T
     (which expands to)  _$2
     def f[T <: B[_]](a: T#T, b: T) = b.m(a)
                                          ^
 t3481.scala:12: error: type mismatch;
  found   : String("Hello")
- required: _$2 where type +_$2
+ required: _$2
     f("Hello", new B[Int])
       ^
 t3481.scala:18: error: type mismatch;
diff --git a/test/files/neg/t4515.check b/test/files/neg/t4515.check
index ce5350b35f..a60d16295f 100644
--- a/test/files/neg/t4515.check
+++ b/test/files/neg/t4515.check
@@ -1,6 +1,6 @@
 t4515.scala:37: error: type mismatch;
  found   : _0(in value $anonfun) where type _0(in value $anonfun)
- required: (some other)_0(in value $anonfun) where type +(some other)_0(in value $anonfun)
+ required: (some other)_0(in value $anonfun)
         handler.onEvent(target, ctx.getEvent, node, ctx)
                                     ^
 one error found
diff --git a/test/files/neg/t5189b.check b/test/files/neg/t5189b.check
index 7f78cbb438..46996e96d0 100644
--- a/test/files/neg/t5189b.check
+++ b/test/files/neg/t5189b.check
@@ -1,8 +1,11 @@
-t5189b.scala:25: error: type mismatch;
- found   : TestNeg.Wrapped[?T2] where type ?T2 <: T
+t5189b.scala:38: error: type mismatch;
+ found   : TestNeg.Wrapped[?T7] where type ?T7 <: T (this is a GADT skolem)
  required: TestNeg.Wrapped[T]
-Note: ?T2 <: T, but class Wrapped is invariant in type W.
+Note: ?T7 <: T, but class Wrapped is invariant in type W.
 You may wish to define W as +W instead. (SLS 4.5)
     case Wrapper/*[_ <: T ]*/(wrapped) => wrapped // : Wrapped[_ <: T], which is a subtype of Wrapped[T] if and only if Wrapped is covariant in its type parameter
                                           ^
-one error found
+t5189b.scala:51: error: value foo is not a member of type parameter T
+    case Some(xs) => xs.foo // the error message should not refer to a skolem (testing extrapolation)
+                        ^
+two errors found
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 {