Add path support for capture checking

[noti0na1]

[odersky]

I tried this version of the old subsumes and compared its outcome with the new subsumes for all the tests in testCompilation.

  final def subsumesOld(y: CaptureRef)(using Context): Boolean =
    (this eq y)
    || this.isRootCapability
    || y.match
        case y: TermRef =>
            y.prefix.match
              case ypre: CaptureRef =>
                this.subsumes(ypre)
                || this.match
                    case x @ TermRef(xpre: CaptureRef, _) =>
                      x.symbol == y.symbol && xpre =:= ypre
                    case _ =>
                      false
              case _ => false
          || y.info.match
              case y1: SingletonCaptureRef => this.subsumes(y1)
              case _ => false
        case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
        case _ => false
    || this.match
        case ReachCapability(x1) => x1.subsumes(y.stripReach)
        case x: TermRef =>
          x.info match
            case x1: SingletonCaptureRef => x1.subsumes(y)
            case _ => false
        case x: TermParamRef => subsumesExistentially(x, y)
        case x: TypeRef => assumedContainsOf(x).contains(y)
        case _ => false

There was no difference in outcomes, and the version here is shorter and clearer. So we should probably use this, unless we have tests that show there is a difference and the version here is wrong.

[odersky]

I would have expected more changes in the recheckSelect rule. Indeed, recheckSelect seems to not make use of path types. Here is a simple test program:

class IO

class C(val f: IO^)

def test(io: IO^) =
  val c = C(io)
  val g = () => println(c.f)

This types g as () ->{c} Unit. But it should be () ->{c.f} Unit.

EDIT: We probably also need to change markFree, so that it stores path types instead of their prefixes. The problem seems to be that we already marlk c free when we see it in c.f. We should recognize that the expected type is a SelectionProto and hold off until we have typechecked the full path.

[odersky]

Also, I tink in light of path types, there's scope for a simplification of recheckSelect. A lot of the contortions there were made to make up for the lack of path types.

[odersky]

Generally, what's missing is a suite of tests that shows how path-dependent types give a more expressive language. Show code that did not typecheck before, but now does.

[odersky]

There's a problem with pattern matching shown in the path-patmat-should-be-pos.scala test.

[odersky]

Rebased to main