Fix lubs over capturing types

Also, fix Seq rechecking so that elements are always box adapted

Author: odersky

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

@@ -719,6 +719,9 @@ class CheckCaptures extends Recheck, SymTransformer:
         openClosures = openClosures.tail
     end recheckClosureBlock
 
+    override def seqLiteralElemProto(tree: SeqLiteral, pt: Type, declared: Type)(using Context) =
+      super.seqLiteralElemProto(tree, pt, declared).boxed
+
     /** Maps mutable variables to the symbols that capture them (in the
      *  CheckCaptures sense, i.e. symbol is referred to from a different method
      *  than the one it is defined in).

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

@@ -2751,6 +2751,11 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       }
     case tp1: TypeVar if tp1.isInstantiated =>
       lub(tp1.underlying, tp2, isSoft = isSoft)
+    case CapturingType(parent1, refs1) =>
+      if tp1.isBoxCompatibleWith(tp2) then
+        tp1.derivedCapturingType(lub(parent1, tp2, isSoft = isSoft), refs1)
+      else // TODO: Analyze cases where they are not box compatible
+        NoType
     case tp1: AnnotatedType if !tp1.isRefining =>
       lub(tp1.underlying, tp2, isSoft = isSoft)
     case _ =>

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

@@ -23,6 +23,7 @@ import reporting.trace
 import annotation.constructorOnly
 import cc.CaptureSet.IdempotentCaptRefMap
 import annotation.tailrec
+import dotty.tools.dotc.cc.boxed
 
 object Recheck:
   import tpd.*
@@ -438,12 +439,16 @@ abstract class Recheck extends Phase, SymTransformer:
       val finalizerType = recheck(tree.finalizer, defn.UnitType)
       TypeComparer.lub(bodyType :: casesTypes)
 
+    def seqLiteralElemProto(tree: SeqLiteral, pt: Type, declared: Type)(using Context): Type =
+      declared.orElse:
+        pt.stripNull().elemType match
+          case NoType => WildcardType
+          case bounds: TypeBounds => WildcardType(bounds)
+          case elemtp => elemtp
+
     def recheckSeqLiteral(tree: SeqLiteral, pt: Type)(using Context): Type =
-      val elemProto = pt.stripNull().elemType match
-        case NoType => WildcardType
-        case bounds: TypeBounds => WildcardType(bounds)
-        case elemtp => elemtp
       val declaredElemType = recheck(tree.elemtpt)
+      val elemProto = seqLiteralElemProto(tree, pt, declaredElemType)
       val elemTypes = tree.elems.map(recheck(_, elemProto))
       seqLitType(tree, TypeComparer.lub(declaredElemType :: elemTypes))
 

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

@@ -26,11 +26,11 @@
    |                                    Required: lazylists.LazyList[Int]^{cap2}
    |
    | longer explanation available when compiling with `-explain`
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:41:48 -------------------------------------
-41 |  val ref4c: LazyList[Int]^{cap1, ref3, cap3} = ref4 // error
-   |                                                ^^^^
-   |                                                Found:    (ref4 : lazylists.LazyList[Int]^{cap3, cap2, ref1})
-   |                                                Required: lazylists.LazyList[Int]^{cap1, ref3, cap3}
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazylist.scala:41:42 -------------------------------------
+41 |  val ref4c: LazyList[Int]^{cap1, ref3} = ref4 // error
+   |                                          ^^^^
+   |                                          Found:    (ref4 : lazylists.LazyList[Int]^{cap3, ref2, ref1})
+   |                                          Required: lazylists.LazyList[Int]^{cap1, ref3}
    |
    | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ----------------------------------------

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

@@ -38,4 +38,4 @@ def test(cap1: Cap, cap2: Cap, cap3: Cap) =
   val ref3 = ref1.map(g)
   val ref3c: LazyList[Int]^{cap2} = ref3 // error
   val ref4 = (if cap1 == cap2 then ref1 else ref2).map(h)
-  val ref4c: LazyList[Int]^{cap1, ref3, cap3} = ref4 // error
+  val ref4c: LazyList[Int]^{cap1, ref3} = ref4 // error

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

@@ -0,0 +1,21 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:17:13 -----------------------------------------
+17 |  val _: D = x1 // error
+   |             ^^
+   |             Found:    (x1 : D^{d1})
+   |             Required: D
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:18:13 -----------------------------------------
+18 |  val _: D = x2 // error
+   |             ^^
+   |             Found:    (x2 : D^{d1})
+   |             Required: D
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lubs.scala:19:13 -----------------------------------------
+19 |  val _: D = x3 // error
+   |             ^^
+   |             Found:    (x3 : D^{d1, d2})
+   |             Required: D
+   |
+   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,20 @@
+import java.sql.Date
+
+class C extends caps.Capability
+class D
+
+def Test(c1: C, c2: C) =
+  val d: D = ???
+  val d1: D^{c1} = ???
+  val d2: D^{c2} = ???
+  val x1 = if ??? then d else d1
+  val _: D^{c1} = x1
+  val x2 = if ??? then d1 else d
+  val _: D^{c1} = x2
+  val x3 = if ??? then d1 else d2
+  val _: D^{c1, c2} = x3
+
+  val _: D = x1 // error
+  val _: D = x2 // error
+  val _: D = x3 // error
+

tests/neg-custom-args/captures/spread-problem.check

@@ -0,0 +1,14 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:8:6 ---------------------------------
+8 |  race(Seq(src1, src2)*) // error
+  |  ^^^^^^^^^^^^^^^^^^^^^^
+  |  Found:    Source[box T^?]^{src1, src2}
+  |  Required: Source[T]
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/spread-problem.scala:11:6 --------------------------------
+11 |  race(src1, src2) // error
+   |  ^^^^^^^^^^^^^^^^
+   |  Found:    Source[box T^?]^{src1, src2}
+   |  Required: Source[T]
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/spread-problem.scala

@@ -0,0 +1,11 @@
+import language.experimental.captureChecking
+
+trait Source[+T]
+
+def race[T](@caps.unbox sources: (Source[T]^)*): Source[T]^{sources*} = ???
+
+def raceTwo[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
+  race(Seq(src1, src2)*) // error
+
+def raceThree[T](src1: Source[T]^, src2: Source[T]^): Source[T]^{} =
+  race(src1, src2) // error