Adjust behaviour of TypeComparer.either for GADTflexible

Author: abgruszecki

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

@@ -775,7 +775,7 @@ object Contexts {
       else assert(thread == Thread.currentThread(), "illegal multithreaded access to ContextBase")
   }
 
-  sealed abstract class GADTMap {
+  sealed abstract class GADTMap extends Showable {
     def addEmptyBounds(sym: Symbol)(implicit ctx: Context): Unit
     def addBound(sym: Symbol, bound: Type, isUpper: Boolean)(implicit ctx: Context): Boolean
     def isLess(sym1: Symbol, sym2: Symbol)(implicit ctx: Context): Boolean
@@ -802,6 +802,14 @@ object Contexts {
   ) extends GADTMap with ConstraintHandling[Context] {
     import dotty.tools.dotc.config.Printers.{gadts, gadtsConstr}
 
+    def subsumes(left: GADTMap, right: GADTMap, pre: GADTMap)(implicit ctx: Context): Boolean = {
+      def extractConstraint(g: GADTMap) = g match {
+        case s: SmartGADTMap => s.constraint
+        case EmptyGADTMap => OrderingConstraint.empty
+      }
+      subsumes(extractConstraint(left), extractConstraint(right), extractConstraint(pre))
+    }
+
     def this() = this(
       myConstraint = new OrderingConstraint(SimpleIdentityMap.Empty, SimpleIdentityMap.Empty, SimpleIdentityMap.Empty),
       mapping = SimpleIdentityMap.Empty,
@@ -950,6 +958,8 @@ object Contexts {
 
     override def constr_println(msg: => String): Unit = gadtsConstr.println(msg)
 
+    override def toText(printer: Printer): Texts.Text = constraint.toText(printer)
+
     override def debugBoundsDescription(implicit ctx: Context): String = {
       val sb = new mutable.StringBuilder
       sb ++= constraint.show
@@ -969,6 +979,7 @@ object Contexts {
     override def fullBounds(sym: Symbol)(implicit ctx: Context): TypeBounds = null
     override def contains(sym: Symbol)(implicit ctx: Context) = false
     override def approximation(sym: Symbol, fromBelow: Boolean)(implicit ctx: Context): Type = unsupported("EmptyGADTMap.approximation")
+    override def toText(printer: Printer): Texts.Text = "EmptyGADTMap"
     override def debugBoundsDescription(implicit ctx: Context): String = "EmptyGADTMap"
     override def fresh = new SmartGADTMap
     override def restore(other: GADTMap): Unit = {

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

@@ -49,7 +49,7 @@ object Mode {
   /** We are in a pattern alternative */
   val InPatternAlternative: Mode = newMode(7, "InPatternAlternative")
 
-  /** Allow GADTFlexType labelled types to have their bounds adjusted */
+  /** Infer GADT constraints during type comparisons `A <:< B` */
   val GADTflexible: Mode = newMode(8, "GADTflexible")
 
   /** Assume -language:strictEquality */

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

@@ -1252,16 +1252,52 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
    */
   private def either(op1: => Boolean, op2: => Boolean): Boolean = {
     val preConstraint = constraint
-    op1 && {
-      val leftConstraint = constraint
-      constraint = preConstraint
-      if (!(op2 && subsumes(leftConstraint, constraint, preConstraint))) {
-        if (constr != noPrinter && !subsumes(constraint, leftConstraint, preConstraint))
-          constr.println(i"CUT - prefer $leftConstraint over $constraint")
-        constraint = leftConstraint
-      }
-      true
-    } || op2
+
+    if (ctx.mode.is(Mode.GADTflexible)) {
+      val preGadt = ctx.gadt.fresh
+      // if GADTflexible mode is on, we always have a SmartGADTMap
+      val pre = preGadt.asInstanceOf[SmartGADTMap]
+      if (op1) {
+        val leftConstraint = constraint
+        val leftGadt = ctx.gadt.fresh
+        constraint = preConstraint
+        ctx.gadt.restore(preGadt)
+        if (op2) {
+          if (pre.subsumes(leftGadt, ctx.gadt, preGadt) && subsumes(leftConstraint, constraint, preConstraint)) {
+            gadts.println(i"GADT CUT - prefer ${ctx.gadt} over $leftGadt")
+            constr.println(i"CUT - prefer $constraint over $leftConstraint")
+            true
+          } else if (pre.subsumes(ctx.gadt, leftGadt, preGadt) && subsumes(constraint, leftConstraint, preConstraint)) {
+            gadts.println(i"GADT CUT - prefer $leftGadt over ${ctx.gadt}")
+            constr.println(i"CUT - prefer $leftConstraint over $constraint")
+            constraint = leftConstraint
+            ctx.gadt.restore(leftGadt)
+            true
+          } else {
+            gadts.println(i"GADT CUT - no constraint is preferable, reverting to $preGadt")
+            constr.println(i"CUT - no constraint is preferable, reverting to $preConstraint")
+            constraint = preConstraint
+            ctx.gadt.restore(preGadt)
+            true
+          }
+        } else {
+          constraint = leftConstraint
+          ctx.gadt.restore(leftGadt)
+          true
+        }
+      } else op2
+    } else {
+      op1 && {
+        val leftConstraint = constraint
+        constraint = preConstraint
+        if (!(op2 && subsumes(leftConstraint, constraint, preConstraint))) {
+          if (constr != noPrinter && !subsumes(constraint, leftConstraint, preConstraint))
+            constr.println(i"CUT - prefer $leftConstraint over $constraint")
+          constraint = leftConstraint
+        }
+        true
+      } || op2
+    }
   }
 
   /** Does type `tp1` have a member with name `name` whose normalized type is a subtype of