Dotty: Pattern matching with type annotations allows impossible cases

[Jacoby6000]

This should not compile:

  sealed trait Foo[T]
  case class Bar[T](s: String)

  def shouldError[T](foo: Foo[T]): String = 
    foo match {
      case bar: Bar[T] => bar.s
    }

Not even a warning is produced, as is.

[allanrenucci]

Note that the warning produced by scalac is not an exhaustivity warning:

warning: abstract type T in type pattern Bar[T] is unchecked since it is eliminated by erasure

scalac (and dotc) will not complain for:

sealed trait Foo
class Bar

class Test {
  def shouldError(foo: Foo) = foo match {
    case _: Bar => 1
  }
}

If Foo is a class, both scalac and dotc reject the program.

[Jacoby6000]

@allanrenucci will your changes cause the sample you and I provided produce an error? I haven't poked around in dotty at all, but in general compilers should error whenever you have a situation where the type being matched on is not a super type of the case.

[Jacoby6000]

@liufengyun I'd like this to be re-opened, since what was resolved was actually unrelated to what I was concerned about. My example was perhaps bad. @allanrenucci touched on what I was talking about.

The below example compiles, but should error:

  sealed trait Foo
  case class Bar(s: String)

  def shouldError(foo: Foo): String = 
    foo match {
      case bar: Bar => bar.s
    }

I'm so used to generalizing that I did an un-necessary generalization in my earlier example which confused the issue.

[liufengyun]

Scalac accepts the code above, as Dotty does. @Jacoby6000 can you specify why you think it should error?

[allanrenucci]

Since Foo is sealed, is it safe to say that case bar: Bar is unreachable?

[smarter]

No, you could have class Bla extends Bar("") with Foo.

[allanrenucci]

No, you could have class Bla extends Bar("") with Foo.

I agree if Foo was not sealed. But in this example, we know such a class Bla does not exist

[smarter]

More complicated example:

sealed trait Foo
trait Child extends Foo
case class Bar(s: String)
class Bla extends Bar("") with Child // This could be in a different file

The only thing we know for sure is that Foo has a single direct child trait Child, but we know nothing about the children of the child trait.

[liufengyun]

Yes, it's unreachable, because the checker knows that Foo doesn't have any child. In @smarter 's example, the checker knows that Child is the only child of Foo, which could have children elsewhere.

However, the Dotty checker tries to save some cycles by avoiding checking redundancy of the first clause. I guess Scalac checker intentionally does that as well. The Dotty checker also avoids doing an intersection of the pattern with the scrutinee for performance reasons.

We can revert the optimisations to generate more warnings, but maybe after we see a real-world example where it causes problems.

[Jacoby6000]

I'm really confused about why there is so much discussion around this. The discussion I've read seems to be worrying about things which do not matter.

Even in the situation that smarter specified, it should not matter. The match is specifically matching on a Foo. It should only check for Foo. It should not allow for matching on types which do not extend Foo. What is the usecase for such a thing? Why should it ever be allowed? It seems like if you ever want to do this, you're doing something wrong anyway.

Ignoring dotty semantics and focusing on what's correct, the scenario @smarter mentioned (or any scenario) should not warrant the pattern matcher treating a concrete type as Any.

The real world example where it causes problems, is anywhere people want type-safety in a pattern match.

I'd argue that supporting this just because of the with case is confusing and surprising to anybody.

[Jacoby6000]

Scalac currently agrees with me: https://scastie.scala-lang.org/Jacoby6000/QrCM9aQ5QVKS5aDMn2r2Yw. Though, in my opinion this should be a type error rather than a warning.

[allanrenucci]

Scalac agrees with you for the same reasons described above. If you remove the sealed modifier from trait Foo then case b: Baz => becomes reachable and scalac won't emit a warning.

[Jacoby6000]

Doesn't this mean that pattern matching on concrete types treats that type as Any? Isn't that wrong?

[Jacoby6000]

I'm starting to understand that as long as the type system has covariance, as well as intersections between types, then this must be supported. I still think it's bad, but you do what you have to do. How about we throw away subtyping and variance and just use proper ADTs? 😃

[smarter]

A compromise would be to disallow (foo: Foo) match { case bar: Bar => ... but allow (foo: Foo) match { case bar: Foo & Bar => ...

[Jacoby6000]

I like that. To me that makes much more sense.