Require array element types to be sealed

Author: odersky

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

@@ -206,6 +206,12 @@ extension (tp: Type)
     case _: TypeRef | _: AppliedType => tp.typeSymbol.hasAnnotation(defn.CapabilityAnnot)
     case _ => false
 
+  def isSealed(using Context): Boolean = tp match
+    case tp: TypeParamRef => tp.underlying.isSealed
+    case tp: TypeBounds => tp.hi.hasAnnotation(defn.Caps_SealedAnnot)
+    case tp: TypeRef => tp.symbol.is(Sealed) || tp.info.isSealed // TODO: drop symbol flag?
+    case _ => false
+
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
     val tm = new TypeMap:

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

@@ -872,6 +872,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")
 
   /** Apply `f` to each element in `xs`, and join result sets with `++` */

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

@@ -148,7 +148,7 @@ object CheckCaptures:
     val check = new TypeTraverser:
 
       extension (tparam: Symbol) def isParametricIn(carrier: Symbol): Boolean =
-        val encl = carrier.owner.enclosingMethodOrClass
+        val encl = carrier.maybeOwner.enclosingMethodOrClass
         if encl.isClass then tparam.isParametricIn(encl)
         else
           def recur(encl: Symbol): Boolean =
@@ -160,11 +160,9 @@ object CheckCaptures:
       def traverse(t: Type) =
         t.dealiasKeepAnnots match
           case t: TypeRef =>
-            capt.println(i"disallow $t, $tp, $what, ${t.symbol.is(Sealed)}")
+            capt.println(i"disallow $t, $tp, $what, ${t.isSealed}")
             t.info match
-              case TypeBounds(_, hi)
-              if !t.symbol.is(Sealed) && !hi.hasAnnotation(defn.Caps_SealedAnnot)
-                  && !t.symbol.isParametricIn(carrier) =>
+              case TypeBounds(_, hi) if !t.isSealed && !t.symbol.isParametricIn(carrier) =>
                 if hi.isAny then
                   report.error(
                     em"""$what cannot $have $tp since
@@ -543,8 +541,8 @@ class CheckCaptures extends Recheck, SymTransformer:
         val TypeApply(fn, args) = tree
         val polyType = atPhase(thisPhase.prev):
           fn.tpe.widen.asInstanceOf[TypeLambda]
-        for case (arg: TypeTree, pinfo, pname) <- args.lazyZip(polyType.paramInfos).lazyZip((polyType.paramNames)) do
-          if pinfo.bounds.hi.hasAnnotation(defn.Caps_SealedAnnot) then
+        for case (arg: TypeTree, formal, pname) <- args.lazyZip(polyType.paramRefs).lazyZip((polyType.paramNames)) do
+          if formal.isSealed then
             def where = if fn.symbol.exists then i" in an argument of ${fn.symbol}" else ""
             disallowRootCapabilitiesIn(arg.knownType, fn.symbol,
               i"Sealed type variable $pname", "be instantiated to",
@@ -1313,6 +1311,23 @@ class CheckCaptures extends Recheck, SymTransformer:
             traverseChildren(tp)
       check.traverse(info)
 
+    def checkArraysAreSealedIn(tp: Type, pos: SrcPos)(using Context): Unit =
+      val check = new TypeTraverser:
+        def traverse(t: Type): Unit =
+          t match
+            case AppliedType(tycon, arg :: Nil) if tycon.typeSymbol == defn.ArrayClass =>
+              if !(pos.span.isSynthetic && ctx.reporter.errorsReported) then
+                CheckCaptures.disallowRootCapabilitiesIn(arg, NoSymbol,
+                  "Array", "have element type",
+                  "Since arrays are mutable, they have to be treated like variables,\nso their element type must be sealed.",
+                  pos)
+              traverseChildren(t)
+            case defn.RefinedFunctionOf(rinfo: MethodType) =>
+              traverse(rinfo)
+            case _ =>
+              traverseChildren(t)
+      check.traverse(tp)
+
     /** Perform the following kinds of checks
      *   - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
      *   - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
@@ -1338,6 +1353,8 @@ class CheckCaptures extends Recheck, SymTransformer:
               case _ =>
           case _: ValOrDefDef | _: TypeDef =>
             checkNoLocalRootIn(tree.symbol, tree.symbol.info, tree.symbol.srcPos)
+          case tree: TypeTree =>
+            checkArraysAreSealedIn(tree.tpe, tree.srcPos)
           case _ =>
         end check
       end checker

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

@@ -596,9 +596,9 @@ abstract class Recheck extends Phase, SymTransformer:
 
   /** Show tree with rechecked types instead of the types stored in the `.tpe` field */
   override def show(tree: untpd.Tree)(using Context): String =
-    atPhase(thisPhase) {
-      super.show(addRecheckedTypes.transform(tree.asInstanceOf[tpd.Tree]))
-    }
+    atPhase(thisPhase):
+      withMode(Mode.Printing):
+        super.show(addRecheckedTypes.transform(tree.asInstanceOf[tpd.Tree]))
 end Recheck
 
 /** A class that can be used to test basic rechecking without any customaization */

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

@@ -0,0 +1,26 @@
+-- Error: tests/neg-custom-args/captures/buffers.scala:11:6 ------------------------------------------------------------
+11 |  var elems: Array[A] = new Array[A](10) // error // error
+   |      ^
+   |      mutable variable elems cannot have type Array[A] since
+   |      that type refers to the type variable A, which is not sealed.
+-- Error: tests/neg-custom-args/captures/buffers.scala:16:38 -----------------------------------------------------------
+16 |  def make[A: ClassTag](xs: A*) = new ArrayBuffer: // error
+   |                                      ^^^^^^^^^^^
+   |                            Sealed type variable A cannot be instantiated to box A^? since
+   |                            that type refers to the type variable A, which is not sealed.
+   |                            This is often caused by a local capability in an argument of constructor ArrayBuffer
+   |                            leaking as part of its result.
+-- Error: tests/neg-custom-args/captures/buffers.scala:11:13 -----------------------------------------------------------
+11 |  var elems: Array[A] = new Array[A](10) // error // error
+   |             ^^^^^^^^
+   |             Array cannot have element type A since
+   |             that type refers to the type variable A, which is not sealed.
+   |             Since arrays are mutable, they have to be treated like variables,
+   |             so their element type must be sealed.
+-- Error: tests/neg-custom-args/captures/buffers.scala:22:9 ------------------------------------------------------------
+22 |  val x: Array[A] = new Array[A](10) // error
+   |         ^^^^^^^^
+   |         Array cannot have element type A since
+   |         that type refers to the type variable A, which is not sealed.
+   |         Since arrays are mutable, they have to be treated like variables,
+   |         so their element type must be sealed.

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

@@ -0,0 +1,30 @@
+import reflect.ClassTag
+
+class Buffer[A]
+
+class ArrayBuffer[sealed A: ClassTag] extends Buffer[A]:
+  var elems: Array[A] = new Array[A](10)
+  def add(x: A): this.type = ???
+  def at(i: Int): A = ???
+
+class ArrayBufferBAD[A: ClassTag] extends Buffer[A]:
+  var elems: Array[A] = new Array[A](10) // error // error
+  def add(x: A): this.type = ???
+  def at(i: Int): A = ???
+
+object ArrayBuffer:
+  def make[A: ClassTag](xs: A*) = new ArrayBuffer: // error
+    elems = xs.toArray
+  def apply[sealed A: ClassTag](xs: A*) = new ArrayBuffer:
+    elems = xs.toArray  // ok
+
+class EncapsArray[A: ClassTag]:
+  val x: Array[A] = new Array[A](10) // error
+
+
+
+
+
+
+
+