Skip to content

Match Types: implement cantPossiblyMatch #5996

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 20 commits into from
Mar 9, 2019
Merged

Match Types: implement cantPossiblyMatch #5996

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
c1b7e84
Minor TypeTestsCasts refactoring
OlivierBlanvillain Feb 11, 2019
6e39fcb
Rename evalOnce to letBind
OlivierBlanvillain Feb 11, 2019
eef623a
Rename cmp to typeComparer
OlivierBlanvillain Feb 11, 2019
6755f52
Remove reduceParallel
OlivierBlanvillain Feb 18, 2019
88cfb7e
Fix spacing for TypeComparer comments
OlivierBlanvillain Feb 21, 2019
bb1515e
Flag ChildrenQueried in hasAnonymousChild
OlivierBlanvillain Feb 22, 2019
f79d937
Implement cantPossiblyMatch
OlivierBlanvillain Mar 1, 2019
60d0e20
Replace Space.inhabited by typeComparer.intersecting
OlivierBlanvillain Feb 28, 2019
d1180cc
Move refineUsingParent to Typer
OlivierBlanvillain Feb 26, 2019
b0c1e7b
Check inhabitation of children in Space
OlivierBlanvillain Feb 28, 2019
c3d23fe
Only trust isSameType for fully instanciated types
OlivierBlanvillain Feb 28, 2019
4f934ad
Use derivesFrom instead of isSubType for classes
OlivierBlanvillain Mar 1, 2019
80c25e3
Handle type parameters using symbol.is(TypeParam)
OlivierBlanvillain Mar 4, 2019
ab74827
Fix AppliedType logic
OlivierBlanvillain Mar 4, 2019
1df0d8b
Revert "Rename evalOnce to letBind"
OlivierBlanvillain Mar 6, 2019
8827eff
Revert "Flag ChildrenQueried in hasAnonymousChild"
OlivierBlanvillain Mar 6, 2019
ffa8acf
Address review
OlivierBlanvillain Mar 6, 2019
e7f6049
Move refineUsingParent to TypeOps
OlivierBlanvillain Mar 6, 2019
f4df58d
Factor out cov. test and use it in the inv. case
OlivierBlanvillain Mar 6, 2019
ea04343
Update inhabited check in Space
OlivierBlanvillain Mar 6, 2019
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
104 changes: 4 additions & 100 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 @@ -298,16 +298,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
// Since projections of types don't include null, intersection with null is empty.
return Empty
}
val and = AndType(tp1, tp2)
// Then, no leaf of the and-type tree `and` is a subtype of `and`.
val res = inhabited(and)
val res = ctx.typeComparer.intersecting(tp1, tp2)

debug.println(s"atomic intersection: ${and.show} = ${res}")
debug.println(s"atomic intersection: ${AndType(tp1, tp2).show} = ${res}")

if (!res) Empty
else if (tp1.isSingleton) Typ(tp1, true)
else if (tp2.isSingleton) Typ(tp2, true)
else Typ(and, true)
else Typ(AndType(tp1, tp2), true)
}

/** Whether the extractor is irrefutable */
Expand Down Expand Up @@ -516,101 +514,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

val childTp = if (child.isTerm) child.termRef else child.typeRef

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

if (!resTp.exists || !inhabited(resTp)) {
Copy link
Contributor

Choose a reason for hiding this comment

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

The first part returning NoType is no longer present. Is that intentional? EDIT: I see that seems to be handled by the next commit "Check inhabitation of children" now. Correct?

Copy link
Contributor

Choose a reason for hiding this comment

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

Also, I don't understand SpaceEngines inhabited enough so I have to ask: Does SpaceEngine follow the same logic that an abstract type / type parameter and a class type can potentially overlap? /cc @liufengyun

Copy link
Contributor

Choose a reason for hiding this comment

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

Yes, it takes the bounds & variance of abstract type & type parameters into consideration.

So it reports non-exhaustive warnings for the following code (it is possible that T = Int | Boolean):

object O {
   sealed trait Expr[+T]
   case class IExpr(x: Int) extends Expr[Int]
   case class BExpr(b: Boolean) extends Expr[Boolean]

   def foo[T](x: Expr[T], y: Expr[T]) = (x, y) match {
      case (IExpr(_), IExpr(_)) => true
      case (BExpr(_), BExpr(_)) => false
   }
}

It does not report warning for the following code, due to nonvariance of the type parameter:

object O {
  sealed trait Expr[T]
  case class BExpr(bool: Boolean) extends Expr[Boolean]
  case class IExpr(int: Int) extends Expr[Int]

  def join[T](e1: Expr[T], e2: Expr[T]): Expr[T] = (e1, e2) match {
    case (IExpr(i1), IExpr(i2)) => IExpr(i1 + i2)
    case (BExpr(b1), BExpr(b2)) => BExpr(b1 & b2)
  }
}

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes I did that in a separate commit because it requires some extra logic: this check from space takes a type as input and looks for unrealizable intersections inside, while the other check started from two types and checks if their intersection is unrealizable. The commits move a test back and forth in /pending to document what is handled by that code.

debug.println(s"[refine] unqualified child ousted: ${childTp.show} !< ${parent.show}")
NoType
}
else {
debug.println(s"$child instantiated ------> $resTp")
resTp.dealias
}
}

/** Can this type be inhabited by a value?
*
* Check is based on the following facts:
*
* - single inheritance of classes
* - final class cannot be extended
* - intersection of a singleton type with another irrelevant type (patmat/i3574.scala)
*
*/
def inhabited(tp: Type)(implicit ctx: Context): Boolean = {
// convert top-level type shape into "conjunctive normal form"
def cnf(tp: Type): Type = tp match {
case AndType(OrType(l, r), tp) =>
OrType(cnf(AndType(l, tp)), cnf(AndType(r, tp)))
case AndType(tp, o: OrType) =>
cnf(AndType(o, tp))
case AndType(l, r) =>
val l1 = cnf(l)
val r1 = cnf(r)
if (l1.ne(l) || r1.ne(r)) cnf(AndType(l1, r1))
else AndType(l1, r1)
case OrType(l, r) =>
OrType(cnf(l), cnf(r))
case tp @ RefinedType(OrType(tp1, tp2), _, _) =>
OrType(
cnf(tp.derivedRefinedType(tp1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)),
cnf(tp.derivedRefinedType(tp2, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo))
)
case tp: RefinedType =>
val parent1 = cnf(tp.parent)
val tp1 = tp.derivedRefinedType(parent1, refinedName = tp.refinedName, refinedInfo = tp.refinedInfo)

if (parent1.ne(tp.parent)) cnf(tp1) else tp1
case tp: TypeAlias =>
cnf(tp.alias)
case _ =>
tp
}

def isSingleton(tp: Type): Boolean = tp.dealias match {
case AndType(l, r) => isSingleton(l) || isSingleton(r)
case OrType(l, r) => isSingleton(l) && isSingleton(r)
case tp => tp.isSingleton
}

def recur(tp: Type): Boolean = tp.dealias match {
case AndType(tp1, tp2) =>
recur(tp1) && recur(tp2) && {
val bases1 = tp1.widenDealias.classSymbols
val bases2 = tp2.widenDealias.classSymbols

debug.println(s"bases of ${tp1.show}: " + bases1)
debug.println(s"bases of ${tp2.show}: " + bases2)
debug.println(s"${tp1.show} <:< ${tp2.show} : " + (tp1 <:< tp2))
debug.println(s"${tp2.show} <:< ${tp1.show} : " + (tp2 <:< tp1))

val noClassConflict =
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym1.isSubClass(sym2))) ||
bases1.forall(sym1 => sym1.is(Trait) || bases2.forall(sym2 => sym2.is(Trait) || sym2.isSubClass(sym1)))

debug.println(s"class conflict for ${tp.show}? " + !noClassConflict)

noClassConflict &&
(!isSingleton(tp1) || tp1 <:< tp2) &&
(!isSingleton(tp2) || tp2 <:< tp1) &&
(!bases1.exists(_ is Final) || tp1 <:< maxTypeMap.apply(tp2)) &&
(!bases2.exists(_ is Final) || tp2 <:< maxTypeMap.apply(tp1))
}
case OrType(tp1, tp2) =>
recur(tp1) || recur(tp2)
case tp: RefinedType =>
recur(tp.parent)
case tp: TypeRef =>
recur(tp.prefix) && !(tp.classSymbol.is(AbstractFinal))
case _ =>
true
}

val res = recur(cnf(tp))

debug.println(s"${tp.show} inhabited? " + res)

res
instantiate(childTp, parent)(ctx.fresh.setNewTyperState()).dealias
}

/** expose abstract type references to their bounds or tvars according to variance */
Expand Down
12 changes: 6 additions & 6 deletions tests/patmat/andtype-opentype-interaction.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait, _: SealedTrait & OpenTrait, _: SealedClass & OpenTrait, _: SealedAbstractClass & OpenTrait
27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedTrait & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2, _: SealedAbstractClass & OpenTrait & OpenTrait2
31: Pattern Match Exhaustivity: _: Trait & OpenClass, _: SealedTrait & OpenClass
35: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenClass, _: SealedTrait & OpenTrait & OpenClass
43: Pattern Match Exhaustivity: _: Trait & OpenAbstractClass, _: SealedTrait & OpenAbstractClass
47: Pattern Match Exhaustivity: _: Trait & OpenClass & (OpenTrait & OpenClassSubclass), _: SealedTrait & OpenClass & (OpenTrait & OpenClassSubclass)
23: Pattern Match Exhaustivity: _: Trait & OpenTrait, _: Clazz & OpenTrait, _: AbstractClass & OpenTrait, _: SealedClass & OpenTrait
27: Pattern Match Exhaustivity: _: Trait & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: SealedClass & 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 & OpenClass & (OpenTrait & OpenClassSubclass)
2 changes: 1 addition & 1 deletion tests/patmat/t6420.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
5: Pattern Match Exhaustivity: (_: List, List(true, _: _*)), (_: List, List(false, _: _*)), (_: List, Nil)
5: Pattern Match Exhaustivity: (List(true, _: _*), List(true, _: _*)), (List(true, _: _*), List(false, _: _*)), (List(true, _: _*), Nil), (List(false, _: _*), List(true, _: _*)), (List(false, _: _*), List(false, _: _*)), (List(false, _: _*), Nil), (Nil, List(true, _: _*)), (Nil, List(false, _: _*)), (Nil, Nil), (_: List, List(true, _: _*)), (_: List, List(false, _: _*)), (_: List, Nil)
2 changes: 1 addition & 1 deletion tests/patmat/t7466.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
8: Pattern Match Exhaustivity: (_, true), (_, false)
8: Pattern Match Exhaustivity: (true, true), (true, false), (false, true), (false, false), (_, true), (_, false)
0 tests/patmat/i3574.scala → tests/pending/i3574.scala
View file
Open in desktop
File renamed without changes.