Somewhat better error notes for box failures

At least we don't get

    Note that cap is not included in {}

anymore. To make this even better we'd have to trace back a box
failure to the original types we were trying to compare. Right now
the box failure error notes are too disconnected from the rest. But
they become clearer when one compiles with -explain.

Author: odersky

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

@@ -576,6 +576,9 @@ object CaptureSet:
     cs.mutability = Mutability.Reader
     cs
 
+  class EmptyOfBoxed(val tp1: Type, val tp2: Type) extends Const(emptyRefs):
+    override def toString = "{} of boxed mismatch"
+
   /** The universal capture set `{cap}` */
   def universal(using Context): Const =
     Const(SimpleIdentitySet(GlobalCap))
@@ -1328,15 +1331,19 @@ object CaptureSet:
       case _ =>
         false
 
-    /** An include failure F1 covers another include failure F2 unless F2
-     *  strictly subsumes F1, which means they describe the same capture sets
-     *  and the element in F2 is more specific than the element in F1.
+    /** An include failure F1 covers another include failure F2 unless one
+     *  of the following two conditons holds:
+     *   1. F2 strictly subsumes F1, which means they describe the same capture sets
+     *      and the element in F2 is more specific than the element in F1.
+     *   2. Both F1 and F2 are the empty set, but only F2 is an empty set synthesized
+     *      when comparing types with different box status
      */
     override def covers(other: Note)(using Context) = other match
       case other @ IncludeFailure(cs1, elem1, _) =>
         val strictlySubsumes =
           cs.elems == cs1.elems
-          && elem1.singletonCaptureSet.mightSubcapture(elem.singletonCaptureSet)
+          && (elem1.singletonCaptureSet.mightSubcapture(elem.singletonCaptureSet)
+              || cs1.isInstanceOf[EmptyOfBoxed] && !cs.isInstanceOf[EmptyOfBoxed])
         !strictlySubsumes
       case _ => false
 
@@ -1377,6 +1384,11 @@ object CaptureSet:
         else
           trailing:
             i"capability ${elem.showAsCapability} cannot be included in capture set $cs"
+      case cs: EmptyOfBoxed =>
+        trailing:
+          val (boxed, unboxed) =
+            if cs.tp1.isBoxedCapturing then (cs.tp1, cs.tp2) else (cs.tp2, cs.tp1)
+          i"${cs.tp1} does not conform to ${cs.tp2} because $boxed is boxed but $unboxed is not"
       case _ =>
         def why =
           val reasons = cs.elems.toList.collect:

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

@@ -2915,8 +2915,8 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         case _ =>
     subc
     && (tp1.isBoxedCapturing == tp2.isBoxedCapturing
-        || refs1.subCaptures(CaptureSet.empty, makeVarState()))
-
+        || refs1.subCaptures(CaptureSet.EmptyOfBoxed(tp1, tp2), makeVarState()))
+        
   protected def logUndoAction(action: () => Unit) =
     undoLog += action
 

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

@@ -4,6 +4,6 @@
   |         Found:    (g : () -> A)
   |         Required: () -> Proc^{f}
   |
-  |         Note that capability f is not included in capture set {}.
+  |         Note that () ->{f} Unit does not conform to Proc^{f} because () ->{f} Unit is boxed but Proc^{f} is not.
   |
   | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,24 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24543.scala:7:23 ----------------------------------------
+7 |  val y: (Ref^, Int) = (x.elem, 1) // error
+  |                       ^^^^^^^^^^^
+  |                       Found:    (T^'s1, Int)
+  |                       Required: (Ref^, Int)
+  |
+  |                       Note that Ref^² does not conform to Ref^ because Ref^² is boxed but Ref^ is not.
+  |
+  |                       where:    ^  refers to a fresh root capability in the type of value y
+  |                                 ^² refers to a fresh root capability in the type of type T
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i24543.scala:9:45 ----------------------------------------
+9 |def h2[T <: Ref^](x: List[T]): (Ref^, Int) = (x.head, 1) // error
+  |                                             ^^^^^^^^^^^
+  |                                  Found:    (T^'s2, Int)
+  |                                  Required: (Ref^, Int)
+  |
+  |                                  Note that Ref^² does not conform to Ref^ because Ref^² is boxed but Ref^ is not.
+  |
+  |                                  where:    ^  refers to a fresh root capability in the result type of method h2
+  |                                            ^² refers to a fresh root capability in the type of type T
+  |
+  | longer explanation available when compiling with `-explain`

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

@@ -0,0 +1,12 @@
+import scala.language.experimental.captureChecking
+
+class Ref
+case class Box[T](elem: T)
+
+def h1[T <: Ref^](x: Box[T]): Unit =
+  val y: (Ref^, Int) = (x.elem, 1) // error
+
+def h2[T <: Ref^](x: List[T]): (Ref^, Int) = (x.head, 1) // error
+
+
+