Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix #3989: Fix several unsoundness problems related to variant refinement #4013

Merged
merged 9 commits into from
Mar 17, 2018

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Feb 19, 2018

This solves a number of unsoundness problems related to variant refinement

Some tests had to be updated or re-classified because they were unsound before. The collection strawman needs to be updated to conform to the new rules.

// - members in other concrete classes, since these have been checked before
// (this is done for efficiency)
// - members in a prefix of inherited parents that all come from Java or Scala2
// (this is done to avoid false negatives since Scala2's rules for checking are different)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"false negatives" = false errors from the typechecker? I'm used to "false positives" (which makes sense for error checking).

More importantly, this means that we should test that Scala 2 material indeed follows Scala 2 rules?

val seenClasses = mutable.Set[Symbol]()
def addDecls(cls: Symbol): Unit =
if (!seenClasses.contains(cls)) {
seenClasses.+=(cls)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not seenClasses += cls? Has idiomatic style changed?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No, hat was an editing breakage.

@odersky
Copy link
Contributor Author

odersky commented Feb 19, 2018

test performance please

@dottybot
Copy link
Member

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

@dottybot
Copy link
Member

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4013/ to see the changes.

Benchmarks is based on merging with master (668c499)

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

That's what I feared - performance is dramatically worse for scala-library, slightly worse for everything else.

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

The collection strawman does not compile under this branch because it contains some patterns that are now recognized as unsound. Some have easy fixes. E.g. ArrayOps needs to extend IndexedSeqOps, not SeqOps. That was probably an oversight. The main cause of errors is WithFilter on maps and sets. Here we lose precision wrt collection.WithFilter which leads to type inconsistencies. /cc @julienrf.

I have disabled the tests involving strawman until this is fixed. We should re-enable them afterwards.

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

test performance please

@dottybot
Copy link
Member

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

@julienrf
Copy link
Contributor

@odersky Do we have to change our implementation? I think the changes you’ve mentioned for ArrayOps are arleady done here. I have to have a look at withFilter…

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

@julienrf Yes, the ArrayOps changes seem to be already done. But WithFilter needs to be fixed. Can you take this branch and see what needs to be done? It already contains the changes to hk-equality which was the previous blocker for compiling the strawman with dotty.

@dottybot
Copy link
Member

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4013/ to see the changes.

Benchmarks is based on merging with master (9053964)

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

@julienrf Also, the later changes here could invalidate some pattern matches. This is because it propagates fewer types from scrutinees to pattern. To fix this, one needs to sometimes write an @unchecked type argument in the pattern. I have noted one such case in IterableOps which now fails.

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

test performance please

@dottybot
Copy link
Member

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

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

Now all variants of problems I could derive from #3989 seem to be fixed.

@Blaisorblade
Copy link
Contributor

Blaisorblade commented Feb 20, 2018

@odersky Just in case, is this example with protected[this] also fixed? scala/bug#7093 (comment)
(EDIT: maybe a good testcase, especially if somebody wants to try optimizations? what I sketched this morning would have broken).

@dottybot
Copy link
Member

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4013/ to see the changes.

Benchmarks is based on merging with master (2a019f3)

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

@Blaisorblade The protected[this] problem is fixed with latest commit. @julienrf: One more thing to update for the collection strawman. Hint: Compiling with -language:Scala2 -migration will give more specific error messages.

@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

Regarding performance, I am inclined to not do anything right now. compileStdLib is an outlier, and I see no obviously safe way to reduce the number of checks.

@odersky odersky changed the title Fix #3989: Check that members of concrete classes are type-correct Fix #3989: Fix several unsoundness problem related to variant refinement Feb 20, 2018
@odersky odersky changed the title Fix #3989: Fix several unsoundness problem related to variant refinement Fix #3989: Fix several unsoundness problems related to variant refinement Feb 20, 2018
@odersky
Copy link
Contributor Author

odersky commented Feb 20, 2018

@olafurpg Here's a problem scala-fix could help with: Insert @uncheckedVariance at the right places if a definition is no longer variance correct according to the new rules. dotc tried to do it, but it's more complex than it looks, so it's currently disabled. See f551646, in particular the two TODO comments there.

@szeiger
Copy link
Contributor

szeiger commented Feb 21, 2018

Effect of this on collection strawman (with failures both in the original design and more in the changes I merged yesterday in scala/collection-strawman#468:

[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/BitSet.scala:40:23
[error] 40 |  protected[this] type BitSetC = C
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type C occurs in invariant position in type  = C of type BitSetC
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:29:43
[error] 29 |  protected[this] def fromSpecificIterable(coll: Iterable[A]): IterableCC[A] = iterableFactory.from(coll)
[error]    |                                           ^^^^^^^^^^^^^^^^^
[error]    |covariant type A occurs in contravariant position in type strawman.collection.Iterable[A] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:30:22
[error] 30 |  protected[this] def newSpecificBuilder(): Builder[A, IterableCC[A]] = iterableFactory.newBuilder[A]()
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type A occurs in contravariant position in type (): strawman.collection.mutable.Builder[A, strawman.collection.Iterable[A]] of method newSpecificBuilder
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:750:24
[error] 750 |    protected[this] def filtered = View.Filter(toIterable, p, isFlipped = false)
[error]     |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |covariant type A occurs in invariant position in type => strawman.collection.View.Filter[A] of method filtered
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:71:23
[error] 71 |  protected[this] type IterableCC[X] = CC[X]
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type CC occurs in invariant position in type  = CC of type IterableCC
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:90:43
[error] 90 |  protected[this] def fromSpecificIterable(coll: Iterable[A]): C
[error]    |                                           ^^^^^^^^^^^^^^^^^
[error]    |covariant type A occurs in contravariant position in type strawman.collection.Iterable[A] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Iterable.scala:110:22
[error] 110 |  protected[this] def newSpecificBuilder(): Builder[A, C]
[error]     |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |covariant type A occurs in contravariant position in type (): strawman.collection.mutable.Builder[A, C] of method newSpecificBuilder
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Map.scala:18:52
[error] 18 |  override protected[this] def fromSpecificIterable(coll: Iterable[(K, V)]): MapCC[K, V] = mapFactory.from(coll)
[error]    |                                                    ^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type V occurs in contravariant position in type strawman.collection.Iterable[(K, V)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Map.scala:19:31
[error] 19 |  override protected[this] def newSpecificBuilder(): mutable.Builder[(K, V), MapCC[K, V]] = mapFactory.newBuilder[K, V]()
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type V occurs in contravariant position in type (): strawman.collection.mutable.Builder[(K, V), strawman.collection.Map[K, V]] of method newSpecificBuilder
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/Map.scala:62:23
[error] 62 |  protected[this] type MapCC[K, V] = CC[K, V]
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type CC occurs in invariant position in type  = CC of type MapCC
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/SortedMap.scala:17:52
[error] 17 |  override protected[this] def fromSpecificIterable(coll: Iterable[(K, V)]): SortedMapCC[K, V] = sortedMapFactory.from(coll)
[error]    |                                                    ^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type V occurs in contravariant position in type strawman.collection.Iterable[(K, V)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/SortedMap.scala:18:31
[error] 18 |  override protected[this] def newSpecificBuilder(): mutable.Builder[(K, V), SortedMapCC[K, V]] = sortedMapFactory.newBuilder[K, V]()
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |  covariant type V occurs in contravariant position in type ():
[error]    |    strawman.collection.mutable.Builder[(K, V),
[error]    |      strawman.collection.SortedMap[K, V]
[error]    |    ] of method newSpecificBuilder
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/SortedMap.scala:29:23
[error] 29 |  protected[this] type SortedMapCC[K, V] = CC[K, V]
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type CC occurs in invariant position in type  = CC of type SortedMapCC
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/SortedSet.scala:22:23
[error] 22 |  protected[this] type SortedIterableCC[X] = CC[X]
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type CC occurs in invariant position in type  = CC of type SortedIterableCC
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/ImmutableArray.scala:29:22
[error] 29 |  protected[this] def elemTag: ClassTag[A]
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type A occurs in invariant position in type => ClassTag[A] of method elemTag
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/ImmutableArray.scala:39:52
[error] 39 |  override protected[this] def fromSpecificIterable(coll: strawman.collection.Iterable[A]): ImmutableArray[A] = ImmutableArray.from[A](coll)(elemTag)
[error]    |                                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type A occurs in contravariant position in type strawman.collection.Iterable[A] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/ImmutableArray.scala:41:31
[error] 41 |  override protected[this] def newSpecificBuilder(): Builder[A, ImmutableArray[A]] = ImmutableArray.newBuilder[A]()(elemTag)
[error]    |  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |  covariant type A occurs in contravariant position in type ():
[error]    |    strawman.collection.mutable.Builder[A,
[error]    |      strawman.collection.immutable.ImmutableArray[A]
[error]    |    ] of method newSpecificBuilder
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/IntMap.scala:172:52
[error] 172 |  override protected[this] def fromSpecificIterable(coll: strawman.collection.Iterable[(Int, T)]): IntMap[T] =
[error]     |                                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |covariant type T occurs in contravariant position in type strawman.collection.Iterable[(scala.Int, T)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/IntMap.scala:180:31
[error] 180 |  override protected[this] def newSpecificBuilder(): Builder[(Int, T), IntMap[T]] =
[error]     |  ^
[error]     |  covariant type T occurs in contravariant position in type ():
[error]     |    strawman.collection.mutable.Builder[(scala.Int, T),
[error]     |      strawman.collection.immutable.IntMap[T]
[error]     |    ] of method newSpecificBuilder
[error] 181 |    new ImmutableBuilder[(Int, T), IntMap[T]](empty) {
[error] 182 |      def addOne(elem: (Int, T)): this.type = { elems = elems + elem; this }
[error] 183 |    }
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/LazyList.scala:231:40
[error] 231 |  protected[this] def cons[T](hd: => T, tl: => CC[T]): CC[T]
[error]     |                                        ^^^^^^^^^^^^
[error]     |covariant type CC occurs in contravariant position in type => CC[T] of value tl
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/LazyList.scala:361:43
[error] 361 |  protected[this] def newCons[T](hd: => T, tl: => CC[T]): CC[T]
[error]     |                                           ^^^^^^^^^^^^
[error]     |covariant type CC occurs in contravariant position in type => CC[T] of value tl
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/LongMap.scala:164:52
[error] 164 |  override protected[this] def fromSpecificIterable(coll: strawman.collection.Iterable[(Long, T)]): LongMap[T] = {
[error]     |                                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |covariant type T occurs in contravariant position in type strawman.collection.Iterable[(scala.Long, T)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/LongMap.scala:171:31
[error] 171 |  override protected[this] def newSpecificBuilder(): Builder[(Long, T), LongMap[T]] =
[error]     |  ^
[error]     |  covariant type T occurs in contravariant position in type ():
[error]     |    strawman.collection.mutable.Builder[(scala.Long, T),
[error]     |      strawman.collection.immutable.LongMap[T]
[error]     |    ] of method newSpecificBuilder
[error] 172 |    new ImmutableBuilder[(Long, T), LongMap[T]](empty) {
[error] 173 |      def addOne(elem: (Long, T)): this.type = { elems = elems + elem; this }
[error] 174 |    }
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/Map.scala:155:54
[error] 155 |    override protected[this] def fromSpecificIterable(coll: collection.Iterable[(K, V)]): WithDefault[K, V] =
[error]     |                                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]     |covariant type V occurs in contravariant position in type strawman.collection.Iterable[(K, V)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/Map.scala:158:33
[error] 158 |    override protected[this] def newSpecificBuilder(): Builder[(K, V), WithDefault[K, V]] =
[error]     |    ^
[error]     |    covariant type V occurs in contravariant position in type ():
[error]     |      strawman.collection.mutable.Builder[(K, V),
[error]     |        strawman.collection.immutable.Map.WithDefault[K, V]
[error]     |      ] of method newSpecificBuilder
[error] 159 |      Map.newBuilder().mapResult((p: Map[K, V]) => new WithDefault[K, V](p, defaultValue))
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/SortedMap.scala:99:54
[error] 99 |    override protected[this] def fromSpecificIterable(coll: strawman.collection.Iterable[(K, V)]): WithDefault[K, V] =
[error]    |                                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |covariant type V occurs in contravariant position in type strawman.collection.Iterable[(K, V)] of value coll
[error] -- Error: /Users/szeiger/code/scala/collection-strawman/collections/src/main/scala/strawman/collection/immutable/SortedMap.scala:102:33
[error] 102 |    override protected[this] def newSpecificBuilder(): Builder[(K, V), WithDefault[K, V]] =
[error]     |    ^
[error]     |    covariant type V occurs in contravariant position in type ():
[error]     |      strawman.collection.mutable.Builder[(K, V),
[error]     |        strawman.collection.immutable.SortedMap.WithDefault[K, V]
[error]     |      ] of method newSpecificBuilder
[error] 103 |      SortedMap.newBuilder().mapResult((p: SortedMap[K, V]) => new WithDefault[K, V](p, defaultValue))
[error] 27 errors found

@smarter
Copy link
Member

smarter commented Feb 21, 2018

Once the collection-strawman is fixed, we should check the performance impact there too.

@odersky
Copy link
Contributor Author

odersky commented Mar 15, 2018

Seems I dropped the ball on this one... Let me take a look at the new issues.

odersky added 8 commits March 16, 2018 15:01
This fixes the second half of scala#3989. Some tests had to be updated or
re-classified because they were unsound before.
It's more efficient. Let's see whether that makes a difference.
Plugging the soundness hole in scala#3989 unveiled problems in the strawman. These need to be
fixed before we can test it again in dotty.
i3989a.scala gives an example which is rejected under the new scheme.
This would pass and fail at runtime under the previous scheme.
@odersky
Copy link
Contributor Author

odersky commented Mar 16, 2018

The problems reported by @liufengyun are now fixed as well. @liufengyun do you want to review the last two commits?

@odersky odersky assigned liufengyun and unassigned Blaisorblade Mar 16, 2018
Copy link
Contributor

@liufengyun liufengyun left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, cannot find another counter-example.

@odersky
Copy link
Contributor Author

odersky commented Mar 17, 2018

LGTM, cannot find another counter-example.

Good news!

@odersky odersky merged commit b499a9a into scala:master Mar 17, 2018
@Blaisorblade Blaisorblade deleted the fix-#3989 branch March 18, 2018 14:04
allanrenucci added a commit to dotty-staging/collection-strawman that referenced this pull request Mar 19, 2018
This version of Dotty fixes several unsoundness issues and remove the
unsound protected[this] escape hatch for variance checking. See
scala/scala3#4013
allanrenucci added a commit to dotty-staging/collection-strawman that referenced this pull request Mar 19, 2018
This version of Dotty fixes several unsoundness issues and remove the
unsound protected[this] escape hatch for variance checking. See
scala/scala3#4013
@adriaanm
Copy link
Contributor

Does this also close the unsoundness illustrated by @TomasMikula in scala/bug#10822 (comment), where GADT matching is unsoundly allowed because a covariant occurrence of a type param is hidden by a type ascription where it only occurs invariantly?

@smarter
Copy link
Member

smarter commented Apr 13, 2018

@adriaanm I think the unsoundness in scalac comes from allowing this to compile:

class Foo[A]
private[this] class Bar[+A] extends Foo[A]

Disabling the variance checks for private[this] is not sound here. In Dotty your example compiles because the variance checks for the extends clause are completely missing, but once we add them we won't special case them for private[this]: #2973

@adriaanm
Copy link
Contributor

adriaanm commented Apr 13, 2018 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

10 participants