Fix #2363: better handle extractors in exhaustivity check #2424

liufengyun · 2017-05-12T20:57:33Z

Fix #2363: better handle extractors in exhaustivity check

Better handle exactors
Translate the pattern List(pat1, pat2, c:_*) to space semantically
Deal with extractors that return Some[_] or option-less type
Reduce redundant counterexamples in the warning

Previously we approximate extractor either to the extracted type space or Empty,
which is too coarse, and it causes some false positives about unreachable case.
Introducing the concept extractor into the theory enables us to inspect the
patterns inside extractors and check more unreachable cases, which is not
supported by Scalac.

Scalac is silent with following code, but Dotty correctly reports both unexhaustive and
unreachable warnings.

    sealed trait Node
    case class NodeA(i: Int) extends Node
    case class NodeB(b: Boolean) extends Node
    case class NodeC(s: String) extends Node

    object Node {
      def unapply(node: Node): Option[(Node, Node)] = ???
    }

    object Test {
      def foo(x: Node): Boolean = x match { // unexhaustive
        case Node(NodeA(_), NodeB(_)) => true
        case Node(NodeA(4), NodeB(false)) => true // unreachable code
      }
    }

liufengyun · 2017-05-12T21:13:00Z

compiler/src/dotty/tools/dotc/reporting/UniqueMessagePositions.scala

@@ -23,7 +23,7 @@ trait UniqueMessagePositions extends Reporter {
        for (pos <- m.pos.start to m.pos.end) {
          positions get (ctx.source, pos) match {
            case Some(level) if level >= m.level => shouldHide = true
-            case _ => positions((ctx.source, pos)) = m.level
+            case _ => // positions((ctx.source, pos)) = m.level


The CI fails because the change of this line. There's some bug hidden in isHidden, I have to comment it out to temporarily make sure all the exhaustivity/unreachability warnings are shown. Otherwise, the unreachable warning in the PR example will be incorrectly hidden.

1. Better handle exactors 2. Translate the pattern `List(pat1, pat2, c:_*)` to space semantically 3. Deal with extractors that return `Some[_]` Previously we approximate extractor either to the extracted type or Empty, which is too coarse, and it causes some false positives about unreachable case. Introducing the concept extractor into the theory enables us to inspect the patterns inside extractors and check more unreachable cases, which is not supported by Scalac. Scalac is silent with following code, but Dotty reports both unexhaustive and unreachable warnings. sealed trait Node case class NodeA(i: Int) extends Node case class NodeB(b: Boolean) extends Node case class NodeC(s: String) extends Node object Node { def unapply(node: Node): Option[(Node, Node)] = ??? } object Test { def foo(x: Node): Boolean = x match { // unexhaustive case Node(NodeA(_), NodeB(_)) => true case Node(NodeA(4), NodeB(false)) => true // unreachable code } }

smarter · 2017-05-12T21:38:13Z

@liufengyun Not directly related to this PR, but while you're working on this code, could you have a look at the exhaustiveness warnings reported against dotty itself when bootstrapping? See http://dotty-ci.epfl.ch/lampepfl/dotty/2267/4 for example. You can reproduce that locally by running dotty-compiler-bootstrapped/compile. It would be good to see which of these warnings are real warnings we need to fix and which one are bugs in the exhaustiveness checker.

liufengyun · 2017-05-12T21:41:19Z

@smarter Sure, I'll examine log to see if there're still false positives.

liufengyun · 2017-05-15T09:45:12Z

Now all false positives about unreachability/exhaustiveness are fixed. True positives will be addressed in #2429 separately.

Could you please review @smarter ?

liufengyun · 2017-05-15T11:36:32Z

@felixmulder The last commit 31ae57b contains some changes to the doc-tool, could you please confirm if the changes make sense?

felixmulder · 2017-05-15T11:46:18Z

doc-tool/src/dotty/tools/dottydoc/util/MemberLookup.scala

@@ -77,6 +77,7 @@ trait MemberLookup {
      case (x :: xs, _) =>
        if (xs.nonEmpty) globalLookup
        else lookup(entity, packages, "scala." + query)
+      case (Nil, _) => ??? // impossible as long as query is not empty


let's do something better than ???, otherwise LGTM

smarter · 2017-05-15T13:07:34Z

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

@@ -426,14 +509,14 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
          case space => List(space)
        }
      case OrType(tp1, tp2) => List(Typ(tp1, true), Typ(tp2, true))
-      case _ if tp =:= ctx.definitions.BooleanType =>
+      case tp if tp =:= ctx.definitions.BooleanType =>


tp.isRef(defn.BooleanClass)

smarter · 2017-05-15T13:10:05Z

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

@@ -549,6 +632,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

        if (ctx.definitions.isTupleType(tp))
          signature(tp).map(_ => "_").mkString("(", ", ", ")")
+        else if (sym.showFullName == "scala.collection.immutable.List")


We should never do string comparisons to determine the type of something. Instead something like sym == defn.ListClass should be used, if ListClass is not defined in Definitions.scala then it should be added.

smarter · 2017-05-15T13:11:24Z

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

        else Empty
      }.reduce((a, b) => Or(List(a, b)))

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

+      debug.println(s"---------------reachable? ${show(curr)}")


I suggest adding a Printer for the exhaustiveness checker in https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/config/Printers.scala instead of using debug here.

The debug is just a rename of the exhaustivity printer :)

smarter · 2017-05-15T13:12:03Z

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

@@ -98,19 +102,31 @@ trait SpaceLogic {
  def show(sp: Space): String

  /** Simplify space using the laws, there's no nested union after simplify */
-  def simplify(space: Space): Space = space match {
+  def simplify(space: Space, aggressive: Boolean = false): Space = space match {


Could you update the documentation of this method to explain what the aggressive parameter is for?

smarter · 2017-05-15T13:12:38Z

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

-        isSubType(tp1, tp2) || tryDecompose1(tp1) || tryDecompose2(tp2)
-      case (Typ(tp1, _), Or(ss)) =>
+        isSubType(tp1, tp2)
+      case (Typ(tp1, _), Or(ss)) =>  // optimization


Maybe improve this comment to explain what this is an optimization of?

smarter · 2017-05-15T13:13:00Z

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

@@ -386,7 +469,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
  /** Is `tp1` a subtype of `tp2`?  */
  def isSubType(tp1: Type, tp2: Type): Boolean = {
    // check SI-9657 and tests/patmat/gadt.scala
-    val res = erase(tp1) <:< erase(tp2)
+    val res = tp1 <:< erase(tp2)


Could you add a comment explaining why it's correct to erase tp2 but not tp1 ?

smarter · 2017-05-15T13:14:12Z

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

@@ -420,7 +420,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
        Kon(pat.tpe.stripAnnots, pats.map(pat => project(pat)))
      else if (fun.symbol.owner == scalaSeqFactoryClass && fun.symbol.name == nme.unapplySeq)
        projectList(pats)
-      else if (fun.symbol.info.resultType.isRef(scalaSomeClass))
+      else if (!fun.symbol.info.finalResultType.isRef(scalaOptionClass))


I don't think this is correct in general, the return type of an option-less patmat may define a def isEmpty: Boolean method, if this method return false, then the case will not be taken.

Sorry, if isEmpty returns true, not false

Ah, I see, then it means we cannot tell from types whether an option-less is exhaustive or not. I'll retract the last commit.

Well, if the method is defined as def isEmpty: false then we know it will always return false :). But we should probably not encode this logic in the exhaustiveness checker until we have a real spec for option-less pattern-matching that explains all cases.

smarter · 2017-05-15T15:16:14Z

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

@@ -469,6 +475,19 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
  /** Is `tp1` a subtype of `tp2`?  */
  def isSubType(tp1: Type, tp2: Type): Boolean = {
    // check SI-9657 and tests/patmat/gadt.scala
+    //
+    // `erase` is a walkaround to make the following code pass the check:


typo: walkaround -> workaround

smarter · 2017-05-15T15:19:55Z

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

  private val scalaSeqFactoryClass = ctx.requiredClass("scala.collection.generic.SeqFactory".toTypeName)
  private val scalaListType        = ctx.requiredClassRef("scala.collection.immutable.List".toTypeName)
  private val scalaNilType         = ctx.requiredModuleRef("scala.collection.immutable.Nil".toTermName)
-  private val scalaConType         = ctx.requiredClassRef("scala.collection.immutable.::".toTypeName)
+  private val scalaConsType        = ctx.requiredClassRef("scala.collection.immutable.::".toTypeName)


You could get rid of all the .toTypeName here if Decorators.PreNamedString is imported.

liufengyun commented May 12, 2017

View reviewed changes

liufengyun force-pushed the fix-2363 branch from fc14c87 to 495ed99 Compare May 12, 2017 21:31

liufengyun added 3 commits May 14, 2017 11:43

fix false positives in bootstrap

9453f6d

add missing @unchecked for for patmat

9d1e94c

Fix false warning about unreachable code in Dotty

9f8c089

liufengyun mentioned this pull request May 15, 2017

Fix true exhaustivity warnings in Bootstrap #2429

Closed

6 tasks

Fix scala#2429: fix true exhaustivity warnings

31ae57b

felixmulder reviewed May 15, 2017

View reviewed changes

liufengyun added 2 commits May 15, 2017 14:03

address review feedback

20448c8

support option-less patmat as complete match

30787e5

smarter reviewed May 15, 2017

View reviewed changes

liufengyun added 2 commits May 15, 2017 15:35

retract the option-less commit

61414c2

address review feedback

c569f23

smarter reviewed May 15, 2017

View reviewed changes

liufengyun added 2 commits May 15, 2017 17:20

fix typo in the comment

fc20768

use decorators to avoid toTypeName and toTermName

1e695ea

felixmulder merged commit e9fd333 into scala:master May 16, 2017

allanrenucci deleted the fix-2363 branch December 14, 2017 19:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix #2363: better handle extractors in exhaustivity check #2424

Fix #2363: better handle extractors in exhaustivity check #2424

liufengyun commented May 12, 2017 •

edited

Loading

liufengyun May 12, 2017

smarter commented May 12, 2017

liufengyun commented May 12, 2017

liufengyun commented May 15, 2017

liufengyun commented May 15, 2017

felixmulder May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

liufengyun May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

liufengyun May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

smarter May 15, 2017

Fix #2363: better handle extractors in exhaustivity check #2424

Fix #2363: better handle extractors in exhaustivity check #2424

Conversation

liufengyun commented May 12, 2017 • edited Loading

Choose a reason for hiding this comment

smarter commented May 12, 2017

liufengyun commented May 12, 2017

liufengyun commented May 15, 2017

liufengyun commented May 15, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

liufengyun commented May 12, 2017 •

edited

Loading