Add captureset levels (draft)

[odersky]

This is an attempt to implement a new scope restriction scheme for capture checking based on levels.

The idea is to have a stack of capture roots where inner capture roots are super-captures of outer roots.

The draft needs to be refined and justified by theory before it can be merged.

[odersky]

Here's a sketch of the underlying theory (not yet precisely implemented):

Let a, b range over root capabilities. Outer roots subcapture nested roots:

Γ₁, a, Γ₂, b, Γ₃ ⊢ a <:< b

Define a translation |T|a, |t|a on types and terms as follows:

|∀(x: A)B|a  =  ∀b.∀(x: |A|b)|B]b
|T^C|a       =  |T|a^[cap := a]C
|X|a         =  X
|☐T|a        =  ☐|T|a

|λ(x: T)t|a  =  λb.λ(x: |T|b)|t|b
|s(t)|a      =  |s|a (a) (|t|a)
|x|a         =  x
|let x = s in t|a
             =  let x = |s|a in |t|a
|☐t|a        =  ☐|t|a
|C -∘ t|a    =  [cap := a]C -∘ |t|a

This translation should be type preserving, i.e. if ⊢ t: T in CC_<:☐ then ⊢ |t|a: |T|a.

With that translation, we can enforce scoped capabilities as follows:

usingFile: ∀[T]∀(op: F^cap ->{cap} T): T =
  λ[T].
    val f: F^cap = newFile
    op(f)

Bad usage:

usingFile:
  λ(f: F^cap).λ(x: Unit). f; ()

These expand to

usingFile: ∀[T]∀b.∀(op: ∀c.F^c ->{b} T): T =
  λ[T].λb.
    val f: F^b = newFile
    op(b)(f)

usingFile:
  λc.λ(f: F^c).λ(x: Unit). f; ()

The argument of usingFile

    : ∀c.F^c -> Unit ->{f} Unit
    : ∀c.F^c -> Unit ->{c} Unit
    : UNTYPABLE as (∀c.F^c -> T) for any type argument T since T cannot
      contain c and c cannot be widened further.

This enforcement works without needing the restriction that box/unbox cannot use a root capability. The previous restriction,
that box/unbox cannot use cap becomes superfluous, since cap is no longer part of the translated terms and types.

The scheme also allows the creation of fresh capabilities that get returned:

newRef: ∀[T]∀a.T -> Ref[T]^a

λb.
  val r: Ref[Int]^b = newRef[Int](b)(22)

[odersky]

Algorithm draft:

• We keep cap as an uncommitted root and add <local-cap owner> as root capabilities nested inside owner, where owner is a method or a class.
• <local-cap _root_> acts as the root capability for all static capabilities.
• Local roots for outer owners subcapture local roots for nested owners
• cap is incompatible with any local root.
• When accessing an ident x we convert outermost cap occurrences in its type to the local root of the owner in which x is defined. The conversion is explained below.
• When accessing a select E.f, we convert outermost cap occurrences in its type to the local root captured by the type of E. That root is supposed to exist.
• When type-checking a method, we enter a new level. All types of parameter symbols are converted at that level. If the computed result type captures a root in its outermost parts, it will also be at that level. On the other hand, the captured references of the body of the method can only store roots outside the method itself. In external result type of the method the local root is then converted back to cap.
• When type checking a closure from A to B, we typecheck its method. The type of the closure is then A' ->C B' where A' and B' derive from A and B by converting roots at the closure's level back to cap. This simulates adding an extra root parameter to the closure. C is the set of captured variables of the closure (which cannot contain a root at the closure's level).
• All capture sets of inferred types are come with a level. That level is the same as the level of a cap in a hypothetical explicit type at the point where the set is created.
• TermRef and ThisType capture references also have a level. For term refs, this is the level associated with their enclosing method or class (or with _root_, if the reference is static). For ThisTypes it is the level of their class.
• It is illegal to add to a capture set at level L a capture reference with a higher level than L. If that would happen, an attempt is made to widen the reference to its underlying capture set and add that set instead. If that is not possible, since one hits a local root of higher level than L, an error is emitted that a reference escapes its scope.

[odersky]

Superseded by #18463