diff options
author | Paul Phillips <paulp@improving.org> | 2012-09-27 06:41:17 -0700 |
---|---|---|
committer | Paul Phillips <paulp@improving.org> | 2012-09-27 09:24:04 -0700 |
commit | 96d4a8646b1962fac2f2fc443b56c6619221b43c (patch) | |
tree | bd39f411275452bb5db2335da966ac8042cd504f | |
parent | 17b409b7832f541e3d52d2776c8ff3c47574ae0f (diff) | |
download | scala-96d4a8646b1962fac2f2fc443b56c6619221b43c.tar.gz scala-96d4a8646b1962fac2f2fc443b56c6619221b43c.tar.bz2 scala-96d4a8646b1962fac2f2fc443b56c6619221b43c.zip |
Nailed down the "impossible match" logic.
I will again defer to a comment.
/** Given classes A and B, can it be shown that nothing which is
* an A will ever be a subclass of something which is a B? This
* entails not only showing that !(A isSubClass B) but that the
* same is true of all their subclasses. Restated for symmetry:
* the same value cannot be a member of both A and B.
*
* 1) A must not be a subclass of B, nor B of A (the trivial check)
* 2) One of A or B must be completely knowable (see isKnowable)
* 3) Assuming A is knowable, the proposition is true if
* !(A' isSubClass B) for all A', where A' is a subclass of A.
*
* Due to symmetry, the last condition applies as well in reverse.
*/
-rw-r--r-- | src/compiler/scala/tools/nsc/typechecker/Checkable.scala | 77 | ||||
-rw-r--r-- | test/files/neg/patmat-type-check.check | 10 | ||||
-rw-r--r-- | test/files/neg/t1872.check | 4 | ||||
-rw-r--r-- | test/files/neg/unchecked-abstract.check | 25 | ||||
-rw-r--r-- | test/files/neg/unchecked-abstract.flags | 1 | ||||
-rw-r--r-- | test/files/neg/unchecked-abstract.scala | 93 | ||||
-rw-r--r-- | test/files/neg/unchecked-impossible.check | 4 | ||||
-rw-r--r-- | test/files/neg/unchecked-impossible.flags | 1 | ||||
-rw-r--r-- | test/files/neg/unchecked-impossible.scala | 16 | ||||
-rw-r--r-- | test/files/neg/unchecked-knowable.check | 4 | ||||
-rw-r--r-- | test/files/neg/unchecked-knowable.flags | 1 | ||||
-rw-r--r-- | test/files/neg/unchecked-knowable.scala | 20 | ||||
-rw-r--r-- | test/files/neg/unchecked2.check | 12 |
13 files changed, 234 insertions, 34 deletions
diff --git a/src/compiler/scala/tools/nsc/typechecker/Checkable.scala b/src/compiler/scala/tools/nsc/typechecker/Checkable.scala index 3a1803038c..2be08d12ea 100644 --- a/src/compiler/scala/tools/nsc/typechecker/Checkable.scala +++ b/src/compiler/scala/tools/nsc/typechecker/Checkable.scala @@ -23,8 +23,8 @@ import Checkability._ * [P3] X <: P if some runtime test is true * [P4] X cannot be checked against P * - * The first two cases correspond to those when there is enough static - * information to say X <: P or that !(X <: P) for all X and P. + * The first two cases correspond to those when there is enough + * static information to say X <: P or that (x ∈ X) ⇒ (x ∉ P). * The fourth case includes unknown abstract types or structural * refinements appearing within a pattern. * @@ -51,6 +51,7 @@ trait Checkable { import global._ import definitions._ + import CheckabilityChecker.{ isNeverSubType, isNeverSubClass } /** The applied type of class 'to' after inferring anything * possible from the knowledge that 'to' must also be of the @@ -100,15 +101,16 @@ trait Checkable { def Xsym = X.typeSymbol def Psym = P.typeSymbol def XR = propagateKnownTypes(X, Psym) + // sadly the spec says (new java.lang.Boolean(true)).isInstanceOf[scala.Boolean] def P1 = X matchesPattern P - def P2 = CheckabilityChecker.isNeverSubType(X, P) + def P2 = !Psym.isPrimitiveValueClass && isNeverSubType(X, P) def P3 = Psym.isClass && (XR matchesPattern P) def P4 = !(P1 || P2 || P3) def summaryString = f""" |Checking checkability of (x: $X) against pattern $P |[P1] $P1%-6s X <: P // $X <: $P - |[P2] $P2%-6s X !<: P // $X !<: $P for all X, P + |[P2] $P2%-6s x ∉ P // (x ∈ $X) ⇒ (x ∉ $P) |[P3] $P3%-6s XR <: P // $XR <: $P |[P4] $P4%-6s None of the above // !(P1 || P2 || P3) """.stripMargin.trim @@ -137,7 +139,8 @@ trait Checkable { opt getOrElse NoType } - def neverMatches = result == StaticallyFalse + def neverSubClass = isNeverSubClass(Xsym, Psym) + def neverMatches = result == StaticallyFalse def isUncheckable = result == Uncheckable def uncheckableMessage = uncheckableType match { case NoType => "something" @@ -150,28 +153,42 @@ trait Checkable { /** X, P, [P1], etc. are all explained at the top of the file. */ private object CheckabilityChecker { - /** Given classes A and B, can it be shown A is never a subclass of B? + /** A knowable class is one which is either effectively final + * itself, or sealed with only knowable children. */ - private def isNeverSubClass(sym1: Symbol, sym2: Symbol) = /*logResult(s"isNeverSubClass($sym1, $sym2)")*/( + def isKnowable(sym: Symbol): Boolean = /*logResult(s"isKnowable($sym)")*/( + sym.initialize.isEffectivelyFinal // pesky .initialize requirement, or we receive lies about isSealed + || sym.isSealed && (sym.children forall isKnowable) + ) + def knownSubclasses(sym: Symbol): List[Symbol] = /*logResult(s"knownSubclasses($sym)")*/(sym :: { + if (sym.isSealed) sym.children.toList flatMap knownSubclasses + else Nil + }) + def excludable(s1: Symbol, s2: Symbol) = /*logResult(s"excludable($s1, $s2)")*/( + isKnowable(s1) + && !(s2 isSubClass s1) + && knownSubclasses(s1).forall(child => !(child isSubClass s2)) + ) + + /** Given classes A and B, can it be shown that nothing which is + * an A will ever be a subclass of something which is a B? This + * entails not only showing that !(A isSubClass B) but that the + * same is true of all their subclasses. Restated for symmetry: + * the same value cannot be a member of both A and B. + * + * 1) A must not be a subclass of B, nor B of A (the trivial check) + * 2) One of A or B must be completely knowable (see isKnowable) + * 3) Assuming A is knowable, the proposition is true if + * !(A' isSubClass B) for all A', where A' is a subclass of A. + * + * Due to symmetry, the last condition applies as well in reverse. + */ + def isNeverSubClass(sym1: Symbol, sym2: Symbol) = /*logResult(s"isNeverSubClass($sym1, $sym2)")*/( sym1.isClass && sym2.isClass - && !(sym1 isSubClass sym2) - && ( - // If B is final, A can only be a subclass of B if it is B itself. - // Therefore, A <: B is impossible unless B <: A. - if (sym2.isEffectivelyFinal) - !(sym2 isSubClass sym1) - // If A is final but B is not, a subclass relationship can - // still be ruled out if B is sealed and A is not a subclass of - // any of B's sealed children. - else ( - sym1.isEffectivelyFinal - && sym2.isSealed - && sym2.children.forall(child => !(sym1 isSubClass child)) - ) - ) + && (excludable(sym1, sym2) || excludable(sym2, sym1)) ) - private def isNeverSubArgs(tps1: List[Type], tps2: List[Type], tparams: List[Symbol]): Boolean = /*logResult(s"isNeverSubArgs($tps1, $tps2, $tparams)")*/{ + private def isNeverSubArgs(tps1: List[Type], tps2: List[Type], tparams: List[Symbol]): Boolean = /*logResult(s"isNeverSubArgs($tps1, $tps2, $tparams)")*/ { def isNeverSubArg(t1: Type, t2: Type, variance: Int) = { if (variance > 0) isNeverSubType(t2, t1) else if (variance < 0) isNeverSubType(t1, t2) @@ -189,7 +206,7 @@ trait Checkable { false } // Important to dealias at any entry point (this is the only one at this writing.) - private def isNeverSubType(tp1: Type, tp2: Type): Boolean = /*logResult(s"isNeverSubType($tp1, $tp2)")*/((tp1.dealias, tp2.dealias) match { + def isNeverSubType(tp1: Type, tp2: Type): Boolean = /*logResult(s"isNeverSubType($tp1, $tp2)")*/((tp1.dealias, tp2.dealias) match { case (TypeRef(_, sym1, args1), TypeRef(_, sym2, args2)) => isNeverSubClass(sym1, sym2) || { (sym1 isSubClass sym2) && { @@ -208,11 +225,13 @@ trait Checkable { * Kind of stuck right now because they just pass us the one tree. * TODO: Eliminate inPattern, canRemedy, which have no place here. */ - def checkCheckable(tree: Tree, P0: Type, X: Type, inPattern: Boolean, canRemedy: Boolean = false) { + def checkCheckable(tree: Tree, P0: Type, X0: Type, inPattern: Boolean, canRemedy: Boolean = false) { def where = if (inPattern) "pattern " else "" // singleton types not considered here val P = P0.widen + val X = X0.widen + P match { // Prohibit top-level type tests for these, but they are ok nested (e.g. case Foldable[Nothing] => ... ) case TypeRef(_, NothingClass | NullClass | AnyValClass, _) => @@ -221,10 +240,12 @@ trait Checkable { case TypeRef(_, sym, _) if sym.isAbstractType && canRemedy => ; case _ => - val checker = new CheckabilityChecker(X.widen, P) + val checker = new CheckabilityChecker(X, P) log(checker.summaryString) - if (checker.neverMatches) - getContext.unit.warning(tree.pos, s"fruitless type test: a $X can never be a $P (but still might match its erasure)") + if (checker.neverMatches) { + val addendum = if (checker.neverSubClass) "" else " (but still might match its erasure)" + getContext.unit.warning(tree.pos, s"fruitless type test: a value of type $X cannot also be a $P$addendum") + } else if (checker.isUncheckable) { val msg = ( if (checker.uncheckableType =:= P) s"abstract type $where$P" diff --git a/test/files/neg/patmat-type-check.check b/test/files/neg/patmat-type-check.check index e045841ce1..721217c314 100644 --- a/test/files/neg/patmat-type-check.check +++ b/test/files/neg/patmat-type-check.check @@ -1,3 +1,12 @@ +patmat-type-check.scala:11: warning: fruitless type test: a value of type Test.Bop4[T] cannot also be a Seq[A] + def s3[T](x: Bop4[T]) = x match { case Seq('b', 'o', 'b') => true } + ^ +patmat-type-check.scala:15: warning: fruitless type test: a value of type Test.Bop5[_$1,T1,T2] cannot also be a Seq[A] + def s4[T1, T2](x: Bop5[_, T1, T2]) = x match { case Seq('b', 'o', 'b') => true } + ^ +patmat-type-check.scala:19: warning: fruitless type test: a value of type Test.Bop3[T] cannot also be a Seq[A] + def f4[T](x: Bop3[T]) = x match { case Seq('b', 'o', 'b') => true } + ^ patmat-type-check.scala:22: error: scrutinee is incompatible with pattern type; found : Seq[A] required: String @@ -18,4 +27,5 @@ patmat-type-check.scala:30: error: scrutinee is incompatible with pattern type; required: Test.Bop3[Char] def f4[T](x: Bop3[Char]) = x match { case Seq('b', 'o', 'b') => true } // fail ^ +three warnings found four errors found diff --git a/test/files/neg/t1872.check b/test/files/neg/t1872.check index ef84ef79e0..c5dc2a8080 100644 --- a/test/files/neg/t1872.check +++ b/test/files/neg/t1872.check @@ -1,4 +1,8 @@ +t1872.scala:3: warning: fruitless type test: a value of type Int cannot also be a scala.util.Random + def f(x: Int) = x.isInstanceOf[util.Random] + ^ t1872.scala:3: error: isInstanceOf cannot test if value types are references. def f(x: Int) = x.isInstanceOf[util.Random] ^ +one warning found one error found diff --git a/test/files/neg/unchecked-abstract.check b/test/files/neg/unchecked-abstract.check new file mode 100644 index 0000000000..dc7a8d93d0 --- /dev/null +++ b/test/files/neg/unchecked-abstract.check @@ -0,0 +1,25 @@ +unchecked-abstract.scala:16: error: abstract type H in type Con[M.this.H] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Con[H]]) + ^ +unchecked-abstract.scala:21: error: abstract type H in type Con[M.this.H] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Con[H]]) + ^ +unchecked-abstract.scala:27: error: abstract type T in type Inv[M.this.T] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[T]]) + ^ +unchecked-abstract.scala:28: error: abstract type L in type Inv[M.this.L] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[L]]) + ^ +unchecked-abstract.scala:31: error: abstract type H in type Inv[M.this.H] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[H]]) + ^ +unchecked-abstract.scala:33: error: abstract type L in type Inv[M.this.L] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[L]]) + ^ +unchecked-abstract.scala:36: error: abstract type H in type Inv[M.this.H] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[H]]) + ^ +unchecked-abstract.scala:37: error: abstract type T in type Inv[M.this.T] is unchecked since it is eliminated by erasure + /* warn */ println(x.isInstanceOf[Inv[T]]) + ^ +8 errors found diff --git a/test/files/neg/unchecked-abstract.flags b/test/files/neg/unchecked-abstract.flags new file mode 100644 index 0000000000..85d8eb2ba2 --- /dev/null +++ b/test/files/neg/unchecked-abstract.flags @@ -0,0 +1 @@ +-Xfatal-warnings diff --git a/test/files/neg/unchecked-abstract.scala b/test/files/neg/unchecked-abstract.scala new file mode 100644 index 0000000000..5b915755f4 --- /dev/null +++ b/test/files/neg/unchecked-abstract.scala @@ -0,0 +1,93 @@ +trait Con[-X] +trait Inv[X] +trait Cov[+X] + +abstract class M { + type H + type L <: H + type T >: L <: H + + def h1(x: Con[H]) = { + /* nowarn */ println(x.isInstanceOf[Con[H]]) + /* nowarn */ println(x.isInstanceOf[Con[T]]) + /* nowarn */ println(x.isInstanceOf[Con[L]]) + } + def h2(x: Con[T]) = { + /* warn */ println(x.isInstanceOf[Con[H]]) + /* nowarn */ println(x.isInstanceOf[Con[T]]) + /* nowarn */ println(x.isInstanceOf[Con[L]]) + } + def h3(x: Con[L]) = { + /* warn */ println(x.isInstanceOf[Con[H]]) + /* warn */ println(x.isInstanceOf[Con[T]]) + /* nowarn */ println(x.isInstanceOf[Con[L]]) + } + def h4(x: Inv[H]) = { + /* nowarn */ println(x.isInstanceOf[Inv[H]]) + /* warn */ println(x.isInstanceOf[Inv[T]]) + /* warn */ println(x.isInstanceOf[Inv[L]]) + } + def h5(x: Inv[T]) = { + /* warn */ println(x.isInstanceOf[Inv[H]]) + /* nowarn */ println(x.isInstanceOf[Inv[T]]) + /* warn */ println(x.isInstanceOf[Inv[L]]) + } + def h6(x: Inv[L]) = { + /* warn */ println(x.isInstanceOf[Inv[H]]) + /* warn */ println(x.isInstanceOf[Inv[T]]) + /* nowarn */ println(x.isInstanceOf[Inv[L]]) + } + def h7(x: Cov[H]) = { + /* nowarn */ println(x.isInstanceOf[Cov[H]]) + /* warn */ println(x.isInstanceOf[Cov[T]]) + /* warn */ println(x.isInstanceOf[Cov[L]]) + } + def h8(x: Cov[T]) = { + /* nowarn */ println(x.isInstanceOf[Cov[H]]) + /* nowarn */ println(x.isInstanceOf[Cov[T]]) + /* warn */ println(x.isInstanceOf[Cov[L]]) + } + def h9(x: Cov[L]) = { + /* nowarn */ println(x.isInstanceOf[Cov[H]]) + /* nowarn */ println(x.isInstanceOf[Cov[T]]) + /* nowarn */ println(x.isInstanceOf[Cov[L]]) + } +} + +object Test extends M { + type H = Any + type T = Int + type L = Nothing + + val conh = new Con[H] { } + val cont = new Con[T] { } + val conl = new Con[L] { } + + val invh = new Inv[H] { } + val invt = new Inv[T] { } + val invl = new Inv[L] { } + + val covh = new Cov[H] { } + val covt = new Cov[T] { } + val covl = new Cov[L] { } + + def main(args: Array[String]): Unit = { + h1(conh) + h2(conh) + h2(cont) + h3(conh) + h3(cont) + h3(conl) + + h4(invh) + h5(invt) + h6(invl) + + h7(covh) + h7(covt) + h7(covl) + h8(covt) + h8(covl) + h9(covl) + } +} diff --git a/test/files/neg/unchecked-impossible.check b/test/files/neg/unchecked-impossible.check new file mode 100644 index 0000000000..0ab371dbaa --- /dev/null +++ b/test/files/neg/unchecked-impossible.check @@ -0,0 +1,4 @@ +unchecked-impossible.scala:5: error: fruitless type test: a value of type T2[Int,Int] cannot also be a Seq[A] + case Seq(x) => + ^ +one error found diff --git a/test/files/neg/unchecked-impossible.flags b/test/files/neg/unchecked-impossible.flags new file mode 100644 index 0000000000..85d8eb2ba2 --- /dev/null +++ b/test/files/neg/unchecked-impossible.flags @@ -0,0 +1 @@ +-Xfatal-warnings diff --git a/test/files/neg/unchecked-impossible.scala b/test/files/neg/unchecked-impossible.scala new file mode 100644 index 0000000000..985a2d0b08 --- /dev/null +++ b/test/files/neg/unchecked-impossible.scala @@ -0,0 +1,16 @@ +final case class T2[+A, +B](a: A, b: B) + +class A { + def f1 = T2(1, 2) match { + case Seq(x) => + case _ => + } + def f2 = T2(1, 2) match { + case _: T2[Int, Int] => /* nowarn */ + case _ => + } + def f3 = T2(1, 2) match { + case _: T2[_, Int] => /* nowarn */ + case _ => + } +} diff --git a/test/files/neg/unchecked-knowable.check b/test/files/neg/unchecked-knowable.check new file mode 100644 index 0000000000..3a6ef994b5 --- /dev/null +++ b/test/files/neg/unchecked-knowable.check @@ -0,0 +1,4 @@ +unchecked-knowable.scala:17: error: fruitless type test: a value of type Bippy cannot also be a A1 + /* warn */ (new Bippy).isInstanceOf[A1] + ^ +one error found diff --git a/test/files/neg/unchecked-knowable.flags b/test/files/neg/unchecked-knowable.flags new file mode 100644 index 0000000000..85d8eb2ba2 --- /dev/null +++ b/test/files/neg/unchecked-knowable.flags @@ -0,0 +1 @@ +-Xfatal-warnings diff --git a/test/files/neg/unchecked-knowable.scala b/test/files/neg/unchecked-knowable.scala new file mode 100644 index 0000000000..667b47f504 --- /dev/null +++ b/test/files/neg/unchecked-knowable.scala @@ -0,0 +1,20 @@ +/** Knowable - only final leaves */ +sealed abstract class A1 +sealed abstract class A2 extends A1 +final class A3 extends A1 +final class A4 extends A2 + +/** Unknowable */ +sealed abstract class B1 +sealed abstract class B2 extends B1 +final class B3 extends B1 +trait B4 extends B2 + +class Bippy +trait Dingus + +class A { + /* warn */ (new Bippy).isInstanceOf[A1] + /* nowarn */ (new Bippy).isInstanceOf[B1] + /* nowarn */ ((new Bippy): Any).isInstanceOf[A1] +} diff --git a/test/files/neg/unchecked2.check b/test/files/neg/unchecked2.check index b4a14358c7..68fdfa82ac 100644 --- a/test/files/neg/unchecked2.check +++ b/test/files/neg/unchecked2.check @@ -1,22 +1,22 @@ -unchecked2.scala:4: error: fruitless type test: a Some[List[Int]] can never be a Option[List[String]] (but still might match its erasure) +unchecked2.scala:4: error: fruitless type test: a value of type Some[List[Int]] cannot also be a Option[List[String]] (but still might match its erasure) /* warn */ Some(List(1)).isInstanceOf[Option[List[String]]] ^ unchecked2.scala:5: error: non-variable type argument Option[_] in type Option[Option[_]] is unchecked since it is eliminated by erasure /* warn */ Some(123).isInstanceOf[Option[Option[_]]] ^ -unchecked2.scala:6: error: fruitless type test: a Some[Int] can never be a Option[String] (but still might match its erasure) +unchecked2.scala:6: error: fruitless type test: a value of type Some[Int] cannot also be a Option[String] (but still might match its erasure) /* warn */ Some(123).isInstanceOf[Option[String]] ^ -unchecked2.scala:7: error: fruitless type test: a Some[Int] can never be a Option[List[String]] (but still might match its erasure) +unchecked2.scala:7: error: fruitless type test: a value of type Some[Int] cannot also be a Option[List[String]] (but still might match its erasure) /* warn */ Some(123).isInstanceOf[Option[List[String]]] ^ -unchecked2.scala:8: error: fruitless type test: a Some[Int] can never be a Option[List[Int => String]] (but still might match its erasure) +unchecked2.scala:8: error: fruitless type test: a value of type Some[Int] cannot also be a Option[List[Int => String]] (but still might match its erasure) /* warn */ Some(123).isInstanceOf[Option[List[Int => String]]] ^ -unchecked2.scala:9: error: fruitless type test: a Some[Int] can never be a Option[(String, Double)] (but still might match its erasure) +unchecked2.scala:9: error: fruitless type test: a value of type Some[Int] cannot also be a Option[(String, Double)] (but still might match its erasure) /* warn */ Some(123).isInstanceOf[Option[(String, Double)]] ^ -unchecked2.scala:10: error: fruitless type test: a Some[Int] can never be a Option[String => Double] (but still might match its erasure) +unchecked2.scala:10: error: fruitless type test: a value of type Some[Int] cannot also be a Option[String => Double] (but still might match its erasure) /* warn */ Some(123).isInstanceOf[Option[String => Double]] ^ unchecked2.scala:14: error: non-variable type argument List[String] in type Option[List[String]] is unchecked since it is eliminated by erasure |