Skip to content

Commit 406a064

Browse files
authored
Merge pull request #3574 from dotty-staging/path-variant-defns
Prune impossible types from exhaustivity checker
2 parents 9de3905 + 9cd9318 commit 406a064

File tree

2 files changed

+62
-5
lines changed

2 files changed

+62
-5
lines changed

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

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -267,8 +267,8 @@ trait SpaceLogic {
267267
else
268268
// `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
269269
Or(ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1).map {
270-
case (ri, i) => Prod(tp1, fun1, sym1, ss1.updated(i, ri), full)
271-
})
270+
case (ri, i) => Prod(tp1, fun1, sym1, ss1.updated(i, ri), full)
271+
})
272272

273273
}
274274

@@ -375,7 +375,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
375375
}
376376

377377
/* Whether the extractor is irrefutable */
378-
def irrefutable(unapp: tpd.Tree): Boolean = {
378+
def irrefutable(unapp: Tree): Boolean = {
379379
// TODO: optionless patmat
380380
unapp.tpe.widen.finalResultType.isRef(scalaSomeClass) ||
381381
(unapp.symbol.is(Synthetic) && unapp.symbol.owner.linkedClass.is(Case)) ||
@@ -557,11 +557,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
557557
def refine(parent: Type, child: Symbol): Type = {
558558
if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match
559559

560-
val childTp = if (child.isTerm) child.termRef else child.typeRef
560+
val childTp = if (child.isTerm) child.termRef else child.typeRef
561561

562562
val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState())
563563

564-
if (!resTp.exists) {
564+
if (!resTp.exists || !inhabited(resTp)) {
565565
debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
566566
NoType
567567
}
@@ -571,6 +571,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
571571
}
572572
}
573573

574+
/** Can this type be inhabited by a value?
575+
*
576+
* Intersection between singleton types and other types is always empty
577+
* the singleton type is not a subtype of the other type.
578+
* See patmat/i3573.scala for an example.
579+
*/
580+
def inhabited(tpe: Type)(implicit ctx: Context): Boolean = {
581+
val emptySingletonIntersection = new ExistsAccumulator({
582+
case AndType(s: SingletonType, t) =>
583+
!(s <:< t)
584+
case AndType(t, s: SingletonType) =>
585+
!(s <:< t)
586+
case x =>
587+
false
588+
})
589+
590+
!emptySingletonIntersection(false, tpe)
591+
}
592+
574593
/** Instantiate type `tp1` to be a subtype of `tp2`
575594
*
576595
* Return the instantiated type if type parameters and this type

tests/patmat/i3574.scala

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
object PathVariantDefns {
2+
sealed trait AtomBase {
3+
sealed trait Atom
4+
case class Zero(value: String) extends Atom
5+
}
6+
7+
trait Atom1 extends AtomBase {
8+
case class One(value: String) extends Atom
9+
}
10+
11+
trait Atom2 extends AtomBase {
12+
case class Two(value: String) extends Atom
13+
}
14+
15+
object Atoms01 extends AtomBase with Atom1 {
16+
def f = {
17+
val a: Atom = null
18+
a match {
19+
case Zero(x) => ???
20+
case One(x) => ???
21+
// match may not be exhaustive.
22+
// It would fail on: PathVariantDefns.Atom2 & PathVariantDefns.Atoms01.type(PathVariantDefns.Atoms01).Two(_)
23+
}
24+
}
25+
}
26+
27+
object Atoms02 extends AtomBase with Atom2 {
28+
def f = {
29+
val a: Atom = null
30+
a match {
31+
case Zero(x) => ???
32+
case Two(x) => ???
33+
// match may not be exhaustive.
34+
// It would fail on: PathVariantDefns.Atom1 & PathVariantDefns.Atoms02.type(PathVariantDefns.Atoms02).One(_)
35+
}
36+
}
37+
}
38+
}

0 commit comments

Comments
 (0)