Extend exhaustivity checks to and-types #2155

abgruszecki · 2017-03-30T16:33:16Z

As discussed on gitter, this PR extends exhaustivity checks to and-types. It's possible to check exhaustivity of pattern matching on them in case of "marker" types like this:

trait Marker
sealed type T
case object A extends T with Marker
case object B extends T with Marker
case object C extends T
def m(s: T & Marker) = s match { case A => ; }
// current behaviour without -YcheckAllPatmat:
//     no warning, since and-types aren't considered checkable
// with -YcheckAllPatmat:
//     warns that _: T & Marker would fail - T & Marker isn't decomposed into A | B

I've defined and-types as checkable if either type is checkable, decomposable if either type is decomposable and used space intersection for decomposition. However, this gives wrong results for this case:

sealed trait T
trait T1 extends T
trait T2 extends T
trait T3
def m(s: T & T3) = s match { case _: T1 => ; }

The underlying issue is that the intersection of two open types was previously approximated to be empty. I've added a check to intersect to see if it's possible to have a value of both types and return a type space of the and-type if that's the case. This changes slightly how space subtraction behaves - it's now possible to get "degenerate" unions from subtracting two constructor spaces ("degenerate" in the sense that one of the spaces is exactly the left-hand-side of the subtraction). This doesn't change the final result of exhaustivity check, though, so I'm not sure if it's an issue.

I'm also not completely sure if I got the isOpen implementation right - I'm not really familiar with how symbols work, so it's entirely possible there's a mistake there.

I'm also aware that commonOpenTypeSpace may sometimes return a space that can't be inhabited, since for instance the types are classes with conflicting methods, but I don't think it's an issue, since a) such and-types should be rare and b) we will at most emit a warning that the match may not be exhaustive.

/cc @liufengyun

smarter · 2017-03-30T19:30:08Z

http://dotty-ci.epfl.ch/lampepfl/dotty/1516/5 :

[error] Test dotty.tools.dotc.CompilationTests.runAll failed: java.lang.AssertionError: Run test failed, but should not, took 288.947 sec
[error] at dotty.tools.dotc.ParallelTesting$CompilationTest.checkRuns(ParallelTesting.scala:811)
[error] at dotty.tools.dotc.CompilationTests.runAll(CompilationTests.scala:166)
[error] ...

@felixmulder This is not a very precise error message :).

liufengyun · 2017-03-30T19:55:28Z

Thanks for the quick turnaround @AleksanderBG . While waiting to see the failures, I think it's possible to merge isOpen and commonOpenTypeSpace into one method to simplify the protocol, as they are used exactly at the same place. Maybe something named intersectAtomTypes? The name atom is justified by the fact that an un-decomposable type must be matched as a whole.

intersectAtomTypes can be further optimised by single inheritance of Scala class system. Namely, if A and B both refer to classes types, then the intersection is empty.

felixmulder · 2017-03-30T20:26:04Z

@smarter: re-ran it locally, seems to work just fine...amending the test suite tomorrow to dump all the logs on any failure. My best guess is that something threw an exception and the test called fail() without printing to stdout/stderr.

smarter · 2017-04-02T21:09:53Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

-   */
-  def commonOpenTypeSpace(tp1: Type, tp2: Type): Space
+  /** Return a space containing the values of both atom (non-decomposable) types. */
+  def intersectAtomTypes(tp1: Type, tp2: Type): Space


nit-pick: I would say AtomicTypes instead of AtomTypes.

Can do - that does sound more correct than the other one.

abgruszecki · 2017-04-02T21:13:20Z

I've merged isOpen/commonOpenTypeSpace as suggested, and checked if at least one of the types is a trait - I hope the code does the right thing. I've tried to read the documentation about symbols, but they're still confusing.

Regarding the test failures, I've been running test locally instead of partest - the second one fails with this message, even on master:

[error] Test dotc.tests.pickle_pickleOK failed: scala.reflect.io.FileOperationException: File 'innerclass.flags' already exists., took 0.019 sec
[error]     at scala.reflect.io.Path$.fail(Path.scala:78)
[error]     at scala.reflect.io.Path.createFile(Path.scala:235)
[error]     at dotty.tools.dotc.CompilerTest.copyFiles(CompilerTest.scala:468)
[error]     at dotty.tools.dotc.CompilerTest.computeDestAndCopyFiles(CompilerTest.scala:446)
[error]     at dotty.tools.dotc.CompilerTest.compileFile(CompilerTest.scala:116)
[error]     at dotty.tools.dotc.CompilerTest.$anonfun$compileFiles$2(CompilerTest.scala:210)
[error]     at scala.compat.java8.JProcedure1.apply(JProcedure1.java:18)
[error]     at scala.compat.java8.JProcedure1.apply(JProcedure1.java:10)
[error]     at scala.collection.IndexedSeqOptimized$class.foreach(IndexedSeqOptimized.scala:33)
[error]     at scala.collection.mutable.ArrayOps$ofRef.foreach(ArrayOps.scala:186)
[error]     at dotty.tools.dotc.CompilerTest.compileFiles(CompilerTest.scala:211)
[error]     at dotc.tests.pickle_pickleOK(tests.scala:110)
[error]     ...

Is there something I should be doing apart from just ;clean; test:compile; partest --show-diff --verbose?

smarter · 2017-04-02T21:18:01Z

@AleksanderBG partest is going to be retired soon so it might not be worth trying to get it working now, but one easy thing you can try is to delete tests/partest-generated. Regarding symbols, etc: if you have specific questions please don't hesitate to ask here or on gitter, otherwise you might be interested in watching this talk which explains some of the core data structures of dotty: https://www.youtube.com/watch?v=WxyyJyB_Ssc (slides: https://www.slideshare.net/Odersky/compilers-are-databases)

liufengyun

We are making some big changes to the CI recently, the CI is most likely to be some instability -- ~~but the partest failure might indicate some problem with our new partest framework. \cc @felixmulder~~.

liufengyun · 2017-04-02T21:32:01Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

+
+    if ((tp1.classSymbol.is(Trait) || tp2.classSymbol.is(Trait))
+        && isOpen(tp1) && isOpen(tp2))
+      Typ(AndType(tp1, tp2), true)


Normally, we expect programmers will not abuse AND-types in pattern matches. However, to be safer, it's better to handle the case if tp1 and tp2 are themselves AND-types if it doesn't significantly complicate the implementation.

Could you elaborate how and-types could be abused here? Judging from the classSymbol implementation, if the type is an and-type, a symbol will be returned only if the and-type is "effectively" a class/trait, which seems to be correct in this case.

We could potentially simplify the and-type here if that's the case, though.

What I've in mind is the case where the two types are Trait1 & Trait2 and Trait3 & Trait4, in which case, the intersection would be Trait1 & Trait2 & Trait3 & Trait4.

liufengyun · 2017-04-02T21:33:04Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -84,6 +84,9 @@ trait SpaceLogic {
  /** Is `tp1` the same type as `tp2`? */
  def isEqualType(tp1: Type, tp2: Type): Boolean

+  /** Return a space containing the values of both atom (non-decomposable) types. */
+  def intersectAtomTypes(tp1: Type, tp2: Type): Space


Better to add one additional note saying that tp1 and tp2 are not subtype of each other.

liufengyun · 2017-04-03T13:56:32Z

BTW, @AleksanderBG I'm not sure if the CLA fails because you haven't signed the CLA? If not, you can do it below:

https://www.lightbend.com/contribute/cla/scala

abgruszecki · 2017-04-06T17:41:24Z

@smarter thank you very much for the presentation - it was quite helpful!
@liufengyun I've handled nested and-types, as well as type aliases and refined types. I'm not sure if the code meets the Dotty standards of efficiency, but I think it's at least correct. I didn't handle structural types, since isSubType treats them conservatively as a supertype of all other types - I don't think we can improve on that without checking for member collisions, since otherwise it'd be possible to miss a case, like here:

sealed trait T
object O { val x = 5 } extends T

(??? : T & { val x: Int }) match { ... }

I had some problems with the compiler output during tests in andtype-refinedtype-interaction.check - there must be spaces at the end of the broken lines, and my IDEA deletes those automatically on save. Would it be possible to increase the maximum line length?

smarter · 2017-04-06T17:58:49Z

Would it be possible to increase the maximum line length?

Possibly by changing the -pagewidth setting used to run tests, but maybe we could fix the output to not contain trailing spaces, or we could cheat and call trim on lines before comparing them in PatmatExhaustivityTest

abgruszecki · 2017-04-06T19:11:17Z

The tests fail since I added an additional line of comment to tests/patmat/andtype-refinedtype-interaction.scala - I'll see if I can do something with the spaces-at-the-EOL while fixing this.

liufengyun · 2017-04-07T08:20:35Z

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

+    implementability(and) match  {
+      case Unimplementable => Empty
+      case _ => Typ(and, true)
+    }


By implementability, I guess you mean whether the greatest lower bound of tp1 and tp2 is possibly inhabited or not.

I'm wondering if there's some facility in Typer to soundly approximate GLB of two types? My intuition is that there should have some similar facilities, in order to simplify intersection types, but I don't know where it's located.

TypeComparer#glb is close, but it seems it does not use the knowledge of Final and single inheritance. Is it possible to refine TypeComparer#glb to take advantage of Final and single inheritance? Ping @smarter @odersky .

I thought about it, but this is slightly different from inhabitation - I'm not interested in whether there exists a value of the given type, but rather whether it's possible to create a class or trait of this type. For instance, a singleton type is inhabited, but not implementable. The type being inhabited is a stronger statement, and I don't think it's necessary to check for it, since all types which are inhabited but not implementable will be caught by the subtyping check.

Checking for inhabitation would work too and I tried to look for an existing method, but I didn't find any. I'd be happy to use it if there's one.

abgruszecki · 2017-04-09T19:08:21Z

implementability should be cleaner now - I concentrated on making it sound.
Atomic intersection now should only return an empty space if the space really
is empty. I've been able to catch an error in andtype-opentype-interaction
test thanks to this - previously sealed was incorrectly treated as impossible
to extend.

There are still some cases to be added to implementability, like type bounds.
I've tried adding a case for HKApply, but I've been unable to get a value of that.

I also looked at the methods in TypeComparer, but I don't think any of
them are particularly helpful - tp1 & tp2 could be used to potentially
simplify the types a bit, but I'd still have to traverse the type returned
by it and determine if there's a class collision. @smarter @odersky if you have
any suggestions regarding what methods could be useful here (possibly as a reference),
I'd be grateful.

As a sidenote - debug printing I've added is only temporary and I'll remove it
before creating a real pull request to avoid conflicts with #2197.

liufengyun · 2017-04-12T06:50:31Z

@AleksanderBG Thanks for the good work. #2197 has been merged, there's some conflict, maybe you can resolve first?

@odersky will have a look at this PR and see if there's some existing facility in typer that can be used, or we keep the hack in the exhaustivity check.

abgruszecki · 2017-04-13T12:35:47Z

Rebased to master & touched up the commit history.

Check if at least one of the types is a trait before deciding that their intersection is non-empty.

Handle: - nested and-types - refined types - type aliasing Add line end trimming to patmat tests to work around an issue where lines end with spaces.

For consistency with or-types.

abgruszecki · 2017-04-20T19:50:27Z

@odersky when can I count on your review? I can improve this if needed,
but working on this has already cut a bit too much into my master's thesis,
so I don't want to do any unnecessary work.

odersky · 2017-04-26T14:54:22Z

I am not too familiar with Space, defer to @liufengyun for that. What I can see LGTM.

liufengyun · 2017-04-26T15:04:25Z

OK, let's merge then. Thanks a lot @AleksanderBG .

abgruszecki · 2017-04-26T18:04:28Z

Thank you too for you help @liufengyun!

smarter reviewed Apr 2, 2017

View reviewed changes

liufengyun reviewed Apr 2, 2017

View reviewed changes

liufengyun reviewed Apr 7, 2017

View reviewed changes

abgruszecki added 6 commits April 20, 2017 20:33

Enable exhaustivity checks on and-types

07285c0

Make space intersection of two open types non-empty

2252d78

Merge isOpen/commonOpenTypeSpace into intersectUnrelatedAtomicTypes

bfa5aea

Check if at least one of the types is a trait before deciding that their intersection is non-empty.

Improve atomic type intersection

6fc2cd9

Handle: - nested and-types - refined types - type aliasing Add line end trimming to patmat tests to work around an issue where lines end with spaces.

Rewrite implementability with soundness in mind

75c4f38

Dealias and-types in canDecompose

50b03c0

For consistency with or-types.

felixmulder assigned odersky Apr 26, 2017

liufengyun changed the title ~~[WIP] Extend exhaustivity checks to and-types~~ Extend exhaustivity checks to and-types Apr 26, 2017

liufengyun merged commit 8815b40 into scala:master Apr 26, 2017

abgruszecki deleted the wip-andtype-exhaustivity branch April 26, 2017 18:04

Extend exhaustivity checks to and-types #2155

Extend exhaustivity checks to and-types #2155

Uh oh!

Conversation

abgruszecki commented Mar 30, 2017

Uh oh!

smarter commented Mar 30, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

liufengyun commented Mar 30, 2017

Uh oh!

felixmulder commented Mar 30, 2017

Uh oh!

smarter Apr 2, 2017

Choose a reason for hiding this comment

Uh oh!

abgruszecki Apr 2, 2017

Choose a reason for hiding this comment

Uh oh!

abgruszecki commented Apr 2, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smarter commented Apr 2, 2017

Uh oh!

liufengyun left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

liufengyun Apr 2, 2017

Choose a reason for hiding this comment

Uh oh!

abgruszecki Apr 3, 2017

Choose a reason for hiding this comment

Uh oh!

liufengyun Apr 3, 2017

Choose a reason for hiding this comment

Uh oh!

liufengyun Apr 2, 2017

Choose a reason for hiding this comment

Uh oh!

liufengyun commented Apr 3, 2017

Uh oh!

abgruszecki commented Apr 6, 2017

Uh oh!

smarter commented Apr 6, 2017

Uh oh!

abgruszecki commented Apr 6, 2017

Uh oh!

liufengyun Apr 7, 2017 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

abgruszecki Apr 7, 2017

Choose a reason for hiding this comment

Uh oh!

abgruszecki commented Apr 9, 2017

Uh oh!

liufengyun commented Apr 12, 2017

Uh oh!

abgruszecki commented Apr 13, 2017

Uh oh!

abgruszecki commented Apr 20, 2017

Uh oh!

odersky commented Apr 26, 2017

Uh oh!

liufengyun commented Apr 26, 2017

Uh oh!

abgruszecki commented Apr 26, 2017

Uh oh!

Uh oh!

smarter commented Mar 30, 2017 •

edited

Loading

abgruszecki commented Apr 2, 2017 •

edited

Loading

liufengyun left a comment •

edited

Loading

liufengyun Apr 7, 2017 •

edited

Loading