Change type lub behaviour for GADT constraints

Author: abgruszecki

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

@@ -27,6 +27,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
@@ -102,7 +103,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

@@ -797,6 +797,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 = try {
@@ -822,21 +826,6 @@ 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 =>

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

@@ -32,6 +32,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
   def constraint: Constraint = state.constraint
   def constraint_=(c: Constraint): Unit = state.constraint = c
 
+  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
@@ -1415,9 +1418,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
@@ -1429,6 +1433,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
@@ -1954,8 +1959,8 @@ 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)") {
+  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)
     }