Use intersection to type selections

Author: odersky

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

@@ -6,6 +6,7 @@ import core.*
 import Symbols.*, Contexts.*, Types.*, ContextOps.*, Decorators.*, SymDenotations.*
 import Flags.*, SymUtils.*, NameKinds.*
 import ast.*
+import Names.Name
 import Phases.Phase
 import DenotTransformers.{DenotTransformer, IdentityDenotTransformer, SymTransformer}
 import NamerOps.{methodType, linkConstructorParams}
@@ -125,17 +126,19 @@ abstract class Recheck extends Phase, SymTransformer:
       tree.tpe
 
     /** Keep the symbol of the `select` but re-infer its type */
-    def recheckSelect(tree: Select)(using Context): Type = tree match
-      case Select(qual, name) =>
-        val qualType = recheck(qual).widenIfUnstable
-        if name.is(OuterSelectName) then tree.tpe
-        else
-          //val pre = ta.maybeSkolemizePrefix(qualType, name)
-          val mbr = qualType.findMember(name, qualType,
-              excluded = if tree.symbol.is(Private) then EmptyFlags else Private
-            ).suchThat(tree.symbol == _)
-          constFold(tree, qualType.select(name, mbr))
-            //.showing(i"recheck select $qualType . $name : ${mbr.symbol.info} = $result")
+    def recheckSelect(tree: Select)(using Context): Type =
+      val Select(qual, name) = tree
+      recheckSelection(tree, recheck(qual).widenIfUnstable, name)
+
+    def recheckSelection(tree: Select, qualType: Type, name: Name)(using Context) =
+      if name.is(OuterSelectName) then tree.tpe
+      else
+        //val pre = ta.maybeSkolemizePrefix(qualType, name)
+        val mbr = qualType.findMember(name, qualType,
+            excluded = if tree.symbol.is(Private) then EmptyFlags else Private
+          ).suchThat(tree.symbol == _)
+        constFold(tree, qualType.select(name, mbr))
+          //.showing(i"recheck select $qualType . $name : ${mbr.symbol.info} = $result")
 
     def recheckBind(tree: Bind, pt: Type)(using Context): Type = tree match
       case Bind(name, body) =>

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

@@ -238,6 +238,18 @@ class CheckCaptures extends Recheck, SymTransformer:
           else i"references $cs1 are not all"
         report.error(i"$header included in allowed capture set ${res.blocking}", pos)
 
+    override def recheckSelection(tree: Select, qualType: Type, name: Name)(using Context) = {
+      val selType = super.recheckSelection(tree, qualType, name)
+      val selCs = selType.widen.captureSet
+      if selCs.isAlwaysEmpty || selType.widen.isBoxedCapturing || qualType.isBoxedCapturing then
+        selType
+      else
+        val qualCs = qualType.captureSet
+        //println(i"intersect $qualType, ${selType.widen}, $qualCs, $selCs")
+        if selCs.subCaptures(qualCs, frozen = true).isOK then selType
+        else selType.widen.stripCapturing.capturing(selCs ** qualCs)
+    }//.showing(i"recheck sel $tree, $qualType = $result")
+
     override def recheckClosure(tree: Closure, pt: Type)(using Context): Type =
       val cs = capturedVars(tree.meth.symbol)
       capt.println(i"typing closure $tree with cvs $cs")

tests/neg-custom-args/captures/caseclass/Test_2.scala

@@ -22,9 +22,4 @@ def test(c: C) =
 
   val y4 = y3 match
     case Ref(xx) => xx
-  val y4c: {x3} () -> Unit = y4  // error (?) found: (y4 : {*} () -> Unit) required: {x3} () -> Unit. (But in fact it should work)
-
-
-
-
-
+  val y4c: {x3} () -> Unit = y4

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

@@ -0,0 +1,6 @@
+class CC
+type Cap = {*} CC
+
+def test(cap1: Cap, cap2: Cap) =
+  var b: List[String => String] = Nil // was error, now OK
+  val bc = b.head // error

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

@@ -9,6 +9,20 @@
 5 |  val x = Foo(m)   // error
   |  ^^^^^^^^^^^^^^
   |  Non-local value x cannot have an inferred type
-  |  {Baz.this.m} Foo{m: {Baz.this.m} String}
-  |  with non-empty capture set {Baz.this.m}.
+  |  {Baz.this} Foo{m: {Baz.this} String}
+  |  with non-empty capture set {Baz.this}.
+  |  The type needs to be declared explicitly.
+-- Error: tests/neg-custom-args/captures/i15116.scala:7:6 --------------------------------------------------------------
+7 |  val x = Foo(m)   // error
+  |  ^^^^^^^^^^^^^^
+  |  Non-local value x cannot have an inferred type
+  |  {Bar1.this.m} Foo{m: {Bar1.this.m} String}
+  |  with non-empty capture set {Bar1.this.m}.
+  |  The type needs to be declared explicitly.
+-- Error: tests/neg-custom-args/captures/i15116.scala:9:6 --------------------------------------------------------------
+9 |  val x = Foo(m)   // error
+  |  ^^^^^^^^^^^^^^
+  |  Non-local value x cannot have an inferred type
+  |  {Baz2.this} Foo{m: {Baz2.this} String}
+  |  with non-empty capture set {Baz2.this}.
   |  The type needs to be declared explicitly.

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

@@ -3,3 +3,7 @@ class Bar(val m: {*} String):
   val x = Foo(m)   // error
 trait Baz(val m: {*} String):
   val x = Foo(m)   // error
+class Bar1(m: {*} String):
+  val x = Foo(m)   // error
+trait Baz2(m: {*} String):
+  val x = Foo(m)   // error

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

@@ -1,7 +1,34 @@
-case class Ref(x: {*} String)
-
 @annotation.capability class C
-def test(c: C) =
-  val x1 = Ref("hello")
-  val y = x1 match
-    case Ref(z) => z
+object test1:
+  case class Ref(x: {*} String)
+
+  def test(c: C) =
+    val x1 = Ref("hello")
+    val y = x1 match
+      case Ref(z) => z
+    val yc: String = y
+
+object test2:
+  case class Ref(x: () => Unit)
+  def test(c: C) =
+
+    val pure: () -> Unit = () => ()
+    val impure: () => Unit = pure
+    val mixed: {c} () -> Unit = pure
+    val x = Ref(impure)
+    val y0 = x.copy(pure)
+    val yc0: Ref = y0
+
+    val x2 = Ref(pure)
+    val _: Ref = x2
+    val y2 = x2.copy()
+    val yc2: Ref = y2
+
+    val x3 = Ref(mixed)
+    val _: {c} Ref = x3
+    val y3 = x3.copy()
+    val yc3: {c} Ref = y3
+
+    val y4 = y3 match
+      case Ref(xx) => xx
+    val y4c: {x3} () -> Unit = y4