Adapt types according to read-only status

[odersky]

Extend type adaptation to read-only status.

Two big improvements:

• we also adapt if the target type is a mutable type with a read-only capture set. So the following compiles:

  class Ref extends Mutable { ... }
  val x: Ref^{cap.rd} = Ref()

• we also adapt deeply inside a type. So the following compiles:

   val refs = List(Ref(), Ref())
   val rdrs: List[Ref^{cap.rd}] = refs

  We even try to track arguments through base types, so the following also compiles:

  val rdrs2: Seq[Ref^{cap.rd}] = refs

  But there are some limits, correlating actual and expected type through base types and as-seen-from is hard.

In the end I had to abandon the original idea to roll everyhting into subtyping. I got the basics to work, but the problem then was that we use deep capture sets in separation checking, and those were not adapted. To do this, we'd have to somehow figure out what a dcs relative to an expected type is. This looks deeply non-trivial, and would probably in the end come down to techniques similar to the adaptation in this PR. So the benefit of also adding and inferring qualifiers to capture sets are not clear.

EDIT: We do need qualifiers for soundness as @Linyxus example below shows. It's now in ro-mut-conformance.scala.
So the adaptation commit has been rebased on the mutability qualifiers branch.

[Linyxus]

LGTM overall!

So the benefit of also adding and inferring qualifiers to capture sets are not clear.

not sure if I understood it correctly, does it mean that qualifier inference may not be that useful given the read-only status adaptation?

A related example:

import language.experimental.captureChecking
import caps.*
class Ref extends Mutable:
  private var _data: Int = 0
  def get: Int = _data
  mut def set(x: Int): Unit = _data = x
def test1(a: Ref^{cap.rd}): Unit =
  a.set(42)  // error, as expected
def test2(a: Ref^{cap.rd}): Unit =
  val t: Ref^{cap} = a  // should be error, but ok
  t.set(42)

right now it only has one error. The second but last line widens Ref^{cap.rd} to Ref^{cap} which implicitly lifts the permission of this reference and is clearly unsound. This is the examples that qualifier inference needs to take care of, I guess.

[odersky]

not sure if I understood it correctly, does it mean that qualifier inference may not be that useful given the read-only status adaptation?

Good point. Yes, we still need the subtyping / inference rules for soundness. The problem is we cannot rely on them exclusively since then our deep capture sets are wrong. What needs to happen is that we adapt read-only status, which according to subtyping means we widen the type. So unlike for box adaptation this widening is possible (since we still conform to the expected type) but not necessary for conformance (since the original type already conformed). It is however necessary to remember that widened type so that we can reduce deep capture sets and don't get spurious separation errors.

I'll add that part tomorrow.