List encoding checking failure due to boxing

[odersky]

Compiler version

3.nightly

Minimized example

package listEncoding
import annotation.retains

class Cap

type Op[T, C] =
  T => C => C


class STR // used to be pure class String but then the errors don't show up.

type List[T] =
  [C] -> (op: Op[T, C]) -> (s: C) ->{op} C

def nil[T]: List[T] =
  [C] => (op: Op[T, C]) => (s: C) => s

def cons[T](hd: T, tl: List[T]): List[T] =
  [C] => (op: Op[T, C]) => (s: C) => op(hd)(tl(op)(s))

def foo(c: Cap^) =
  def f(x: STR @retains[c.type], y: STR @retains[c.type]) =
    cons(x, cons(y, nil))  // error, should this work?
  def f_explicit(x: STR @retains[c.type], y: STR @retains[c.type])
    : [C] => (op: STR^{x, y} => C => C) -> (s: C) ->{op} C =
    cons(x, cons(y, nil))  // error, should this work?
  def g(x: STR @retains[c.type], y: Any) =
    cons(x, cons(y, nil))
  def h(x: STR, y: Any @retains[c.type]) =
    cons(x, cons(y, nil))

Output

-- Error: list-encoding.scala:23:8 ---------------------------------------------
23 |    cons(x, cons(y, nil))  // error, should this work?
   |    ^^^^^^^^^^^^^^^^^^^^^
   |listEncoding.STR^? ->? C ->? C cannot be box-converted to box listEncoding.STR^{x, y} ->{cap, x, y} C² => C²
   |since the additional capture set {x, y} resulting from box conversion is not allowed in box listEncoding.STR^{x, y} => C² => C²
   |
   |where:    =>  refers to the universal root capability
   |          C   is a type variable
   |          C²  is a type variable
   |          cap is the universal root capability
-- Error: list-encoding.scala:26:8 ---------------------------------------------
26 |    cons(x, cons(y, nil))  // error, should this work?
   |    ^^^^^^^^^^^^^^^^^^^^^
   |listEncoding.STR^{x, y} => C => C cannot be box-converted to box listEncoding.STR^{x, y} ->{cap, x, y} C² => C²
   |since the additional capture set {x, y} resulting from box conversion is not allowed in box listEncoding.STR^{x, y} => C² => C²
   |
   |where:    =>  refers to the universal root capability
   |          C   is a type variable
   |          C²  is a type variable
   |          cap is the universal root capability
2 errors found

Expectation

Not sure. Should this compile, or are the box errors correct? This used to work with String instead of STR, but String is a pure class which means its capture set is ignored. So because of that the problem was likely hidden for a long time.

[odersky]

The failing test will be in pending/pos-custom-args/captures/list-encoding.scala