Introduce maybe capabilities x?

Introduce maybe capabilities x? to handle the case where a capture set
appears invariantly in its surrounding type.

Maybe capabilities are similar to TypeBounds types, but
restricted to capture sets. For instance,

     Array[C^{x?}]

should be morally equivaelent to

     Array[_ >: C^{} <: C^{x}]

but it has fewer issues with type inference.

Author: odersky

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

@@ -220,9 +220,31 @@ extension (tp: Type)
    *  type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
    *  are unrelated.
    */
-  def reach(using Context): CaptureRef =
-    assert(tp.isTrackableRef)
-    AnnotatedType(tp, Annotation(defn.ReachCapabilityAnnot, util.Spans.NoSpan))
+  def reach(using Context): CaptureRef = tp match
+    case tp: CaptureRef if tp.isTrackableRef =>
+      if tp.isReach then tp else ReachCapability(tp)
+
+  /** If `x` is a capture ref, its maybe capability `x?`, represented internally
+   *  as `x @maybeCapability`. `x?` stands for a capability `x` that might or might
+   *  not be part of a capture set. We have `{} <: {x?} <: {x}`. Maybe capabilities
+   *  cannot be propagated between sets. If `a <: b` and `a` acquires `x?` then
+   *  `x` is propagated to `b` as a conservative approximation.
+   *
+   *  Maybe capabilities should only arise for caoture sets that appear in invariant
+   *  position in their surrounding type. They are similar to TypeBunds types, but
+   *  restricted to capture sets. For instance,
+   *
+   *      Array[C^{x?}]
+   *
+   *  should be morally equivaelent to
+   *
+   *      Array[_ >: C^{} <: C^{x}]
+   *
+   *   but it has fewer issues with type inference. 
+   */
+  def maybe(using Context): CaptureRef = tp match
+    case tp: CaptureRef if tp.isTrackableRef =>
+      if tp.isMaybe then tp else MaybeCapability(tp)
 
   /** If `ref` is a trackable capture ref, and `tp` has only covariant occurrences of a
    *  universal capture set, replace all these occurrences by `{ref*}`. This implements
@@ -422,9 +444,14 @@ object ReachCapabilityApply:
 /** An extractor for `ref @annotation.internal.reachCapability`, which is used to express
  *  the reach capability `ref*` as a type.
  */
-object ReachCapability:
+class AnnotatedCapability(annot: Context ?=> ClassSymbol):
+  def apply(tp: Type)(using Context) =
+    AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
   def unapply(tree: AnnotatedType)(using Context): Option[SingletonCaptureRef] = tree match
-    case AnnotatedType(parent: SingletonCaptureRef, ann)
-    if ann.symbol == defn.ReachCapabilityAnnot => Some(parent)
+    case AnnotatedType(parent: SingletonCaptureRef, ann) if ann.symbol == annot => Some(parent)
     case _ => None
 
+object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
+object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot)
+
+

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

@@ -145,15 +145,16 @@ sealed abstract class CaptureSet extends Showable:
 
   /** x subsumes x
    *   this subsumes this.f
-   *   x subsumes y  ==>  x* subsumes y
-   *   x subsumes y  ==>  x* subsumes y*
+   *   x subsumes y  ==>  x* subsumes y, x subsumes y?
+   *   x subsumes y  ==>  x* subsumes y*, x? subsumes y?
    */
   extension (x: CaptureRef)
      private def subsumes(y: CaptureRef)(using Context): Boolean =
       (x eq y)
       || x.isRootCapability
       || y.match
-          case y: TermRef => !y.isReach && (y.prefix eq x)
+          case y: TermRef => y.prefix eq x
+          case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
           case _ => false
       || x.match
           case ReachCapability(x1) => x1.subsumes(y.stripReach)
@@ -312,6 +313,8 @@ sealed abstract class CaptureSet extends Showable:
   def substParams(tl: BindingType, to: List[Type])(using Context) =
     map(Substituters.SubstParamsMap(tl, to))
 
+  def maybe(using Context): CaptureSet = map(MaybeMap())
+
   /** Invoke handler if this set has (or later aquires) the root capability `cap` */
   def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
     if isUniversal then handler()
@@ -445,6 +448,8 @@ object CaptureSet:
     def isConst = isSolved
     def isAlwaysEmpty = false
 
+    def isMaybeSet = false // overridden in BiMapped
+
     /** A handler to be invoked if the root reference `cap` is added to this set */
     var rootAddedHandler: () => Context ?=> Unit = () => ()
 
@@ -490,9 +495,10 @@ object CaptureSet:
         if elem.isRootCapability then
           rootAddedHandler()
         newElemAddedHandler(elem)
+        val normElem = if isMaybeSet then elem else elem.stripMaybe
         // assert(id != 5 || elems.size != 3, this)
         val res = (CompareResult.OK /: deps): (r, dep) =>
-          r.andAlso(dep.tryInclude(elem, this))
+          r.andAlso(dep.tryInclude(normElem, this))
         res.orElse:
           elems -= elem
           res.addToTrace(this)
@@ -508,6 +514,8 @@ object CaptureSet:
           levelLimit.isContainedIn(elem.cls.levelOwner)
         case ReachCapability(elem1) =>
           levelOK(elem1)
+        case MaybeCapability(elem1) =>
+          levelOK(elem1)
         case _ =>
           true
 
@@ -760,6 +768,7 @@ object CaptureSet:
       if source eq origin then supApprox.map(bimap.inverse)
       else source.upperApprox(this).map(bimap) ** supApprox
 
+    override def isMaybeSet: Boolean = bimap.isInstanceOf[MaybeMap]
     override def toString = s"BiMapped$id($source, elems = $elems)"
   end BiMapped
 
@@ -840,8 +849,7 @@ object CaptureSet:
       upper.isAlwaysEmpty || upper.isConst && upper.elems.size == 1 && upper.elems.contains(r1)
     if variance > 0 || isExact then upper
     else if variance < 0 then CaptureSet.empty
-    else if ctx.mode.is(Mode.Printing) then upper
-    else assert(false, i"trying to add $upper from $r via ${tm.getClass} in a non-variant setting")
+    else upper.maybe
 
   /** Apply `f` to each element in `xs`, and join result sets with `++` */
   def mapRefs(xs: Refs, f: CaptureRef => CaptureSet)(using Context): CaptureSet =
@@ -980,6 +988,26 @@ object CaptureSet:
   /** The current VarState, as passed by the implicit context */
   def varState(using state: VarState): VarState = state
 
+  /** Maps `x` to `x?` */
+  private class MaybeMap(using Context) extends BiTypeMap:
+
+    def apply(t: Type) = t match
+      case t: CaptureRef if t.isTrackableRef => t.maybe
+      case _ => mapOver(t)
+
+    override def toString = "Maybe"
+
+    lazy val inverse = new BiTypeMap:
+
+      def apply(t: Type) = t match
+        case t: CaptureRef if t.isMaybe => t.stripMaybe
+        case t => mapOver(t)
+
+      def inverse = MaybeMap.this
+
+      override def toString = "Maybe.inverse"
+  end MaybeMap
+
   /* Not needed:
   def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
     CaptureSet.empty

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

@@ -68,11 +68,6 @@ object CheckCaptures:
    */
   final class SubstParamsMap(from: BindingType, to: List[Type])(using Context)
   extends ApproximatingTypeMap, IdempotentCaptRefMap:
-    /** This SubstParamsMap is exact if `to` only contains `CaptureRef`s. */
-    private val isExactSubstitution: Boolean = to.forall(_.isTrackableRef)
-
-    /** As long as this substitution is exact, there is no need to create `Range`s when mapping invariant positions. */
-    override protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = !isExactSubstitution
 
     def apply(tp: Type): Type =
       tp match

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

@@ -1054,6 +1054,7 @@ class Definitions {
   @tu lazy val FunctionalInterfaceAnnot: ClassSymbol = requiredClass("java.lang.FunctionalInterface")
   @tu lazy val TargetNameAnnot: ClassSymbol = requiredClass("scala.annotation.targetName")
   @tu lazy val VarargsAnnot: ClassSymbol = requiredClass("scala.annotation.varargs")
+  @tu lazy val MaybeCapabilityAnnot = requiredClass("scala.annotation.internal.maybeCapability")
   @tu lazy val ReachCapabilityAnnot = requiredClass("scala.annotation.internal.reachCapability")
   @tu lazy val RequiresCapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.internal.requiresCapability")
   @tu lazy val RetainsAnnot: ClassSymbol = requiredClass("scala.annotation.retains")

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

@@ -540,18 +540,6 @@ object TypeOps:
         val sym = tp.symbol
         forbidden.contains(sym)
 
-      /** We need to split the set into upper and lower approximations
-       *  only if it contains a local element. The idea here is that at the
-       *  time we perform an `avoid` all local elements are already accounted for
-       *  and no further elements will be added afterwards. So we can just keep
-       *  the set as it is. See comment by @linyxus on #16261.
-       */
-      override def needsRangeIfInvariant(refs: CaptureSet): Boolean =
-        refs.elems.exists {
-          case ref: TermRef => toAvoid(ref)
-          case _ => false
-        }
-
       override def apply(tp: Type): Type = tp match
         case tp: TypeVar if mapCtx.typerState.constraint.contains(tp) =>
           val lo = TypeComparer.instanceType(

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

@@ -2200,7 +2200,11 @@ object Types extends TypeUtils {
     /** Is this a reach reference of the form `x*`? */
     def isReach(using Context): Boolean = false // overridden in AnnotatedType
 
+    /** Is this a maybe reference of the form `x?`? */
+    def isMaybe(using Context): Boolean = false // overridden in AnnotatedType
+
     def stripReach(using Context): CaptureRef = this // overridden in AnnotatedType
+    def stripMaybe(using Context): CaptureRef = this // overridden in AnnotatedType
 
     /** Is this reference the generic root capability `cap` ? */
     def isRootCapability(using Context): Boolean = false
@@ -5620,14 +5624,21 @@ object Types extends TypeUtils {
     }
 
     override def isTrackableRef(using Context) =
-      isReach && parent.isTrackableRef
+      (isReach || isMaybe) && parent.isTrackableRef
 
     /** Is this a reach reference of the form `x*`? */
     override def isReach(using Context): Boolean =
       annot.symbol == defn.ReachCapabilityAnnot
 
-    override def stripReach(using Context): SingletonCaptureRef =
-      (if isReach then parent else this).asInstanceOf[SingletonCaptureRef]
+    /** Is this a reach reference of the form `x*`? */
+    override def isMaybe(using Context): Boolean =
+      annot.symbol == defn.MaybeCapabilityAnnot
+
+    override def stripReach(using Context): CaptureRef =
+      if isReach then parent.asInstanceOf[CaptureRef] else this
+
+    override def stripMaybe(using Context): CaptureRef =
+      if isMaybe then parent.asInstanceOf[CaptureRef] else this
 
     override def normalizedRef(using Context): CaptureRef =
       if isReach then AnnotatedType(stripReach.normalizedRef, annot) else this
@@ -6477,15 +6488,6 @@ object Types extends TypeUtils {
             tp.derivedLambdaType(tp.paramNames, formals, restpe)
       }
 
-    /** Overridden in TypeOps.avoid and in CheckCaptures.substParamsMap */
-    protected def needsRangeIfInvariant(refs: CaptureSet): Boolean = true
-
-    override def mapCapturingType(tp: Type, parent: Type, refs: CaptureSet, v: Int): Type =
-      if v == 0 && needsRangeIfInvariant(refs) /* && false*/ then
-        range(mapCapturingType(tp, parent, refs, -1), mapCapturingType(tp, parent, refs, 1))
-      else
-        super.mapCapturingType(tp, parent, refs, v)
-
     protected def reapply(tp: Type): Type = apply(tp)
   }
 

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

@@ -15,7 +15,7 @@ import util.SourcePosition
 import scala.util.control.NonFatal
 import scala.annotation.switch
 import config.{Config, Feature}
-import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, isBoxed, levelOwner, retainedElems}
+import cc.{CapturingType, RetainingType, CaptureSet, ReachCapability, MaybeCapability, isBoxed, levelOwner, retainedElems}
 
 class PlainPrinter(_ctx: Context) extends Printer {
 
@@ -404,6 +404,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
       case tp: TermRef if tp.symbol == defn.captureRoot => Str("cap")
       case tp: SingletonType => toTextRef(tp)
       case ReachCapability(tp1) => toTextRef(tp1) ~ "*"
+      case MaybeCapability(tp1) => toTextRef(tp1) ~ "?"
       case _ => toText(tp)
 
   protected def isOmittablePrefix(sym: Symbol): Boolean =

library/src/scala/annotation/internal/maybeCapability.scala

@@ -0,0 +1,8 @@
+package scala.annotation
+package internal
+
+/** An annotation that marks a capture ref as a maybe capability.
+ *  `x?` is encoded as `x.type @maybeCapability`
+ */
+class maybeCapability extends StaticAnnotation
+

library/src/scala/annotation/internal/reach.scala renamed to library/src/scala/annotation/internal/reachCapability.scala

@@ -160,8 +160,8 @@ trait IterableFactory[+CC[_]] extends Serializable, Pure {
     *  @param   elem the element computation
     *  @return  A $coll that contains the results of `n1 x n2` evaluations of `elem`.
     */
-  def fill[A](n1: Int, n2: Int)(elem: => A): CC[CC[A] @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
-  	??? // fill(n1)(fill(n2)(elem))
+  def fill[A](n1: Int, n2: Int)(elem: => A): CC[(CC[A]^{elem}) @uncheckedVariance]^{elem} =
+  	fill[CC[A]^{elem}](n1)(fill(n2)(elem)) // !!! explicit type argument required under cc
 
   /** Produces a three-dimensional $coll containing the results of some element computation a number of times.
     *  @param   n1  the number of elements in the 1st dimension
@@ -170,8 +170,8 @@ trait IterableFactory[+CC[_]] extends Serializable, Pure {
     *  @param   elem the element computation
     *  @return  A $coll that contains the results of `n1 x n2 x n3` evaluations of `elem`.
     */
-  def fill[A](n1: Int, n2: Int, n3: Int)(elem: => A): CC[CC[CC[A]] @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
-    ??? // fill(n1)(fill(n2, n3)(elem)).unsafeAssumePure
+  def fill[A](n1: Int, n2: Int, n3: Int)(elem: => A): CC[(CC[CC[A]^{elem}]^{elem}) @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
+    fill[CC[CC[A]^{elem}]^{elem}](n1)(fill(n2, n3)(elem)) // !!! explicit type argument required under cc
 
   /** Produces a four-dimensional $coll containing the results of some element computation a number of times.
     *  @param   n1  the number of elements in the 1st dimension
@@ -181,8 +181,8 @@ trait IterableFactory[+CC[_]] extends Serializable, Pure {
     *  @param   elem the element computation
     *  @return  A $coll that contains the results of `n1 x n2 x n3 x n4` evaluations of `elem`.
     */
-  def fill[A](n1: Int, n2: Int, n3: Int, n4: Int)(elem: => A): CC[CC[CC[CC[A]]] @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
-    ??? // fill(n1)(fill(n2, n3, n4)(elem))
+  def fill[A](n1: Int, n2: Int, n3: Int, n4: Int)(elem: => A): CC[(CC[CC[CC[A]^{elem}]^{elem}]^{elem}) @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
+    fill[CC[CC[CC[A]^{elem}]^{elem}]^{elem}](n1)(fill(n2, n3, n4)(elem)) // !!! explicit type argument required under cc
 
   /** Produces a five-dimensional $coll containing the results of some element computation a number of times.
     *  @param   n1  the number of elements in the 1st dimension
@@ -193,8 +193,9 @@ trait IterableFactory[+CC[_]] extends Serializable, Pure {
     *  @param   elem the element computation
     *  @return  A $coll that contains the results of `n1 x n2 x n3 x n4 x n5` evaluations of `elem`.
     */
-  def fill[A](n1: Int, n2: Int, n3: Int, n4: Int, n5: Int)(elem: => A): CC[CC[CC[CC[CC[A]]]] @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
-    ??? // fill(n1)(fill(n2, n3, n4, n5)(elem))
+  def fill[A](n1: Int, n2: Int, n3: Int, n4: Int, n5: Int)(elem: => A): CC[(CC[CC[CC[CC[A]^{elem}]^{elem}]^{elem}]^{elem}) @uncheckedVariance]^{elem} = // !!! problem with checking rhs under cc
+    fill[CC[CC[CC[CC[A]^{elem}]^{elem}]^{elem}]^{elem}](n1)(fill(n2, n3, n4, n5)(elem)) // !!! explicit type argument required under cc
+
 
   /** Produces a $coll containing values of a given function over a range of integer values starting from 0.
     *  @param  n   The number of elements in the $coll