Dotty: A variable should be best instantiation of pattern type (SI-6680 redux)

[S11001001]

Given

trait Stream[+A] 
case class Unfold[S,+A](s: S, f: S => Option[(A,S)]) extends Stream[A] 

You get this warning, and an associated unsound inferred type, as in SI-6680 “Unsoundness bug in pattern matcher when pattern reveals existentials”:

scala> def unbox[A](s: Stream[A]) = s match {case Unfold(s, f) => (s, f)} 
-- Warning: <console> ----------------------------------------------------------
7 |def unbox[A](s: Stream[A]) = s match {case Unfold(s, f) => (s, f)}
  |                                           ^^^^^^^^^^^^
  |           There is no best instantiation of pattern type Unfold[Any^, A^]
  |           that makes it a subtype of selector type Stream[A].
  |           Non-variant type variable S cannot be uniquely instantiated.
  |           (This would be an error under strict mode)
def unbox[A](s: Stream[A]): [A] => (s: Stream[A])(Any, Any => Option[(A, Any)])

But there is a ‘best’ choice, which is moreover sound, which is to introduce a fresh type variable, as you can write explicitly with type pattern variables.

scala> def unbox[A](s: Stream[A]) = s match {
  case u: Unfold[ts, A] =>
    u.s: ts  // the name chosen in this block
    (u.s, u.f)
} 
def unbox[A](s: Stream[A]): [A] => (s: Stream[A])(Any, _ => Option[(A, Any)])

This is based on 39c27b6a8aaa2c7303db54011082246ada06c0a0.

/cc @pchiusano

[smarter]

I agree. I wrote down some thoughts on GADTs at https://gist.github.com/smarter/2e1c564c83bae58c65b4f3f041bfb15f but haven't had time to actually fix things yet. There was also some related discussions recently at https://gist.github.com/AleksanderBG/34ee1d9a9de3925800901f6ce7cb5c93

Before fixing this it would probably be wise to take care of https://github.com/lampepfl/dotty/issues/1754

[odersky]

This is fixed by #3889