Things to do for separation checking

[odersky]

#22539 is a first prototype for separation checking. But it is quite incomplete, many things remain to do until this is something we can merge and release, even if it's only under an experimental language import. Here's a todo list:

• Separation checking for class members. We need to assure the following: If we have a class with two members (defined or inherited) that both contain fresh references, then these references are separate in all instances.
• Separation checking for type variables. Clarify what the rules should be. Are types referring to type variables always assumed to be separate from what we can see elsewhere? If yes, what conditions need to be enforced at type application sites. If not, how do we define separation status of type variables.
• Separation checking for capture set variables. Same as previous issue, but for capture set variables instead of type variables.
• Handle pattern matching and non-recursive ADTs. We know how to handle product types and path selection. But what about sums of products? These are not selected directly using paths, but need a pattern matching step beforehand.
• Separation checking for existentials. The subtype theory of existentials currently does not take separation into account. What needs to be done to assure separation? Might be superseded by next issue.
• Uniform representation of maximal capabilities. Right now maximal capabilities appear in three forms depending on where they are used:
  - As caps.cap instances, initially and in parameters,
  - As Fresh.Cap instances, to track hidden sets in the current scope,
  - As existentially bound variables (which currently don't have hidden sets, so no separation checking is possible.
  It would be good to find a more uniform representation, so fewer conversions would be necessary and code could become simpler. Maybe settle on Fresh.Cap with an additional field that indicates to which method result type they are tied? Not sure our type handling infrastructure would support such a thing already.
• Handle nested expressions with fresh capturesets. Right now we cannot write Pair(Ref(), Ref()) since that would instantiate Pair's type parameters with types referring to cap. We have to write { val r1 = Ref(); val r2 = Ref(); Pair(r1, r2) } instead. To overcome this restriction, we could try to skolemize types of nested expressions. Or we manage to lift the restrictions on type parameter instantiation to some degree.
• Update design document in Separation checking for product types #22539 to reflect current code. Right now it is outdated.
• Update doc page for capture checking., in general and specifically to include separation.
  • Update Capture Checking Language Reference #22041
• Implement "read-only" qualifier for mutable types. Right now we need an explicitly declared supertype such as ReadOnlyMatrix of Matrix to be able to establish read-only access.

We should track completion of issues here and add more issues as they come up.