Skip to content

Prune impossible types from exhaustivity checker #3574

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.

Sign up for GitHub

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 2 commits into from
Dec 14, 2017
Merged

Prune impossible types from exhaustivity checker #3574

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e55c931
Prune impossible types from exaustivity checker
OlivierBlanvillain Nov 28, 2017
9cd9318
Refactor check to an inhabited function
OlivierBlanvillain Nov 28, 2017
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
26 changes: 22 additions & 4 deletions compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)) ||
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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)
}
Expand All @@ -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
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In the check, there's a facility named implementability from a contributor which does more or less the same thing. What do you think we can generalise/adapt implementability to handle the case?

In particular, I think it's good to rename it to def inhabited(tp: Type): Boolean, and it should be able to handle the current case as well. WDYT?

Copy link
Contributor Author

@OlivierBlanvillain OlivierBlanvillain Nov 28, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think implementability computes if a type can be implemented by other types (singleton types can't!), while inhabited would need to check if there could actually exists an instance of that type, so I'm not sure two logics can be merged.

@AleksanderBG what's your opinion on that?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think implementability should be refactored to have the semantics of inhabited. According to the core algorithm of exhaustivity check, it should only depend on the semantics of def inhabited(tp: Type): Boolean.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@OlivierBlanvillain I believe @liufengyun is correct - the function can be safely changed to check if a type is inhabited instead. This won't change the result for and-types, which is the only result intersectUnrelatedAtomicTypes should care about. I considered a similar refactoring myself when working on #3454. With the benefit of hindsight, type inhabitation is a far more generic notion and I should've tried to implement it from the beginning.


/** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
Expand Down
38 changes: 38 additions & 0 deletions tests/patmat/i3574.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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(_)
}
}
}
}