Unsoundness in handling of variance in pattern matching

[TomasMikula]

sealed trait Optional[A]
case class No[+A]() extends Optional[A]
object Noo extends No[Nothing]

object Test {
  def coerce[A, B]: A => B = {
    ((Noo: No[A]): Optional[A]) match {
      case Noo => (identity: Nothing => B)
      case _ => ???
    }
  }

  def boom: Int = coerce[String, Int]("foo")
}

Test.boom produces

java.lang.ClassCastException: java.lang.String cannot be cast to scala.runtime.Nothing$

Tested with dotty-0.5.0-RC1.

[TomasMikula]

Now Scala 2.x avoids this by not allowing the variance in a subtype to be looser than in the base type:

sealed trait Optional[A]
case class No[+A]() extends Optional[A]

       case class No[+A]() extends Optional[A]
                  ^
On line 2: error: covariant type A occurs in invariant position in type [+A]AnyRef
               with Optional[A]
               with Product
               with Serializable {

but I'm going to argue that this should be resolved differently than in Scala 2.x. Namely that

1. variance in a subtype should be allowed to be looser than in the base type (as in the above snippet); and
2. the opposite (i.e. restricting variance in a subtype) should be disallowed.

The argument for 2. is monotonicity of type-checking: If a program typechecks with some type information, then it should still typecheck with more type information.

This is violated in both Scala 2.x and Dotty:

trait Foo[+A]
class Bar[A] extends Foo[A]

def g[F[+_]](fi: F[Int]): F[Any] = fi

g(new Bar[Int]: Foo[Int]) // OK
g(new Bar[Int])           // does not typecheck, despite having strictly more
                          // information about the type of the argument

My argument for 1. is that it would be consistent with how type aliases already work. Consider an abstract type Optional[A] inside a trait.

trait OptionalModule {
  type Optional[A]
}

In the implementation, invariant Optional can be a type alias for a covariant Option:

object OptionalImpl extends OptionalModule {
  type Optional[A] = Option[A] // OK
}

So Optional provides an invariant interface to a covariant implementation.

But in Scala 2.x, invariant interface to covariant implementation cannot be achieved directly by subclassing:

sealed trait Optional[A]
case class Yes[+A](a: A) extends Optional[A] // error: covariant type A occurs in invariant position

[smarter]

I don't see how we can allow what you're proposing, allowing the variance to be looser in the subtype always leads to unsoundness:

trait Foo[A](var x: A)

class Bar[+A](_x: A) extends Foo[A](_x)

object Test {
  def main(args: Array[String]): Unit = {
    val bars: Bar[String] = new Bar("foo")
    val bara: Bar[Any] = bars
    bara.x = 1
    println(bars.x.length) // ClassCastException
  }
}

[smarter]

Closing as a duplicate of #2973, feel free to comment there if there's something I'm missing :)

[TomasMikula]

If the base class is declared as invariant, but actually uses the type parameter in contravariant position, the subclasses would be allowed to loosen it only to contravariant, not covariant. The compiler (and binaries) would have to keep track of actual variance of a type parameter, in addition to just the declared one.

In your example

trait Foo[A](var x: A)

the type parameter A, although declared invariant, actually occurs in both covariant and contravariant position. Therefore, no loosening would be allowed.

[smarter]

So you're proposing to replace the concept of variance (which is one of the concept of Scala that confuses newcomers the most) with two concepts of declared variance and actual variance, something like that would require a very well motivated and detailed proposal.
I don't find your second example convincing, if you can write case class Yes[+A](a: A) extends Optional[A] then Optional is effectively covariant, so why not declare it covariant? Your first example sounds like something that could be fixed by better higher-kinded unification, feel free to open an issue for that.

[TomasMikula]

I don't find your second example convincing, if you can write case class Yes[+A](a: A) extends Optional[A] then Optional is effectively covariant, so why not declare it covariant?

You can conclude that Optional is effectively covariant only after seeing the implementation. But sometimes I would like to just declare an interface, without restricting it to a single implementation. Optional[A] admits more implementations than Optional[+A].

I already mentioned another motivation before, namely consistency: If an abstract invariant type can have covariant implementation, why not abstract invariant class/trait?

So you're proposing to replace the concept of variance (which is one of the concept of Scala that confuses newcomers the most) with two concepts of declared variance and actual variance, something like that would require a very well motivated and detailed proposal.

I think at this stage it is premature to argue based on what impact it would have on newcomers and we should stick to technical arguments. But anyway, I subjectively think the net impact on newcomers would be positive (more consistent language, monotonic type inference). The "actual" variance would show up to the user only if they mix interface and implementation (such as in your trait Foo[A](var x: A)), which is not considered a good idea even in OOP. If the interface does not include implementation, then actual variance is the same as declared variance.

[Blaisorblade]

@TomasMikula I agree with @smarter here, though

something like that would require a very well motivated and detailed proposal.

remains an option.

I see basically two arguments: a technical one about type inference ("monotonicity"), and one about language aesthetics and "consistency".

The argument for 2. is monotonicity of type-checking: If a program typechecks with some type information, then it should still typecheck with more type information.

I'd say this is Liskov's substitution principle and is a very good heuristic, but there are multiple cases where type inference isn't able to recover the appropriate typing derivation, while adding upcasts fixes the issue. That's because type inference can give better result with more information about the desired typing derivation.

Just looking at DOT, if x.A >: L <: U, Dotty (and IIRC Scalac) don't automatically upcast L to U without an intervening upcast to x.A (see https://arxiv.org/abs/1708.05437, also published at Scala'17).

On this point:

Your first example sounds like something that could be fixed by better higher-kinded unification, feel free to open an issue for that.

==

On consistency, your arguments is interesting, but I'm not convinced base traits and type aliases should be related, and that's relevant to most of your points. In terms of ML modules (which is the relevant and principled design), type aliases/members are the interface, and base traits are part of the implementation. In Scala you have extra freedom to try other designs, but that alone doesn't mean we can support all of them well.

If you use type aliases/members for the interface and traits as part of the implementation, you currently end up with some boilerplate. That's annoying, but in many common cases the implementation can be expressed with less boilerplate using enum.

[TomasMikula]

Thanks for pointing out the relationship to Liskov's substitution principle. What I mean is more like a substitution principle for types and type constructors rather than values. (Allow me to handwave the argument somewhat.) Consider a subtype relation on type constructors. Then, given the definitions as above

trait Foo[+A]
class Bar[A] extends Foo[A]

we might ask whether Bar (as a type constructor) is a subtype of Foo (as a type constructor). The substitution principle would require that Bar can be used (as type argument) wherever Foo can be used. But that's not the case:

def h[F[+_]]: Unit = ()

h[Foo]  // OK
h[Bar]  // ERROR

Since the substitution principle is violated, we might conclude that, at least internally to Scala, Bar is not a subtype of Foo. Externally, however, we might reason that since Bar[A] <: Foo[A] for all types A, Bar is indeed a subtype of Foo (assuming this sort of "extensionality" holds in our model of Scala). I think my proposal reduces the gap between what's derivable in Scala and what's valid in the model.