An opaque type should not be covariant when the underlying type is invariant

[Atry]

Compiler version

3.1.0

Minimized code

opaque type CovariantArray[+A] = Array[A]

object CovariantArray:
  def crash() =
    val stringArray: CovariantArray[String] = Array("foo", "bar")
    val anyArray: CovariantArray[Any] = stringArray
    anyArray(0) = 42
    stringArray(0).length

CovariantArray.crash()

Output

java.lang.ArrayStoreException: java.lang.Integer
	at Playground$CovariantArray$.crash(main.scala:9)
	at Playground$.<clinit>(main.scala:12)
	... 13 more

Expectation

Should not compile

[KacperFKorban]

Looks like a soundness issue. For non-primitives, it throws ClassCastException at runtime, with no compilation errors.

case class Invariant[A](var a: A)

opaque type CovariantArray[+A] = Invariant[A]

object CovariantArray:
  def crash() =
    val stringArray: CovariantArray[String] = Invariant("foo")
    val anyArray: CovariantArray[Any] = stringArray
    anyArray.a = 42
    stringArray.a.length

@main
def main =
  CovariantArray.crash()

Stacktrace:

Exception in thread main: java.lang.ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String (java.lang.Integer and java.lang.String are in module java.base of loader 'bootstrap')
    at method crash in main$package$CovariantArray$:10 
    at method main in main.scala:14

[smarter]

The variance checker on top-level types should be called from https://github.com/lampepfl/dotty/blob/51828cc215ac2b181b6a978144e33e971ba01589/compiler/src/dotty/tools/dotc/transform/PostTyper.scala#L380, I don't know if it's not called at all here or if the check is incomplete.

[prolativ]

Actually I would say we could still preserve soundness if only the compiler was able to prove that if we define an opaque type with covariant or contravariant type parameters we don't use them in contravariant and covariant manners respectively. E.g.
this code makes sense and doesn't have soundness problems

import scala.reflect.ClassTag

trait Polygon(val edgesCount: Int)

class Triangle extends Polygon(3)
class Square extends Polygon(4)

object Opaque:
  opaque type CovariantArray[+A] = Array[A]
  
  object CovariantArray:
    def apply[A : ClassTag](elems: A*): CovariantArray[A] = Array(elems*)

    extension [A : ClassTag](arr: CovariantArray[A])
      def ++[B : ClassTag](arr2: CovariantArray[B])(using ClassTag[A | B]): CovariantArray[A | B] =
        val elems: Seq[A | B] = arr.toSeq ++ arr2.toSeq
        elems.toArray
      def elems: Seq[A] = arr.toSeq

import Opaque.CovariantArray

def countEgdes(polygons: CovariantArray[Polygon]) = polygons.elems.map(_.edgesCount).sum[Int]

@main def run() =
  val triangles: CovariantArray[Triangle] = CovariantArray(new Triangle)
  val squares: CovariantArray[Square] = CovariantArray(new Square)
  val polygons: CovariantArray[Polygon] = triangles ++ squares
  println(countEgdes(triangles))
  println(countEgdes(polygons))

Not sure how useful this would be but we can implement a covariant/immutable data structure backed by an invariant/mutable one

[smarter]

opaque type CovariantArray[+A] = Array[A]

We can already achieve something like this using wildcards: https://github.com/lampepfl/dotty/blob/51828cc215ac2b181b6a978144e33e971ba01589/library/src/scala/IArray.scala#L8, more complicated checks don't seem worth it (and would be very hard to implement correctly I think).

[prolativ]

The trick with a wildcard will indeed prevent you from inserting an Int to an array of Strings but then you can't even insert a String, which should work:

opaque type CovariantArray[+A] = Array[_ <: A]

object CovariantArray:
  def test() =
    val stringArray: CovariantArray[String] = Array("foo", "bar")
    stringArray(0) = "baz"

@main def run() =
  CovariantArray.test()

[error] Found:    ("baz" : String)
[error] Required: stringArray.T
[error]     stringArray(0) = "baz"
[error]                      ^^^^^

[smarter]

In any case you can always use @uncheckedVariance if you believe you know better than the compiler.

[prolativ]

@smarter where should I put the annotation? I tried putting it in different places to make my example work but the code still doesn't compile.

[smarter]

type CovariantArray[+A] = Array[A @scala.annotation.unchecked.uncheckedVariance]