Add path support for capture checking

[noti0na1]

No description provided.

[odersky]

Why was this check removed?

[noti0na1]

When implementing the path, I considered the rule for a singleton type with a capture set. I don't think this check is necessary, as we can already achieve the same result by creating a type alias with a capture set.

[odersky]

So you are saying the rule is incomplete? But then maybe we should dealias before we check? What is the argument for removing it?

[noti0na1]

What I mean is it is okey to let users add a capture set to a singleton type, if they just want to explicitly indicate what the underlying type capturing (for example, in the member function signature def f: this.file^{this.io}).

[odersky]

We need to get better reassurance that this does the right thing. It looks too complicated to be able to argue it's obviously correct. What would help:

• A formal set of rules for subcapturing.
• A rendition of these rules as a doc comment for this method. It's a shame that the old doc comment was not updated in any way.
• More extensive tests that try to test all combinations. I saw we have neg tests but no new pos tests.

[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.

[noti0na1]

We can recur on left and right tress as well.

[noti0na1]

If x.symbol == y.symbol, then x.prefix must equivalent to y.prefix in order to show x subsumes y. Is it simpler to just use TypeCompare to check them? I think we have to prove (x subsumes y) && (y subsumes x) ==> x =:= y.