@@ -63,7 +63,7 @@ case object Empty extends Space
6363 * @param decomposed: does the space result from decomposition? Used for pretty print
6464 *
6565 */
66- case class Typ (tp : Type , decomposed : Boolean ) extends Space
66+ case class Typ (tp : Type , decomposed : Boolean = true ) extends Space
6767
6868/** Space representing an extractor pattern */
6969case class Prod (tp : Type , unappTp : Type , unappSym : Symbol , params : List [Space ], full : Boolean ) extends Space
@@ -288,6 +288,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
288288 private val scalaNilType = ctx.requiredModuleRef(" scala.collection.immutable.Nil" )
289289 private val scalaConsType = ctx.requiredClassRef(" scala.collection.immutable.::" )
290290
291+ private val nullType = ConstantType (Constant (null ))
292+ private val nullSpace = Typ (nullType)
293+
291294 override def intersectUnrelatedAtomicTypes (tp1 : Type , tp2 : Type ) = {
292295 val and = AndType (tp1, tp2)
293296 // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
@@ -296,7 +299,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
296299
297300 debug.println(s " atomic intersection: ${and.show} = ${res}" )
298301
299- if (res) Typ (and, true ) else Empty
302+ if (! res) Empty
303+ else if (tp1.isSingleton) Typ (tp1, true )
304+ else if (tp2.isSingleton) Typ (tp2, true )
305+ else Typ (and, true )
300306 }
301307
302308 /** Whether the extractor is irrefutable */
@@ -315,6 +321,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
315321 else
316322 Typ (ConstantType (c), false )
317323 case _ : BackquotedIdent => Typ (pat.tpe, false )
324+ case Ident (nme.WILDCARD ) =>
325+ Or (Typ (pat.tpe.stripAnnots, false ) :: nullSpace :: Nil )
318326 case Ident (_) | Select (_, _) =>
319327 Typ (pat.tpe.stripAnnots, false )
320328 case Alternative (trees) => Or (trees.map(project(_)))
@@ -331,6 +339,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
331339 case Typed (pat @ UnApply (_, _, _), _) => project(pat)
332340 case Typed (expr, tpt) =>
333341 Typ (erase(expr.tpe.stripAnnots), true )
342+ case This (_) =>
343+ Typ (pat.tpe.stripAnnots, false )
344+ case EmptyTree => // default rethrow clause of try/catch, check tests/patmat/try2.scala
345+ Typ (WildcardType , false )
334346 case _ =>
335347 debug.println(s " unknown pattern: $pat" )
336348 Empty
@@ -345,8 +357,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
345357 OrType (erase(tp1), erase(tp2))
346358 case AndType (tp1, tp2) =>
347359 AndType (erase(tp1), erase(tp2))
348- case tp : RefinedType =>
349- tp.derivedRefinedType(erase(tp. parent), tp. refinedName, WildcardType )
360+ case tp @ RefinedType (parent, refinedName, _) if refinedName.isTermName => // see pos/dependent-extractors.scala
361+ tp.derivedRefinedType(erase(parent), refinedName, WildcardType )
350362 case _ => tp
351363 }
352364
@@ -370,7 +382,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
370382
371383 /** Is `tp1` a subtype of `tp2`? */
372384 def isSubType (tp1 : Type , tp2 : Type ): Boolean = {
373- val res = tp1 <:< tp2
385+ val res = (tp1 != nullType || tp2 == nullType) && tp1 <:< tp2
374386 debug.println(s " ${tp1.show} <:< ${tp2.show} = $res" )
375387 res
376388 }
@@ -543,13 +555,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
543555 case tp => tp.isSingleton
544556 }
545557
546- def superType (tp : Type ): Type = tp match {
547- case tp : TypeProxy => tp.superType
548- case OrType (tp1, tp2) => OrType (superType(tp1), superType(tp2))
549- case AndType (tp1, tp2) => AndType (superType(tp1), superType(tp2))
550- case _ => tp
551- }
552-
553558 def recur (tp : Type ): Boolean = tp.dealias match {
554559 case AndType (tp1, tp2) =>
555560 recur(tp1) && recur(tp2) && {
@@ -570,8 +575,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
570575 noClassConflict &&
571576 (! isSingleton(tp1) || tp1 <:< tp2) &&
572577 (! isSingleton(tp2) || tp2 <:< tp1) &&
573- (! bases1.exists(_ is Final ) || tp1 <:< superType( tp2) ) &&
574- (! bases2.exists(_ is Final ) || tp2 <:< superType( tp1) )
578+ (! bases1.exists(_ is Final ) || tp1 <:< tp2) &&
579+ (! bases2.exists(_ is Final ) || tp2 <:< tp1)
575580 }
576581 case OrType (tp1, tp2) =>
577582 recur(tp1) || recur(tp2)
@@ -842,7 +847,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
842847 flatten(s).map(doShow(_, false )).distinct.mkString(" , " )
843848 }
844849
845- def checkable ( tree : Match ): Boolean = {
850+ private def exhaustivityCheckable ( sel : Tree ): Boolean = {
846851 // Possible to check everything, but be compatible with scalac by default
847852 def isCheckable (tp : Type ): Boolean =
848853 ! tp.hasAnnotation(defn.UncheckedAnnot ) && {
@@ -860,26 +865,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
860865 (defn.isTupleType(tpw) && tpw.argInfos.exists(isCheckable(_)))
861866 }
862867
863- val Match (sel, cases) = tree
864868 val res = isCheckable(sel.tpe)
865- debug.println(s " checkable: ${sel.show} = $res" )
869+ debug.println(s " exhaustivity checkable: ${sel.show} = $res" )
866870 res
867871 }
868872
869873 /** Whehter counter-examples should be further checked? True for GADTs. */
870- def shouldCheckExamples (tp : Type ): Boolean = {
874+ private def shouldCheckExamples (tp : Type ): Boolean =
871875 new TypeAccumulator [Boolean ] {
872876 override def apply (b : Boolean , tp : Type ): Boolean = tp match {
873877 case tref : TypeRef if tref.symbol.is(TypeParam ) && variance != 1 => true
874878 case tp => b || foldOver(b, tp)
875879 }
876880 }.apply(false , tp)
877- }
878881
879882 def checkExhaustivity (_match : Match ): Unit = {
880883 val Match (sel, cases) = _match
881884 val selTyp = sel.tpe.widen.dealias
882885
886+ if (! exhaustivityCheckable(sel)) return
883887
884888 val patternSpace = cases.map({ x =>
885889 val space = project(x.pat)
@@ -890,36 +894,72 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
890894 val checkGADTSAT = shouldCheckExamples(selTyp)
891895
892896 val uncovered =
893- flatten(simplify(minus(Typ (selTyp, true ), patternSpace), aggressive = true ))
894- .filter(s => s != Empty && (! checkGADTSAT || satisfiable(s)))
897+ flatten(simplify(minus(Typ (selTyp, true ), patternSpace), aggressive = true )).filter { s =>
898+ s != Empty && (! checkGADTSAT || satisfiable(s))
899+ }
895900
896901 if (uncovered.nonEmpty)
897902 ctx.warning(PatternMatchExhaustivity (show(Or (uncovered))), sel.pos)
898903 }
899904
905+ private def redundancyCheckable (sel : Tree ): Boolean =
906+ ! sel.tpe.hasAnnotation(defn.UncheckedAnnot )
907+
900908 def checkRedundancy (_match : Match ): Unit = {
901909 val Match (sel, cases) = _match
902- // ignore selector type for now
903910 val selTyp = sel.tpe.widen.dealias
904911
905- (0 until cases.length).foreach { i =>
906- // in redundancy check, take guard as false in order to soundly approximate
907- val prevs =
908- if (i == 0 )
909- Empty
910- else
911- cases.take(i).map { x =>
912- if (x.guard.isEmpty) project(x.pat)
913- else Empty
914- }.reduce((a, b) => Or (List (a, b)))
912+ if (! redundancyCheckable(sel)) return
913+
914+ val targetSpace =
915+ if (selTyp.classSymbol.isPrimitiveValueClass)
916+ Typ (selTyp, true )
917+ else
918+ Or (Typ (selTyp, true ) :: nullSpace :: Nil )
915919
916- val curr = project(cases(i).pat)
920+ // in redundancy check, take guard as false in order to soundly approximate
921+ def projectPrevCases (cases : List [CaseDef ]): Space =
922+ cases.map { x =>
923+ if (x.guard.isEmpty) project(x.pat)
924+ else Empty
925+ }.reduce((a, b) => Or (List (a, b)))
917926
918- debug.println(s " ---------------reachable? ${show(curr)}" )
919- debug.println(s " prev: ${show(prevs)}" )
927+ def isNull (tree : Tree ): Boolean = tree match {
928+ case Literal (Constant (null )) => true
929+ case _ => false
930+ }
920931
921- if (isSubspace(intersect(curr, Typ (selTyp, false )), prevs)) {
922- ctx.warning(MatchCaseUnreachable (), cases(i).body.pos)
932+ (1 until cases.length).foreach { i =>
933+ val prevs = projectPrevCases(cases.take(i))
934+
935+ val pat = cases(i).pat
936+
937+ if (pat != EmptyTree ) { // rethrow case of catch uses EmptyTree
938+ val curr = project(pat)
939+
940+ debug.println(s " ---------------reachable? ${show(curr)}" )
941+ debug.println(s " prev: ${show(prevs)}" )
942+
943+ var covered = simplify(intersect(curr, targetSpace))
944+ debug.println(s " covered: $covered" )
945+
946+ // `covered == Empty` may happen for primitive types with auto-conversion
947+ // see tests/patmat/reader.scala tests/patmat/byte.scala
948+ if (covered == Empty ) covered = curr
949+
950+ if (isSubspace(covered, prevs)) {
951+ ctx.warning(MatchCaseUnreachable (), pat.pos)
952+ }
953+
954+ // if last case is `_` and only matches `null`, produce a warning
955+ if (i == cases.length - 1 && ! isNull(pat) ) {
956+ simplify(minus(covered, prevs)) match {
957+ case Typ (`nullType`, _) =>
958+ ctx.warning(MatchCaseOnlyNullWarning (), pat.pos)
959+ case _ =>
960+ }
961+
962+ }
923963 }
924964 }
925965 }
0 commit comments