Check that patterns in val/var defs are irrefutable

... unless followed by `: @unchecked`.

For the moment, this requires -strict mode. We plan to turn this on
by default once bootstrap compiler supports `: @unchecked` in patterns
(i.e. once this PR is part of the bootstrap compiler).

Author: odersky

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -1528,13 +1528,17 @@ object Types {
      */
     def signature(implicit ctx: Context): Signature = Signature.NotAMethod
 
-    def dropRepeatedAnnot(implicit ctx: Context): Type = this match {
-      case AnnotatedType(parent, annot) if annot.symbol eq defn.RepeatedAnnot => parent
-      case tp @ AnnotatedType(parent, annot) =>
-        tp.derivedAnnotatedType(parent.dropRepeatedAnnot, annot)
-      case tp => tp
+    /** Drop annotation of given `cls` from this type */
+    def dropAnnot(cls: Symbol)(implicit ctx: Context): Type = stripTypeVar match {
+      case self @ AnnotatedType(pre, annot) =>
+        if (annot.symbol eq cls) pre
+        else self.derivedAnnotatedType(pre.dropAnnot(cls), annot)
+      case _ =>
+        this
     }
 
+    def dropRepeatedAnnot(implicit ctx: Context): Type = dropAnnot(defn.RepeatedAnnot)
+
     def annotatedToRepeated(implicit ctx: Context): Type = this match {
       case tp @ ExprType(tp1) => tp.derivedExprType(tp1.annotatedToRepeated)
       case AnnotatedType(tp, annot) if annot matches defn.RepeatedAnnot =>

compiler/src/dotty/tools/dotc/typer/Applications.scala

@@ -1105,7 +1105,7 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
           if (selType <:< unapplyArgType) {
             unapp.println(i"case 1 $unapplyArgType ${ctx.typerState.constraint}")
             fullyDefinedType(unapplyArgType, "pattern selector", tree.span)
-            selType
+            selType.dropAnnot(defn.UncheckedAnnot) // need to drop @unchecked. Just because the selector is @unchecked, the pattern isn't.
           } else if (isSubTypeOfParent(unapplyArgType, selType)(ctx.addMode(Mode.GADTflexible))) {
             val patternBound = maximizeType(unapplyArgType, tree.span, fromScala2x)
             if (patternBound.nonEmpty) unapplyFn = addBinders(unapplyFn, patternBound)

compiler/src/dotty/tools/dotc/typer/Checking.scala

@@ -25,6 +25,7 @@ import Decorators._
 import ErrorReporting.{err, errorType}
 import config.Printers.typr
 import NameKinds.DefaultGetterName
+import Applications.unapplyArgs
 
 import collection.mutable
 import SymDenotations.{NoCompleter, NoDenotation}
@@ -596,23 +597,46 @@ trait Checking {
       ctx.error(ex"$cls cannot be instantiated since it${rstatus.msg}", pos)
   }
 
-  /** Check that pattern definition is either marked @unchecked or has a right
-   *  hand side with a type that conforms to the pattern's type.
+  /** Check that pattern `pat` is irrefutable for scrutinee tye `pt`.
+   *  This means `pat` is either marked @unchecked or `pt` conforms to the
+   *  pattern's type. If pattern is an UnApply, do the check recursively.
    */
-  def checkPatDefMatch(tree: Tree, pt: Type)(implicit ctx: Context): Unit = tree match {
-    case Match(_, CaseDef(pat, _, _) :: _)
-    if !pat.tpe.widen.hasAnnotation(defn.UncheckedAnnot) && !(pt <:< pat.tpe) =>
-      val pt1 = pt match {
-        case AnnotatedType(pt1, annot) if annot.matches(defn.UncheckedAnnot) => pt1
-        case _ => pt
+  def checkIrrefutable(pat: Tree, pt: Type)(implicit ctx: Context): Boolean = {
+    patmatch.println(i"check irrefutable $pat: ${pat.tpe} against $pt")
+
+    def check(pat: Tree, pt: Type): Boolean = {
+      if (pt <:< pat.tpe)
+        true
+      else {
+        ctx.errorOrMigrationWarning(
+          ex"""pattern's type ${pat.tpe} is more specialized than the right hand side expression's type ${pt.dropAnnot(defn.UncheckedAnnot)}
+              |
+              |If the narrowing is intentional, this can be communicated by writing `: @unchecked` after the full pattern.${err.rewriteNotice}""",
+          pat.sourcePos)
+        false
+      }
+    }
+
+    !ctx.settings.strict.value || // only in -strict mode for now since mitigations work only after this PR
+    pat.tpe.widen.hasAnnotation(defn.UncheckedAnnot) || {
+      pat match {
+        case Bind(_, pat1) =>
+          checkIrrefutable(pat1, pt)
+        case UnApply(fn, _, pats) =>
+          check(pat, pt) && {
+            val argPts = unapplyArgs(fn.tpe.finalResultType, fn, pats, pat.sourcePos)
+            pats.corresponds(argPts)(checkIrrefutable)
+          }
+        case Alternative(pats) =>
+          pats.forall(checkIrrefutable(_, pt))
+        case Typed(arg, tpt) =>
+          check(pat, pt) && checkIrrefutable(arg, pt)
+        case Ident(nme.WILDCARD) =>
+          true
+        case _ =>
+          check(pat, pt)
       }
-      ctx.errorOrMigrationWarning(
-        ex"""pattern's type ${pat.tpe.widen} is more specialized than the right hand side expression's type $pt1
-            |
-            |If the narrowing is intentional, this can be communicated by writing `: @unchecked` after the pattern.${err.rewriteNotice}""",
-        pat.sourcePos)
-      if (ctx.scala2Mode) patch(Span(pat.span.end), ": @unchecked")
-    case _ =>
+    }
   }
 
   /** Check that `path` is a legal prefix for an import or export clause */

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1036,10 +1036,15 @@ class Typer extends Namer
         if (tree.isInline) checkInInlineContext("inline match", tree.posd)
         val sel1 = typedExpr(tree.selector)
         val selType = fullyDefinedType(sel1.tpe, "pattern selector", tree.span).widen
-        val res = typedMatchFinish(tree, sel1, selType, tree.cases, pt)
-        if (tree.selector.removeAttachment(desugar.PatDefMatch).isDefined)
-          checkPatDefMatch(res, sel1.tpe)
-        res
+        val result = typedMatchFinish(tree, sel1, selType, tree.cases, pt)
+        result match {
+          case Match(sel, CaseDef(pat, _, _) :: _)
+          if (tree.selector.removeAttachment(desugar.PatDefMatch).isDefined) =>
+            if (!checkIrrefutable(pat, sel.tpe) && ctx.scala2Mode)
+              patch(Span(pat.span.end), ": @unchecked")
+          case _ =>
+        }
+        result
     }
   }
 
@@ -1820,8 +1825,11 @@ class Typer extends Namer
           }
         case _ => arg1
       }
-      val tpt = TypeTree(AnnotatedType(arg1.tpe.widenIfUnstable, Annotation(annot1)))
-      assignType(cpy.Typed(tree)(arg2, tpt), tpt)
+      val argType =
+        if (arg1.isInstanceOf[Bind]) arg1.tpe.widen // bound symbol is not accessible outside of Bind node
+        else arg1.tpe.widenIfUnstable
+      val annotatedTpt = TypeTree(AnnotatedType(argType, Annotation(annot1)))
+      assignType(cpy.Typed(tree)(arg2, annotatedTpt), annotatedTpt)
     }
   }
 

tests/neg/unchecked-patterns.scala

@@ -2,5 +2,9 @@ object Test {
   val (y1: Some[Int] @unchecked) = Some(1): Option[Int]  // OK
   val y2: Some[Int] @unchecked = Some(1): Option[Int]    // error
 
-  val x :: xs = List(1, 2, 3)  // error
+  val x :: xs = List(1, 2, 3)        // error
+  val (1, c) = (1, 2)                // error
+  val 1 *: cs = 1 *: ()              // error
+
+  val (_: Int | _: Any) = ??? : Any  // error
 }

tests/run/unchecked-patterns.scala

@@ -3,4 +3,7 @@ object Test extends App {
   val (y1: Some[Int] @unchecked) = Some(1): Option[Int]
 
   val a :: as: @unchecked = List(1, 2, 3)
+  val lst @ b :: bs: @unchecked = List(1, 2, 3)
+  val (1, c): @unchecked = (1, 2)
+  val 1 *: cs: @unchecked = 1 *: ()        // error
 }