Skip to content

Extend exhaustivity checks to and-types #2155

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Apr 26, 2017
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
112 changes: 110 additions & 2 deletions compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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) ||
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand Down
3 changes: 3 additions & 0 deletions tests/patmat/aliasing.check
Original file line number Diff line number Diff line change
@@ -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}
26 changes: 26 additions & 0 deletions tests/patmat/aliasing.scala
Original file line number Diff line number Diff line change
@@ -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 => ;
}
}
6 changes: 6 additions & 0 deletions tests/patmat/andtype-opentype-interaction.check
Original file line number Diff line number Diff line change
@@ -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
50 changes: 50 additions & 0 deletions tests/patmat/andtype-opentype-interaction.scala
Original file line number Diff line number Diff line change
@@ -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 => ;
}
}
10 changes: 10 additions & 0 deletions tests/patmat/andtype-refinedtype-interaction.check
Original file line number Diff line number Diff line change
@@ -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}
82 changes: 82 additions & 0 deletions tests/patmat/andtype-refinedtype-interaction.scala
Original file line number Diff line number Diff line change
@@ -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 => ;
}
}
3 changes: 3 additions & 0 deletions tests/patmat/andtype.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
9: Pattern Match Exhaustivity: _: B
13: Pattern Match Exhaustivity: _: B
17: Pattern Match Exhaustivity: _: B
20 changes: 20 additions & 0 deletions tests/patmat/andtype.scala
Original file line number Diff line number Diff line change
@@ -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 => ;
}
}
1 change: 1 addition & 0 deletions tests/patmat/nontrivial-andtype.check
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
16: Pattern Match Exhaustivity: D, _: C, B(), _: A
Loading