implementation of exhaustivity and redundancy check

11 files changed, 699 insertions, 17 deletions

diff --git a/src/dotty/tools/dotc/ast/Desugar.scala b/src/dotty/tools/dotc/ast/Desugar.scala
index 8a4b9cfe8..346af42b8 100644
--- a/src/dotty/tools/dotc/ast/Desugar.scala
+++ b/src/dotty/tools/dotc/ast/Desugar.scala
@@ -616,16 +616,20 @@ object desugar {
    *
    *       { cases }
    *  ==>
-   *       x$1 => x$1 match { cases }
+   *       x$1 => (x$1 @unchecked) match { cases }
    *
    *  If `nparams` != 1, expand instead to
    *
-   *       (x$1, ..., x$n) => (x$0, ..., x${n-1}) match { cases }
+   *       (x$1, ..., x$n) => (x$0, ..., x${n-1} @unchecked) match { cases }
    */
-  def makeCaseLambda(cases: List[CaseDef], nparams: Int = 1)(implicit ctx: Context) = {
+  def makeCaseLambda(cases: List[CaseDef], nparams: Int = 1, unchecked: Boolean = true)(implicit ctx: Context) = {
     val params = (1 to nparams).toList.map(makeSyntheticParameter(_))
     val selector = makeTuple(params.map(p => Ident(p.name)))
-    Function(params, Match(selector, cases))
+
+    if (unchecked)
+      Function(params, Match(Annotated(New(ref(defn.UncheckedAnnotType)), selector), cases))
+    else
+      Function(params, Match(selector, cases))
   }
 
   /** Map n-ary function `(p1, ..., pn) => body` where n != 1 to unary function as follows:
@@ -753,7 +757,7 @@ object desugar {
         case VarPattern(named, tpt) =>
           Function(derivedValDef(named, tpt, EmptyTree, Modifiers(Param)) :: Nil, body)
         case _ =>
-          makeCaseLambda(CaseDef(pat, EmptyTree, body) :: Nil)
+          makeCaseLambda(CaseDef(pat, EmptyTree, body) :: Nil, unchecked = false)
       }
 
       /** If `pat` is not an Identifier, a Typed(Ident, _), or a Bind, wrap
@@ -799,7 +803,7 @@ object desugar {
         val cases = List(
           CaseDef(pat, EmptyTree, Literal(Constant(true))),
           CaseDef(Ident(nme.WILDCARD), EmptyTree, Literal(Constant(false))))
-        Apply(Select(rhs, nme.withFilter), Match(EmptyTree, cases))
+        Apply(Select(rhs, nme.withFilter), makeCaseLambda(cases))
       }
 
       /** Is pattern `pat` irrefutable when matched against `rhs`?
diff --git a/src/dotty/tools/dotc/config/ScalaSettings.scala b/src/dotty/tools/dotc/config/ScalaSettings.scala
index 5d5903584..c090a5515 100644
--- a/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -163,6 +163,7 @@ class ScalaSettings extends Settings.SettingGroup {
   val YkeepComments = BooleanSetting("-Ykeep-comments", "Keep comments when scanning source files.")
   val YforceSbtPhases = BooleanSetting("-Yforce-sbt-phases", "Run the phases used by sbt for incremental compilation (ExtractDependencies and ExtractAPI) even if the compiler is ran outside of sbt, for debugging.")
   val YdumpSbtInc = BooleanSetting("-Ydump-sbt-inc", "For every compiled foo.scala, output the API representation and dependencies used for sbt incremental compilation in foo.inc, implies -Yforce-sbt-phases.")
+  val YcheckAllPatmat = BooleanSetting("-Ycheck-all-patmat", "Check exhaustivity and redundancy of all pattern matching (used for testing the algorithm)")
   def stop = YstopAfter
 
   /** Area-specific debug output.
diff --git a/src/dotty/tools/dotc/core/Types.scala b/src/dotty/tools/dotc/core/Types.scala
index 1bfd6eaee..ad27f924e 100644
--- a/src/dotty/tools/dotc/core/Types.scala
+++ b/src/dotty/tools/dotc/core/Types.scala
@@ -841,6 +841,13 @@ object Types {
       case _ => this
     }
 
+    /** Eliminate anonymous classes */
+    final def deAnonymize(implicit ctx: Context): Type = this match {
+      case tp:TypeRef if tp.symbol.isAnonymousClass =>
+        tp.symbol.asClass.typeRef.asSeenFrom(tp.prefix, tp.symbol.owner)
+      case tp => tp
+    }
+
     /** Follow aliases and dereferences LazyRefs and instantiated TypeVars until type
      *  is no longer alias type, LazyRef, or instantiated type variable.
      */
diff --git a/src/dotty/tools/dotc/core/classfile/ClassfileParser.scala b/src/dotty/tools/dotc/core/classfile/ClassfileParser.scala
index 4ea98f7c3..1570dbca0 100644
--- a/src/dotty/tools/dotc/core/classfile/ClassfileParser.scala
+++ b/src/dotty/tools/dotc/core/classfile/ClassfileParser.scala
@@ -85,6 +85,7 @@ class ClassfileParser(
     val jflags       = in.nextChar
     val isAnnotation = hasAnnotation(jflags)
     val sflags       = classTranslation.flags(jflags)
+    val isEnum       = (jflags & JAVA_ACC_ENUM) != 0
     val nameIdx      = in.nextChar
     currentClassName = pool.getClassName(nameIdx)
 
@@ -140,6 +141,15 @@ class ClassfileParser(
       setClassInfo(classRoot, classInfo)
       setClassInfo(moduleRoot, staticInfo)
     }
+
+    // eager load java enum definitions for exhaustivity check of pattern match
+    if (isEnum) {
+      instanceScope.toList.map(_.ensureCompleted())
+      staticScope.toList.map(_.ensureCompleted())
+      classRoot.setFlag(Flags.Enum)
+      moduleRoot.setFlag(Flags.Enum)
+    }
+
     result
   }
 
diff --git a/src/dotty/tools/dotc/transform/ExpandSAMs.scala b/src/dotty/tools/dotc/transform/ExpandSAMs.scala
index d9445d046..04c6864b1 100644
--- a/src/dotty/tools/dotc/transform/ExpandSAMs.scala
+++ b/src/dotty/tools/dotc/transform/ExpandSAMs.scala
@@ -74,7 +74,8 @@ class ExpandSAMs extends MiniPhaseTransform { thisTransformer =>
             Bind(defaultSym, Underscore(selector.tpe.widen)),
             EmptyTree,
             Literal(Constant(false)))
-        cpy.Match(applyRhs)(paramRef, cases.map(translateCase) :+ defaultCase)
+        val annotated = Annotated(New(ref(defn.UncheckedAnnotType)), paramRef)
+        cpy.Match(applyRhs)(annotated, cases.map(translateCase) :+ defaultCase)
       case _ =>
         tru
     }
diff --git a/src/dotty/tools/dotc/transform/PatternMatcher.scala b/src/dotty/tools/dotc/transform/PatternMatcher.scala
index 839189948..21b56959b 100644
--- a/src/dotty/tools/dotc/transform/PatternMatcher.scala
+++ b/src/dotty/tools/dotc/transform/PatternMatcher.scala
@@ -24,6 +24,7 @@ import Applications._
 import TypeApplications._
 import SymUtils._, core.NameOps._
 import core.Mode
+import patmat._
 
 import dotty.tools.dotc.util.Positions.Position
 import dotty.tools.dotc.core.Decorators._
@@ -52,6 +53,13 @@ class PatternMatcher extends MiniPhaseTransform with DenotTransformer {thisTrans
   override def transformMatch(tree: Match)(implicit ctx: Context, info: TransformerInfo): Tree = {
     val translated = new Translator()(ctx).translator.translateMatch(tree)
 
+    // check exhaustivity and unreachability
+    val engine = new SpaceEngine
+    if (engine.checkable(tree)) {
+      engine.checkExhaustivity(tree)
+      engine.checkRedundancy(tree)
+    }
+
     translated.ensureConforms(tree.tpe)
   }
 
@@ -1244,13 +1252,6 @@ class PatternMatcher extends MiniPhaseTransform with DenotTransformer {thisTrans
       case _                                                => false
     }
 
-    def elimAnonymousClass(t: Type) = t match {
-      case t:TypeRef if t.symbol.isAnonymousClass =>
-        t.symbol.asClass.typeRef.asSeenFrom(t.prefix, t.symbol.owner)
-      case _ =>
-        t
-    }
-
     /** Implement a pattern match by turning its cases (including the implicit failure case)
       * into the corresponding (monadic) extractors, and combining them with the `orElse` combinator.
       *
@@ -1264,7 +1265,7 @@ class PatternMatcher extends MiniPhaseTransform with DenotTransformer {thisTrans
     def translateMatch(match_ : Match): Tree = {
       val Match(sel, cases) = match_
 
-      val selectorTp = elimAnonymousClass(sel.tpe.widen/*withoutAnnotations*/)
+      val selectorTp = sel.tpe.widen.deAnonymize/*withoutAnnotations*/
 
       val selectorSym = freshSym(sel.pos, selectorTp, "selector")
 
@@ -1273,6 +1274,7 @@ class PatternMatcher extends MiniPhaseTransform with DenotTransformer {thisTrans
         case _                                                    => (cases, None)
       }
 
+
       // checkMatchVariablePatterns(nonSyntheticCases) // only used for warnings
 
       // we don't transform after uncurry
diff --git a/src/dotty/tools/dotc/transform/PostTyper.scala b/src/dotty/tools/dotc/transform/PostTyper.scala
index b71284049..fd22a0ad9 100644
--- a/src/dotty/tools/dotc/transform/PostTyper.scala
+++ b/src/dotty/tools/dotc/transform/PostTyper.scala
@@ -39,6 +39,8 @@ import Symbols._, TypeUtils._
  *
  *  (9) Adds SourceFile annotations to all top-level classes and objects
  *
+ *  (10) Adds Child annotations to all sealed classes
+ *
  *  The reason for making this a macro transform is that some functions (in particular
  *  super and protected accessors and instantiation checks) are naturally top-down and
  *  don't lend themselves to the bottom-up approach of a mini phase. The other two functions
@@ -243,6 +245,13 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer  { thisTran
                   ctx.compilationUnit.source.exists &&
                   sym != defn.SourceFileAnnot)
                 sym.addAnnotation(Annotation.makeSourceFile(ctx.compilationUnit.source.file.path))
+
+              if (!sym.isAnonymousClass) // ignore anonymous class
+                for (parent <- sym.asClass.classInfo.classParents) {
+                  val pclazz = parent.classSymbol
+                  if (pclazz.is(Sealed)) pclazz.addAnnotation(Annotation.makeChild(sym))
+                }
+
               tree
             }
             else {
diff --git a/src/dotty/tools/dotc/transform/patmat/Space.scala b/src/dotty/tools/dotc/transform/patmat/Space.scala
new file mode 100644
index 000000000..d942c6853
--- /dev/null
+++ b/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -0,0 +1,619 @@
+package dotty.tools.dotc
+package transform
+package patmat
+
+import core.Types._
+import core.Contexts._
+import core.Flags._
+import ast.Trees._
+import ast.tpd
+import core.Decorators._
+import core.Symbols._
+import core.StdNames._
+import core.NameOps._
+import core.Constants._
+
+/** Space logic for checking exhaustivity and unreachability of pattern matching
+ *
+ *  Space can be thought of as a set of possible values. A type or a pattern
+ *  both refer to spaces. The space of a type is the values that inhabit the
+ *  type. The space of a pattern is the values that can be covered by the
+ *  pattern.
+ *
+ *  Space is recursively defined as follows:
+ *
+ *      1. `Empty` is a space
+ *      2. For a type T, `Typ(T)` is a space
+ *      3. A union of spaces `S1 | S2 | ...` is a space
+ *      4. For a case class Kon(x1: T1, x2: T2, .., xn: Tn), if S1, S2, ..., Sn
+ *          are spaces, then `Kon(S1, S2, ..., Sn)` is a space.
+ *      5. A constant `Const(value, T)` is a point in space
+ *      6. A stable identifier `Var(sym, T)` is a space
+ *
+ *  For the problem of exhaustivity check, its formulation in terms of space is as follows:
+ *
+ *      Is the space Typ(T) a subspace of the union of space covered by all the patterns?
+ *
+ *  The problem of unreachable patterns can be formulated as follows:
+ *
+ *      Is the space covered by a pattern a subspace of the space covered by previous patterns?
+ *
+ *  Assumption:
+ *    (1) One case class cannot be inherited directly or indirectly by another
+ *        case class.
+ *    (2) Inheritance of a case class cannot be well handled by the algorithm.
+ *
+ */
+
+
+/** space definition */
+sealed trait Space
+
+/** Empty space */
+case object Empty extends Space
+
+/** Space representing the set of all values of a type
+ *
+ * @param tp: the type this space represents
+ * @param decomposed: does the space result from decomposition? Used for pretty print
+ *
+ */
+case class Typ(tp: Type, decomposed: Boolean) extends Space
+
+/** Space representing a constructor pattern */
+case class Kon(tp: Type, params: List[Space]) extends Space
+
+/** Union of spaces */
+case class Or(spaces: List[Space]) extends Space
+
+/** Point in space */
+sealed trait Point extends Space
+
+/** Point representing variables(stable identifier) in patterns */
+case class Var(sym: Symbol, tp: Type) extends Point
+
+/** Point representing literal constants in patterns */
+case class Const(value: Constant, tp: Type) extends Point
+
+/** abstract space logic */
+trait SpaceLogic {
+  /** Is `tp1` a subtype of `tp2`? */
+  def isSubType(tp1: Type, tp2: Type): Boolean
+
+  /** Is `tp1` the same type as `tp2`? */
+  def isEqualType(tp1: Type, tp2: Type): Boolean
+
+  /** Is the type `tp` decomposable? i.e. all values of the type can be covered
+   *  by its decomposed types.
+   *
+   * Abstract sealed class, OrType, Boolean and Java enums can be decomposed.
+   */
+  def canDecompose(tp: Type): Boolean
+
+  /** Return term parameter types of the case class `tp` */
+  def signature(tp: Type): List[Type]
+
+  /** Get components of decomposable types */
+  def decompose(tp: Type): List[Space]
+
+  /** Simplify space using the laws, there's no nested union after simplify */
+  def simplify(space: Space): Space = space match {
+    case Kon(tp, spaces) =>
+      val sp = Kon(tp, spaces.map(simplify _))
+      if (sp.params.contains(Empty)) Empty
+      else sp
+    case Or(spaces) =>
+      val set = spaces.map(simplify _).flatMap {
+        case Or(ss) => ss
+        case s => Seq(s)
+      } filter (_ != Empty)
+
+      if (set.isEmpty) Empty
+      else if (set.size == 1) set.toList(0)
+      else Or(set)
+    case Typ(tp, _) =>
+      if (canDecompose(tp) && decompose(tp).isEmpty) Empty
+      else space
+    case _ => space
+  }
+
+  /** Flatten space to get rid of `Or` for pretty print */
+  def flatten(space: Space): List[Space] = space match {
+    case Kon(tp, spaces) =>
+      val flats = spaces.map(flatten _)
+
+      flats.foldLeft(List[Kon]()) { (acc, flat) =>
+        if (acc.isEmpty) flat.map(s => Kon(tp, Nil :+ s))
+        else for (Kon(tp, ss) <- acc; s <- flat) yield Kon(tp, ss :+ s)
+      }
+    case Or(spaces) =>
+      spaces.flatMap(flatten _)
+    case _ => List(space)
+  }
+
+  /** Is `a` a subspace of `b`? Equivalent to `a - b == Empty`, but faster */
+  def isSubspace(a: Space, b: Space): Boolean = {
+    def tryDecompose1(tp: Type) = canDecompose(tp) && isSubspace(Or(decompose(tp)), b)
+    def tryDecompose2(tp: Type) = canDecompose(tp) && isSubspace(a, Or(decompose(tp)))
+
+    (a, b) match {
+      case (Empty, _) => true
+      case (_, Empty) => false
+      case (Or(ss), _) => ss.forall(isSubspace(_, b))
+      case (Typ(tp1, _), Typ(tp2, _)) =>
+        isSubType(tp1, tp2) || tryDecompose1(tp1) || tryDecompose2(tp2)
+      case (Typ(tp1, _), Or(ss)) =>
+        ss.exists(isSubspace(a, _)) || tryDecompose1(tp1)
+      case (Typ(tp1, _), Kon(tp2, ss)) =>
+        isSubType(tp1, tp2) && isSubspace(Kon(tp2, signature(tp2).map(Typ(_, false))), b) ||
+        tryDecompose1(tp1)
+      case (Kon(tp1, ss), Typ(tp2, _)) =>
+        isSubType(tp1, tp2) ||
+          simplify(a) == Empty ||
+          (isSubType(tp2, tp1) && tryDecompose1(tp1)) ||
+          tryDecompose2(tp2)
+      case (Kon(_, _), Or(_)) =>
+        simplify(minus(a, b)) == Empty
+      case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
+        isEqualType(tp1, tp2) && ss1.zip(ss2).forall((isSubspace _).tupled)
+      case (Const(v1, _), Const(v2, _)) => v1 == v2
+      case (Const(_, tp1), Typ(tp2, _)) => isSubType(tp1, tp2) || tryDecompose2(tp2)
+      case (Const(_, _), Or(ss)) => ss.exists(isSubspace(a, _))
+      case (Const(_, _), _) => false
+      case (_, Const(_, _)) => false
+      case (Var(x, _), Var(y, _)) => x == y
+      case (Var(_, tp1), Typ(tp2, _)) => isSubType(tp1, tp2) || tryDecompose2(tp2)
+      case (Var(_, _), Or(ss)) => ss.exists(isSubspace(a, _))
+      case (Var(_, _), _) => false
+      case (_, Var(_, _)) => false
+    }
+  }
+
+  /** Intersection of two spaces  */
+  def intersect(a: Space, b: Space): Space = {
+    def tryDecompose1(tp: Type) = intersect(Or(decompose(tp)), b)
+    def tryDecompose2(tp: Type) = intersect(a, Or(decompose(tp)))
+
+    (a, b) match {
+      case (Empty, _) | (_, Empty) => Empty
+      case (_, Or(ss)) => Or(ss.map(intersect(a, _)).filterConserve(_ ne Empty))
+      case (Or(ss), _) => Or(ss.map(intersect(_, b)).filterConserve(_ ne Empty))
+      case (Typ(tp1, _), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) a
+        else if (isSubType(tp2, tp1)) b
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else Empty
+      case (Typ(tp1, _), Kon(tp2, ss)) =>
+        if (isSubType(tp2, tp1)) b
+        else if (isSubType(tp1, tp2)) a // problematic corner case: inheriting a case class
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else Empty
+      case (Kon(tp1, ss), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) a
+        else if (isSubType(tp2, tp1)) a  // problematic corner case: inheriting a case class
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else Empty
+      case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
+        if (!isEqualType(tp1, tp2)) Empty
+        else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) Empty
+        else Kon(tp1, ss1.zip(ss2).map((intersect _).tupled))
+      case (Const(v1, _), Const(v2, _)) =>
+        if (v1 == v2) a else Empty
+      case (Const(_, tp1), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) a
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else Empty
+      case (Const(_, _), _) => Empty
+      case (Typ(tp1, _), Const(_, tp2)) =>
+        if (isSubType(tp2, tp1)) b
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else Empty
+      case (_, Const(_, _)) => Empty
+      case (Var(x, _), Var(y, _)) =>
+        if (x == y) a else Empty
+      case (Var(_, tp1), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) a
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else Empty
+      case (Var(_, _), _) => Empty
+      case (Typ(tp1, _), Var(_, tp2)) =>
+        if (isSubType(tp2, tp1)) b
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else Empty
+      case (_, Var(_, _)) => Empty
+    }
+  }
+
+  /** The space of a not covered by b */
+  def minus(a: Space, b: Space): Space = {
+    def tryDecompose1(tp: Type) = minus(Or(decompose(tp)), b)
+    def tryDecompose2(tp: Type) = minus(a, Or(decompose(tp)))
+
+    (a, b) match {
+      case (Empty, _) => Empty
+      case (_, Empty) => a
+      case (Typ(tp1, _), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) Empty
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else a
+      case (Typ(tp1, _), Kon(tp2, ss)) =>
+        // corner case: inheriting a case class
+        // rationale: every instance of `tp1` is covered by `tp2(_)`
+        if (isSubType(tp1, tp2)) minus(Kon(tp2, signature(tp2).map(Typ(_, false))), b)
+        else if (canDecompose(tp1)) tryDecompose1(tp1)
+        else a
+      case (_, Or(ss)) =>
+        ss.foldLeft(a)(minus)
+      case (Or(ss), _) =>
+        Or(ss.map(minus(_, b)))
+      case (Kon(tp1, ss), Typ(tp2, _)) =>
+        // uncovered corner case: tp2 :< tp1
+        if (isSubType(tp1, tp2)) Empty
+        else if (simplify(a) == Empty) Empty
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else a
+      case (Kon(tp1, ss1), Kon(tp2, ss2)) =>
+        if (!isEqualType(tp1, tp2)) a
+        else if (ss1.zip(ss2).exists(p => simplify(intersect(p._1, p._2)) == Empty)) a
+        else if (ss1.zip(ss2).forall((isSubspace _).tupled)) Empty
+        else
+          // `(_, _, _) - (Some, None, _)` becomes `(None, _, _) | (_, Some, _) | (_, _, Empty)`
+          Or(ss1.zip(ss2).map((minus _).tupled).zip(0 to ss2.length - 1).map {
+              case (ri, i) => Kon(tp1, ss1.updated(i, ri))
+            })
+      case (Const(v1, _), Const(v2, _)) =>
+        if (v1 == v2) Empty else a
+      case (Const(_, tp1), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) Empty
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else a
+      case (Const(_, _), _) => a
+      case (Typ(tp1, _), Const(_, tp2)) =>  // Boolean & Java enum
+        if (canDecompose(tp1)) tryDecompose1(tp1)
+        else a
+      case (_, Const(_, _)) => a
+      case (Var(x, _), Var(y, _)) =>
+        if (x == y) Empty else a
+      case (Var(_, tp1), Typ(tp2, _)) =>
+        if (isSubType(tp1, tp2)) Empty
+        else if (canDecompose(tp2)) tryDecompose2(tp2)
+        else a
+      case (Var(_, _), _) => a
+      case (_, Var(_, _)) => a
+    }
+  }
+}
+
+/** Scala implementation of space logic */
+class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
+  import tpd._
+
+  /** Return the space that represents the pattern `pat`
+   *
+   *  If roundUp is true, approximate extractors to its type,
+   *  otherwise approximate extractors to Empty
+   */
+  def project(pat: Tree, roundUp: Boolean = true)(implicit ctx: Context): Space = pat match {
+    case Literal(c) => Const(c, c.tpe)
+    case _: BackquotedIdent => Var(pat.symbol, pat.tpe)
+    case Ident(_) | Select(_, _) =>
+      pat.tpe.stripAnnots match {
+        case tp: TermRef =>
+          if (pat.symbol.is(Enum))
+            Const(Constant(pat.symbol), tp)
+          else if (tp.underlyingIterator.exists(_.classSymbol.is(Module)))
+            Typ(tp.widenTermRefExpr.stripAnnots, false)
+          else
+            Var(pat.symbol, tp)
+        case tp => Typ(tp, false)
+      }
+    case Alternative(trees) => Or(trees.map(project(_, roundUp)))
+    case Bind(_, pat) => project(pat)
+    case UnApply(_, _, pats) =>
+      if (pat.tpe.classSymbol.is(CaseClass))
+        Kon(pat.tpe.stripAnnots, pats.map(pat => project(pat, roundUp)))
+      else if (roundUp) Typ(pat.tpe.stripAnnots, false)
+      else Empty
+    case Typed(pat @ UnApply(_, _, _), _) => project(pat)
+    case Typed(expr, _) => Typ(expr.tpe.stripAnnots, true)
+    case _ =>
+      Empty
+  }
+
+  /* Erase a type binding according to erasure semantics in pattern matching */
+  def erase(tp: Type): Type = {
+    def doErase(tp: Type): Type = tp match {
+      case tp: HKApply => erase(tp.superType)
+      case tp: RefinedType => erase(tp.parent)
+      case _ => tp
+    }
+
+    tp match {
+      case OrType(tp1, tp2) =>
+        OrType(erase(tp1), erase(tp2))
+      case AndType(tp1, tp2) =>
+        AndType(erase(tp1), erase(tp2))
+      case _ =>
+        val origin = doErase(tp)
+        if (origin =:= defn.ArrayType) tp else origin
+    }
+  }
+
+  /** Is `tp1` a subtype of `tp2`?  */
+  def isSubType(tp1: Type, tp2: Type): Boolean = {
+    // check SI-9657 and tests/patmat/gadt.scala
+    erase(tp1) <:< erase(tp2)
+  }
+
+  def isEqualType(tp1: Type, tp2: Type): Boolean = tp1 =:= tp2
+
+  /** Parameter types of the case class type `tp`  */
+  def signature(tp: Type): List[Type] = {
+    val ktor = tp.classSymbol.primaryConstructor.info
+
+    val meth = ktor match {
+      case ktor: PolyType =>
+        ktor.instantiate(tp.classSymbol.typeParams.map(_.typeRef)).asSeenFrom(tp, tp.classSymbol)
+      case _ => ktor
+    }
+
+    // refine path-dependent type in params. refer to t9672
+    meth.firstParamTypes.map(_.asSeenFrom(tp, tp.classSymbol))
+  }
+
+  /** Decompose a type into subspaces -- assume the type can be decomposed */
+  def decompose(tp: Type): List[Space] = {
+    val children = tp.classSymbol.annotations.filter(_.symbol == ctx.definitions.ChildAnnot).map { annot =>
+      // refer to definition of Annotation.makeChild
+      annot.tree match {
+        case Apply(TypeApply(_, List(tpTree)), _) => tpTree.symbol
+      }
+    }
+
+    tp match {
+      case OrType(tp1, tp2) => List(Typ(tp1, true), Typ(tp2, true))
+      case _ if tp =:= ctx.definitions.BooleanType =>
+        List(
+          Const(Constant(true), ctx.definitions.BooleanType),
+          Const(Constant(false), ctx.definitions.BooleanType)
+        )
+      case _ if tp.classSymbol.is(Enum) =>
+        children.map(sym => Const(Constant(sym), tp))
+      case _ =>
+        val parts = children.map { sym =>
+          if (sym.is(ModuleClass))
+            sym.asClass.classInfo.selfType
+          else if (sym.info.typeParams.length > 0 || tp.isInstanceOf[TypeRef])
+            refine(tp, sym.typeRef)
+          else
+            sym.typeRef
+        } filter { tpe =>
+          // Child class may not always be subtype of parent:
+          // GADT & path-dependent types
+          tpe <:< expose(tp)
+        }
+
+        parts.map(Typ(_, true))
+    }
+  }
+
+  /** Refine tp2 based on tp1
+   *
+   *  E.g. if `tp1` is `Option[Int]`, `tp2` is `Some`, then return
+   *  `Some[Int]`.
+   *
+   *  If `tp1` is `path1.A`, `tp2` is `path2.B`, and `path1` is subtype of
+   *  `path2`, then return `path1.B`.
+   */
+  def refine(tp1: Type, tp2: Type): Type = (tp1, tp2) match {
+    case (tp1: RefinedType, _) => tp1.wrapIfMember(refine(tp1.parent, tp2))
+    case (tp1: HKApply, _) => refine(tp1.superType, tp2)
+    case (TypeRef(ref1: TypeProxy, _), tp2 @ TypeRef(ref2: TypeProxy, name)) =>
+      if (ref1.underlying <:< ref2.underlying) TypeRef(ref1, name) else tp2
+    case _ => tp2
+  }
+
+  /** Abstract sealed types, or-types, Boolean and Java enums can be decomposed */
+  def canDecompose(tp: Type): Boolean = {
+    tp.classSymbol.is(allOf(Abstract, Sealed)) ||
+      tp.classSymbol.is(allOf(Trait, Sealed)) ||
+      tp.isInstanceOf[OrType] ||
+      tp =:= ctx.definitions.BooleanType ||
+      tp.classSymbol.is(Enum)
+  }
+
+  /** Show friendly type name with current scope in mind
+   *
+   *  E.g.    C.this.B     -->  B     if current owner is C
+   *          C.this.x.T   -->  x.T   if current owner is C
+   *          X[T]         -->  X
+   *          C            -->  C     if current owner is C !!!
+   *
+   */
+  def showType(tp: Type): String = {
+    val enclosingCls = ctx.owner.enclosingClass.asClass.classInfo.symbolicTypeRef
+
+    def isOmittable(sym: Symbol) =
+      sym.isEffectiveRoot || sym.isAnonymousClass || sym.name.isReplWrapperName ||
+        ctx.definitions.UnqualifiedOwnerTypes.exists(_.symbol == sym) ||
+        sym.showFullName.startsWith("scala.") ||
+        sym == enclosingCls.typeSymbol
+
+    def refinePrefix(tp: Type): String = tp match {
+      case NoPrefix => ""
+      case tp: NamedType if isOmittable(tp.symbol) => ""
+      case tp: ThisType => refinePrefix(tp.tref)
+      case tp: RefinedType => refinePrefix(tp.parent)
+      case tp: NamedType => tp.name.show.stripSuffix("$")
+    }
+
+    def refine(tp: Type): String = tp match {
+      case tp: RefinedType => refine(tp.parent)
+      case tp: ThisType => refine(tp.tref)
+      case tp: NamedType =>
+        val pre = refinePrefix(tp.prefix)
+        if (tp.name == tpnme.higherKinds) pre
+        else if (pre.isEmpty) tp.name.show.stripSuffix("$")
+        else pre + "." + tp.name.show.stripSuffix("$")
+      case _ => tp.show.stripSuffix("$")
+    }
+
+    val text = tp.stripAnnots match {
+      case tp: OrType => showType(tp.tp1) + " | " + showType(tp.tp2)
+      case tp => refine(tp)
+    }
+
+    if (text.isEmpty) enclosingCls.show.stripSuffix("$")
+    else text
+  }
+
+  /** Display spaces */
+  def show(s: Space): String = {
+    def doShow(s: Space, mergeList: Boolean = false): String = s match {
+      case Empty => ""
+      case Const(v, _) => v.show
+      case Var(x, _) => x.show
+      case Typ(tp, decomposed) =>
+        val sym = tp.widen.classSymbol
+
+        if (sym.is(ModuleClass))
+          showType(tp)
+        else if (ctx.definitions.isTupleType(tp))
+          signature(tp).map(_ => "_").mkString("(", ", ", ")")
+        else if (sym.showFullName == "scala.collection.immutable.::")
+          if (mergeList) "_" else "List(_)"
+        else if (tp.classSymbol.is(CaseClass))
+        // use constructor syntax for case class
+          showType(tp) + signature(tp).map(_ => "_").mkString("(", ", ", ")")
+        else if (signature(tp).nonEmpty)
+          tp.classSymbol.name + signature(tp).map(_ => "_").mkString("(", ", ", ")")
+        else if (decomposed) "_: " + showType(tp)
+        else "_"
+      case Kon(tp, params) =>
+        if (ctx.definitions.isTupleType(tp))
+          "(" + params.map(doShow(_)).mkString(", ") + ")"
+        else if (tp.widen.classSymbol.showFullName == "scala.collection.immutable.::")
+          if (mergeList) params.map(doShow(_, mergeList)).mkString(", ")
+          else params.map(doShow(_, true)).filter(_ != "Nil").mkString("List(", ", ", ")")
+        else
+          showType(tp) + params.map(doShow(_)).mkString("(", ", ", ")")
+      case Or(_) =>
+        throw new Exception("incorrect flatten result " + s)
+    }
+
+    flatten(s).map(doShow(_, false)).distinct.mkString(", ")
+  }
+
+  def checkable(tree: Match): Boolean = {
+    def isCheckable(tp: Type): Boolean = tp match {
+      case AnnotatedType(tp, annot) =>
+        (ctx.definitions.UncheckedAnnot != annot.symbol) && isCheckable(tp)
+      case _ =>
+        // Possible to check everything, but be compatible with scalac by default
+        ctx.settings.YcheckAllPatmat.value ||
+          tp.typeSymbol.is(Sealed) ||
+          tp.isInstanceOf[OrType] ||
+          tp.typeSymbol == ctx.definitions.BooleanType.typeSymbol ||
+          tp.typeSymbol.is(Enum) ||
+          canDecompose(tp) ||
+          (defn.isTupleType(tp) && tp.dealias.argInfos.exists(isCheckable(_)))
+    }
+
+    val Match(sel, cases) = tree
+    isCheckable(sel.tpe.widen.deAnonymize.dealias)
+  }
+
+
+  /** Expose refined type to eliminate reference to type variables
+   *
+   *  A = B                      M { type T = A }        ~~>  M { type T = B }
+   *
+   *  A <: X :> Y                M { type T = A }        ~~>  M { type T <: X :> Y }
+   *
+   *  A <: X :> Y  B <: U :> V   M { type T <: A :> B }  ~~>  M { type T <: X :> V }
+   *
+   *  A = X  B = Y               M { type T <: A :> B }  ~~>  M { type T <: X :> Y }
+   */
+  def expose(tp: Type): Type = {
+    def follow(tp: Type, up: Boolean): Type = tp match {
+      case tp: TypeProxy =>
+        tp.underlying match {
+          case TypeBounds(lo, hi) =>
+            follow(if (up) hi else lo, up)
+          case _ =>
+            tp
+        }
+      case OrType(tp1, tp2) =>
+        OrType(follow(tp1, up), follow(tp2, up))
+      case AndType(tp1, tp2) =>
+        AndType(follow(tp1, up), follow(tp2, up))
+    }
+
+    tp match {
+      case tp: RefinedType =>
+        tp.refinedInfo match {
+          case tpa : TypeAlias =>
+            val hi = follow(tpa.alias, true)
+            val lo = follow(tpa.alias, false)
+            val refined = if (hi =:= lo)
+              tpa.derivedTypeAlias(hi)
+            else
+              tpa.derivedTypeBounds(lo, hi)
+
+            tp.derivedRefinedType(
+              expose(tp.parent),
+              tp.refinedName,
+              refined
+            )
+          case tpb @ TypeBounds(lo, hi) =>
+            tp.derivedRefinedType(
+              expose(tp.parent),
+              tp.refinedName,
+              tpb.derivedTypeBounds(follow(lo, false), follow(hi, true))
+            )
+        }
+      case _ => tp
+    }
+  }
+
+  def checkExhaustivity(_match: Match): Unit = {
+    val Match(sel, cases) = _match
+    val selTyp = sel.tpe.widen.deAnonymize.dealias
+
+
+    val patternSpace = cases.map(x => project(x.pat)).reduce((a, b) => Or(List(a, b)))
+    val uncovered = simplify(minus(Typ(selTyp, true), patternSpace))
+
+    if (uncovered != Empty) {
+      ctx.warning(
+        "match may not be exhaustive.\n" +
+        s"It would fail on the following input: " +
+        show(uncovered), _match.pos
+      )
+    }
+  }
+
+  def checkRedundancy(_match: Match): Unit = {
+    val Match(sel, cases) = _match
+    // ignore selector type for now
+    // val selTyp = sel.tpe.widen.deAnonymize.dealias
+
+    // starts from the second, the first can't be redundant
+    (1 until cases.length).foreach { i =>
+      // in redundancy check, take guard as false, take extractor as match
+      // nothing in order to soundly approximate
+      val prevs = cases.take(i).map { x =>
+        if (x.guard.isEmpty) project(x.pat, false)
+        else Empty
+      }.reduce((a, b) => Or(List(a, b)))
+
+      val curr = project(cases(i).pat)
+
+      if (isSubspace(curr, prevs)) {
+        ctx.warning("unreachable code", cases(i).body.pos)
+      }
+    }
+  }
+}
diff --git a/src/dotty/tools/dotc/typer/Namer.scala b/src/dotty/tools/dotc/typer/Namer.scala
index b8e75664c..3c0a45e94 100644
--- a/src/dotty/tools/dotc/typer/Namer.scala
+++ b/src/dotty/tools/dotc/typer/Namer.scala
@@ -414,6 +414,16 @@ class Namer { typer: Typer =>
     case mdef: DefTree =>
       val sym = enterSymbol(createSymbol(mdef))
       setDocstring(sym, stat)
+
+      // add java enum constants
+      mdef match {
+        case vdef: ValDef if (isEnumConstant(vdef)) =>
+          val enumClass = sym.owner.linkedClass
+          if (!(enumClass is Flags.Sealed)) enumClass.setFlag(Flags.AbstractSealed)
+          enumClass.addAnnotation(Annotation.makeChild(sym))
+        case _ =>
+      }
+
       ctx
     case stats: Thicket =>
       for (tree <- stats.toList) {
@@ -425,6 +435,24 @@ class Namer { typer: Typer =>
       ctx
   }
 
+  /** Determines whether this field holds an enum constant.
+    * To qualify, the following conditions must be met:
+    *  - The field's class has the ENUM flag set
+    *  - The field's class extends java.lang.Enum
+    *  - The field has the ENUM flag set
+    *  - The field is static
+    *  - The field is stable
+    */
+  def isEnumConstant(vd: ValDef)(implicit ctx: Context) = {
+    // val ownerHasEnumFlag =
+    // Necessary to check because scalac puts Java's static members into the companion object
+    // while Scala's enum constants live directly in the class.
+    // We don't check for clazz.superClass == JavaEnumClass, because this causes a illegal
+    // cyclic reference error. See the commit message for details.
+    //  if (ctx.compilationUnit.isJava) ctx.owner.companionClass.is(Enum) else ctx.owner.is(Enum)
+    vd.mods.is(allOf(Enum,  Stable, JavaStatic, JavaDefined)) // && ownerHasEnumFlag
+  }
+
   def setDocstring(sym: Symbol, tree: Tree)(implicit ctx: Context) = tree match {
     case t: MemberDef => ctx.docbase.addDocstring(sym, t.rawComment)
     case _ => ()
diff --git a/src/dotty/tools/dotc/typer/TypeAssigner.scala b/src/dotty/tools/dotc/typer/TypeAssigner.scala
index a6e2deb23..36404a68f 100644
--- a/src/dotty/tools/dotc/typer/TypeAssigner.scala
+++ b/src/dotty/tools/dotc/typer/TypeAssigner.scala
@@ -488,7 +488,7 @@ trait TypeAssigner {
     tree.withType(sym.nonMemberTermRef)
 
   def assignType(tree: untpd.Annotated, annot: Tree, arg: Tree)(implicit ctx: Context) =
-    tree.withType(AnnotatedType(arg.tpe, Annotation(annot)))
+    tree.withType(AnnotatedType(arg.tpe.widen, Annotation(annot)))
 
   def assignType(tree: untpd.PackageDef, pid: Tree)(implicit ctx: Context) =
     tree.withType(pid.symbol.valRef)
diff --git a/src/dotty/tools/dotc/typer/Typer.scala b/src/dotty/tools/dotc/typer/Typer.scala
index 52470ba87..c798a4fc1 100644
--- a/src/dotty/tools/dotc/typer/Typer.scala
+++ b/src/dotty/tools/dotc/typer/Typer.scala
@@ -741,7 +741,8 @@ class Typer extends Namer with TypeAssigner with Applications with Implicits wit
     tree.selector match {
       case EmptyTree =>
         val (protoFormals, _) = decomposeProtoFunction(pt, 1)
-        typed(desugar.makeCaseLambda(tree.cases, protoFormals.length) withPos tree.pos, pt)
+        val unchecked = pt <:< defn.PartialFunctionType
+        typed(desugar.makeCaseLambda(tree.cases, protoFormals.length, unchecked) withPos tree.pos, pt)
       case _ =>
         val sel1 = typedExpr(tree.selector)
         val selType = widenForMatchSelector(