Subtyping info lost when pattern matching on type of expression

[prolativ]

Compiler version

3.2.1-RC1-bin-20220721-634c580-NIGHTLY and earlier

Minimized code

//> using scala "3.2.1-RC1-bin-20220721-634c580-NIGHTLY"

import scala.quoted.*

trait Foo:
  type Number <: Int

trait Bar[T <: Int]

private def collectImpl[T : Type](using Quotes) =
  val expr: Expr[Foo] = ???
  expr match
    case '{ $enc: Foo { type Number = num } } =>
      Type.of[T] match
        case '[Bar[`num`]] => '{}

Output

[error] Macro.scala:15:20: Type argument num does not conform to upper bound Int
[error]         case '[Bar[`num`]] => '{}
[error]                    ^

Expectation

The compiler should be aware that num has to be a subtype of Int and the compilation should succeed

[nightscape]

@prolativ I'm just looking at the code of iskra, trying to implement the *.
Is this the reason the effort got stuck?

[prolativ]

No, this should not be a blocker. I believe this problem could be worked around by replacing

case '[Bar[`num`]] =>

with

case '[Bar[n]] if Type.of[n] == Type.of[num] =>

[nicolasstucki]

You probably need something like

Type.of[n] =:= Type.of[num]

[nicolasstucki]

Solution

-    case '{ $enc: Foo { type Number = num } } =>
+    case '{ type num <: Int; $enc: Foo { type Number = `num` } } =>

[prolativ]

@nicolasstucki was there any code changed in the compiler to fix this (there's no PR linked here)? Or is your SIP supposed to actually solve the problem?

[nicolasstucki]

It is not a feature that is intended to work. In general, we have many issues related to type variable bound inference. We know that we should not be inferring those bounds because this kind of inference goes beyond what Scala is supposed to be able to do. A second issue is that this inference can infer useless bounds such as <: Nothing, while correct it makes the patterns not match the intended cases.

I am still working on a migration path out of this issue. I will open a SIP once I have all the pieces figured out.

This ability to infer type variable bounds was added as a workaround to be able have type matches with the variables that are bounded. Now we solved the original limitation with SIP-53. This SIP was the first step toward fixing this problem.

I also need to revisit #16932 (now revisited in #18195).