dotty
8815b402266e
Merge pull request #2155 from AleksanderBG/wip-andtype-exhaustivity
liu fengyun
2 days ago
Extend exhaustivity checks to and-types

72 73 74 75 76 77 78 79 80 81 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
def isSubType(tp1: Type, tp2: Type): Boolean /** 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. * * Abstract sealed class, OrType, Boolean and Java enums can be decomposed. */
...
169 170 171 172 173 174 175 176 177 178 179 176 177 178 179 180 181 182 183 184 185 186
case (Typ(tp1, _), Typ(tp2, _)) => if (isSubType(tp1, tp2)) a 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 else if (canDecompose(tp1)) tryDecompose1(tp1) else Empty
...
237 238 239 240 241 242 243 244 245 246 247 248 249 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342
res } }
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, * otherwise approximate extractors to Empty
...
323 324 325 326 327 328 329 330 331 332 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431
} 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( Typ(ConstantType(Constant(true)), true), Typ(ConstantType(Constant(false)), true)
...
375 376 377 378 379 380 381 382 383 384 385 386 387 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
case _ => tp2 } /** 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 debug.println(s"decomposable: ${tp.show} = $res")
...
475 476 477 478 479 480 481 482 483 484 579 580 581 582 583 584 585 586 587 588 589 590 591 592
case _ => // Possible to check everything, but be compatible with scalac by default 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) || (defn.isTupleType(tp) && tp.dealias.argInfos.exists(isCheckable(_))) }

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
case e: Throwable => println(s"Compile $file exception:") 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) }
...
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
case e: Throwable => println(s"Compile $file exception:") 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) }

1 2 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}

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 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 => ; } }

1 2 3 4 5 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

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 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 => ; } }

1 2 3 4 5 6 7 8 9 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}

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 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 => ; } }

1 2 3
9: Pattern Match Exhaustivity: _: B 13: Pattern Match Exhaustivity: _: B 17: Pattern Match Exhaustivity: _: B

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 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
16: Pattern Match Exhaustivity: D, _: C, B(), _: A

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
object Test { sealed trait Marker trait M1 extends Marker sealed trait Marker2 extends Marker sealed trait M2 extends Marker2 sealed trait T trait A extends T with M2 sealed trait T2 extends T case class B() extends T2 with Marker class C extends T2 with M1 case object D extends T2 with Marker trait Unrelated def m1(s: T & Marker) = s match { case _: Unrelated => ; } }
About FluentSend Feedback