Add capture checks for mutable variables

 - Mutable variables have boxed types, so that we do not
   need to track them when computing capture sets of classes.
 - Mutable variable types cannot capture `*` in order to
   prevent scope extrusion.

Author: odersky

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

@@ -76,7 +76,7 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
       val symd = sym.denot
       symd.validFor.firstPhaseId == thisPhase.id && (sym.originDenotation ne symd)
 
-    def transformType(tp: Type, inferred: Boolean)(using Context): Type = tp
+    def transformType(tp: Type, inferred: Boolean, boxed: Boolean = false)(using Context): Type = tp
 
     object transformTypes extends TreeTraverser:
 
@@ -110,12 +110,19 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
             mapOver(t)
       end SubstParams
 
+      private def transformTT(tree: TypeTree, boxed: Boolean)(using Context) =
+        transformType(tree.tpe, tree.isInstanceOf[InferredTypeTree], boxed).rememberFor(tree)
+
       def traverse(tree: Tree)(using Context) =
-        traverseChildren(tree)
         tree match
-
+          case tree @ ValDef(_, tpt: TypeTree, _) if tree.symbol.is(Mutable) =>
+            transformTT(tpt, boxed = true)
+            traverse(tree.rhs)
+          case _ =>
+            traverseChildren(tree)
+        tree match
           case tree: TypeTree =>
-            transformType(tree.tpe, tree.isInstanceOf[InferredTypeTree]).rememberFor(tree)
+            transformTT(tree, boxed = false)
           case tree: ValOrDefDef =>
             val sym = tree.symbol
 

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

@@ -115,7 +115,7 @@ class CheckCaptures extends Recheck:
   class CaptureChecker(ictx: Context) extends Rechecker(ictx):
     import ast.tpd.*
 
-    override def transformType(tp: Type, inferred: Boolean)(using Context): Type =
+    override def transformType(tp: Type, inferred: Boolean, boxed: Boolean)(using Context): Type =
 
       def addInnerVars(tp: Type): Type = tp match
         case tp @ AppliedType(tycon, args) =>
@@ -191,15 +191,15 @@ class CheckCaptures extends Recheck:
               apply(parent)
             case _ =>
               mapOver(t)
-        addVars(addFunctionRefinements(cleanup(tp)))
+        addVars(addFunctionRefinements(cleanup(tp)), boxed)
           .showing(i"reinfer $tp --> $result", capt)
       else
-        val addBoxes = new TypeTraverser:
-          def setBoxed(t: Type) = t match
-            case AnnotatedType(_, annot) if annot.symbol == defn.RetainsAnnot =>
-              annot.tree.setBoxedCapturing()
-            case _ =>
+        def setBoxed(t: Type) = t match
+          case AnnotatedType(_, annot) if annot.symbol == defn.RetainsAnnot =>
+            annot.tree.setBoxedCapturing()
+          case _ =>
 
+        val addBoxes = new TypeTraverser:
           def traverse(t: Type) =
             t match
               case AppliedType(tycon, args) if !defn.isNonRefinedFunction(t) =>
@@ -208,8 +208,8 @@ class CheckCaptures extends Recheck:
                 setBoxed(lo); setBoxed(hi)
               case _ =>
             traverseChildren(t)
-        end addBoxes
 
+        if boxed then setBoxed(tp)
         addBoxes.traverse(tp)
         tp
     end transformType
@@ -417,12 +417,15 @@ class CheckCaptures extends Recheck:
               val what = if ref.isRootCapability then "universal" else "global"
               if isGlobal then
                 val notAllowed = i" is not allowed to capture the $what capability $ref"
-                def msg = tree match
-                  case tree: InferredTypeTree =>
-                    i"""inferred type argument ${knownType(tree)}$notAllowed
-                        |
-                        |The inferred arguments are: [${allArgs.map(knownType)}%, %]"""
-                  case _ => s"type argument$notAllowed"
+                def msg =
+                  if allArgs.isEmpty then
+                    i"type of mutable variable ${knownType(tree)}$notAllowed"
+                  else tree match
+                    case tree: InferredTypeTree =>
+                      i"""inferred type argument ${knownType(tree)}$notAllowed
+                          |
+                          |The inferred arguments are: [${allArgs.map(knownType)}%, %]"""
+                    case _ => s"type argument$notAllowed"
                 report.error(msg, tree.srcPos)
 
     object PostRefinerCheck extends TreeTraverser:
@@ -463,6 +466,8 @@ class CheckCaptures extends Recheck:
                         |The type needs to be declared explicitly.""", t.srcPos)
                 case _ =>
               inferred.foreachPart(checkPure, StopAt.Static)
+          case t: ValDef if t.symbol.is(Mutable) =>
+            checkNotGlobal(t.tpt)
           case _ =>
         traverseChildren(tree)
 

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

@@ -0,0 +1,17 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:11:24 -----------------------------------------
+11 |  val z2c: () => Unit = z2  // error
+   |                        ^^
+   |                        Found:    (z2 : {x, cap1} () => Unit)
+   |                        Required: () => Unit
+
+longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/vars.scala:13:10 --------------------------------------------------------------
+13 |  var a: {*} String => String = f // error
+   |          ^^^^^^^^^^^^^^^^^^^
+   |  type of mutable variable box {*} String => String is not allowed to capture the universal capability (* : Any)
+-- Error: tests/neg-custom-args/captures/vars.scala:27:2 ---------------------------------------------------------------
+27 |  local { cap3 => // error
+   |  ^^^^^
+   |inferred type argument {*} (x$0: ? String) => ? String is not allowed to capture the universal capability (* : Any)
+   |
+   |The inferred arguments are: [{*} (x$0: ? String) => ? String]

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

@@ -0,0 +1,37 @@
+class CC
+type Cap = {*} CC
+
+def test(cap1: Cap, cap2: Cap) =
+  def f(x: String): String = if cap1 == cap1 then "" else "a"
+  var x = f
+  val y = x
+  val z = () => if x("") == "" then "a" else "b"
+  val zc: {cap1} () => String = z
+  val z2 = () => { x = identity }
+  val z2c: () => Unit = z2  // error
+
+  var a: {*} String => String = f // error
+
+  def scope =
+    val cap3: Cap = CC()
+    def g(x: String): String = if cap3 == cap3 then "" else "a"
+    a = g
+    val gc = g
+    g
+
+  val s = scope
+  val sc: {*} String => String = scope
+
+  def local[T](op: Cap => T): T = op(CC())
+
+  local { cap3 => // error
+    def g(x: String): String = if cap3 == cap3 then "" else "a"
+    g
+  }
+
+  class Ref:
+    var elem: {cap1} String => String = null
+
+  val r = Ref()
+  r.elem = f
+  val fc = r.elem

tests/pos-custom-args/captures/vars.scala

@@ -0,0 +1,18 @@
+class CC
+type Cap = {*} CC
+
+def test(cap1: Cap, cap2: Cap) =
+  def f(x: String): String = if cap1 == cap1 then "" else "a"
+  var x = f
+  val y = x
+  val z = () => if x("") == "" then "a" else "b"
+  val zc: {cap1} () => String = z
+  val z2 = () => { x = identity }
+  val z2c: {cap1} () => Unit = z2
+
+  class Ref:
+    var elem: {cap1} String => String = null
+
+  val r = Ref()
+  r.elem = f
+  val fc: {cap1} String => String = r.elem