Skip to content

Commit f029755

Browse files
liufengyunliufengyun
authored
Merge pull request #3891 from dotty-staging/fix-3144
Fix #3144: more aggressively check unreachability
2 parents 7862aaf + 26f384b commit f029755

File tree

15 files changed

+177
-116
lines changed

15 files changed

+177
-116
lines changed

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

Lines changed: 103 additions & 104 deletions
Original file line numberDiff line numberDiff line change
@@ -278,21 +278,8 @@ trait SpaceLogic {
278278
}
279279
}
280280

281-
object SpaceEngine {
282-
private sealed trait Implementability {
283-
def show(implicit ctx: Context) = this match {
284-
case SubclassOf(classSyms) => s"SubclassOf(${classSyms.map(_.show)})"
285-
case other => other.toString
286-
}
287-
}
288-
private case object ClassOrTrait extends Implementability
289-
private case class SubclassOf(classSyms: List[Symbol]) extends Implementability
290-
private case object Unimplementable extends Implementability
291-
}
292-
293281
/** Scala implementation of space logic */
294282
class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
295-
import SpaceEngine._
296283
import tpd._
297284

298285
private val scalaSomeClass = ctx.requiredClass("scala.Some")
@@ -301,77 +288,15 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
301288
private val scalaNilType = ctx.requiredModuleRef("scala.collection.immutable.Nil")
302289
private val scalaConsType = ctx.requiredClassRef("scala.collection.immutable.::")
303290

304-
/** Checks if it's possible to create a trait/class which is a subtype of `tp`.
305-
*
306-
* - doesn't handle member collisions (will not declare a type unimplementable because of one)
307-
* - expects that neither Any nor Object reach it
308-
* (this is currently true due to both isSubType and and/or type simplification)
309-
*
310-
* See [[intersectUnrelatedAtomicTypes]].
311-
*/
312-
private def implementability(tp: Type): Implementability = tp.dealias match {
313-
case AndType(tp1, tp2) =>
314-
(implementability(tp1), implementability(tp2)) match {
315-
case (Unimplementable, _) | (_, Unimplementable) => Unimplementable
316-
case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
317-
(for {
318-
sym1 <- classSyms1
319-
sym2 <- classSyms2
320-
result <-
321-
if (sym1 isSubClass sym2) List(sym1)
322-
else if (sym2 isSubClass sym1) List(sym2)
323-
else Nil
324-
} yield result) match {
325-
case Nil => Unimplementable
326-
case lst => SubclassOf(lst)
327-
}
328-
case (ClassOrTrait, ClassOrTrait) => ClassOrTrait
329-
case (SubclassOf(clss), _) => SubclassOf(clss)
330-
case (_, SubclassOf(clss)) => SubclassOf(clss)
331-
}
332-
case OrType(tp1, tp2) =>
333-
(implementability(tp1), implementability(tp2)) match {
334-
case (ClassOrTrait, _) | (_, ClassOrTrait) => ClassOrTrait
335-
case (SubclassOf(classSyms1), SubclassOf(classSyms2)) =>
336-
SubclassOf(classSyms1 ::: classSyms2)
337-
case (SubclassOf(classSyms), _) => SubclassOf(classSyms)
338-
case (_, SubclassOf(classSyms)) => SubclassOf(classSyms)
339-
case _ => Unimplementable
340-
}
341-
case _: SingletonType =>
342-
// singleton types have no instantiable subtypes
343-
Unimplementable
344-
case tp: RefinedType =>
345-
// refinement itself is not considered - it would at most make
346-
// a type unimplementable because of a member collision
347-
implementability(tp.parent)
348-
case other =>
349-
val classSym = other.classSymbol
350-
if (classSym.exists) {
351-
if (classSym is Final) Unimplementable
352-
else if (classSym is Trait) ClassOrTrait
353-
else SubclassOf(List(classSym))
354-
} else {
355-
// if no class symbol exists, conservatively say that anything
356-
// can implement `tp`
357-
ClassOrTrait
358-
}
359-
}
360-
361291
override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
362292
val and = AndType(tp1, tp2)
363293
// Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
364294
// Then, no leaf of the and-type tree `and` is a subtype of `and`.
365-
// Then, to create a value of type `and` you must instantiate a trait (class/module)
366-
// which is a subtype of all the leaves of `and`.
367-
val imp = implementability(and)
295+
val res = inhabited(and)
368296

369-
debug.println(s"atomic intersection: ${and.show} ~ ${imp.show}")
297+
debug.println(s"atomic intersection: ${and.show} = ${res}")
370298

371-
imp match {
372-
case Unimplementable => Empty
373-
case _ => Typ(and, true)
374-
}
299+
if (res) Typ(and, true) else Empty
375300
}
376301

377302
/* Whether the extractor is irrefutable */
@@ -574,21 +499,92 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
574499

575500
/** Can this type be inhabited by a value?
576501
*
577-
* Intersection between singleton types and other types is always empty
578-
* the singleton type is not a subtype of the other type.
579-
* See patmat/i3573.scala for an example.
502+
* Check is based on the following facts:
503+
*
504+
* - single inheritance of classes
505+
* - final class cannot be extended
506+
* - intersection of a singleton type with another irrelevant type (patmat/i3574.scala)
507+
*
580508
*/
581-
def inhabited(tpe: Type)(implicit ctx: Context): Boolean = {
582-
val emptySingletonIntersection = new ExistsAccumulator({
583-
case AndType(s: SingletonType, t) =>
584-
!(s <:< t)
585-
case AndType(t, s: SingletonType) =>
586-
!(s <:< t)
587-
case x =>
588-
false
589-
})
590-
591-
!emptySingletonIntersection(false, tpe)
509+
def inhabited(tp: Type)(implicit ctx: Context): Boolean = {
510+
// convert top-level type shape into "conjunctive normal form"
511+
def cnf(tp: Type): Type = tp match {
512+
case AndType(OrType(l, r), tp) =>
513+
OrType(cnf(AndType(l, tp)), cnf(AndType(r, tp)))
514+
case AndType(tp, o: OrType) =>
515+
cnf(AndType(o, tp))
516+
case AndType(l, r) =>
517+
val l1 = cnf(l)
518+
val r1 = cnf(r)
519+
if (l1.ne(l) || r1.ne(r)) cnf(AndType(l1, r1))
520+
else AndType(l1, r1)
521+
case OrType(l, r) =>
522+
OrType(cnf(l), cnf(r))
523+
case tp @ RefinedType(OrType(tp1, tp2), _, _) =>
524+
OrType(
525+
cnf(tp.derivedRefinedType(tp1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)),
526+
cnf(tp.derivedRefinedType(tp2, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo))
527+
)
528+
case tp: RefinedType =>
529+
val parent1 = cnf(tp.parent)
530+
val tp1 = tp.derivedRefinedType(parent1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)
531+
532+
if (parent1.ne(tp.parent)) cnf(tp1) else tp1
533+
case tp: TypeAlias =>
534+
cnf(tp.alias)
535+
case _ =>
536+
tp
537+
}
538+
539+
def isSingleton(tp: Type): Boolean = tp.dealias match {
540+
case AndType(l, r) => isSingleton(l) || isSingleton(r)
541+
case OrType(l, r) => isSingleton(l) && isSingleton(r)
542+
case tp => tp.isSingleton
543+
}
544+
545+
def superType(tp: Type): Type = tp match {
546+
case tp: TypeProxy => tp.superType
547+
case OrType(tp1, tp2) => OrType(superType(tp1), superType(tp2))
548+
case AndType(tp1, tp2) => AndType(superType(tp1), superType(tp2))
549+
case _ => tp
550+
}
551+
552+
def recur(tp: Type): Boolean = tp.dealias match {
553+
case AndType(tp1, tp2) =>
554+
recur(tp1) && recur(tp2) && {
555+
val bases1 = tp1.widenDealias.classSymbols
556+
val bases2 = tp2.widenDealias.classSymbols
557+
558+
debug.println(s"bases of ${tp1.show}: " + bases1)
559+
debug.println(s"bases of ${tp2.show}: " + bases2)
560+
561+
val noClassConflict =
562+
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym1.isSubClass(sym2))) ||
563+
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym2.isSubClass(sym1)))
564+
565+
debug.println(s"class conflict for ${tp.show}? " + !noClassConflict)
566+
567+
noClassConflict &&
568+
(!isSingleton(tp1) || tp1 <:< tp2) &&
569+
(!isSingleton(tp2) || tp2 <:< tp1) &&
570+
(!bases1.exists(_ is Final) || tp1 <:< superType(tp2)) &&
571+
(!bases2.exists(_ is Final) || tp2 <:< superType(tp1))
572+
}
573+
case OrType(tp1, tp2) =>
574+
recur(tp1) || recur(tp2)
575+
case tp: RefinedType =>
576+
recur(tp.parent)
577+
case tp: TypeRef =>
578+
recur(tp.prefix) && !(tp.classSymbol.is(AbstractFinal))
579+
case _ =>
580+
true
581+
}
582+
583+
val res = recur(cnf(tp))
584+
585+
debug.println(s"${tp.show} inhabited? " + res)
586+
587+
res
592588
}
593589

594590
/** Instantiate type `tp1` to be a subtype of `tp2`
@@ -708,8 +704,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
708704
/** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
709705
def canDecompose(tp: Type): Boolean = {
710706
val dealiasedTp = tp.dealias
711-
val res = tp.classSymbol.is(allOf(Abstract, Sealed)) ||
712-
tp.classSymbol.is(allOf(Trait, Sealed)) ||
707+
val res =
708+
(tp.classSymbol.is(Sealed) &&
709+
tp.classSymbol.is(AbstractOrTrait) &&
710+
tp.classSymbol.children.nonEmpty ) ||
713711
dealiasedTp.isInstanceOf[OrType] ||
714712
(dealiasedTp.isInstanceOf[AndType] && {
715713
val and = dealiasedTp.asInstanceOf[AndType]
@@ -905,24 +903,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
905903
def checkRedundancy(_match: Match): Unit = {
906904
val Match(sel, cases) = _match
907905
// ignore selector type for now
908-
// val selTyp = sel.tpe.widen.dealias
909-
910-
if (cases.length == 1) return
906+
val selTyp = sel.tpe.widen.dealias
911907

912-
// starts from the second, the first can't be redundant
913-
(1 until cases.length).foreach { i =>
908+
(0 until cases.length).foreach { i =>
914909
// in redundancy check, take guard as false in order to soundly approximate
915-
val prevs = cases.take(i).map { x =>
916-
if (x.guard.isEmpty) project(x.pat)
917-
else Empty
918-
}.reduce((a, b) => Or(List(a, b)))
910+
val prevs =
911+
if (i == 0)
912+
Empty
913+
else
914+
cases.take(i).map { x =>
915+
if (x.guard.isEmpty) project(x.pat)
916+
else Empty
917+
}.reduce((a, b) => Or(List(a, b)))
919918

920919
val curr = project(cases(i).pat)
921920

922921
debug.println(s"---------------reachable? ${show(curr)}")
923922
debug.println(s"prev: ${show(prevs)}")
924923

925-
if (isSubspace(curr, prevs)) {
924+
if (isSubspace(intersect(curr, Typ(selTyp, false)), prevs)) {
926925
ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)
927926
}
928927
}

‎tests/patmat/3144.check‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
6: Pattern Match Exhaustivity: _: Foo

‎tests/patmat/3144c.check‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
6: Pattern Match Exhaustivity: _: Foo

‎tests/patmat/3144c.scala‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
sealed trait Foo
2+
case class Bar(s: String)
3+
4+
object Test {
5+
def shouldError(foo: Foo): String =
6+
foo match {
7+
case bar: Bar => bar.s
8+
}
9+
}

‎tests/patmat/3145.scala‎

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
object Test {
2+
sealed trait Foo
3+
class Bar(val s: String) extends Foo
4+
sealed abstract class Baz(val s: String) extends Foo
5+
6+
val f: Foo => String = {
7+
case bar: Bar => bar.s
8+
case baz: Baz => baz.s
9+
}
10+
}
11+
12+
object Test2 {
13+
sealed trait Foo
14+
class Bar extends Foo
15+
sealed trait Baz extends Foo
16+
17+
def f(x: Foo) = x match {
18+
case bar: Bar => 1
19+
case baz: Baz => 2
20+
}
21+
}
22+
23+
object Test3 {
24+
sealed trait Foo
25+
class Bar extends Foo
26+
sealed trait Baz extends Foo
27+
28+
def foo = {
29+
val x: Foo = new Baz {}
30+
x match {
31+
case bar: Bar => 1
32+
case baz: Baz => 2
33+
}
34+
}
35+
36+
def bar = {
37+
val x: Baz = new Baz {}
38+
x match {
39+
case bar: Bar => 1
40+
case baz: Baz => 2
41+
}
42+
}
43+
}

‎tests/patmat/andtype-opentype-interaction.check‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
23: Pattern Match Exhaustivity: _: SealedClass & OpenTrait, _: AbstractClass & OpenTrait, _: Clazz & OpenTrait, _: Trait & OpenTrait
2-
27: Pattern Match Exhaustivity: _: SealedClass & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & OpenTrait & OpenTrait2
3-
31: Pattern Match Exhaustivity: _: Trait & OpenClass
4-
35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass
5-
43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass
6-
47: Pattern Match Exhaustivity: _: Trait & OpenClass & OpenTrait & OpenClassSubclass
1+
23: Pattern Match Exhaustivity: _: SealedAbstractClass & OpenTrait, _: SealedClass & OpenTrait, _: SealedTrait & OpenTrait, _: AbstractClass & OpenTrait, _: Clazz & OpenTrait, _: Trait & OpenTrait
2+
27: Pattern Match Exhaustivity: _: SealedAbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2, _: SealedTrait & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & OpenTrait & OpenTrait2
3+
31: Pattern Match Exhaustivity: _: SealedTrait & OpenClass, _: Trait & OpenClass
4+
35: Pattern Match Exhaustivity: _: SealedTrait & OpenTrait & OpenClass, _: Trait & OpenTrait & OpenClass
5+
40: Match case Unreachable
6+
43: Pattern Match Exhaustivity: _: SealedTrait & OpenAbstractClass, _: Trait & OpenAbstractClass
7+
47: Pattern Match Exhaustivity: _: SealedTrait & OpenClass & OpenTrait & OpenClassSubclass, _: Trait & OpenClass & OpenTrait & OpenClassSubclass

‎tests/patmat/andtype-refinedtype-interaction.check‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
32: Pattern Match Exhaustivity: _: Trait & C1{x: Int}
2+
37: Match case Unreachable
3+
43: Match case Unreachable
24
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}
35
54: Pattern Match Exhaustivity: _: Trait & (C1 | C2 | T1){x: Int} & C3{x: Int}
6+
60: Match case Unreachable
47
65: Pattern Match Exhaustivity: _: Trait & (C1 | C2){x: Int} & (C3 | SubC1){x: Int}
58
72: Pattern Match Exhaustivity: _: Trait & (T1 & (C1 | SubC2)){x: Int} & (T2 & (C2 | C3 | SubC1)){x: Int} &
69
SubSubC1{x: Int}

‎tests/patmat/i2253.check‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1-
27: Pattern Match Exhaustivity: HasIntXIntM, HasIntXStringM
2-
28: Pattern Match Exhaustivity: HasIntXIntM
1+
28: Pattern Match Exhaustivity: HasIntXIntM, HasIntXStringM
32
29: Pattern Match Exhaustivity: HasIntXIntM
3+
29: Match case Unreachable
4+
30: Pattern Match Exhaustivity: HasIntXIntM
5+
30: Match case Unreachable

‎tests/patmat/i2253.scala‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@ object HasIntXIntM extends S {
2222
}
2323

2424
trait T
25+
case class TA(val x: Int) extends T with S
2526

2627
class Test {
2728
def onlyIntX(s: S { val x: Int }) = s match { case _: T => ; }

‎tests/patmat/patmatexhaust.check‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
49: Pattern Match Exhaustivity: _: Gp
55
59: Pattern Match Exhaustivity: Nil
66
75: Pattern Match Exhaustivity: _: B
7+
87: Pattern Match Exhaustivity: _: C1
78
100: Pattern Match Exhaustivity: _: C1
89
114: Pattern Match Exhaustivity: D2(), D1
910
126: Pattern Match Exhaustivity: _: C1

0 commit comments

Comments
 (0)