Implement boxing for singleton type arguments

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

@@ -203,6 +203,39 @@ extension (tp: Type)
     case _ =>
       tp
 
+  /** If `tp` is an unboxed capturing type or a function returning an unboxed capturing type,
+   *  convert it to be boxed.
+   */
+  def boxDeeply(using Context): Type =
+    def recur(tp: Type): Type = tp.dealiasKeepAnnotsAndOpaques match
+      case tp @ CapturingType(parent, refs) =>
+        if tp.isBoxed || parent.derivesFrom(defn.Caps_CapSet) then tp
+        else tp.boxed
+      case tp @ AnnotatedType(parent, ann) =>
+        if ann.symbol.isRetains && !parent.derivesFrom(defn.Caps_CapSet)
+        then CapturingType(parent, ann.tree.toCaptureSet, boxed = true)
+        else tp.derivedAnnotatedType(parent.boxDeeply, ann)
+      case tp: (Capability & SingletonType) if tp.isTrackableRef && !tp.isAlwaysPure =>
+        recur(CapturingType(tp, CaptureSet(tp)))
+      case tp1 @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp1) =>
+        val res = args.last
+        val boxedRes = recur(res)
+        if boxedRes eq res then tp
+        else tp1.derivedAppliedType(tycon, args.init :+ boxedRes)
+      case tp1 @ defn.RefinedFunctionOf(rinfo: MethodType) =>
+        val boxedRinfo = recur(rinfo)
+        if boxedRinfo eq rinfo then tp
+        else boxedRinfo.toFunctionType(alwaysDependent = true)
+      case tp1: MethodOrPoly =>
+        val res = tp1.resType
+        val boxedRes = recur(res)
+        if boxedRes eq res then tp
+        else tp1.derivedLambdaType(resType = boxedRes)
+      case _ => tp
+    tp match
+      case tp: MethodOrPoly => tp // don't box results of methods outside refinements
+      case _ => recur(tp)
+
   /** The capture set consisting of all top-level captures of `tp` that appear under a box.
    *  Unlike for `boxed` this also considers parents of capture types, unions and
    *  intersections, and type proxies other than abstract types.
@@ -621,9 +654,12 @@ object ContainsImpl:
 object ContainsParam:
   def unapply(sym: Symbol)(using Context): Option[(TypeRef, Capability)] =
     sym.info.dealias match
-      case AppliedType(tycon, (cs: TypeRef) :: (ref: Capability) :: Nil)
+      case AppliedType(tycon, (cs: TypeRef) :: arg2 :: Nil)
       if tycon.typeSymbol == defn.Caps_ContainsTrait
-          && cs.typeSymbol.isAbstractOrParamType => Some((cs, ref))
+          && cs.typeSymbol.isAbstractOrParamType =>
+        arg2.stripCapturing match // ref.type was converted to box ref.type^{ref} by boxing
+          case ref: Capability => Some((cs, ref))
+          case _ => None
       case _ => None
 
 /** A class encapsulating the assumulator logic needed for `CaptureSet.ofTypeDeeply`

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

@@ -684,6 +684,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       //   - the selection is either a trackable capture reference or a pure type
       if noWiden(selType, pt)
           || qualType.isBoxedCapturing
+          || selType.isBoxedCapturing
           || selWiden.isBoxedCapturing
           || selType.isTrackableRef
           || selWiden.captureSet.isAlwaysEmpty
@@ -882,7 +883,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         val cs = csArg.nuType.captureSet
         val ref = refArg.nuType
         capt.println(i"check contains $cs , $ref")
-        ref match
+        ref.stripCapturing match
           case ref: Capability if ref.isTracked =>
             checkElem(ref, cs, tree.srcPos)
           case _ =>
@@ -1677,7 +1678,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       actual.isSingleton
       && expected.match
           case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags)
-          case _ => expected.isSingleton || expected == LhsProto
+          case _ => expected.stripCapturing.isSingleton || expected == LhsProto
 
     /** Adapt `actual` type to `expected` type. This involves:
      *   - narrow toplevel captures of `x`'s underlying type to `{x}` according to CC's VAR rule
@@ -1686,7 +1687,14 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     def adapt(actual: Type, expected: Type, tree: Tree)(using Context): Type =
       if noWiden(actual, expected) then
-        actual
+        expected match
+          case expected @ CapturingType(_, _) if expected.isBoxed =>
+            // actual is a singleton type and expected is of the form box x.type^cs.
+            // Convert actual to the same form.
+            actual.boxDeeply
+              .showing(i"adapt single $actual / $result vs $expected", capt)
+          case _ =>
+            actual
       else
         // Compute the widened type. Drop `@use` and `@consume` annotations from the type,
         // since they obscures the capturing type.

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

@@ -162,37 +162,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     else symd
   end transformSym
 
-  /** If `tp` is an unboxed capturing type or a function returning an unboxed capturing type,
-   *  convert it to be boxed.
-   */
-  private def box(tp: Type)(using Context): Type =
-    def recur(tp: Type): Type = tp.dealiasKeepAnnotsAndOpaques match
-      case tp @ CapturingType(parent, refs) =>
-        if tp.isBoxed || parent.derivesFrom(defn.Caps_CapSet) then tp
-        else tp.boxed
-      case tp @ AnnotatedType(parent, ann) =>
-        if ann.symbol.isRetains && !parent.derivesFrom(defn.Caps_CapSet)
-        then CapturingType(parent, ann.tree.toCaptureSet, boxed = true)
-        else tp.derivedAnnotatedType(box(parent), ann)
-      case tp1 @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp1) =>
-        val res = args.last
-        val boxedRes = recur(res)
-        if boxedRes eq res then tp
-        else tp1.derivedAppliedType(tycon, args.init :+ boxedRes)
-      case tp1 @ defn.RefinedFunctionOf(rinfo: MethodType) =>
-        val boxedRinfo = recur(rinfo)
-        if boxedRinfo eq rinfo then tp
-        else boxedRinfo.toFunctionType(alwaysDependent = true)
-      case tp1: MethodOrPoly =>
-        val res = tp1.resType
-        val boxedRes = recur(res)
-        if boxedRes eq res then tp
-        else tp1.derivedLambdaType(resType = boxedRes)
-      case _ => tp
-    tp match
-      case tp: MethodOrPoly => tp // don't box results of methods outside refinements
-      case _ => recur(tp)
-
   private trait SetupTypeMap extends FollowAliasesMap:
     private var isTopLevel = true
 
@@ -257,9 +226,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         CapturingType(OrType(tp1, parent2, tp.isSoft), refs2, tp2.isBoxed)
       case tp @ AppliedType(tycon, args)
       if !defn.isFunctionClass(tp.dealias.typeSymbol) && (tp.dealias eq tp) =>
-        tp.derivedAppliedType(tycon, args.mapConserve(box))
+        tp.derivedAppliedType(tycon, args.mapConserve(_.boxDeeply))
       case tp: RealTypeBounds =>
-        tp.derivedTypeBounds(tp.lo, box(tp.hi))
+        tp.derivedTypeBounds(tp.lo, tp.hi.boxDeeply)
       case tp: LazyRef =>
         normalizeCaptures(tp.ref)
       case _ =>
@@ -542,7 +511,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
           if tree.isInferred
           then transformInferredType(tree.tpe)
           else transformExplicitType(tree.tpe, sym, freshen = !boxed, tptToCheck = tree)
-        if boxed then transformed = box(transformed)
+        if boxed then transformed = transformed.boxDeeply
         tree.setNuType(
           if sym.hasAnnotation(defn.UncheckedCapturesAnnot) then makeUnchecked(transformed)
           else transformed)
@@ -612,7 +581,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
 
         case tree @ SeqLiteral(elems, tpt: TypeTree) =>
           traverse(elems)
-          tpt.setNuType(box(transformInferredType(tpt.tpe)))
+          tpt.setNuType(transformInferredType(tpt.tpe).boxDeeply)
 
         case tree @ Try(body, catches, finalizer) =>
           val tryOwner = firstCanThrowEvidence(body) match

tests/neg-custom-args/captures/i23207.check

@@ -0,0 +1,14 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:15:17 ---------------------------------------
+15 |  val a: A = box.x // error
+   |             ^^^^^
+   |             Found:    (box.x : (b : B^{io})^{b})
+   |             Required: A
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:16:11 ---------------------------------------
+16 |  b.getBox.x // error
+   |  ^^^^^^^^^^
+   |  Found:    (Box[(b : B^{io})^{b}]#x : (b : B^{io})^{b})
+   |  Required: A^?
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/i23207.scala

@@ -0,0 +1,16 @@
+import language.experimental.captureChecking
+import caps.*
+
+case class Box[T](x: T)
+
+class A:
+  def getBox: Box[this.type] = Box(this)
+
+def leak(io: AnyRef^): A =
+  class B extends A:
+    val hide: AnyRef^{io} = io
+
+  val b = new B
+  val box = b.getBox
+  val a: A = box.x // error
+  b.getBox.x // error

tests/pos-custom-args/captures/singleton-subtyping.scala

@@ -0,0 +1,16 @@
+class Box[+T](x: T)
+
+def Test(c: Object^): Unit =
+  val x: Object^{c} = c
+
+  val x2: x.type^{x} = x
+  val x3: x.type = x2
+
+  val b: Box[x.type] = Box(x)
+  val b1: Box[x.type^{x}] = b
+  val b2: Box[x.type] = b1
+
+
+
+
+