Plug soundness hole for reach capabilities

[odersky]

To prevent that a reach capability is undermined by passing in a local capability from the outside, we disallow function arguments where reach capabilities appear in contravariant or invariant positions.

New scheme:

Enforce an analogous restriction to the one for creating reach capabilities
for all values. The type of a value cannot both have a reach capability with variance >= 0 and at the same time a universal capability with variance <= 0.

[Linyxus]

I found a varation of this counter-example on this branch:

  import language.experimental.captureChecking
  trait File:
    def close(): Unit

  def withFile[R](path: String)(op: File^ => R): R = ???

  trait Foo[+X]:
    def use(x: File^): X
  class Bar extends Foo[File^]:
    def use(x: File^): File^ = x

  def bad(): Unit =
    val backdoor: Foo[File^] = new Bar
    val boom: Foo[File^{backdoor*}] = backdoor

    var escaped: File^{backdoor*} = null
    withFile("hello.txt"): f =>
      escaped = boom.use(f)
        // boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed
        // f: File^, so there is no reach capabilities

[odersky]

OK, so we have to tighten the screws further. My intuition is that the restrictions that prevent us from lowering cap to a reach capabaility should also apply to all other values that get reach capabilities through substitution.

[odersky]

The new scheme also excludes the second unsoundness example, and compiles stdlib and all previous pos tests successfully.

[Linyxus]

thanks, LGTM!