Wrong result of subtyping with modularity, refined types, and singleton types

[noti0na1]

Compiler version

3.7.3-RC1-bin-SNAPSHOT-nonbootstrapped-git-699296f

Minimized code

import language.experimental.modularity

class A[+T]

class B(tracked val x: AnyRef) extends A[x.type]

def test1 =
  val a: AnyRef = ???
  val b: B { val x: a.type } = B(a)
  val c: A[a.type] = b

A version with capture sets:

import language.experimental.captureChecking
import language.experimental.modularity
import caps.*

class A[+T]:
  def f: A[T]^{this} = this

class B(tracked val x: AnyRef^) extends A[AnyRef^{x}]

def test1 =
  val a: AnyRef^ = ???
  val b = B(a)
  val c: A[AnyRef^{a}]^{a} = b

Output

-- [E007] Type Mismatch Error ------------------------------
    |  val c: A[a.type] = b
    |                     ^
    |                     Found:    (b : B{val x: (a : AnyRef)})
    |                     Required: A[(a : AnyRef)]
    |---------------------------------------------------------------------------
    | Explanation (enabled by `-explain`)
    |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    |
    | Tree:
    |
    | b
    |
    | I tried to show that
    |   (b : B{val x: (a : AnyRef)})
    | conforms to
    |   A[(a : AnyRef)]
    | but none of the attempts shown below succeeded:
    |
    |   ==> (b : B{val x: (a : AnyRef)})  <:  A[(a : AnyRef)]
    |     ==> A[(B.this.x : AnyRef)]  <:  A[(a : AnyRef)]
    |       ==> (B.this.x : AnyRef)  <:  (a : AnyRef)
    |         ==> AnyRef  <:  (a : AnyRef)
    |           ==> Object  <:  (a : AnyRef)  = false
    |
    | The tests were made under the empty constraint
     ---------------------------------------------------------------------------

Expectation

Subtyping success