Dotty: Intersection types are not commutative for overriding and overloading

[panacekcz]

Although A & B and B & A are claimed to be the same type, the are not the same for overriding and overloading.
It seems to be "caused" by erasue, which erases A & B to A and B & A to B.

Overriding

trait A
trait B

class Base{
  def m(ab: A&B) = ab
}
class Derived extends Base{
  override def m(ab: B&A) = ab // unexpected error
}

Output:

8 |  override def m(ab: B&A) = ab // unexpected error
  |               ^
  |       error overriding method m in class Base of type (ab: A & B): A & B;
  |         method m of type (ab: B & A): A & B has incompatible type

On the other hand, if the override is omitted, an error is correctly issued.

class Derived2 extends Base{
  def m(ab: B&A)=ab // OK - "needs override" error when expected
}

Also, when the first type in the intersection is the same (therefore erased type is the same), overriding works as expected:

trait C
class Base3{
  def m(abc: A&B&C) = abc
}
class Derived3 extends Base3{
  override def m(abc: A&C&B) = abc // OK - no error
}

Overloading

Similarly, overloading is allowed when the first type differs.

class Overload{
  def m(ab: A&B) = ab
  def m(ab: B&A) = ab // No error when expected
}

On the other hand, such methods cannot be called, as expected:

object Caller{
  Overload.m(new A with B) // OK - "ambiguous overload" error when expected
}

That seems to be the same behavior as with scalac.

[sjrd]

I think I suggested at some point that erasure should choose deterministically, for example by:

• prefer class over trait (for performance reasons)
• tie break: lexicographically first class/trait name

[panacekcz]

Using lexicographical order of names would mean that code could break when you rename a trait even if its name is not mentioned anywhere, like

trait B
trait A { // Rename A to C
 def m(a:B&this.type) = 1
 def m(a:B) = 2 // Ok in A, conflict in C
}

That seems brittle. You would also give up any programmer control over the erasure for a quite arbitrary rule.

Would it be reasonable to just put the current behavior into the specification? You'd have to weaken the claim that A & B is the same type as B & A, and say something like & is commutative except for erasure and its consequences.

[sjrd]

and say something like & is commutative except for erasure and its consequences.

That is even more brittle, because the compiler can and might change the order of an & internally for arbitrary reasons.

At least my proposal is specifiable.

[smarter]

FWIW, the rules for erasure of & are at https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeErasure.scala#L299 and the rules for | are at https://github.com/lampepfl/dotty/blob/master/compiler/src/dotty/tools/dotc/core/TypeErasure.scala#L244

The lexicographic tie break makes sense to me, but it doesn't match what scalac is doing (we already don't always match what scalac is doing, but I was hoping we could fix that: https://github.com/lampepfl/dotty/issues/4619 for example), which can lead to issues when using scalac-compiled libraries.
It could also break code that abuses how erasure works to implement tagged type by assuming that Int & AMarkerTrait erases to Integer and not AMarkerTrait (I think scalaz used to do this but may have gone with something saner since then).

[smarter]

We could potentially have different erasure rules for symbols that are Scala2-defined or override something that is Scala2-defined, but that seems rather involved.

[odersky]

Why would the current behavior not be specifiable? It seems we need to take erasure into account only for types that are written down. Those won't be re-arranged by the compiler. Going lexicographic has the mentioned disadvantages wrt renaming and Scala-2 interop.

[odersky]

The error messages given in the issue are confusing. They stem from the fact that methods are classified according to their _signature_, which is essentially a string representation of their erased type. Since the erasure of A & B and B & A is not the same, the methods are classified as different, so can't override each other. The compiler could double-check in this case and issue a more specific error message saying that the erased types of the methods differ.

[odersky]

Another TODO: Be more precise about what we mean in

Unlike with types, & is commutative: A & B is the same type as B & A.

Something like:

& is commutative: A & B and B & A are equivalent types, in the sense that each is a subtype of the other.

The issue with with types is not that they were not commutative (they were treated as such) it was that the commutative law for with types did not respect the Liskov substitution principle. But that's a bit much to explain in a tutorial page.

[sjrd]

It seems we need to take erasure into account only for types that are written down.

No, you need to take erasure of the result type of a method into account, and that can be an inferred/lub'ed type. For example, what's the erasure of the following method?

def foo(x: Int) =
  if (x > 0) (??? : (A & B))
  else (??? : (B & A))

The spec won't say anything regarding whether A & B or B & A will be chosen as the result of the if/else, and yet that will be the result type of foo.

[odersky]

@sjrd Why does erasure matter for result types? ... and what does scalac do in this case?

[sjrd]

Result types are part of a JVM method signature. foo(String)String is a different method than foo(String)List. So they're important for erasure. If foo above erases to foo(int)A in one case but foo(int)B in another case, they won't be compatible. That's also why we need bridges for covariant result types (and javac does too).

scalac appears to select the one coming from the then branch, but I would bet it's pure accident.

[abgruszecki]

@smarter Is this related to #4619?

[smarter]

It's a separate issue, dotty does not erase intersections like scala 2, and neither of them is commutative. The plan is to handle intersections coming from scala 2 specially, but we didn't reach a decision for this issue on whether we want to change the dotty-defined intersection type erasure to be commutative (which would be nice indeed).