Allow more than one existential per binder.

In a type like

  () -> (Ref^, Ref^)

we need to map the two caps to different existentially bound variables. One could do it with
two binders, like this:

  () -> (ex1: Exists) -> (ex2: Exists) -> (Ref^{ex1}, Ref^{ex2})

But that's impractical since we need to guess the number of binders needed for inferred types
where the `cap` occurrences are inferred late. We therefore keep a single binder but use annotated
types for the actual references, like this:

  () -> (ex: Exists) -> (Ref^{ex @Existential}, Ref^{ex @Existential})

Each occurrence of @Existential is a fresh annotation. Therefore, the two
capabilities in the previous example count as different.

We need to keep the distinction in one-to-one mappings between Fresh.Cap and
existentials.

TODO: Extend hidden sets and separation checking to existentials. Right now,
subtyping identifies existentials on the same level as mutually subsuming
references. This is incorrect, we need to be more precise here.

Author: odersky

compiler/src/dotty/tools/dotc/cc/CaptureOps.scala

@@ -194,8 +194,8 @@ extension (tp: Type)
    *    - annotated types that represent reach or maybe capabilities
    */
   final def isTrackableRef(using Context): Boolean = tp match
-    case _: (ThisType | TermParamRef) =>
-      true
+    case _: ThisType => true
+    case tp: TermParamRef => !Existential.isBinder(tp)
     case tp: TermRef =>
       ((tp.prefix eq NoPrefix)
       || tp.symbol.isField && !tp.symbol.isStatic && tp.prefix.isTrackableRef
@@ -205,6 +205,7 @@ extension (tp: Type)
       tp.symbol.isType && tp.derivesFrom(defn.Caps_CapSet)
     case tp: TypeParamRef =>
       tp.derivesFrom(defn.Caps_CapSet)
+    case Existential.Var(_) => true
     case AnnotatedType(parent, annot) =>
       defn.capabilityWrapperAnnots.contains(annot.symbol) && parent.isTrackableRef
     case _ =>

compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

@@ -110,7 +110,7 @@ trait CaptureRef extends TypeProxy, ValueType:
    */
   final def isMaxCapability(using Context): Boolean = this match
     case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
-    case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
+    case Existential.Var(_) => true
     case Fresh.Cap(_) => true
     case ReadOnlyCapability(tp1) => tp1.isMaxCapability
     case _ => false
@@ -228,8 +228,8 @@ trait CaptureRef extends TypeProxy, ValueType:
         case _ => false
     || this.match
         case ReachCapability(x1) => x1.subsumes(y.stripReach)
+        case Existential.Var(bv) => subsumesExistentially(bv, y)
         case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
-        case x: TermParamRef => subsumesExistentially(x, y)
         case x: TypeRef if assumedContainsOf(x).contains(y) => true
         case x: TypeRef if x.derivesFrom(defn.Caps_CapSet) =>
           x.info match

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

@@ -103,7 +103,9 @@ sealed abstract class CaptureSet extends Showable:
     elems.exists(_.stripReadOnly.isCap)
 
   final def isUnboxable(using Context) =
-    elems.exists(elem => elem.isRootCapability || Existential.isExistentialVar(elem))
+    elems.exists:
+      case Existential.Var(_) => true
+      case elem => elem.isRootCapability
 
   final def isReadOnly(using Context): Boolean =
     elems.forall(_.isReadOnly)
@@ -428,7 +430,10 @@ object CaptureSet:
 
   def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty
-    else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*))
+    else
+      for elem <- elems do
+        assert(elem.isTrackableRef, i"not a trackable ref: $elem")
+      Const(SimpleIdentitySet(elems*))
 
   def apply(elems: Refs)(using Context): CaptureSet.Const =
     if elems.isEmpty then empty else Const(elems)
@@ -563,12 +568,12 @@ object CaptureSet:
     private def levelOK(elem: CaptureRef)(using Context): Boolean =
       if elem.isRootCapability then
         !noUniversal
-      else if Existential.isExistentialVar(elem) then
-        !noUniversal
-        && !TypeComparer.isOpenedExistential(elem)
-          // Opened existentials on the left cannot be added to nested capture sets on the right
-          // of a comparison. Test case is open-existential.scala.
       else elem match
+        case Existential.Var(bv) =>
+          !noUniversal
+          && !TypeComparer.isOpenedExistential(bv)
+            // Opened existentials on the left cannot be added to nested capture sets on the right
+            // of a comparison. Test case is open-existential.scala.
         case elem: TermRef if level.isDefined =>
           elem.prefix match
             case prefix: CaptureRef =>
@@ -621,10 +626,13 @@ object CaptureSet:
         computingApprox = true
         try
           val approx = computeApprox(origin).ensuring(_.isConst)
-          if approx.elems.exists(Existential.isExistentialVar(_)) then
+          if approx.elems.exists:
+            case Existential.Var(_) => true
+            case _ => false
+          then
             ccState.approxWarnings +=
                 em"""Capture set variable $this gets upper-approximated
-                    |to existential variable from $approx, using {cap} instead."""
+                  |to existential variable from $approx, using {cap} instead."""
             universal
           else approx
         finally computingApprox = false
@@ -1169,6 +1177,8 @@ object CaptureSet:
         try pred finally seen -= ref
       else false
 
+    override def toString = "open varState"
+
   object VarState:
 
     /** A class for states that do not allow to record elements or dependent sets.
@@ -1181,6 +1191,7 @@ object CaptureSet:
       override def putElems(v: Var, refs: Refs) = false
       override def putDeps(v: Var, deps: Deps) = false
       override def isOpen = false
+      override def toString = "closed varState"
 
     /** A closed state that allows a Fresh.Cap instance to subsume a
      *  reference `r` only if `r` is already present in the hidden set of the instance.
@@ -1189,6 +1200,7 @@ object CaptureSet:
     @sharable
     object Separate extends Closed:
       override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = false
+      override def toString = "separating varState"
 
     /** A special state that turns off recording of elements. Used only
      *  in `addSub` to prevent cycles in recordings.
@@ -1199,13 +1211,15 @@ object CaptureSet:
       override def putDeps(v: Var, deps: Deps) = true
       override def rollBack(): Unit = ()
       override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = true
+      override def toString = "unrecorded varState"
 
     /** A closed state that turns off recording of hidden elements (but allows
      *  adding them). Used in `mightAccountFor`.
      */
     @sharable
     private[CaptureSet] object ClosedUnrecorded extends Closed:
       override def addHidden(hidden: HiddenSet, elem: CaptureRef)(using Context): Boolean = true
+      override def toString = "closed unrecorded varState"
 
   end VarState
 
@@ -1282,6 +1296,8 @@ object CaptureSet:
         case tp: (TypeRef | TypeParamRef) =>
           if tp.derivesFrom(defn.Caps_CapSet) then tp.captureSet
           else empty
+        case tp @ Existential.Var(_) =>
+          tp.captureSet
         case CapturingType(parent, refs) =>
           recur(parent) ++ refs
         case tp @ AnnotatedType(parent, ann) if ann.hasSymbol(defn.ReachCapabilityAnnot) =>

compiler/src/dotty/tools/dotc/cc/Existential.scala

@@ -11,7 +11,10 @@ import typer.ErrorReporting.errorType
 import Names.TermName
 import NameKinds.ExistentialBinderName
 import NameOps.isImpureFunction
+import CaptureSet.IdempotentCaptRefMap
 import reporting.Message
+import util.EqHashMap
+import util.Spans.NoSpan
 
 /**
 
@@ -229,6 +232,19 @@ object Existential:
   def apply(mk: TermParamRef => Type)(using Context): Type =
     exMethodType(mk).toFunctionType(alwaysDependent = true)
 
+  /** The (super-) type of existentially bound references */
+  type Var = AnnotatedType
+
+  /** An extractor for existentially bound references of the form ex @existential
+   *  where ex is a TermParamRef of type Exists
+   */
+  object Var:
+    def apply(boundVar: TermParamRef)(using Context): Var =
+      AnnotatedType(boundVar, Annotation(defn.ExistentialAnnot, NoSpan))
+    def unapply(tp: Var)(using Context): Option[TermParamRef] = tp match
+      case AnnotatedType(bv: TermParamRef, ann) if ann.symbol == defn.ExistentialAnnot => Some(bv)
+      case _ => None
+
   /** Create existential if bound variable appears in result of `mk` */
   def wrap(mk: TermParamRef => Type)(using Context): Type =
     val mt = exMethodType(mk)
@@ -242,10 +258,23 @@ object Existential:
       case _ =>
         core
 
+  /** Map existentially bound references referring to `boundVar` one-to-one
+   *  to Fresh.Cap instances
+   */
+  def boundVarToCap(boundVar: TermParamRef, tp: Type)(using Context) =
+    val subst = new IdempotentCaptRefMap:
+      val seen = EqHashMap[Annotation, CaptureRef]()
+      def apply(t: Type): Type = t match
+        case t @ Var(`boundVar`) =>
+          seen.getOrElseUpdate(t.annot, Fresh.Cap(NoSymbol))
+        case _ =>
+          mapOver(t)
+    subst(tp)
+
   /** Map top-level existentials to `Fresh.Cap`. */
   def toCap(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match
     case Existential(boundVar, unpacked) =>
-      unpacked.substParam(boundVar, Fresh.Cap(NoSymbol))
+      boundVarToCap(boundVar, unpacked)
     case tp1 @ CapturingType(parent, refs) =>
       tp1.derivedCapturingType(toCap(parent), refs)
     case tp1 @ AnnotatedType(parent, ann) =>
@@ -256,7 +285,7 @@ object Existential:
    */
   def toCapDeeply(tp: Type)(using Context): Type = tp.dealiasKeepAnnots match
     case Existential(boundVar, unpacked) =>
-      toCapDeeply(unpacked.substParam(boundVar, Fresh.Cap(NoSymbol)))
+      toCapDeeply(boundVarToCap(boundVar, unpacked))
     case tp1 @ FunctionOrMethod(args, res) =>
       val tp2 = tp1.derivedFunctionOrMethod(args, toCapDeeply(res))
       if tp2 ne tp1 then tp2 else tp
@@ -293,11 +322,13 @@ object Existential:
           super.mapOver(t)
 
     class Wrap(boundVar: TermParamRef) extends CapMap:
+      private val seen = EqHashMap[CaptureRef, Var]()
+
       def apply(t: Type) = t match
-        case t: CaptureRef if t.isCapOrFresh => // !!! we should map different fresh refs to different existentials
+        case t: CaptureRef if t.isCapOrFresh =>
           if variance > 0 then
             needsWrap = true
-            boundVar
+            seen.getOrElseUpdate(t, Var(boundVar))
           else
             if variance == 0 then
               fail(em"""$tp captures the root capability `cap` in invariant position""")
@@ -310,16 +341,27 @@ object Existential:
           if variance > 0 then
             needsWrap = true
             super.mapOver:
-              defn.FunctionNOf(args, res, contextual).capturing(boundVar.singletonCaptureSet)
+              defn.FunctionNOf(args, res, contextual)
+                .capturing(Var(boundVar).singletonCaptureSet)
           else mapOver(t)
         case _ =>
           mapOver(t)
         //.showing(i"mapcap $t = $result")
 
       lazy val inverse = new BiTypeMap:
-        lazy val freshCap = Fresh.Cap(NoSymbol)
         def apply(t: Type) = t match
-          case t: TermParamRef if t eq boundVar => freshCap
+          case t @ Var(`boundVar`) =>
+            // do a reverse getOrElseUpdate on `seen` to produce the
+            // `Fresh.Cap` assosicated with `t`
+            val it = seen.iterator
+            var ref: CaptureRef | Null = null
+            while it.hasNext && ref == null do
+              val (k, v) = it.next
+              if v.annot eq t.annot then ref = k
+            if ref == null then
+              ref = Fresh.Cap(NoSymbol)
+              seen(ref) = t
+            ref
           case _ => mapOver(t)
         def inverse = Wrap.this
         override def toString = "Wrap.inverse"
@@ -359,8 +401,8 @@ object Existential:
     case (info: TypeRef) :: rest => info.symbol == defn.Caps_Exists && rest.isEmpty
     case _ => false
 
-  /** Is `ref` this an existentially bound variable? */
-  def isExistentialVar(ref: CaptureRef)(using Context) = ref match
+  /** Is `ref` a TermParamRef representing existentially bound variables? */
+  def isBinder(ref: CaptureRef)(using Context) = ref match
     case ref: TermParamRef => isExistentialMethod(ref.binder)
     case _ => false
 

compiler/src/dotty/tools/dotc/cc/Setup.scala

@@ -376,7 +376,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
                 checkSharedOK:
                   CapturingType(parent2, ann.tree.toCaptureSet)
               catch case ex: IllegalCaptureRef =>
-                report.error(em"Illegal capture reference: ${ex.getMessage.nn}", tptToCheck.srcPos)
+                if !tptToCheck.isEmpty then
+                  report.error(em"Illegal capture reference: ${ex.getMessage.nn}", tptToCheck.srcPos)
                 parent2
             else if ann.symbol == defn.UncheckedCapturesAnnot then
               makeUnchecked(apply(parent))
@@ -917,7 +918,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     var retained = ann.retainedElems.toArray
     for i <- 0 until retained.length do
       val refTree = retained(i)
-      for ref <- refTree.toCaptureRefs do
+      val refs =
+        try refTree.toCaptureRefs
+        catch case ex: IllegalCaptureRef =>
+          report.error(em"Illegal capture reference: ${ex.getMessage.nn}", refTree.srcPos)
+          Nil
+      for ref <- refs do
         def pos =
           if refTree.span.exists then refTree.srcPos
           else if ann.span.exists then ann.srcPos

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1071,6 +1071,7 @@ class Definitions {
   @tu lazy val UseAnnot:  ClassSymbol = requiredClass("scala.caps.use")
   @tu lazy val ConsumeAnnot:  ClassSymbol = requiredClass("scala.caps.consume")
   @tu lazy val RefineOverrideAnnot:  ClassSymbol = requiredClass("scala.caps.refineOverride")
+  @tu lazy val ExistentialAnnot:  ClassSymbol = requiredClass("scala.caps.existential")
   @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
   @tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature")
   @tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -2840,14 +2840,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     def canInstantiateWith(assoc: ExAssoc): Boolean = assoc match
       case (bv, bvs) :: assoc1 =>
         if bv == tp1 then
-          !Existential.isExistentialVar(tp2)
-          || bvs.contains(tp2)
-          || assoc1.exists(_._1 == tp2)
+          tp2 match
+            case Existential.Var(bv2) =>
+              bvs.contains(bv2) || assoc1.exists(_._1 == bv2)
+            case _ =>
+              true
         else
           canInstantiateWith(assoc1)
       case Nil =>
         false
-    Existential.isExistentialVar(tp1) && canInstantiateWith(assocExistentials)
+    tp2 match
+      case Existential.Var(bv2) if tp1 eq bv2 =>
+        true // for now, existential references referring to the same
+             // binder are identified. !!! TODO this needs to be revised
+      case _ =>
+        canInstantiateWith(assocExistentials)
 
   def isOpenedExistential(ref: CaptureRef)(using Context): Boolean =
     openedExistentials.contains(ref)
@@ -2864,7 +2871,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         .showing(i"existential match not found for $t in $assoc", capt)
 
     def apply(t: Type) = t match
-      case t: TermParamRef if Existential.isExistentialVar(t) =>
+      case t: TermParamRef if Existential.isBinder(t) =>
         // Find outermost existential on the right that can be instantiated to `t`,
         // or `badExistential` if none exists.
         def findMapped(assoc: ExAssoc): CaptureRef = assoc match
@@ -2884,7 +2891,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
      */
     lazy val inverse = new BiTypeMap:
       def apply(t: Type) = t match
-        case t: TermParamRef if Existential.isExistentialVar(t) =>
+        case t: TermParamRef if Existential.isBinder(t) =>
           assoc.find(_._1 == t) match
             case Some((_, bvs)) if bvs.nonEmpty => bvs.head
             case _ => bad(t)
@@ -3980,7 +3987,7 @@ class ExplainingTypeComparer(initctx: Context, short: Boolean) extends TypeCompa
     }
 
   override def subCaptures(refs1: CaptureSet, refs2: CaptureSet, vs: CaptureSet.VarState)(using Context): CaptureSet.CompareResult =
-    traceIndented(i"subcaptures $refs1 <:< $refs2, varState = ${vs.toString}") {
+    traceIndented(i"subcaptures $refs1 <:< $refs2 in ${vs.toString}") {
       super.subCaptures(refs1, refs2, vs)
     }
 

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -6082,7 +6082,7 @@ object Types extends TypeUtils {
         case tp: TypeAlias =>
           ensureTrackable(tp.alias)
         case _ =>
-          assert(false, i"not a trackable captureRef ref: $result, ${result.underlyingIterator.toList}")
+          assert(false, i"not a trackable CaptureRef: $result with underlying ${result.underlyingIterator.toList}")
       ensureTrackable(result)
 
     /** A restriction of the inverse to a function on tracked CaptureRefs */

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -441,6 +441,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case ReadOnlyCapability(tp1) => toTextCaptureRef(tp1) ~ ".rd"
       case ReachCapability(tp1) => toTextCaptureRef(tp1) ~ "*"
       case MaybeCapability(tp1) => toTextCaptureRef(tp1) ~ "?"
+      case Existential.Var(bv) => toTextRef(bv)
       case Fresh.Cap(hidden) =>
         val idStr = if showUniqueIds then s"#${hidden.id}" else ""
         if printFreshDetailed then s"<cap$idStr hiding " ~ toTextCaptureSet(hidden) ~ ">"

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -19,7 +19,6 @@ import typer.ErrorReporting.{Addenda, NothingToAdd}
 import config.Printers.recheckr
 import util.Property
 import StdNames.nme
-import reporting.trace
 import annotation.constructorOnly
 import cc.CaptureSet.IdempotentCaptRefMap
 import annotation.tailrec