Spurious is instanceOf warning

[liufengyun]

As reported by @allanrenucci in #4245, the following code will get a warning saying Some[Int] cannot be checked at runtime.

class Test {
  def test[X <: Option[Int]](x: X) = x.isInstanceOf[Some[Int]]
}

Initial diagnosis shows that type inference somehow failed to infer a <: Int, given Some[a] <: X and X <: Option[Int].

[Blaisorblade]

@liufengyun In this vein, looks like unchecked warning need to use (more of) the constraint solver, even when not handling GADTs (which we did defer):

def test1[Y <: Int, X <: Option[Y]](x: X) = x.isInstanceOf[Some[Int]] // gives unchecked warning but shouldn't

Here are a few more ones:

class Test {
  def test2(x: Any) = x.isInstanceOf[Function1[Nothing, _]] // no warning, correct
  def test3(x: Any) = x.isInstanceOf[Function1[Any, _]] // no warning, wrong (see below)
  def test3(x: Any) = x.isInstanceOf[Function1[Int, _]] // no warning, wrong  — the `_` seems to cause warnings on the whole type to be ignored, here and below
  // Let's get to trickier cases. I initially got a few of these wrong, because of how many degrees of liberty there are:
  def test4[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[Int, _]] // no warning, wrong: 
  def test5[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[Int, Unit]]  // warning, should warn because it can't check `Int`
  def test6[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[Int, Any]] // no warning, incorrect
  def test7[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[_, Unit]] // no warning, correct
}

Because Function1 is contravariant, .isInstanceOf[Function1[Any, _]] should give an unchecked warning:

scala> def test3(x: Any) = x.isInstanceOf[Function1[Any, _]]
def test3(x: Any): Boolean
scala> test3((x: Int) => x + 1)
val res0: Boolean = true
scala> ((x: Int) => x + 1): Function1[Any, Int]
1 |((x: Int) => x + 1): Function1[Any, Int]
  |                  ^
  |                  found:    Int => Int
  |                  required: Any => Int
  |
scala> def test4[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[Int, _]] // no warning, wrong:
def test4[Y <: Int, X <: Y => Unit](x: X): Boolean
scala> test4[Y = Nothing]((x: String) => x)
val res0: Boolean = true
scala> def test6[Y <: Int, X <: Function1[Y, Unit]](x: X) = x.isInstanceOf[Function1[Int, Any]]
def test6[Y <: Int, X <: Y => Unit](x: X): Boolean
scala> test6[Y = Nothing, X = Function1[String, Unit]]((x: String) => x)
val res1: Boolean = true

[Blaisorblade]

Initial diagnosis shows that type inference somehow failed to infer a <: Int, given Some[a] <: X and X <: Some[Int].

But X <: Some[Int] should be X <: Option[Int], since that's what we know, no?

[liufengyun]

But X <: Some[Int] should be X <: Option[Int], since that's what we know, no?

Yes, good catch, I updated the description.