epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

Allow for redundant type checks for pattern matching #1489

Closed mario-bucev closed 8 months ago

mario-bucev commented 8 months ago

Allows for ascribing type parameters to e.g. tuples patterns, such as in the following snippet:

def test[A, B, C](a: A, b: B, c: C): Unit = {
  // annotating aa, bb and cc with their respecting type
  val (aa: A, bb: B, cc: C) = (a, b, c)
}

This was previously rejected. Note that the Scala 2 compiler will issue spurious warnings saying that these type tests cannot be checked at runtime (which is true, but they can be checked at compile time :yum:).