Canonicalize capture variable subtype comparisons

[bracevac]

Fixes #22103

Subtype problems where at least one side is a type variable representing a capture variable are canonicalized to capturing type comparisons on the special CapSet for the universe capture sets. For example, C <: CapSet^{C^} becomes CapSet^{C^} <: CapSet^{C^}, and A <: B becomes CapSet^{A^} <: CapSet^{B^} if both A and B are capture variables.

Supersedes #22183 and #22289. This solution is overall cleaner and does not require adding a new bit to the TypeComparer's ApproxState.

TODOs/Issues/Questions:

• Fix extension method in test cc-poly-varargs.scala. Currently causes an infinite regress.
  • Fix the aftermath
    • tests/neg-custom-args/captures/lazylists-exceptions.scala
    • tests/neg-custom-args/captures/exceptions.scala
    • tests/neg-custom-args/captures/real-try.scala
    • tests/run-custom-args/captures/colltest5
• Some negative cases in test capture-vars-subtyping.scala pass: D <: E fails, but its canonicalized form CapSet^{D^} <: CapSet^{E^} now succeeds. Potential problem in the subcapturing implementation.
• Extend to intersection/unions def f[C^, D^, E <: C | D, F <: C & D](...) = ... etc. Lacking good uses cases, not planned right now.
• If we have C^ declared in the current context, should there be a difference between C vs. C^ for subsequent mentions? We currently do, but seems a bit too subtle for users. Will be addressed by a new scheme for declaring capture variables using context bounds.

[bracevac]

Moved to dotty @odersky

[bracevac]

Notes on the extension-method problem:

The example in cc-poly-varargs.scala seems to loop infinitely on extrapolateCaptureRef in CaptureSet.scala.

However, a simpler version of it does not diverge, but reveals another problem (not clear if it is related):

import language.experimental.captureChecking

abstract class Source[+T, Cap^] 

extension [T, Cap^](src: Source[T, Cap]^)
  def transformValuesWith[U](f: (T -> U)^{Cap^}): Source[U, Cap]^{src, f} = ???

def simpler[T, Cap^](src: Source[T, Cap]^{Cap^}): Source[T, Cap]^{Cap^} = // <- need to annotate the explicit return type, otherwise error
  src.transformValuesWith(identity)

If we leave out the return type of simpler, we get the error

-- [E007] Type Mismatch Error: local/cc-poly-varargs.scala:12:74 ---------------
12 |def simpler[T, Cap^](src: Source[T, Cap]^{Cap^}) = src.transformValuesWith(identity)
   |                                                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |         Found:    Source[box T^?, caps.CapSet^{Cap^}]^{src}
   |         Required: Source[T, caps.CapSet]
   |
   |         Note that the expected type Source[T, caps.CapSet]
   |         is the previously inferred result type of method simpler
   |         which is also the type seen in separately compiled sources.
   |         The new inferred type Source[box T^?, caps.CapSet^{Cap^}]^{src}
   |         must conform to this type.
   |
   | longer explanation available when compiling with `-explain`

Edit: It looks like the initial problem that we had with race.

Edit2: This seems to be the expected behavior, we need to annotate the return type if it's impure.

[bracevac]

A simpler example that exhibits the divergence:

import language.experimental.captureChecking

abstract class Source[+T, Cap^] 

def id[T, Cap^](src: Source[T, Cap]^): Source[T, Cap]^{src} = src
def promote[T, Cap^](src: Source[T, Cap]^{Cap^}): Source[T, Cap]^{Cap^} = src

def fun[T, Cap^](src: Source[T, Cap]^{Cap^}): Source[T, Cap]^{Cap^} =
  val res = id(src)
  promote(res)

Applying promote causes res to appear deeply in Source[T, CapSet^{Cap^,res}], and TypeOps.avoid gets hung up on that when removing res.
With the latest fix, we get it to terminate and can obtain an -Xprint:cc that clearly shows this:

...
def fun[T, Cap >: caps.CapSet <: caps.CapSet^](src: Source[T, Cap]^{Cap^}):
      Source[T, Cap]^{Cap^} =
      {
        val res: Source[box T^?, caps.CapSet^{Cap^, res}]^{src} =
          id[box T^?, caps.CapSet^{Cap^, res}](src)
        promote[box T^?, caps.CapSet^{res, Cap^}](res)
      }

We already have a cyclic reference at res: Source[box T^?, caps.CapSet^{Cap^, res}]^{src}!

But even with an explicit ascription

val res: Source[T, Cap]^{src} = ...

the last line will still carry res

def fun[T, Cap >: caps.CapSet <: caps.CapSet^](src: Source[T, Cap]^{Cap^}):
      Source[T, Cap]^{Cap^} =
      {
        val res: Source[T, Cap]^{src} = id[box T^?, caps.CapSet^{Cap^}](src)
        promote[box T^?, caps.CapSet^{res, Cap^}](res)
      }

[bracevac]

Part of the problem seems to stem from subsumes: Cap does not subsume res in the implementation, but should it not hold because res reaches src which reaches Cap?

[odersky]

Nice that the problem in AvoidMap got solved by the changes in subsumes. The changes make sense. I'd like to understand better why the AvoidMap problem poppsed up without these changes.

[odersky]

Also maybe squash the commits, since they tried several things that got reverted afterwards?

[odersky]

I squashed all the commits into one. Will push some polishing changes on top.

[noti0na1]

Why does this condition check this instead of info?

[noti0na1]

The case here does not look currect for me.viaInfo is used only if there is some equivalent relation from singleton types.

[bracevac]

It's tailored to the case that we want to check that a term variable reaches a capture variable (resp. the capture variable subsumes the term variable, so we check the this), because of the issue outlined in
#22299 (comment)
Not sure if this is best place to do it, but logically we have to chase along the infos of the context entries. The case y: TermRef if !y.isRootCapability => part will invoke this function as a last resort, and since we have to follow the info then, we might as well do it here.

Feel free to open a new PR if you see a better way to do it.

[noti0na1]

In theory, we should never have an instance of CapSet. I don't think we need to test CapSet^{C^, c}, a singleton c with type CapSet inside a capture set. Because this is confusing to handle whether a CaptureRef is representing a value or its underlying capture set.

[bracevac]

The point of this is to test subtyping relations between capture sets. The term bindings are a crutch. Back then I could not do it in the "obvious" way using e.g. summon[C <:< CapSet^{C^}], because resolution happens before capture checking.

[noti0na1]

I think the assignments are fine to test. I mean the c inside the capture set.