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/ConstraintHandling.scala

@@ -30,6 +30,7 @@ trait ConstraintHandling[AbstractContext] {
 
   protected def isSubType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean
   protected def isSameType(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Boolean
+  protected def typeLub(tp1: Type, tp2: Type)(implicit actx: AbstractContext): Type
 
   protected def constraint: Constraint
   protected def constraint_=(c: Constraint): Unit
@@ -126,7 +127,7 @@ trait ConstraintHandling[AbstractContext] {
           homogenizeArgs = Config.alignArgsInAnd
           try
             if (isUpper) oldBounds.derivedTypeBounds(lo, hi & bound)
-            else oldBounds.derivedTypeBounds(lo | bound, hi)
+            else oldBounds.derivedTypeBounds(typeLub(lo, bound), hi)
           finally homogenizeArgs = saved
         }
         val c1 = constraint.updateEntry(param, narrowedBounds)

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

@@ -803,6 +803,10 @@ object Contexts {
     override def isSubType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSubType(tp1, tp2)
     override def isSameType(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = ctx.typeComparer.isSameType(tp1, tp2)
 
+    override protected def typeLub(tp1: Type, tp2: Type)(implicit ctx: Context): Type = {
+      ctx.typeComparer.lub(tp1, tp2, admitSingletons = true)
+    }
+
     override def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit = tvar(sym)
 
     override def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean = {

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

@@ -34,6 +34,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   override protected def externalize(param: TypeParamRef)(implicit ctx: Context): Type = param
 
+  override protected def typeLub(tp1: Type, tp2: Type)(implicit actx: AbsentContext): Type =
+    lub(tp1, tp2)
+
+
   private[this] var pendingSubTypes: mutable.Set[(Type, Type)] = null
   private[this] var recCount = 0
   private[this] var monitored = false
@@ -1429,9 +1433,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   /** The least upper bound of two types
    *  @param canConstrain  If true, new constraints might be added to simplify the lub.
-   *  @note  We do not admit singleton types in or-types as lubs.
+   *  @param admitSingletons We only admit singletons as parts of lubs when we must maintain necessary conditions,
+   *                         such as when inferring GADT constraints.
    */
-  def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false): Type = /*>|>*/ trace(s"lub(${tp1.show}, ${tp2.show}, canConstrain=$canConstrain)", subtyping, show = true) /*<|<*/ {
+  def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, admitSingletons: Boolean = false): Type = /*>|>*/ trace(s"lub(${tp1.show}, ${tp2.show}, canConstrain=$canConstrain)", subtyping, show = true) /*<|<*/ {
     if (tp1 eq tp2) tp1
     else if (!tp1.exists) tp1
     else if (!tp2.exists) tp2
@@ -1443,6 +1448,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
       else {
         val t2 = mergeIfSuper(tp2, tp1, canConstrain)
         if (t2.exists) t2
+        else if (admitSingletons) orType(tp1.widenExpr, tp2.widenExpr)
         else {
           val tp1w = tp1.widen
           val tp2w = tp2.widen
@@ -1968,9 +1974,9 @@ class ExplainingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       super.hasMatchingMember(name, tp1, tp2)
     }
 
-  override def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false): Type =
-    traceIndented(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain)") {
-      super.lub(tp1, tp2, canConstrain)
+  override def lub(tp1: Type, tp2: Type, canConstrain: Boolean = false, admitSingletons: Boolean = false): Type =
+    traceIndented(s"lub(${show(tp1)}, ${show(tp2)}, canConstrain=$canConstrain, admitSingletons=$admitSingletons)") {
+      super.lub(tp1, tp2, canConstrain, admitSingletons)
     }
 
   override def glb(tp1: Type, tp2: Type): Type =

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
+    }
+  }
 }