From e55c931333c9d0ea205593d29e0fc3072e0d7c9d Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Tue, 28 Nov 2017 11:48:42 +0100 Subject: [PATCH 1/2] Prune impossible types from exaustivity checker --- .../tools/dotc/transform/patmat/Space.scala | 26 +++++++++++-- tests/patmat/i3574.scala | 38 +++++++++++++++++++ 2 files changed, 60 insertions(+), 4 deletions(-) create mode 100644 tests/patmat/i3574.scala diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index bce2752d7164..d2fb0f042b9f 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -375,7 +375,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { } /* Whether the extractor is irrefutable */ - def irrefutable(unapp: tpd.Tree): Boolean = { + def irrefutable(unapp: Tree): Boolean = { // TODO: optionless patmat unapp.tpe.widen.finalResultType.isRef(scalaSomeClass) || (unapp.symbol.is(Synthetic) && unapp.symbol.owner.linkedClass.is(Case)) || @@ -557,11 +557,11 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { def refine(parent: Type, child: Symbol): Type = { if (child.isTerm && child.is(Case, butNot = Module)) return child.termRef // enum vals always match - val childTp = if (child.isTerm) child.termRef else child.typeRef + val childTp = if (child.isTerm) child.termRef else child.typeRef val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState()) - if (!resTp.exists) { + if (!resTp.exists) { debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}") NoType } @@ -625,7 +625,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) } val protoTp1 = thisTypeMap(tp1.appliedTo(tvars)) - if (protoTp1 <:< tp2) { + val result = if (protoTp1 <:< tp2) { if (isFullyDefined(protoTp1, force)) protoTp1 else instUndetMap(protoTp1) } @@ -640,6 +640,24 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { NoType } } + + // The intersection between a singleton type s and another type t is + // always empty when s is not a subtype of t. See patmat/i3573.scala + val hasEmptyIntersections = new ExistsAccumulator({ + case AndType(s: SingletonType, t) => + !(s <:< t) + case AndType(t, s: SingletonType) => + !(s <:< t) + case x => + false + }) + + if (hasEmptyIntersections(false, result)) { + debug.println(s"hasEmptyIntersections($protoTp1) = true") + NoType + } else { + result + } } /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */ diff --git a/tests/patmat/i3574.scala b/tests/patmat/i3574.scala new file mode 100644 index 000000000000..d8c544ade3f0 --- /dev/null +++ b/tests/patmat/i3574.scala @@ -0,0 +1,38 @@ +object PathVariantDefns { + sealed trait AtomBase { + sealed trait Atom + case class Zero(value: String) extends Atom + } + + trait Atom1 extends AtomBase { + case class One(value: String) extends Atom + } + + trait Atom2 extends AtomBase { + case class Two(value: String) extends Atom + } + + object Atoms01 extends AtomBase with Atom1 { + def f = { + val a: Atom = null + a match { + case Zero(x) => ??? + case One(x) => ??? + // match may not be exhaustive. + // It would fail on: PathVariantDefns.Atom2 & PathVariantDefns.Atoms01.type(PathVariantDefns.Atoms01).Two(_) + } + } + } + + object Atoms02 extends AtomBase with Atom2 { + def f = { + val a: Atom = null + a match { + case Zero(x) => ??? + case Two(x) => ??? + // match may not be exhaustive. + // It would fail on: PathVariantDefns.Atom1 & PathVariantDefns.Atoms02.type(PathVariantDefns.Atoms02).One(_) + } + } + } +} From 9cd931873a9388a7d76883761514d87bb5c16180 Mon Sep 17 00:00:00 2001 From: Olivier Blanvillain Date: Tue, 28 Nov 2017 13:56:33 +0100 Subject: [PATCH 2/2] Refactor check to an inhabited function --- .../tools/dotc/transform/patmat/Space.scala | 45 ++++++++++--------- 1 file changed, 23 insertions(+), 22 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index d2fb0f042b9f..e3e280250867 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala @@ -267,8 +267,8 @@ trait SpaceLogic { else // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)` Or(ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1).map { - case (ri, i) => Prod(tp1, fun1, sym1, ss1.updated(i, ri), full) - }) + case (ri, i) => Prod(tp1, fun1, sym1, ss1.updated(i, ri), full) + }) } @@ -561,7 +561,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { val resTp = instantiate(childTp, parent)(ctx.fresh.setNewTyperState()) - if (!resTp.exists) { + if (!resTp.exists || !inhabited(resTp)) { debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}") NoType } @@ -571,6 +571,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { } } + /** Can this type be inhabited by a value? + * + * Intersection between singleton types and other types is always empty + * the singleton type is not a subtype of the other type. + * See patmat/i3573.scala for an example. + */ + def inhabited(tpe: Type)(implicit ctx: Context): Boolean = { + val emptySingletonIntersection = new ExistsAccumulator({ + case AndType(s: SingletonType, t) => + !(s <:< t) + case AndType(t, s: SingletonType) => + !(s <:< t) + case x => + false + }) + + !emptySingletonIntersection(false, tpe) + } + /** Instantiate type `tp1` to be a subtype of `tp2` * * Return the instantiated type if type parameters and this type @@ -625,7 +644,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { val tvars = tp1.typeParams.map { tparam => newTypeVar(tparam.paramInfo.bounds) } val protoTp1 = thisTypeMap(tp1.appliedTo(tvars)) - val result = if (protoTp1 <:< tp2) { + if (protoTp1 <:< tp2) { if (isFullyDefined(protoTp1, force)) protoTp1 else instUndetMap(protoTp1) } @@ -640,24 +659,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic { NoType } } - - // The intersection between a singleton type s and another type t is - // always empty when s is not a subtype of t. See patmat/i3573.scala - val hasEmptyIntersections = new ExistsAccumulator({ - case AndType(s: SingletonType, t) => - !(s <:< t) - case AndType(t, s: SingletonType) => - !(s <:< t) - case x => - false - }) - - if (hasEmptyIntersections(false, result)) { - debug.println(s"hasEmptyIntersections($protoTp1) = true") - NoType - } else { - result - } } /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */