Very obscure error message when cause is unboxing of parameter bounds

[odersky]

Compiler version

3.8.0-RC2

Minimized example

import scala.language.experimental.captureChecking

def hh[T <: Ref^](x: Box[T]): Unit =
  val y: (Ref^, Int) = (x.elem, 1)

Output

4 |  val y: (Ref^, Int) = (x.elem, 1)
  |                       ^^^^^^^^^^^
  |    Found:    (T^'s1, Int)
  |    Required: (Ref^, Int)
  |
  |    Note that capability cap is not included in capture set {}.
  |
  |    where:    ^   refers to a fresh root capability in the type of value y
  |              cap is a fresh root capability in the type of type T
  |
  | longer explanation available when compiling with `-explain`

Expectation

Either no error, or a clearer error message that shows the cause of the problem. If I compile with -explain -Ycc-verbose I see

4 |  val y: (Ref^, Int) = (x.elem, 1)
  |                       ^^^^^^^^^^^
  |          Found:    (box T^'s1, Int)
  |          Required: (box Ref^{cap}, Int)
  |
  |          Note that capability cap² is not included in capture set {}.
  |
  |          where:    cap  is a fresh root capability in the type of value y
  |                    cap² is a fresh root capability in the type of type T
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree:
  |
  | Tuple2.apply[T, Int](x.elem, 1)
  |
  | I tried to show that
  |   (box T^'s1, Int)
  | conforms to
  |   (box Ref^{<fresh in value y hiding 's2>}, Int)
  | but none of the attempts shown below succeeded:
  |
  |   ==> (box T^'s1, Int)  <:  (box Ref^{<fresh in value y hiding 's2>}, Int)
  |     ==> box T^'s1  <:  box Ref^{<fresh in value y hiding 's2>}
  |       ==> T  <:  Ref^{<fresh in value y hiding 's2>}
  |         ==> T  <:  Ref
  |           ==> box Ref^{<fresh in method hh hiding 's3>}  <:  Ref
  |             ==> subcaptures {<fresh in method hh hiding 's3>} <:< {} in open varState
  |               ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |         ==> box Ref^{<fresh in method hh hiding 's3>}  <:  Ref^{<fresh in value y hiding 's2>}
  |           ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |           ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |     ==> (box T^'s1, Int)  <:  (box Ref^{<fresh in value y hiding '{<fresh in method hh hiding 's3>}>}, Int)
  |       ==> box T^'s1  <:  box Ref^{<fresh in value y hiding '{<fresh in method hh hiding 's3>}>}
  |         ==> T  <:  Ref^{<fresh in value y hiding '{<fresh in method hh hiding 's3>}>}
  |           ==> T  <:  Ref
  |             ==> box Ref^{<fresh in method hh hiding 's3>}  <:  Ref
  |               ==> subcaptures {<fresh in method hh hiding 's3>} <:< {} in open varState
  |                 ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |           ==> box Ref^{<fresh in method hh hiding 's3>}  <:  Ref^{<fresh in value y hiding '{<fresh in method hh hiding 's3>}>}
  |             ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |             ==> {} accountsFor <fresh in method hh hiding 's3> with {<fresh in method hh hiding 's3>}  = false
  |
  | The tests were made under the empty constraint

The critical part are in the last three lines: We are comparing a box Ref^ with a Ref^, that's why it fails.

[Linyxus]

Looking at the trace, I think this is an expressiveness issue. For instance, the following perfectly valid code will not compile either, with the same error message:

import scala.language.experimental.captureChecking
class Ref
case class Box[+T](elem: T)

def test1(a: Ref^): Unit =
  def hh[T <: Ref^{a}](x: Box[T]): Unit =
    val y: (Ref^{a}, Int) = (x.elem, 1)

[odersky]

I agree it's an expressiveness issue. This should have undergone box adaptation before we run into the error. I am not sure why box adaptation does not work here.

[odersky]

Interestingly, it compiles if we do it in two steps:

def test1(a: Ref^): Unit =
  def hh[T <: Ref^{a}](x: Box[T]): Unit =
    val y = (x.elem, 1)
    val z: (Ref^{a}, Int) = y  // ok!

[Linyxus]

Indeed! What happened is that:

• We try to show box T^s1 is a subtype of box Ref^{a}. Note: the box T^s1 type is already a bit surprising to me, since T is a type parameter and should always be boxed, yet we are still installing capture set variables for it. This happens in Tuple2.apply[box T^s1, Int](...), where T is passed as a type argument to the tuple constructor. This actually makes this type a "doubly"-boxed type: box T^s1 is now upper bounded by box (box Ref^{a})^s1.
• We see both sides are boxed, so we simply stripped boxes from both sides. But on the LHS, there is one more level of boxes inside.
• When the subtype test proceeds, we will fail with unmatched box status.

[odersky]

@Linyxus Your analysis was right on spot. I could now fix the underlying problem in #24546.