Capture Checking of Lazy Vals

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

@@ -81,7 +81,7 @@ object CheckCaptures:
   end Env
 
   def definesEnv(sym: Symbol)(using Context): Boolean =
-    sym.is(Method) || sym.isClass
+    sym.isOneOf(MethodOrLazy) || sym.isClass
 
   /** Similar normal substParams, but this is an approximating type map that
    *  maps parameters in contravariant capture sets to the empty set.
@@ -225,7 +225,7 @@ object CheckCaptures:
       def needsSepCheck: Boolean
 
       /** If a tree is an argument for which needsSepCheck is true,
-       *  the type of the formal paremeter corresponding to the argument.
+       *  the type of the formal parameter corresponding to the argument.
        */
       def formalType: Type
 
@@ -441,7 +441,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
-        if sym.isTerm || !sym.owner.isStaticOwner
+        if sym.isTerm || !sym.owner.isStaticOwner || sym.is(Lazy)
         then CaptureSet.Var(sym, nestedOK = false)
         else CaptureSet.empty)
 
@@ -578,7 +578,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           if !isOfNestedMethod(env) then
             val nextEnv = nextEnvToCharge(env)
             if nextEnv != null && !nextEnv.owner.isStaticOwner then
-              if env.owner.isReadOnlyMethod && nextEnv.owner != env.owner then
+              if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then
                 checkReadOnlyMethod(included, env)
               recur(included, nextEnv, env)
           	// Under deferredReaches, don't propagate out of methods inside terms.
@@ -665,8 +665,10 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
       val sym = tree.symbol
-      if sym.is(Method) then
-        // If ident refers to a parameterless method, charge its cv to the environment
+      if sym.isOneOf(MethodOrLazy) then
+        // If ident refers to a parameterless method or lazy val, charge its cv to the environment.
+        // Lazy vals are like parameterless methods: accessing them may trigger initialization
+        // that uses captured references.
         includeCallCaptures(sym, sym.info, tree)
       else if sym.exists && !sym.isStatic then
         markPathFree(sym.termRef, pt, tree)
@@ -688,7 +690,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         case pt: PathSelectionProto if ref.isTracked =>
           // if `ref` is not tracked then the selection could not give anything new
           // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
-          if pt.select.symbol.isReadOnlyMethod then
+          if pt.select.symbol.isReadOnlyMethodOrLazyVal then
             markFree(ref.readOnly, tree)
           else
             val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef]
@@ -708,8 +710,8 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     override def selectionProto(tree: Select, pt: Type)(using Context): Type =
       val sym = tree.symbol
-      if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic
-          || sym.isReadOnlyMethod
+      if !sym.isOneOf(MethodOrLazyOrMutable) && !sym.isStatic
+          || sym.isReadOnlyMethodOrLazyVal
       then PathSelectionProto(tree, pt)
       else super.selectionProto(tree, pt)
 
@@ -1103,6 +1105,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *   - for externally visible definitions: check that their inferred type
      *     does not refine what was known before capture checking.
      *   - Interpolate contravariant capture set variables in result type.
+     *   - for lazy vals: create a nested environment to track captures (similar to methods)
      */
     override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Type =
       val savedEnv = curEnv
@@ -1125,8 +1128,16 @@ class CheckCaptures extends Recheck, SymTransformer:
                 ""
             disallowBadRootsIn(
               tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
-          if runInConstructor then
+
+          // Lazy vals need their own environment to track captures from their RHS,
+          // similar to how methods work
+          if sym.is(Lazy) then
+            val localSet = capturedVars(sym)
+            if localSet ne CaptureSet.empty then
+              curEnv = Env(sym, EnvKind.Regular, localSet, curEnv, nestedClosure = NoSymbol)
+          else if runInConstructor then
             pushConstructorEnv()
+
           checkInferredResult(super.recheckValDef(tree, sym), tree)
       finally
         if !sym.is(Param) then
@@ -1137,8 +1148,9 @@ class CheckCaptures extends Recheck, SymTransformer:
           interpolateIfInferred(tree.tpt, sym)
 
         def declaredCaptures = tree.tpt.nuType.captureSet
+        curEnv = savedEnv
+
         if runInConstructor && savedEnv.owner.isClass then
-          curEnv = savedEnv
           markFree(declaredCaptures, tree, addUseInfo = false)
 
         if sym.owner.isStaticOwner && !declaredCaptures.elems.isEmpty && sym != defn.captureRoot then

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

@@ -53,21 +53,21 @@ object Mutability:
       sym.isAllOf(Mutable | Method)
         && (!sym.isSetter || sym.field.is(Transparent))
 
-    /** A read-only methid is a real method (not an accessor) in a type extending
-     *  Mutable that is not an update method.
+    /** A read-only method is a real method (not an accessor) in a type extending
+     *  Mutable that is not an update method. Included are also lazy vals in such types.
      */
-    def isReadOnlyMethod(using Context): Boolean =
-      sym.is(Method, butNot = Mutable | Accessor) && sym.owner.derivesFrom(defn.Caps_Mutable)
+    def isReadOnlyMethodOrLazyVal(using Context): Boolean =
+      sym.isOneOf(MethodOrLazy, butNot = Mutable | Accessor)
+      && sym.owner.derivesFrom(defn.Caps_Mutable)
 
     private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity =
       import Exclusivity.*
-      val encl = sym.enclosingMethodOrClass.skipConstructor
       if sym == cls then OK // we are directly in `cls` or in one of its constructors
-      else if encl.owner == cls then
-        if encl.isUpdateMethod then OK
-        else NotInUpdateMethod(encl, cls)
-      else if encl.isStatic then OutsideClass(cls)
-      else encl.owner.inExclusivePartOf(cls)
+      else if sym.owner == cls then
+        if sym.isUpdateMethod || sym.isConstructor then OK
+        else NotInUpdateMethod(sym, cls)
+      else if sym.isStatic then OutsideClass(cls)
+      else sym.owner.inExclusivePartOf(cls)
 
   extension (tp: Type)
     /** Is this a type extending `Mutable` that has non-private update methods

docs/_docs/reference/experimental/capture-checking/basics.md

@@ -172,6 +172,63 @@ def f(x: ->{c} Int): Int
 ```
 Here, the actual argument to `f` is allowed to use the `c` capability but no others.
 
+## Lazy Vals
+
+Lazy vals receive special treatment under capture checking, similar to parameterless methods. A lazy val has two distinct capture sets:
+
+1. **The initializer's capture set**: What capabilities the initialization code uses
+2. **The result's capture set**: What capabilities the lazy val's value captures
+
+### Initializer Captures
+
+When a lazy val is declared, its initializer is checked in its own environment (like a method body). The initializer can capture capabilities, and these are tracked separately:
+
+```scala
+def example(console: Console^) =
+  lazy val x: () -> String =
+    console.println("Computing x")  // console captured by initializer
+    () => "Hello, World!"           // result doesn't capture console
+
+  val fun: () ->{console} String = () => x()   // ok: accessing x uses console
+  val fun2: () -> String = () => x()           // error: x captures console
+```
+
+Here, the initializer of `x` uses `console` (to print a message), so accessing `x` for the first time will use the `console` capability. However, the **result** of `x` is a pure function `() -> String` that doesn't capture any capabilities.
+
+The type system tracks that accessing `x` requires the `console` capability, even though the resulting value doesn't. This is reflected in the function types: `fun` must declare `{console}` in its capture set because it accesses `x`.
+
+### Lazy Val Member Selection
+
+When accessing a lazy val member through a qualifier, the qualifier is charged to the current capture set, just like calling a parameterless method:
+
+```scala
+trait Container:
+  lazy val lazyMember: String
+
+def client(c: Container^): Unit =
+  val f1: () -> String = () => c.lazyMember        // error
+  val f2: () ->{c} String = () => c.lazyMember     // ok
+```
+
+Accessing `c.lazyMember` can trigger initialization, which may use capabilities from `c`. Therefore, the capture set must include `c`.
+
+### Equivalence with Methods
+
+For capture checking purposes, lazy vals behave identically to parameterless methods:
+
+```scala
+trait T:
+  def methodMember: String
+  lazy val lazyMember: String
+
+def test(t: T^): Unit =
+  // Both require {t} in the capture set
+  val m: () ->{t} String = () => t.methodMember
+  val l: () ->{t} String = () => t.lazyMember
+```
+
+This equivalence reflects that both can trigger computation using capabilities from their enclosing object.
+
 ## Subtyping and Subcapturing
 
 Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -215,6 +215,50 @@ val b1: Ref^{a.rd} = a
 val b2: Ref^{cap.rd} = a
 ```
 
+## Lazy Vals and Read-Only Restrictions
+
+Lazy val initializers in `Mutable` classes are subject to read-only restrictions similar to those for normal methods. Specifically, a lazy val initializer in a `Mutable` class cannot call update methods or refer to non-local exclusive capabilities, i.e., capabilities defined outside the lazy val's scope.
+
+For example, when a lazy val is declared in a local method's scope, its initializer may freely use capabilities from the surrounding environment:
+```scala
+def example(r: Ref[Int]^) =
+  lazy val goodInit: () ->{r.rd} Int =
+    val i = r.get() // ok: read-only access
+    r.set(100 * i)  // ok: can call update method
+    () => r.get() + i
+```
+However, within a `Mutable` class, a lazy val declaration has only read access to non-local exclusive capabilities:
+```scala
+class Wrapper(val r: Ref[Int]^) extends Mutable:
+  lazy val badInit: () ->{r} Int =
+    r.set(100) // error: call to update method
+    () => r.set(r.get() * 2); r.get() // error: call to update method
+
+  lazy val goodInit: () ->{r.rd} Int =
+    val i = r.get()   // ok
+    () => r.get() * i // ok
+```
+The initializer of `badInit` attempts to call `r.set(100)`, an update method on the non-local exclusive capability `r`.
+This is rejected because initializers should not perform mutations on external state.
+
+### Local Capabilities
+
+The restriction applies only to **non-local** capabilities. A lazy val can freely call update methods on capabilities it creates locally within its initializer:
+
+```scala
+class Example:
+  lazy val localMutation: () => Int =
+    val local: Ref[Int]^ = Ref(10)  // created in initializer
+    local.set(100)             // ok: local capability
+    () => local.get()
+```
+
+Here, `local` is created within the lazy val's initializer, so it counts as a local capability. The initializer can call update methods on it.
+
+This makes lazy vals behave like normal methods in `Mutable` classes: they can read from their environment but cannot update it unless explicitly marked.
+Unlike for methods, there's currently no `update` modifier for lazy vals in `Mutable` classes, so their initialization is always read-only with respect to non-local capabilities. A future version of capture checking might
+support `update lazy val` if there are compelling use cases and there is sufficient community demand.
+
 ## Update Restrictions
 
 If a capability `r` is a read-only access, then one cannot use `r` to call an update method of `r` or to assign to a field of `r`. E.g. `r.set(22)` and `r.current = 22` are both disallowed.

library/src/scala/collection/SeqView.scala

@@ -151,7 +151,7 @@ object SeqView {
 
       def apply(i: Int): A = _reversed.apply(i)
       def length: Int = len
-      def iterator: Iterator[A] = Iterator.empty ++ _reversed.iterator // very lazy
+      def iterator: Iterator[A]^{this} = Iterator.empty ++ _reversed.iterator // very lazy
       override def knownSize: Int = len
       override def isEmpty: Boolean = len == 0
       override def to[C1](factory: Factory[A, C1]): C1 = _reversed.to(factory)

tests/neg-custom-args/captures/lazyvals-sep.check

@@ -0,0 +1,63 @@
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:30:6 -------------------------------------------------------
+30 |    r.set(current * 100)  // error - exclusive access in initializer
+   |    ^^^^^
+   |    Cannot call update method set of TestClass.this.r
+   |    since the access is in lazy value lazyVal2, which is not an update method.
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:36:12 ------------------------------------------------------
+36 |    () => r.set(current); r.get()  // error, even though exclusive access is in closure, not initializer
+   |          ^^^^^
+   |          Cannot call update method set of TestClass.this.r
+   |          since the access is in lazy value lazyVal3, which is not an update method.
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:42:10 ------------------------------------------------------
+42 |        r.set(100)  // error
+   |        ^^^^^
+   |        Cannot call update method set of TestClass.this.r
+   |        since the access is in lazy value lazyVal4, which is not an update method.
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:61:6 -------------------------------------------------------
+61 |    r.set(200)  // error
+   |    ^^^^^
+   |    Cannot call update method set of TestClass.this.r
+   |    since the access is in lazy value lazyVal6, which is not an update method.
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:71:6 -------------------------------------------------------
+71 |    r.set(200)  // error
+   |    ^^^^^
+   |    Cannot call update method set of TestClass.this.r
+   |    since the access is in lazy value lazyVal8, which is not an update method.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:72:12 ---------------------------------
+72 |    Wrapper(r)  // error
+   |            ^
+   |Found:    Ref^{TestClass.this.r.rd}
+   |Required: Ref^
+   |
+   |Note that capability TestClass.this.r.rd is not included in capture set {}.
+   |
+   |Note that {cap} is an exclusive capture set of the mutable type Ref^,
+   |it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
+   |
+   |where:    ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 ---------------------------------
+77 |    Wrapper(r) // error
+   |            ^
+   |Found:    Ref^{TestClass.this.r.rd}
+   |Required: Ref^
+   |
+   |Note that capability TestClass.this.r.rd is not included in capture set {}.
+   |
+   |Note that {cap} is an exclusive capture set of the mutable type Ref^,
+   |it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
+   |
+   |where:    ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 -------------------------------------------------------
+82 |      r.set(0)  // error exclusive access in conditional
+   |      ^^^^^
+   |      Cannot call update method set of TestClass.this.r
+   |      since the access is in lazy value lazyVal10, which is not an update method.
+-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:90:8 -------------------------------------------------------
+90 |      r.set(42)  // error
+   |      ^^^^^
+   |      Cannot call update method set of TestClass.this.r
+   |      since the access is in lazy value lazyVal11, which is not an update method.