Fix #3324: add `isInstanceOf` check #4045

liufengyun · 2018-02-27T14:38:01Z

Fix #3324: add isInstanceOf check.

This specification is different from the scalac compiler implementation. I hope it's more understandable.

liufengyun · 2018-03-05T16:16:16Z

tests/neg-custom-args/isInstanceOf/Result.scala

+  enum Result[+T, +E] {
+    case OK [T](x: T) extends Result[T, Nothing]
+    case Err[E](e: E) extends Result[Nothing, E]
+  }


Add a comment why this test?

liufengyun · 2018-03-05T16:17:05Z

compiler/src/dotty/tools/dotc/transform/SyntheticMethods.scala

@@ -152,7 +153,7 @@ class SyntheticMethods(thisPhase: DenotTransformer) {
     *  def equals(that: Any): Boolean =
     *    (this eq that) || {
     *      that match {
-     *        case x$0 @ (_: C) => this.x == this$0.x && this.y == x$0.y
+     *        case x$0 @ (_: C @unchecked) => this.x == this$0.x && this.y == x$0.y


Add comment warning maintainers this code is fragile, since unchecked might hide type errors...

Blaisorblade · 2018-03-06T13:21:20Z

tests/neg-custom-args/isInstanceOf/enum-approx2.scala

+  def eval[T](e: Exp[T]) = e match {
+    case Fun(x: Fun[Int, Double]) => ???          // error
+    case Fun(x: Exp[Int => String]) => ???        // error
+  }


Looking at this with @liufengyun, we realize this complication has to do with compiling a match like:

def eval[T](e: Exp[T]) = e match { case f @ Fun(x: Fun[Int, Double]) => ??? }

The correct desugaring is a bit surprising to me, because we want to ensure f: Fun[Int, Double], but this is not justified where f is bound but only after the inner match.

def eval[T](e: Exp[T]) = e match { case f1: Fun[a1, b1] => f1.f match { case f2: Fun[Int, Double] => //***Here*** we learn that a1 = Int and b1 = Double //So only ***here*** we can bind `f` with the correct type. val f: Fun[Int, Double] = f1 } }

We suspect the typechecker currently refines type variables a1 and b1 too soon, which has been fine until now, but strictly speaking means (I think) the current typechecker output is not well-typed in a sound typesystem.

EDIT: as usual, up to misunderstandings.

smarter · 2018-03-06T14:43:22Z

Haven't looked at what this PR does in details, but one thing to note is that right now the GADT bounds are stored separately in typer and not preserved in subsequent phases. There used to be code in PostTyper to do this that got removed (I don't know why), you may need to bring it back: eb21d24#diff-21d08d8a179119a483e67f9f0f994e99L62

liufengyun · 2018-03-07T08:55:20Z

Thanks for the tip @smarter . Upon reflection, it seems to correctly handle GADTs in patterns, we need some context-sensitive typing, the type of a term name or type name could be refined in a context depending on type test. The refinement should be in sync with the type test.

In TypeScript, there's a related feature called type guards, which can refine the type of a variable in a context:

// Type is 'SpaceRepeatingPadder | StringPadder'
let padder: Padder = getRandomPadder();

if (padder instanceof SpaceRepeatingPadder) {
    padder; // type narrowed to 'SpaceRepeatingPadder'
}
if (padder instanceof StringPadder) {
    padder; // type narrowed to 'StringPadder'
}

I've no idea how this works in theory. In our case, we need to refine the type of types names (as @Blaisorblade points out in the example) instead of / (in addition to) term names.

liufengyun · 2018-03-07T12:37:48Z

An example related to GADT typing of Dotty trees:

class Test {
  trait Type
  class Tree[-T]
  case class Ident[-T](x: String) extends Tree[T]

  trait Base extends Tree[Type]
  class DummyIdent extends Ident[Null]("hello") with Base

  def foo(tree: Tree[Type]): Ident[Type] = tree match {
    case id @ Ident(x) => id                   // should we emit warnings here?
  }

  foo(new DummyIdent)
}

Blaisorblade · 2018-03-07T13:11:17Z

@liufengyun DummyIdent should be forbidden by the PR for #3989 — as I said, I'd wait for that PR before trying to get right variant GADTs.

I've no idea how this works in theory

TypeScript has flow-sensitive typing; in Haskell's internal language used for GADTs, IIUC, matches produce evidence that some type is equal or smaller than another (=:= and <:<). Doing that properly would require adapting the theory though, which isn't an immediate step.

Blaisorblade · 2018-03-07T16:42:55Z

I just confirmed that scalac's established behavior with isInstanceOf and ClassTag is likely incorrect:

https://gist.github.com/Blaisorblade/a0eebb6a4f35344e48c4c60dc2a14ce6

Blaisorblade · 2018-03-08T01:47:30Z

And people pointed me to scala/bug#9565 and https://groups.google.com/d/msg/scala-internals/KYZACmy8_Qg/Wh1T0coqBYYJ.

For this PR, I suspect ClassTag-based isInstanceOf should just warn iff we are not in Scala2 mode (to be compatible in Scala2 mode and sound in Dotty mode), since picking a fix will take a while.

liufengyun · 2018-03-08T16:55:12Z

@Blaisorblade If we always warn for a ClassTag-based test like x: T, it makes this feature not usable. (BTW, ClassTag will not generate isInstanceOf, but just a call to uanpply on the evidence)

I think soundness is not the only concern here. Giving that it happens rarely, I think we should optimize for usability as Scalac does.

smarter · 2018-03-08T17:05:54Z

@Blaisorblade If we always warn for a ClassTag-based test like x: T, it makes this feature not usable.

It's not great, but one can always use @unchecked to suppress the warning.

Blaisorblade · 2018-03-08T20:11:54Z

tests/neg-custom-args/isInstanceOf/3324g.scala

@@ -12,7 +12,7 @@ class Test {
  }

  def quux[T](a: A[T]): Unit = a match {
-    case _: B[T] => // error
+    case _: B[T] => // err-or: cannot handle this for now


maybe replace err-or with should be an error or such?

liufengyun · 2018-03-09T13:00:56Z

For (x: X).isInstanceOf[P], scalac emits an unchecked warning when:

We designate another type, XR, which is essentially the intersection of X and |P|, where |P| is the erasure of P. If XR <: P, then no warning is emitted.

ref: https://github.com/scala/scala/blob/94cee79eb63b4449d21dc74cb9175d6412cc8a55/src/compiler/scala/tools/nsc/typechecker/Checkable.scala#L12-L64

However, the above specification cannot explain why we should not produce a warning in the following case:

sealed trait A[T]
class B[T] extends A[T]

def g(x: A[Int]) = x match { case _: B[Int] => }

The specification in this PR can be seen as making the obscurity in Scalac specification clear by resorting to type inference. Otherwise, the two are equivalent in spirit.

allanrenucci · 2018-03-22T09:38:02Z

test performance please

dottybot · 2018-03-22T09:38:55Z

performance test scheduled: 1 job(s) in queue, 0 running.

allanrenucci

Otherwise LGTM

allanrenucci · 2018-03-22T09:34:42Z

compiler/src/dotty/tools/dotc/transform/IsInstanceOfChecker.scala

+      case fn: Select if fn.symbol == defn.Any_typeTest =>
+        ensureCheckable(fn.qualifier, tree.args.head)
+      case fn: Select if fn.symbol == defn.Any_isInstanceOf =>
+        ensureCheckable(fn.qualifier, tree.args.head)


Why not merge the first two cases:

case fn: Select if fn.symbol == defn.Any_typeTest || fn.symbol == defn.Any_isInstanceOf => ensureCheckable(fn.qualifier, tree.args.head)

allanrenucci · 2018-03-22T10:00:25Z

compiler/src/dotty/tools/dotc/transform/IsInstanceOfChecker.scala

+    def replaceP(implicit ctx: Context) = new TypeMap {
+      def apply(tp: Type) = tp match {
+        case tref: TypeRef
+        if !tref.typeSymbol.isClass && tref.symbol.is(Case) => WildcardType


Can you explain what this test does?

allanrenucci · 2018-03-22T10:05:00Z

compiler/src/dotty/tools/dotc/transform/IsInstanceOfChecker.scala

+   *  1. if `X <:< P`, TRUE
+   *  2. if `P` is a singleton type, TRUE
+   *  3. if `P` refers to an abstract type member or type parameter, FALSE
+   *  4. if `P = Array[T]`, checkable(E, T) where `E` is the element type of `X`, defaults to `Any`.


Can you explain why there is a special treatment for Array?

Thanks @allanrenucci for the helpful feedback, I've addressed them in the latest commit.

For Array, we need a special treatment, because JVM carries type information of array elements, it's possible to test the element type at runtime [1]:

scala> Array(1, 2, 3).getClass res2: Class[_ <: Array[Int]] = class [I // where the string "[I" is the run-time type signature for the class // object "array with component type int".

[1]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-10.html

allanrenucci · 2018-03-22T10:14:29Z

compiler/src/dotty/tools/dotc/transform/IsInstanceOfChecker.scala

+   *     (a) replace `Ts` with fresh type variables `Xs`
+   *     (b) constrain `Xs` with `pre.F[Xs] <:< X`
+   *     (c) instantiate Xs and check `pre.F[Xs] <:< P`
+   *  6. if `P = T1 | T2` or `P = T1 & T2`, checkable(X, T1) && checkable(X, T2).


Can you add a test for & types. For example:

trait Marker def foo[T](x: T) = x match { case _: T & Marker => // no warning // case _: T with Marker => // scalac emits a warning case _ => }

Scalac emits a warning but I believe it is erroneous.
Use case:

def foo[T](xs: List[T]): List[T] = xs.collect { case x: T with Marker => x }

allanrenucci · 2018-03-23T16:32:49Z

compiler/src/dotty/tools/dotc/transform/IsInstanceOfChecker.scala

+    def replaceX(implicit ctx: Context) = new TypeMap {
+      def apply(tp: Type) = tp match {
+        case tref: TypeRef
+        if !tref.typeSymbol.isClass && tref.symbol.is(Case) =>


Could be isPatternTypeSymbol(tref.typeSymbol)

allanrenucci · 2018-03-23T16:33:40Z

tests/neg-custom-args/isInstanceOf/3324h.scala

+  trait Marker
+  def foo[T](x: T) = x match {
+    case _: (T & Marker)       => // no warning
+    // case _: T with Marker => // scalac emits a warning


This should probably tested too

allanrenucci · 2018-03-23T16:35:17Z

tests/neg-custom-args/isInstanceOf/3324h.scala

+    case _ =>
+  }
+
+  def bar(x: Any) = x.isInstanceOf[List[String]]  // error


You could remove this line and it pos test. This already tested in i3324.scala

Thanks for the catch. This line is intended to make the test a neg test. Make it a pos test will not work, as we want to check warnings here, -fatal-warning is required. And it's nice to have all related tests of a feature under one folder.

allanrenucci · 2018-03-23T16:36:00Z

tests/neg-custom-args/isInstanceOf/3324c.scala

+
+  def g(x: A[Int]) = x match { case _: B[Int] => }
+
+  def foo(x: Any) = x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

allanrenucci · 2018-03-23T16:36:06Z

tests/neg-custom-args/isInstanceOf/3324d.scala

+  }
+
+  def foo(x: Any): Boolean =
+    x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

allanrenucci · 2018-03-23T16:36:38Z

tests/neg-custom-args/isInstanceOf/Result.scala

+  }
+
+  def foo(x: Any): Boolean =
+    x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

allanrenucci · 2018-03-23T16:37:03Z

tests/neg-custom-args/isInstanceOf/Result.scala

+  // test parametric case classes, which synthesis `canEqual` and `equals`
+  enum Result[+T, +E] {
+    case OK [T](x: T) extends Result[T, Nothing]
+    case Err[E](e: E) extends Result[Nothing, E]


What is tested here? There is no pattern match

Here the synthesized code will generate pattern match in canEqual and equals.

allanrenucci · 2018-03-23T16:37:10Z

tests/neg-custom-args/isInstanceOf/classTag.scala

+  }
+
+  def foo(x: Any): Boolean =
+    x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

allanrenucci · 2018-03-23T16:37:23Z

tests/neg-custom-args/isInstanceOf/gadt.scala

+  eval(exp)(Env.empty)
+
+  def foo(x: Any): Boolean =
+    x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

allanrenucci · 2018-03-23T16:37:31Z

tests/neg-custom-args/isInstanceOf/t2755.scala

+  }
+
+  def foo(x: Any): Boolean =
+    x.isInstanceOf[List[String]]  // error


Remove this line. Tested in i3324.scala?

liufengyun · 2018-04-05T19:01:19Z

Merge now, so that we can fix bugs related to this feature.

liufengyun assigned allanrenucci Feb 27, 2018

liufengyun requested a review from allanrenucci February 27, 2018 16:03

liufengyun force-pushed the fix-3324 branch 2 times, most recently from b42414e to 3dbb2fa Compare March 2, 2018 16:16

liufengyun commented Mar 5, 2018

View reviewed changes

Blaisorblade self-assigned this Mar 5, 2018

Blaisorblade reviewed Mar 6, 2018

View reviewed changes

liufengyun force-pushed the fix-3324 branch 2 times, most recently from 6a14322 to 4bdcaa8 Compare March 7, 2018 08:38

Blaisorblade reviewed Mar 8, 2018

View reviewed changes

liufengyun force-pushed the fix-3324 branch from 2e38f70 to 2cc6ad6 Compare March 9, 2018 12:12

allanrenucci approved these changes Mar 22, 2018

View reviewed changes

allanrenucci assigned liufengyun and unassigned allanrenucci Mar 22, 2018

liufengyun force-pushed the fix-3324 branch from 2cc6ad6 to 2d5f2d4 Compare March 23, 2018 12:14

allanrenucci reviewed Mar 23, 2018

View reviewed changes

liufengyun force-pushed the fix-3324 branch from a45a2b3 to ae0814d Compare March 26, 2018 19:46

allanrenucci added the stat:needs rebase label Mar 26, 2018

liufengyun force-pushed the fix-3324 branch from 61c697b to c097dde Compare March 27, 2018 09:48

liufengyun added 25 commits April 5, 2018 16:26

fix typo in numbering of rules

825dbdf

add more tests

183be33

fix nested @unchecked

974a7c1

add test case

daf2260

adapt specification

9ee4518

tune specification

545930d

Fix scala#1828: add test

8719a88

Allow test for abstract types if it is always true

5fc5db0

code refactoring

d263372

fix test for abstract types

3f12d28

adapt specification for unrelated types

ed13d25

Fix GADT test failures

a90f060

fix fromTasty test

37f4e32

Adapt specification to handle narrowed GADT bounds

ac696da

WIP - address review

e836b71

add more tests

7adc838

instantiate if current class is final

734afb3

fix test

5348b31

ignore GADT related issues for now

0d84bcc

add classTag test

f3d1d90

address review

ac0ec6d

address review

2b23c69

use isPatternTypeSymbol to avoid duplicate

c31c917

move pos test to pos-special/isInstanceOf

a05074d

fix tests

2b00b7a

liufengyun force-pushed the fix-3324 branch from c097dde to 2b00b7a Compare April 5, 2018 14:26

liufengyun merged commit b1d9162 into scala:master Apr 5, 2018

liufengyun deleted the fix-3324 branch April 5, 2018 19:01

karolchmist mentioned this pull request Jun 7, 2018

dotty: 0.6.0-RC1 -> 0.8.0-RC1 NixOS/nixpkgs#41626

Merged

8 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix #3324: add `isInstanceOf` check #4045

Fix #3324: add `isInstanceOf` check #4045

liufengyun commented Feb 27, 2018 •

edited

Loading

liufengyun Mar 5, 2018

liufengyun Mar 5, 2018

Blaisorblade Mar 6, 2018 •

edited

Loading

smarter commented Mar 6, 2018

liufengyun commented Mar 7, 2018

liufengyun commented Mar 7, 2018

Blaisorblade commented Mar 7, 2018

Blaisorblade commented Mar 7, 2018

Blaisorblade commented Mar 8, 2018

liufengyun commented Mar 8, 2018

smarter commented Mar 8, 2018

Blaisorblade Mar 8, 2018

liufengyun commented Mar 9, 2018

allanrenucci commented Mar 22, 2018

dottybot commented Mar 22, 2018

allanrenucci left a comment

allanrenucci Mar 22, 2018

allanrenucci Mar 22, 2018

allanrenucci Mar 22, 2018

liufengyun Mar 23, 2018

allanrenucci Mar 22, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

liufengyun Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

liufengyun Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

allanrenucci Mar 23, 2018

liufengyun commented Apr 5, 2018


		def g(x: A[Int]) = x match { case _: B[Int] => }

		def foo(x: Any) = x.isInstanceOf[List[String]] // error

Fix #3324: add isInstanceOf check #4045

Fix #3324: add isInstanceOf check #4045

Conversation

liufengyun commented Feb 27, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Blaisorblade Mar 6, 2018 • edited Loading

Choose a reason for hiding this comment

smarter commented Mar 6, 2018

liufengyun commented Mar 7, 2018

liufengyun commented Mar 7, 2018

Blaisorblade commented Mar 7, 2018

Blaisorblade commented Mar 7, 2018

Blaisorblade commented Mar 8, 2018

liufengyun commented Mar 8, 2018

smarter commented Mar 8, 2018

Choose a reason for hiding this comment

liufengyun commented Mar 9, 2018

allanrenucci commented Mar 22, 2018

dottybot commented Mar 22, 2018

allanrenucci left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

liufengyun commented Apr 5, 2018

Fix #3324: add `isInstanceOf` check #4045

Fix #3324: add `isInstanceOf` check #4045

liufengyun commented Feb 27, 2018 •

edited

Loading

Blaisorblade Mar 6, 2018 •

edited

Loading