Unsoundness with distribution of intersection over covariant types

[SimonGuilloud]

Compiler version

3.3.6 and 3.7.0

Minimized code

trait L[+A]{val a:A}
trait R[+B]{val b: B}

class LR(val a: Int, val b: String) extends L[Int] with R[String]


type E[+A] = L[A] | R[A]

val x: E[Int] & E[String] = LR(4, "hi")

val y: E[Int&String] = x

val z = y match
    case l : L[Int&String] => l.a
    case r : R[Int&String] => r.b

z:String // java.lang.ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String

Expectation

I expect line val y: E[Int&String] = x to raise an error.

The problem is due to the normalization

E[Int] & E[String] =:= E[Int&String]

as described in https://dotty.epfl.ch/docs/reference/new-types/intersection-types-spec.html
"if C is covariant, C[A] & C[B] ~> C[A & B]"

I found this rule logically dubious (it certainly does not hold in a set-theoretic model), even if it is convenient for typechecking. So I tried to explicitely construct an unsoundness.

Note that the same issue happen if Eis replaced by a trait with

sealed trait E[+A]

trait L[+A] extends E[A] :
    def a : A

trait R[+A] extends E[A] :
    def b : A


class LR(val a: Int, val b: String) extends L[Int] with R[String]

summon[(E[Int] & E[String]) =:= E[Int&String]]

val x: E[Int] & E[String] = LR(4, "hi")

val y: E[Int&String] = x

val z = y match
    case l : L[Int&String] => l.a
    case r : R[Int&String] => r.b

z:String

Note also that the matching over x is proven exhaustive.

[EugeneFlesselle]

Nice catch!

Minimized, using commutativity of union:

type Or[+A, +B] = A | B

val x: Or[Int, String] & Or[String, Int] = 3
val y: Or[Int & String, Int & String] = x
val z: Int & String = y

[SimonGuilloud]

This one is pretty fun !

[odersky]

I think the original intuition was that if C is a covariant class or trait, then C[A & B] =:= C[A & B]. But even that
does not seem to be the case as Simon's second example shows. Can one of you make a PR to drop the rule and check what breaks if we do that?

[EugeneFlesselle]

But even that does not seem to be the case as Simon's second example shows.

Yes, I think it would perhaps hold (though still uncertain) if we ruled out inheriting from the base class E through multiple direct parents.

Can one of you make a PR to drop the rule and check what breaks if we do that?

Will do

[SimonGuilloud]

Intuitively, it should hold for some types, such as options or lists. My intuition says the following:

We have both (semantically)
Option[A] & Option[B] = Option[A&B] and Option[A] | Option[B] = Option[A|B]
on the other hand, we have
List[A] & List[B] = List[A&B] but not List[A] | list[B] = List[A|B]

The difference is that List[T] can hold multiple T. In a sense, List[T] is a "true product" over T, while Option[T] is not.
Meanwhile, both of them are not "true sum" over T, since in each case only one branch (Some and Cons) depend on T.

This was my intuition to construct my example, which is inspired from the true sum "either" construct.
So here is my conjecture for when such equalities can hold:
C[A|B] = C[A] | C[B] holds when C[T]is linear in T, i.e. Tis only used once (in each branch)
C[A&B] = C[A] & C[B] holds when C[T]is colinear in T, i.e. Tis only used in a single branch (but possibly multiple times)

or something like that. For example,
Either[String|Int] =:= Either[String] | Either[Int] (where Either is the symmetrical-typed version of the usual Either) intuitively make sense, and Either is linear: T is only used once in Left and once in Right.

For function types, I'm not sure. I don't like anyway that (A => B) & (C => D) =:= (A|C) => (B&D), because it doesn't make sense semantically and if it is sound it is only because the language is not expressive enough to build a counterexample. I expect that it will be an issue with refinement types. But I also believe it is a very convenient assumption for typechecking?

[Linyxus]

I find this quite interesting so I had some thoughts. Here are some quick notes:

• It seems to me that, like in GADT, the classes in question must be in a closed domain (i.e. traits being sealed and classes being final), otherwise it will be really hard. Specifically, like what Simon gave,

class C[+A]
class B1[A](val a: A) extends C[A]
class B2[A](val b: A) extends C[A]
class LR[A, B](val a: A, val b: B) extends B1[A], B2[B]
// LR[Int, String] => B1[Int] & B2[String] => C[Int] & C[String] => C[Int & String]  // boom with pattern matching

• If we were to understand type constructors as functions on types, then it seems that we are looking for homomorphisms on the type lattice (over the binops & and |). One interesting analogy is to understand & as * and | as +, then type constructors satisfying F[A] & F[B] = F[A & B] are like "multiplicative functions" and those that F[A] | F[B] = F[A | B] like "additive functions". We have another perspective of Simon's conjecture that C[A | B] = C[A] | C[B] for a linear C[_]: all linear functions (f(x) = ax + b) are additive. If a type parameter is used twice in a branch, then it becomes a quadratic function.

[SimonGuilloud]

I'll add that a homomorphism over either | or & implies monotonicity.

suppose $A <: B$ and $F[X \land Y] = F[X] \land F[Y]$. Then
$$F[A] \land F[B] <: F[A]$$
$$F[A \land B] <: F[A]$$
$$F[A] <: F[B]$$

Alternatively if $F[X | Y] = F[X] | F[Y]$,
$$F[A] <: F[A] | F[B]$$
$$F[A] <: F[A | B]$$
$$F[A] <: F[B]$$

So covariance is a necessary condition (but not sufficient).