Type bound breaks extraction of covariant type parameter from singleton type

[prolativ]

Compiler version

3.2.1, 3.3.0-RC1-bin-20221209-231f9ab-NIGHTLY
Used to work in 3.1.3

Minimized code

class Box[+A](a: A)
val box: Box[Int] = Box(123)

type Elem[T] = T match
  case Box[a] => a

def x1[F](f: F): Elem[f.type] = ???
def y1 = x1(box)

def x2[F <: Box[Any]](f: F): Elem[f.type] = ???
def y2 = x2(box)

Output

As seen in REPL:

// defined case class Box
val box: Box[Int] = Box(123)
def x1[F](f: F): Elem[f.type]
def y1: Int
def x2[F <: Box[Any]](f: F): Any
def y2: Any

Expectation

Elem[f.type] should be properly computed as Int, as in 3.1.3:

// defined case class Box
val box: Box[Int] = Box(123)
def x1[F](f: F): Elem[f.type]
def y1: Int
def x2[F <: Box[Any]](f: F): Elem[f.type]
def y2: Int

[odersky]

I don't think you can expect this to work with a covariant box, since the match type has nothing to work with. It certainly cannot give a unique instantiation of a.

It does work if Box is invariant:

class Box[A](a: A)
val box: Box[Int] = Box(123)

type Elem[T] = T match
  case Box[a] => a

def x1[F](f: F): Elem[f.type] = ???
def y1 = x1(box)

def x2[F <: Box[?]](f: F): Elem[f.type] = ???
def y2: Elem[box.type] = x2(box)

[prolativ]

What seems strange to me here is that it works with a covariant Box if we give the compiler less clues by not specifying a type bound at all

def x1[F](f: F): Elem[f.type]
def y1: Int

Also somehow this used to work for some time with covariance and a type bound. I'm trying to bisect it now. Currently I got to this point:

Last good release: 3.2.0-RC1-bin-20220530-d6e3d12-NIGHTLY
First bad release: 3.2.0-RC1-bin-20220531-e2efddc-NIGHTLY
Starting bisecting commits d6e3d12..e2efddc

[prolativ]

Bisection seems to point to 02f775f791

[dwijnand]

Looks similar enough that it would probably compile as desired with #16206.

[dwijnand]

Yeah, like that issue, Elem[f.type] eagerly widens to Any, leaving no chance for when f: Box[Int] for the result to become Int. In the other issue y eagerly widens to NatT, so the reduction gets stuck.

[DmytroMitin]

Not reproducible in 3.2.2 https://scastie.scala-lang.org/DmytroMitin/eECHNH2IRdCKRUNPU4x0Vg/1

[prolativ]

@DmytroMitin the issue is still there but it's not directly observable when you just compile this snippet in a file or in scastie. It becomes evident if you change def y2 = x2(box) to def y2: Int = x2(box)

[dwijnand]

Fixed with #17180