Fix #18246: correctly compute capture sets in TypeComparer.glb (#18254

)

Intuitively, `glb(S1^C1, S2^C2)` should capture `C1 ⊓ C2`, where `⊓`
denotes the glb of capture sets. When computing `glb(tp1, tp2)`, if
`tp1` matches `CapturingType(parent1, refs1)`, it captures `C0 ++ refs1`
where `C0` is the nested capture sets inside `parent1`. Denote the
capture set of `tp2` with `C2`, the result should capture `(C0 ++ refs1)
⊓ C2`. Presumably, `⊓` distributes over the union (`++`); therefore `(C0
++ refs1) ⊓ C2` equals `C0 ⊓ C2 ++ refs1 ⊓ C2`.

Previously, if `C2` is a subcapture of `refs1`, it is simply dropped.
However, based on the above reasoning, we have `refs1 ⊓ C2` equals `C2`;
therefore `C0 ⊓ C2 ++ refs1 ⊓ C2` equals `C0 ⊓ C2 ++ C2`. `C2` should
not be dropped, but rather kept. This PR fixes the logic to behave
correctly.

Fixes #18246.

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -2618,12 +2618,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     case tp1: TypeVar if tp1.isInstantiated =>
       tp1.underlying & tp2
     case CapturingType(parent1, refs1) =>
-      if subCaptures(tp2.captureSet, refs1, frozen = true).isOK
+      val refs2 = tp2.captureSet
+      if subCaptures(refs2, refs1, frozen = true).isOK
         && tp1.isBoxedCapturing == tp2.isBoxedCapturing
-      then
-        parent1 & tp2
-      else
-        tp1.derivedCapturingType(parent1 & tp2, refs1)
+      then (parent1 & tp2).capturing(refs2)
+      else tp1.derivedCapturingType(parent1 & tp2, refs1)
     case tp1: AnnotatedType if !tp1.isRefining =>
       tp1.underlying & tp2
     case _ =>

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -1940,7 +1940,7 @@ object Types {
      *  the two capture sets are combined.
      */
     def capturing(cs: CaptureSet)(using Context): Type =
-      if cs.isConst && cs.subCaptures(captureSet, frozen = true).isOK then this
+      if cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(captureSet, frozen = true).isOK then this
       else this match
         case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)
         case _ => CapturingType(this, cs)

tests/neg-custom-args/captures/cc-glb.check

@@ -0,0 +1,7 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-glb.scala:7:19 ----------------------------------------
+7 |  val x2: Foo[T] = x1  // error
+  |                   ^^
+  |                   Found:    (x1 : (Foo[T]^) & (Foo[Any]^{io}))
+  |                   Required: Foo[T]
+  |
+  | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/cc-glb.scala

@@ -0,0 +1,8 @@
+import language.experimental.captureChecking
+trait Cap
+trait Foo[+T]
+
+def magic[T](io: Cap^, x: Foo[T]^{io}): Foo[T]^{} =
+  val x1: Foo[T]^{cap} & Foo[Any]^{io} = x
+  val x2: Foo[T] = x1  // error
+  x2  // boom, an impure value becomes pure