Avoid direct Skolem types in lower GADT bounds

By constraining T s.t. T >: Sko(U) and T >: Sko(U), we end up with
T >: Sko(U) | Sko(U), which is a singleton type union and is
simplified to T >: U, which is wrong for this case.

To avoid this, we record only the _consequence_ of having a Skolem type
in a bound.

This is a temporary workaround while we cannot take unions and
intersections of singleton types and should be removed in the future.

Author: abgruszecki

compiler/src/dotty/tools/dotc/core/Contexts.scala

@@ -779,6 +779,21 @@ object Contexts {
         }, gadts)
       }
 
+      // avoid recording skolems in lower bounds
+      // recording two skolem bounds results in an union, which is then simplified
+      // T >: Sko(U) | Sko(U) is simplified to T >: U, which is simply wrong
+      // instead, we only ensure that new bounds would be satisfiable
+      // TODO: this likely causes unsoundness
+      // TODO: it should be removed after we added support for singleton type unions
+      if (!isUpper) bound match {
+        case _: SkolemType =>
+          val TypeBounds(lo, hi) = bounds(sym)
+          val newLo = lo | bound
+          gadts.println(i"replacing skolem bound  $sym <:< $bound  with  $newLo <:< $hi")
+          return newLo <:< hi
+        case _ => ;
+      }
+
       val symTvar: TypeVar = stripInternalTypeVar(tvar(sym)) match {
         case tv: TypeVar => tv
         case inst =>

tests/neg/int-extractor.scala

@@ -8,10 +8,24 @@ object Test {
       0 // error
   }
 
+  def foo2[T](t: T): T = t match {
+    case EssaInt(_) => t match {
+      case EssaInt(_) =>
+        0 // error
+    }
+  }
+
   case class Inv[T](t: T)
 
   def bar1[T](t: T): T = Inv(t) match {
     case Inv(EssaInt(_)) =>
       0 // error
   }
+
+  def bar2[T](t: T): T = t match {
+    case Inv(EssaInt(_)) => t match {
+      case Inv(EssaInt(_)) =>
+        0 // error
+    }
+  }
 }

tests/neg/invariant-gadt.scala

@@ -17,4 +17,11 @@ object `invariant-gadt` {
         0 // error
     }
   }
+
+  def unsoundTwice[T](t: T): T = Invariant(t) match {
+    case Invariant(_: Int) => Invariant(t) match {
+      case Invariant(_: Int) =>
+        0 // error
+    }
+  }
 }