Member selection does not take GADT constraints into account

[wdanilo]

minimized code

case class Seg[T](pat:Pat[T], body:T)

trait Pat[T]
object Pat {
  case class Expr()            extends Pat[Int]
  case class Opt[S](el:Pat[S]) extends Pat[Option[S]]
}
  
def test[T](s:Seg[T]):Int = s match {
  case Seg(Pat.Expr(),body)          => (body: Int) + 1
  case Seg(Pat.Opt(Pat.Expr()),body) => (body: Option[Int]).get
}

expectation

As a long-time Haskeller, I would expect the above code to compile without providing the explicit signatures (body: Int) and (body: Option[Int]). The compiler has enough information to know that (especially as it does not allow me to write any other signature there). Writing them by hand is cumbersome and breaks the beauty of GADTs. I feel this is a very serious GADTs limitation in Dotty. I know that in Scala 2.x it was worse and unsound, but what we see in Dotty is rather a partial solution, not a final one.

[bishabosha]

Hi thanks for reporting, this is very related to #6323, perhaps you could add your comments to it?

[smarter]

Yeah this is a duplicate of #6323

[abgruszecki]

Opening in preference to #6323.