Match Types: implement cantPossiblyMatch

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

@@ -13,6 +13,7 @@ import TypeErasure.{erasedLub, erasedGlb}
 import TypeApplications._
 import Constants.Constant
 import transform.TypeUtils._
+import transform.SymUtils._
 import scala.util.control.NonFatal
 import typer.ProtoTypes.constrained
 import reporting.trace
@@ -1875,6 +1876,133 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] {
 
   /** Returns last check's debug mode, if explicitly enabled. */
   def lastTrace(): String = ""
+
+  /** Do `tp1` and `tp2` share a non-null inhabitant?
+   *
+   *  `false` implies that we found a proof; uncertainty default to `true`.
+   *
+   *  Proofs rely on the following properties of Scala types:
+   *
+   *  1. Single inheritance of classes
+   *  2. Final classes cannot be extended
+   *  3. ConstantTypes with distinc values are non intersecting
+   *  4. There is no value of type Nothing
+   */
+  def intersecting(tp1: Type, tp2: Type)(implicit ctx: Context): Boolean = {
+    // println(s"intersecting(${tp1.show}, ${tp2.show})")
+    /** Can we enumerate all instantiations of this type? */
+    def isClosed(tp: Symbol): Boolean =
+      tp.is(Sealed) && tp.is(AbstractOrTrait) && !tp.hasAnonymousChild
+
+    /** Splits a close type into a disjunction of smaller types.
+     *  It should hold that `tp` and `decompose(tp).reduce(_ or _)`
+     *  denote the same set of values.
+     */
+    def decompose(sym: Symbol, tp: Type): List[Type] = {
+      import dotty.tools.dotc.transform.patmat.SpaceEngine
+      val se = new SpaceEngine
+      sym.children.map(x => se.refine(tp, x)).filter(_.exists)
+    }
+
+    (tp1.dealias, tp2.dealias) match {
+      case (tp1: ConstantType, tp2: ConstantType) =>
+        tp1 == tp2
+      case (tp1: TypeRef, tp2: TypeRef) if tp1.symbol.isClass && tp2.symbol.isClass =>
+        if (isSubType(tp1, tp2) || isSubType(tp2, tp1)) {
+          true
+        } else {
+          val cls1 = tp1.classSymbol
+          val cls2 = tp2.classSymbol
+          if (cls1.is(Final) || cls2.is(Final))
+            // One of these types is final and they are not mutually
+            // subtype, so they must be unrelated.
+            false
+          else if (!cls2.is(Trait) && !cls1.is(Trait))
+            // Both of these types are classes and they are not mutually
+            // subtype, so they must be unrelated by single inheritance
+            // of classes.
+            false
+          else if (isClosed(cls1))
+            decompose(cls1, tp1).exists(x => intersecting(x, tp2))
+          else if (isClosed(cls2))
+            decompose(cls2, tp2).exists(x => intersecting(x, tp1))
+          else
+            true
+        }
+      case (AppliedType(tycon1, args1), AppliedType(tycon2, args2)) =>
+        // Unboxed x.zip(y).zip(z).forall { case ((a, b), c) => f(a, b, c) }
+        def zip_zip_forall[A, B, C](x: List[A], y: List[B], z: List[C])(f: (A, B, C) => Boolean): Boolean =
+          x match {
+            case x :: xs => y match {
+              case y :: ys => z match {
+                case z :: zs => f(x, y, z) && zip_zip_forall(xs, ys, zs)(f)
+                case _ => true
+              }
+              case _ => true
+            }
+            case _ => true
+          }
+
+        tycon1 == tycon2 &&
+          zip_zip_forall(args1, args2, tycon1.typeParams) {
+            (arg1, arg2, tparam) =>
+              val v = tparam.paramVariance
+              // Note that the logic below is conservative in that is
+              // assumes that Covariant type parameters are Contravariant
+              // type
+              if (v > 0)
+                intersecting(arg1, arg2) || {
+                  // We still need to proof that `Nothing` is not a valid
+                  // instantiation of this type parameter. We have two ways
+                  // to get to that conclusion:
+                  // 1. `Nothing` does not conform to the type parameter's lb
+                  // 2. `tycon1` has a field typed with this type parameter.
+                  //
+                  // Because of separate compilation, the use of 2. is
+                  // limited to case classes.
+                  import dotty.tools.dotc.typer.Applications.productSelectorTypes
+                  val lowerBoundedByNothing = tparam.paramInfo.bounds.lo eq NothingType
+                  val typeUsedAsField =
+                    productSelectorTypes(tycon1, null).exists {
+                      case tp: TypeRef =>
+                        (tp.designator: Any) == tparam // Bingo!
+                      case _ =>
+                        false
+                    }
+                  lowerBoundedByNothing && !typeUsedAsField
+                }
+              else if (v < 0)
+                // Contravariant case: a value where this type parameter is
+                // instantiated to `Any` belongs to both types.
+                true
+              else
+                isSameType(arg1, arg2) // TODO: handle uninstanciated types
+        }
+      case (tp1: HKLambda, tp2: HKLambda) =>
+        intersecting(tp1.resType, tp2.resType)
+      case (_: HKLambda, _) =>
+        // The intersection is ill kinded and therefore empty.
+        false
+      case (_, _: HKLambda) =>
+        false
+      case (tp1: OrType, _)  =>
+        intersecting(tp1.tp1, tp2) || intersecting(tp1.tp2, tp2)
+      case (_, tp2: OrType)  =>
+        intersecting(tp1, tp2.tp1) || intersecting(tp1, tp2.tp2)
+      case (tp1: AndType, _) =>
+        intersecting(tp1.tp1, tp2) && intersecting(tp1.tp2, tp2) && intersecting(tp1.tp1, tp1.tp2)
+      case (_, tp2: AndType) =>
+        intersecting(tp1, tp2.tp1) && intersecting(tp1, tp2.tp2) && intersecting(tp2.tp1, tp2.tp2)
+      case (tp1: TypeProxy, tp2: TypeProxy) =>
+        intersecting(tp1.underlying, tp2) && intersecting(tp1, tp2.underlying)
+      case (tp1: TypeProxy, _) =>
+        intersecting(tp1.underlying, tp2)
+      case (_, tp2: TypeProxy) =>
+        intersecting(tp1, tp2.underlying)
+      case _ =>
+        true
+    }
+  }
 }
 
 object TypeComparer {
@@ -1969,8 +2097,7 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
     super.typeVarInstance(tvar)
   }
 
-  def matchCase(scrut: Type, cas: Type, instantiate: Boolean)(implicit ctx: Context): Type = {
-
+  def matchCases(scrut: Type, cases: List[Type])(implicit ctx: Context): Type = {
     def paramInstances = new TypeAccumulator[Array[Type]] {
       def apply(inst: Array[Type], t: Type) = t match {
         case t @ TypeParamRef(b, n) if b `eq` caseLambda =>
@@ -1989,29 +2116,45 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
       }
     }
 
-    val saved = constraint
-    try {
-      inFrozenConstraint {
-        val cas1 = cas match {
-          case cas: HKTypeLambda =>
-            caseLambda = constrained(cas)
-            caseLambda.resultType
-          case _ =>
-            cas
-        }
-        val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
-        if (isSubType(scrut, pat))
-          caseLambda match {
-            case caseLambda: HKTypeLambda if instantiate =>
-              val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
-              instantiateParams(instances)(body)
+    var result: Type = NoType
+    var remainingCases = cases
+    while (!remainingCases.isEmpty) {
+      val (cas :: cass) = remainingCases
+      remainingCases = cass
+      val saved = constraint
+      try {
+        inFrozenConstraint {
+          val cas1 = cas match {
+            case cas: HKTypeLambda =>
+              caseLambda = constrained(cas)
+              caseLambda.resultType
             case _ =>
-              body
+              cas
           }
-        else NoType
+          val defn.FunctionOf(pat :: Nil, body, _, _) = cas1
+          if (isSubType(scrut, pat)) {
+            // `scrut` is a subtype of `pat`: *It's a Match!*
+            result = caseLambda match {
+              case caseLambda: HKTypeLambda =>
+                val instances = paramInstances(new Array(caseLambda.paramNames.length), pat)
+                instantiateParams(instances)(body)
+              case _ =>
+                body
+            }
+            remainingCases = Nil
+          } else if (!intersecting(scrut, pat)) {
+            // We found a proof that `scrut` and  `pat` are incompatible.
+            // The search continues.
+          } else {
+            // We are stuck: this match type instanciation is irreducible.
+            result = NoType
+            remainingCases = Nil
+          }
+        }
       }
+      finally constraint = saved
     }
-    finally constraint = saved
+    result
   }
 }
 

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

@@ -3764,22 +3764,10 @@ object Types {
 
     override def tryNormalize(implicit ctx: Context): Type = reduced.normalized
 
-    final def cantPossiblyMatch(cas: Type)(implicit ctx: Context): Boolean =
-      true  // should be refined if we allow overlapping cases
-
     def reduced(implicit ctx: Context): Type = {
       val trackingCtx = ctx.fresh.setTypeComparerFn(new TrackingTypeComparer(_))
       val typeComparer = trackingCtx.typeComparer.asInstanceOf[TrackingTypeComparer]
 
-      def reduceSequential(cases: List[Type])(implicit ctx: Context): Type = cases match {
-        case Nil => NoType
-        case cas :: cases1 =>
-          val r = typeComparer.matchCase(scrutinee, cas, instantiate = true)
-          if (r.exists) r
-          else if (cantPossiblyMatch(cas)) reduceSequential(cases1)
-          else NoType
-      }
-
       def contextInfo(tp: Type): Type = tp match {
         case tp: TypeParamRef =>
           val constraint = ctx.typerState.constraint
@@ -3812,7 +3800,7 @@ object Types {
           trace(i"reduce match type $this $hashCode", typr, show = true) {
             try
               if (defn.isBottomType(scrutinee)) defn.NothingType
-              else reduceSequential(cases)(trackingCtx)
+              else typeComparer.matchCases(scrutinee, cases)(trackingCtx)
             catch {
               case ex: Throwable =>
                 handleRecursive("reduce type ", i"$scrutinee match ...", ex)

compiler/src/dotty/tools/dotc/typer/Applications.scala

@@ -42,7 +42,7 @@ object Applications {
     val ref = extractorMember(tp, name)
     if (ref.isOverloaded)
       errorType(i"Overloaded reference to $ref is not allowed in extractor", errorPos)
-    ref.info.widenExpr.annotatedToRepeated.dealiasKeepAnnots
+    ref.info.widenExpr.annotatedToRepeated
   }
 
   /** Does `tp` fit the "product match" conditions as an unapply result type

compiler/test/dotty/tools/dotc/reporting/ErrorMessagesTests.scala

@@ -1362,7 +1362,7 @@ class ErrorMessagesTests extends ErrorMessagesTest {
         assertMessageCount(1, messages)
         val UnapplyInvalidNumberOfArguments(qual, argTypes) :: Nil = messages
         assertEquals("Boo", qual.show)
-        assertEquals("(class Int, class String)", argTypes.map(_.typeSymbol).mkString("(", ", ", ")"))
+        assertEquals("(class Int, type String)", argTypes.map(_.typeSymbol).mkString("(", ", ", ")"))
       }
 
   @Test def unapplyInvalidReturnType =