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.

[Blaisorblade]

What I mean is more like a substitution principle for types and type constructors rather than values. (Allow me to handwave the argument somewhat.)

Ah, that's indeed an important distinction, thanks for clarifying I was confused. I'm afraid this argument is not convincing, and the handwaving you're doing might be confusing you (even though in general I'm happy to concede handwaving if helpful).
I've never seen statements or arguments for the substitution principle you imagine, and it fails in the F<: calculus (see below), and I'm not aware of problems from either the mathematical or software-engineering point of view. I'll stick to types since they're sufficient for a counterexample, but I guess the arguments can be extended to type constructors.

It's not true that if A <: B and f[B] is well-typed then f[A] is well-typed, and not just in the example you give — dropping datatype semantics, lower bounds give a counterexample.
But that's a superficial answer. Functions can restrict their type arguments, and those restrictions need not respect subtyping, neither in the syntax nor in a model.

For an example with just upper bounds (so that its core translates more easily to the standard F<: calculus), let's take Int <: Any and try using the substitution on this function:

def f[X <: Any, Y <: X => String]: Any

f[Int, Int => String] //allowed
f[Any, Int => String] //forbidden, because Int => String violates the bound <: Any => String

And before you start pointing out that X appears in a contravariant position, I'm still wondering on the software engineering benefits of this principle.

LSP says something much different — it basically reminds us that if x \in A and A \subset B then x \in B, and once you have a set-theoretic model (or something close enough) that's true whether you add a rule to the syntax or not. I'm indeed studying such models formally at the moment and this was quite helpful, since I could define the model and observe the rules it satisfied.

[TomasMikula]

I'm still wondering on the software engineering benefits of this principle.

My original example is a software engineering benefit, namely avoiding the need to upcast in certain situations. Recall the definition of method g from above

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

To make g(new Bar[Int]) typecheck, we need the type parameter F to be instantiated to Foo, as in g(new Bar[Int]: Foo[Int]) or g[Foo](new Bar[Int]). But with the mentioned substitution principle, F instantiated to Bar would have to work as well, therefore g(new Bar[Int]) would typecheck without any changes to type inference.

---

You guessed my response to the counter-example with bounds and type (constructor) in contravariant position.

[Blaisorblade]

Corrections: the example with def f[X <: Any, Y <: X => String]: Any is not a counterexample, because I fooled myself (and you): it just shows that we can refine invalid f[Any, Int => String] to valid f[Int, Int => String], but that's not surprising. I rechecked because otherwise it'd be a counterexample to the actual lemma for F<: (of unclear status in DOT) which is narrowing:

1. If Gamma, X <: Q, Delta |- S <: T, and Gamma |- P <: Q, then Gamma, X <: P, Delta |- S <: T.
2. Same with t: T instead of S <: T, so: if Gamma, X <: Q, Delta |- t : T, and Gamma |- P <: Q, then Gamma, X <: P, Delta |- t : T.

I looked this up because I was sure I'd never seen the substitution lemma you mention, but I concede your intuition was right. (I might not have time to look this up next time, but I will have to restudy a few systems with subtyping).

Still, this example, while counterintuitive, is not necessarily a violation of narrowing, because while Bar[X] <: Foo[X] for all X, while Bar <: Foo fails in our example:

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

Maybe I should look at how higher-order subtyping systems handle this.
And OK, maybe we should require Bar[+A] extends Foo[A] (though this change raises questions), and this might be the easiest way to improve inference.

===

Regarding the other half of your proposal:

variance in a subtype should be allowed to be looser than in the base type (as in the above snippet);

absent a good SIP, I'd still leave the more restrictive rule in place, because of @smarter's argument about usability. In any case, I'd treat them as separate, and handle the above part first.

[TomasMikula]

I'd treat them as separate, and handle the above part first.

👍

[TomasMikula]

Btw, 👍 to considering type aliases/members as interface and base traits as part of the implementation. However, if I want exhaustive pattern matching, a sealed trait is currently the only option.

[Blaisorblade]

However, if I want exhaustive pattern matching, a sealed trait is currently the only option.

I imagined that the pattern match would be written against the implementation — see traits Base and BaseExp in https://infoscience.epfl.ch/record/150347/files/gpce63-rompf.pdf:

trait Intf {
  type Rep[T]
}
trait Impl extends Intf {
  type Rep[T] = Exp[T]
  trait Exp[T] // FIXED
  case class IntExp extends Exp[Int] // FIXED
}

Unless if your interface describes your entire ADT (which you can), you still don't get exhaustivity warning.
EDIT: fixed errors in the snippet above.

[TomasMikula]

I imagined that the pattern match would be written against the implementation

In my musings about hypothetical Scala there is no such restriction.

Unless if your interface describes your entire ADT (which you can), you still don't get exhaustivity warning.

For starters, I would take if I could just tell the compiler to trust me that an appointed set of methods deconstructs an abstract type exhaustively.

Anyway, that's another discussion.

[TomasMikula]

Interestingly enough,

sealed trait Optional[A]
object Optional {
  private[this] case class No[+A]() extends Optional[A]
}

already works in Scala. (I only just noticed this in scala/bug#10822 (comment).) This issue is then about being able to omit that private[this].

[TomasMikula]

Actually, here's a simple counter argument to the part of my proposal that in

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

Bar should be required to preserve variance on A, i.e. Bar[+A].

It breaks down with

trait Function[-A, +B]
class Identity[X] extends Function[X, X]

The proposal would require Identity to be both covariant and contravariant in X, i.e. that it doesn't use X in either contravariant or covariant position, i.e. doesn't use X at all.