Merge pull request #2155 from AleksanderBG/wip-andtype-exhaustivity

Extend exhaustivity checks to and-types

Author: liufengyun

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -74,6 +74,13 @@ trait SpaceLogic {
   /** Is `tp1` the same type as `tp2`? */
   def isEqualType(tp1: Type, tp2: Type): Boolean
 
+  /** Return a space containing the values of both types.
+   *
+   * The types should be atomic (non-decomposable) and unrelated (neither
+   * should be a subtype of the other).
+   */
+  def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type): Space
+
   /** Is the type `tp` decomposable? i.e. all values of the type can be covered
    *  by its decomposed types.
    *
@@ -171,7 +178,7 @@ trait SpaceLogic {
         else if (isSubType(tp2, tp1)) b
         else if (canDecompose(tp1)) tryDecompose1(tp1)
         else if (canDecompose(tp2)) tryDecompose2(tp2)
-        else Empty
+        else intersectUnrelatedAtomicTypes(tp1, tp2)
       case (Typ(tp1, _), Kon(tp2, ss)) =>
         if (isSubType(tp2, tp1)) b
         else if (isSubType(tp1, tp2)) a // problematic corner case: inheriting a case class
@@ -239,10 +246,96 @@ trait SpaceLogic {
   }
 }
 
+object SpaceEngine {
+  private sealed trait Implementability {
+    def show(implicit ctx: Context) = this match {
+      case SubclassOf(classSyms) => s"SubclassOf(${classSyms.map(_.show)})"
+      case other => other.toString
+    }
+  }
+  private case object ClassOrTrait extends Implementability
+  private case class SubclassOf(classSyms: List[Symbol]) extends Implementability
+  private case object Unimplementable extends Implementability
+}
+
 /** Scala implementation of space logic */
 class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
+  import SpaceEngine._
   import tpd._
 
+  /** Checks if it's possible to create a trait/class which is a subtype of `tp`.
+   *
+   * - doesn't handle member collisions (will not declare a type unimplementable because of one)
+   * - expects that neither Any nor Object reach it
+   *   (this is currently true due to both isSubType and and/or type simplification)
+   *
+   * See [[intersectUnrelatedAtomicTypes]].
+   */
+  private def implementability(tp: Type): Implementability = tp.dealias match {
+    case AndType(tp1, tp2) =>
+      (implementability(tp1), implementability(tp2)) match {
+        case (Unimplementable, _) | (_, Unimplementable) => Unimplementable
+        case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
+          (for {
+            sym1 <- classSyms1
+            sym2 <- classSyms2
+            result <-
+              if (sym1 isSubClass sym2) List(sym1)
+              else if (sym2 isSubClass sym1) List(sym2)
+              else Nil
+          } yield result) match {
+            case Nil => Unimplementable
+            case lst => SubclassOf(lst)
+          }
+        case (ClassOrTrait, ClassOrTrait) => ClassOrTrait
+        case (SubclassOf(clss), _) => SubclassOf(clss)
+        case (_, SubclassOf(clss)) => SubclassOf(clss)
+      }
+    case OrType(tp1, tp2) =>
+      (implementability(tp1), implementability(tp2)) match {
+        case (ClassOrTrait, _) | (_, ClassOrTrait) => ClassOrTrait
+        case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
+          SubclassOf(classSyms1 ::: classSyms2)
+        case (SubclassOf(classSyms), _) => SubclassOf(classSyms)
+        case (_, SubclassOf(classSyms)) => SubclassOf(classSyms)
+        case _ => Unimplementable
+      }
+    case _: SingletonType =>
+      // singleton types have no instantiable subtypes
+      Unimplementable
+    case tp: RefinedType =>
+      // refinement itself is not considered - it would at most make
+      // a type unimplementable because of a member collision
+      implementability(tp.parent)
+    case other =>
+      val classSym = other.classSymbol
+      if (classSym.exists) {
+        if (classSym is Final) Unimplementable
+        else if (classSym is Trait) ClassOrTrait
+        else SubclassOf(List(classSym))
+      } else {
+        // if no class symbol exists, conservatively say that anything
+        // can implement `tp`
+        ClassOrTrait
+      }
+  }
+
+  override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
+    val and = AndType(tp1, tp2)
+    // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
+    // Then, no leaf of the and-type tree `and` is a subtype of `and`.
+    // Then, to create a value of type `and` you must instantiate a trait (class/module)
+    // which is a subtype of all the leaves of `and`.
+    val imp = implementability(and)
+
+    debug.println(s"atomic intersection: ${and.show} ~ ${imp.show}")
+
+    imp match {
+      case Unimplementable => Empty
+      case _ => Typ(and, true)
+    }
+  }
+
   /** Return the space that represents the pattern `pat`
    *
    *  If roundUp is true, approximate extractors to its type,
@@ -325,6 +418,12 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
     debug.println(s"candidates for ${tp.show} : [${children.map(_.show).mkString(", ")}]")
 
     tp.dealias match {
+      case AndType(tp1, tp2) =>
+        intersect(Typ(tp1, false), Typ(tp2, false)) match {
+          case Or(spaces) => spaces
+          case Empty => Nil
+          case space => List(space)
+        }
       case OrType(tp1, tp2) => List(Typ(tp1, true), Typ(tp2, true))
       case _ if tp =:= ctx.definitions.BooleanType =>
         List(
@@ -377,9 +476,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
 
   /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
   def canDecompose(tp: Type): Boolean = {
+    val dealiasedTp = tp.dealias
     val res = tp.classSymbol.is(allOf(Abstract, Sealed)) ||
       tp.classSymbol.is(allOf(Trait, Sealed)) ||
-      tp.dealias.isInstanceOf[OrType] ||
+      dealiasedTp.isInstanceOf[OrType] ||
+      (dealiasedTp.isInstanceOf[AndType] && {
+        val and = dealiasedTp.asInstanceOf[AndType]
+        canDecompose(and.tp1) || canDecompose(and.tp2)
+      }) ||
       tp =:= ctx.definitions.BooleanType ||
       tp.classSymbol.is(allOf(Enum, Sealed))  // Enum value doesn't have Sealed flag
 
@@ -477,6 +581,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
         ctx.settings.YcheckAllPatmat.value ||
           tp.typeSymbol.is(Sealed) ||
           tp.isInstanceOf[OrType] ||
+          (tp.isInstanceOf[AndType] && {
+            val and = tp.asInstanceOf[AndType]
+            isCheckable(and.tp1) || isCheckable(and.tp2)
+          }) ||
           tp.typeSymbol == ctx.definitions.BooleanType.typeSymbol ||
           tp.typeSymbol.is(Enum) ||
           canDecompose(tp) ||

compiler/test/dotty/tools/dotc/transform/PatmatExhaustivityTest.scala

@@ -28,11 +28,11 @@ class PatmatExhaustivityTest {
         e.printStackTrace()
     }
 
-    val actual = stringBuffer.toString.trim
+    val actual = stringBuffer.toString.trim.replaceAll("\\s+\n", "\n")
     val checkFilePath = file.getAbsolutePath.stripSuffix(".scala") + ".check"
     val checkContent =
       if (new File(checkFilePath).exists)
-        fromFile(checkFilePath).getLines.mkString("\n").trim
+        fromFile(checkFilePath).getLines.map(_.replaceAll("\\s+$", "")).mkString("\n").trim
       else ""
 
     (file, checkContent, actual)
@@ -55,11 +55,11 @@ class PatmatExhaustivityTest {
         e.printStackTrace()
     }
 
-    val actual = stringBuffer.toString.trim
+    val actual = stringBuffer.toString.trim.replaceAll("\\s+\n", "\n")
     val checkFilePath = file.getPath + File.separator + "expected.check"
     val checkContent =
       if (new File(checkFilePath).exists)
-        fromFile(checkFilePath).getLines.mkString("\n").trim
+        fromFile(checkFilePath).getLines.map(_.replaceAll("\\s+$", "")).mkString("\n").trim
       else ""
 
     (file, checkContent, actual)

tests/patmat/aliasing.check

@@ -0,0 +1,3 @@
+14: Pattern Match Exhaustivity: _: Clazz & Test.Alias1, _: Trait & Test.Alias1
+19: Pattern Match Exhaustivity: _: Trait & Test.Alias2
+23: Pattern Match Exhaustivity: _: Trait & (Test.Alias2 & OpenTrait2){x: Int}

tests/patmat/aliasing.scala

@@ -0,0 +1,26 @@
+sealed trait T
+trait Trait extends T
+class Clazz extends T
+object Obj extends T
+
+trait OpenTrait
+trait OpenTrait2
+class OpenClass
+
+trait Unrelated
+
+object Test {
+  type Alias1 = OpenTrait
+  def traitAndClass(s: T & Alias1) = s match {
+    case _: Unrelated => ;
+  }
+
+  type Alias2 = OpenTrait & OpenClass
+  def classOnly(s: T & Alias2) = s match {
+    case _: Unrelated => ;
+  }
+
+  def classOnlyRefined(s: T & (Alias2 & OpenTrait2) { val x: Int }) = s match {
+    case _: Unrelated => ;
+  }
+}

tests/patmat/andtype-opentype-interaction.check

@@ -0,0 +1,6 @@
+23: Pattern Match Exhaustivity: _: SealedClass & OpenTrait, _: AbstractClass & OpenTrait, _: Clazz & OpenTrait, _: Trait & OpenTrait
+27: Pattern Match Exhaustivity: _: SealedClass & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & OpenTrait & OpenTrait2
+31: Pattern Match Exhaustivity: _: Trait & OpenClass
+35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass
+43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass
+47: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClassSubclass

tests/patmat/andtype-opentype-interaction.scala

@@ -0,0 +1,50 @@
+sealed trait T
+trait Trait extends T
+class Clazz extends T
+abstract class AbstractClass extends T
+// none of the below can be extended
+sealed trait SealedTrait extends T
+final class FinalClass extends T
+sealed class SealedClass extends T
+sealed abstract class SealedAbstractClass extends T
+object Obj extends T
+
+trait OpenTrait
+class OpenClass
+class OpenClassSubclass extends OpenClass
+abstract class OpenAbstractClass
+
+trait Unrelated
+
+trait OpenTrait2
+class OpenClass2
+
+object Test {
+  def m1a(s: T & OpenTrait) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m1b(s: T & OpenTrait & OpenTrait2) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m2(s: T & OpenClass) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m2b(s: T & OpenTrait & OpenClass) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m2c(s: (T & OpenClass) & (OpenTrait & OpenClass2)) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m3(s: T & OpenAbstractClass) = s match {
+    case _: Unrelated => ;
+  }
+
+  def m4(s: (T & OpenClass) & (OpenTrait & OpenClassSubclass)) = s match {
+    case _: Unrelated => ;
+  }
+}

tests/patmat/andtype-refinedtype-interaction.check

@@ -0,0 +1,10 @@
+32: Pattern Match Exhaustivity: _: Trait & C1{x: Int}
+48: Pattern Match Exhaustivity: _: Clazz & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}, _: Trait & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}
+54: Pattern Match Exhaustivity: _: Trait & (C1 | C2 | T1){x: Int} & C3{x: Int}
+65: Pattern Match Exhaustivity: _: Trait & (C1 | C2){x: Int} & (C3 | SubC1){x: Int}
+72: Pattern Match Exhaustivity: _: Trait & (T1 & C1 | T1 & SubC2){x: Int} &
+  (T2 & C2 | T2 & C3 | T2 & SubC1){x: Int}
+ & SubSubC1{x: Int}
+79: Pattern Match Exhaustivity: _: Trait & (T1 & C1 | T1 & SubC2){x: Int} &
+  (T2 & C2 | T2 & C3 | T2 & SubC1){x: Int}
+ & SubSubC2{x: Int}

tests/patmat/andtype-refinedtype-interaction.scala

@@ -0,0 +1,82 @@
+sealed trait S
+trait Trait extends S
+class Clazz extends S
+object Obj extends S
+
+trait T1
+trait T2
+
+class C1
+class C2
+class C3
+class C4
+
+class SubC1 extends C1
+class SubSubC1 extends SubC1
+class SubC2 extends C2
+class SubSubC2 extends SubC2
+
+trait Unrelated
+
+object Test {
+  /*
+  Note: error message on this suggests Obj to be unmatched as well.
+  This isn't a bug in atomic type intersection, but a consequence
+  of approximating all types to be a subtype of a structural type.
+
+  def basic1(s: S & { val x: Int }) = s match {
+    case _: Unrelated => ;
+  }
+  */
+
+  def basic2(s: S & C1 { val x: Int }) = s match {
+    case _: Unrelated => ;
+  }
+
+  def doubleInheritance1(s: S & C1 { val x: Int } & C2) = s match {
+    case _: Unrelated => ;
+  }
+
+  def doubleInheritance2(s: S & C1 { val x: Int }
+                              & C2 { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def classOrTrait(s: S & (C1 | (C2 | T1)) { val x: Int }
+                        & (C3 | (C4 | T2)) { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def traitOnly(s: S & (C1 | (C2 | T1)) { val x: Int }
+                     & C3 { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def nestedDoubleInheritance(s: S & (C1 & C2) { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def subclassingA(s: S & (C1 | C2) { val x: Int }
+                        & (C3 | SubC1) { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def subclassingB(s: S & (T1 & (C1 | SubC2)) { val x: Int }
+                        & (T2 & (C2 | C3 | SubC1)) { val x: Int }
+                        & SubSubC1 { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+
+  def subclassingC(s: S & (T1 & (C1 | SubC2)) { val x: Int }
+                        & (T2 & (C2 | C3 | SubC1)) { val x: Int }
+                        & SubSubC2 { val x: Int }) =
+    s match {
+      case _: Unrelated => ;
+    }
+}

tests/patmat/andtype.check

@@ -0,0 +1,3 @@
+9: Pattern Match Exhaustivity: _: B
+13: Pattern Match Exhaustivity: _: B
+17: Pattern Match Exhaustivity: _: B

tests/patmat/andtype.scala

@@ -0,0 +1,20 @@
+object Test {
+  trait Marker
+
+  sealed trait T
+  trait A extends T with Marker
+  trait B extends T with Marker
+  case object C extends T
+
+  def m1(s: T & Marker) = s match {
+    case _: A => ;
+  }
+
+  def m2(s: Marker & T) = s match {
+    case _: A => ;
+  }
+
+  def m3(s: (A | B) & Marker) = s match {
+    case _: A => ;
+  }
+}

tests/patmat/nontrivial-andtype.check

@@ -0,0 +1 @@
+16: Pattern Match Exhaustivity: D, _: C, B(), _: A