Prevent matching into or out of an opaque type

[LPTK]

One of the stated goals of opaque types is to statically enforce invariants about some values without wrapping them. To achieve this, we must control what values are allowed to get converted into and out of the opaque type.

Matching on opaque types is currently allowed, and break this. For instance, it is possible to convert an immutable array into a mutable one by matching on it, which defeats its purpose.

minimized code

@main def main = {
  
  // conversion into the opaque type:
  val arr = Array(1,2,3)
  val imm0: IArray[Int] // supposedly immutable
    = oops(arr)
  println(imm0(0)) // 1
  arr(0) = 0
  println(imm0(0)) // 0, the value has changed!
  
  // conversion out of the opaque type:
  val imm1 = IArray(1,2,3) // supposedly immutable
  println(imm1(0)) // 1
  imm1 match {
    case a: Array[Int] =>
      a(0) = 0
  }
  println(imm1(0)) // 0
  
}

def oops(a: Array[Int]): IArray[Int] = a match {
  case a: IArray[Int] => a
}

https://scastie.scala-lang.org/hV46dfNWR6iTP2uLIMfS2g

expectation

Both matches should be rejected, or at the very least give warnings.

[odersky]

I agree they should give unchecked warnings.

[abgruszecki]

See also #5467, which may be counted as a duplicate.

[odersky]

In fact, matching against an Array cannot be put under an unchecked flag, so whatever we do it's still leaky. You can detect & flag

imm1 match {
    case a: Array[Int] =>
      a(0) = 0
  }

but you cannot flag

imm1: Any match {
    case a: Array[Int] =>
      a(0) = 0
  }

So, what's the point? You can check against IArray[T], but that's only one direction (and the less important one, it seems).

[LPTK]

Good point. The abstraction is really leaky.

So, what's the point?

I think it's still useful to flag both of the specific examples I showed above.

The ability to silence warnings by upcasting to Any is not specific to this (it can also be done for exhaustiveness warnings, where it also leads to bad things — runtime match errors).

Also, coding guidelines like scalazzi discourage using Any, and especially discourage matching on a scrutinee of a type like Any (or a type parameter) on which we know nothing. The idea is that matching to gain hidden type information breaks parametricity. If a user follows these guidelines and respects the warnings I propose, then the abstraction is not leaky anymore.

[odersky]

So, this is much harder than it looks at first. If one of the two types in the comparison is an opaque type (or has one in a union or intersection), and the other is a different type, we have to figure out whether the match is already implied by the types, or whether it needs runtime information. This looks like a fairly hard problem, similar to the problem of deciding whether a cast can fail.

I think the problem should be solved, by not by myself. I have too much else on my plate.

[abgruszecki]

It sounds very similar to what we need to do when inferring GADT constraints - I'll take a look at it when I have the time.

[dwijnand]

Note that the second half of this ticket ("conversion out of the opaque type") is fixed under -source future with the introduction of Matchable (see the Parametric Top Type backlink).

Converting into an opaque type is still an issue. Let's call this one fixed, and use #5467 for the part about emitting unchecked warnings when one uses an opaque type in a type pattern.