Regression from Scala 2: Type variable in pattern match works with invariant type, fails with covariant

[SethTisue]

Scala 2.13.8 accepts both of these:

scala> def foo[T](xs: Set[T]): T = xs match { case xs: Set[u] => xs.head: u }
def foo[T](xs: Set[T]): T

scala> def foo[T](xs: List[T]): T = xs match { case xs: List[u] => xs.head: u }
def foo[T](xs: List[T]): T

Scala 3 accepts the Set one, but fails on the List version. with -explain for verbosity,

scala> def foo[T](xs: List[T]): T = xs match { case xs: List[u] => xs.head: u }
-- [E007] Type Mismatch Error: -------------------------------------------------
1 |def foo[T](xs: List[T]): T = xs match { case xs: List[u] => xs.head: u }
  |                                                            ^^^^^^^^^^
  |                                                            Found:    u
  |                                                            Required: T
  |-----------------------------------------------------------------------------
  | Explanation (enabled by `-explain`)
  |- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
  |
  | Tree: xs.head:u
  | I tried to show that
  |   u
  | conforms to
  |   T
  | but the comparison trace ended with `false`:
  |
  |   ==> u  <:  T
  |     ==> u  <:  Nothing in frozen constraint
  |       ==> Any  <:  Nothing (left is approximated) in frozen constraint
  |       <== Any  <:  Nothing (left is approximated) in frozen constraint = false
  |       ==> Any  <:  Nothing in frozen constraint
  |       <== Any  <:  Nothing in frozen constraint = false
  |     <== u  <:  Nothing in frozen constraint = false
  |     ==> Any  <:  T (left is approximated)
  |       ==> Any  <:  Nothing in frozen constraint
  |       <== Any  <:  Nothing in frozen constraint = false
  |     <== Any  <:  T (left is approximated) = false
  |     ==> Any  <:  T in frozen constraint
  |       ==> Any  <:  Nothing in frozen constraint
  |       <== Any  <:  Nothing in frozen constraint = false
  |     <== Any  <:  T in frozen constraint = false
  |   <== u  <:  T = false
  |
  | The tests were made under the empty constraint
   -----------------------------------------------------------------------------

I assume that the difference between Set and List here is that Set is invariant, List covariant.

(fyi @dwijnand; this came up during one of our pairing sessions)

[dwijnand]

This came up during the fix https://github.com/lampepfl/dotty/pull/14425/files, but the changes there are only in quotes so it's still broken now.

[odersky]

I think that's because the Scala 2 version is unsound. I let @abgruszecki confirm.

[dwijnand]

Unless you're referring to something else, I see now: it's not inferring the right type because it fears the type could have been refined to some unrelated type, i.e. why #11834 wants a warning. But List is sealed so it's plausible GADT reasoning could allow for that type to be inferred, I believe, as it sees that there are no funky mixing of List and another instantiation of IterableOps +A type parameter (which is where def head: A is defined). Unless we're concerned that under separate compilation someone could introduce that problematic class?

Also, this should work with the change I'm trying to make for that very issue #11834 by making funky mixes illegal.

[abgruszecki]

It's not an unsoundness problem, we definitely should be able to do better. In fact, we would do better if we had an unapply method that would do the typecheck for us, i.e. something like this:

object Lst:
  def unapply[T](l: List[T]): Option[List[T]] = Some(l)
def foo[T](l: List[T]) = l match { case Lst(l2) => l2 : List[T] }

This issue is just a deficiency in how we handle type case patterns.

[anatoliykmetyuk]

This issue was picked for the Issue Spree 14 of 12th April which takes place in a week from now. @dwijnand and @dos65 will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

[anatoliykmetyuk]

This issue was picked for the Issue Spree 15 of May 3rd which takes place a week from now. @dwijnand and @joke1196 will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.