Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Buggy or undocumented behavior concerning subtyping relationships with unions, intersections and variance #5980

Closed
anatoliykmetyuk opened this issue Feb 23, 2019 · 2 comments

Comments

Projects
None yet
1 participant
@anatoliykmetyuk
Copy link
Contributor

commented Feb 23, 2019

Not sure if it is a bug or an unintuitive/undocumented behavior.

trait A
trait B

trait Covariant[F[+_]] {
  trait G[+X]

  def fx: F[A  &   B] = ???  // fy: Type Mismatch Error
  def fy: F[A] & F[B] = fx

  def gx: G[A  &   B] = gy
  def gy: G[A] & G[B] = gx
}

Above, fx = fy gives a type mismatch error. However, gx = gy does not. My guess is, in case of fx = fy, the only fact the compiler knows about F is that it is covariant. According to the covariance laws, fx = fy is illegal. However, in case of gx = gy, the compiler knows the actual type G. It hence can compute what exactly members should G[A & B] and G[A] & G[B] have, and see that these members are identical, and hence allow for gx = gy.

However, this logic does not stand the contravariance test:

trait Contravariant[F[-_]] {
  trait G[-X]

  def fx: F[A  &   B] = fy  
  def fy: F[A] | F[B] = ??? // fx: Type Mismatch Error

  def gx: G[A  &   B] = gy
  def gy: G[A] | G[B] = ??? // gx: Type Mismatch Error
}

Here, fy = fx is illegal according to contravariance laws, and the fact that F is contravariant is the only thing the compiler knows about F. However, if the Covariant example reasoning above is correct, then the compiler will take into account the information available about the concrete G trait. Following the covariant example logic, in case of gy = gx, the compiler should be able to compute that G[A] | G[B] type has the same members as G[A & B]. And, if gx = gy is allowed for the covariant case, following the same logic, gy = gx should be allowed for the contravariant case. However, this does not happen, and the compiler appears to be guided only by the contravariance laws, ignoring this time the distinction between the type parameters and traits.

A similar case makes its appearance in the documentation on intersection types, precisely, the snippet of:

val x: A & B = new C
val ys: List[A & B] = x.children

There, the documentation says:

The type of children in A & B is the intersection of children's type in A and its type in B, which is List[A] & List[B]. This can be further simplified to List[A & B] because List is covariant.

The simplification can indeed be done when defining C, so that the children method returns List[A & B], because List[A & B] <: List[A] & List[B]. However, what exactly happens in case of val ys: List[A & B] = x.children?

val x: A & B = new C
def f(x: C) = ???
f(x)

The above fails with

[error] 14 |  f(x)
[error]    |    ^
[error]    |    Found:    (A & B)(Official.x)
[error]    |    Required: C

So, there is no chance that when doing val ys: List[A & B] = x.children, the compiler knows that x is of type C. The compiler thinks that x is of type A & B. And what should the type of children of A & B be? According to the doc on the intersection types:

If a member appears in both A and B, its type in A & B is the intersection of its type in A and its type in B. For instance, assume the definitions:

Hence, the type of children in A & B must be List[A] & List[B], and List[A] & List[B] >: List[A & B]. I can't see any reason for the compiler to make the type in question a more special List[A & B].

Hence, the assignment val ys: List[A & B] = x.children should not be possible, because x is of type A & B and x.children is inferred to List[A] & List[B], and List[A & B] <: List[A] & List[B].

One way it can be possible is if the compiler utilizes the information it has about the List type and computes that List[A] & List[B] =:= List[A & B]. However, this does not appear to be true:

[error] 15 |  implicitly[List[A & B] =:= List[A] & List[B]]
[error]    |                                               ^
[error]    |no implicit argument of type List[A & B] =:= List[A] & List[B] was found for parameter ev of method implicitly in object DottyPredef

And, if this was the case, then why does it not work with the union type as described above?

So, is it a bug, or is there some logic regarding subtyping rules with covariance/contravariance and unions/intersections that the documentation does not mention?

I tested the above code on dotty 0.13.0-RC1 and 0.14.0-bin-20190222-789269d-NIGHTLY.

@anatoliykmetyuk

This comment has been minimized.

Copy link
Contributor Author

commented Feb 24, 2019

Hence, the type of children in A & B must be List[A] & List[B], and List[A] & List[B] >: List[A & B]. I can't see any reason for the compiler to make the type in question a more special List[A & B].

It turns out that at least in the Scala console, the type is List[A & B]:

scala> trait A { def children: List[A] }
// defined trait A

scala> trait B { def children: List[B] }
// defined trait B

scala> def x: A & B = ???
def x: A & B

scala> :type x.children
List[A & B]

And, in general:

scala> type F <: [+A] => Any

scala> trait C { def children: F[C] }
// defined trait C

scala> trait D { def children: F[D] }
// defined trait D

scala> def x: C & D = ???
def x: C & D

scala> :type x.children
F[C & D]

scala> type F <: [A] => Any

scala> trait C { def children: F[C] }
// defined trait C

scala> trait D { def children: F[D] }
// defined trait D

scala> def x: C & D = ???
def x: C & D

scala> :type x.children
F[C] & F[D]

So, when given a choice between F[C] & F[D] and F[C & D] for the type of the member of the C & D type, the compiler goes for the more specific alternative, F[C & D], when it can. This clarifies the documentation example, however, what about the Covariant and Contravariant cases above – why does Covariant case allow for gx = gy?

@anatoliykmetyuk

This comment has been minimized.

Copy link
Contributor Author

commented Feb 24, 2019

This clarifies the documentation example

... or not:

trait CovariantExample[F[+_]] {
  trait A { def children: F[A] }
  trait B { def children: F[B] }
  trait C extends A with B { def children: F[A] & F[B] = ??? }

  def fc1: C     = new C {}
  def fc2: A & B = fc1

  // def fy1: F[A & B] = fc1.children  // Type error
  def fy2: F[A & B] = fc2.children
}

It is legal to define children in C as F[A] & F[B], since F[A] & F[B] <: F[A] and F[A] & F[B] <: F[B].

However, the problem is that we can then assign an instance of C to A & B - because A & B's children is supposed to be F[A & B], and F[A & B] <: F[A] & F[B]. So, A & B must have a member with a more specific return type, but we give it a member with a more generic return type.

I guess the compiler shouldn't go for the more specific alternative when given a choice between F[A] & F[B] and F[A & B] in the covariant case, since it is possible to imagine a case when we explicitly specify the more generic type F[A] & F[B] as above.

And it still has to do with the Covariant example at the beginning of the issue. If you modify the example by specifying a concrete type F as follows:

trait CovariantExample {
  trait F[+X]

  trait A { def children: F[A] }
  trait B { def children: F[B] }
  trait C extends A with B { def children: F[A] & F[B] = ??? }

  def fc1: C     = new C {}
  def fc2: A & B = fc1

  def fy1: F[A & B] = fc1.children
  def fy2: F[A & B] = fc2.children
}

It compiles fine.

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 4, 2019

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 10, 2019

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 10, 2019

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 10, 2019

Fix lampepfl#5980: Distribute type parameters of covariant type const…
…ructors

When performing subtyping comparisons of the `F[A] & F[B] <:< C` kind,
 if `F` is a type parameter (e.g. as in `trait Foo[F[+_]]`), the compiler
 decides the relationship to be true if either `F[A] <: C` or `F[B] <: C`.
 However, in case of covariant `F[+_]`, it is possible to distribute the
 type arguments when performing the `&` operation: `F[A] & F[B] ~> F[A & B]`.
 Hence there is one more case to be considered when checking `<:<`
 relationship. This commit adds such a check to the `<:<` logic. Now,
 `F[A] & F[B] <:< C` is true (for covariant `F`) if either of the following
 is true:
 - F[A] <: C
 - F[B] <: C
 - F[A & B] <: C

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 10, 2019

Fix lampepfl#5980: Distribute type parameters of covariant type const…
…ructors

When performing subtyping comparisons of the `F[A] & F[B] <:< C` kind,
if `F` is a type parameter (e.g. as in `trait Foo[F[+_]]`), the compiler
decides the relationship to be true if either `F[A] <: C` or `F[B] <: C`.
However, in case of covariant `F[+_]`, it is possible to distribute the
type arguments when performing the `&` operation: `F[A] & F[B] ~> F[A & B]`.
Hence there is one more case to be considered when checking `<:<`
relationship. This commit adds such a check to the `<:<` logic. Now,
`F[A] & F[B] <:< C` is true (for covariant `F`) if either of the following
is true:
- F[A] <: C
- F[B] <: C
- F[A & B] <: C

anatoliykmetyuk added a commit to anatoliykmetyuk/dotty that referenced this issue Mar 10, 2019

Fix lampepfl#5980: Distribute type parameters of covariant type const…
…ructors

When performing subtyping comparisons of the `F[A] & F[B] <:< C` kind,
if `F` is a type parameter (e.g. as in `trait Foo[F[+_]]`), the compiler
decides the relationship to be true if either `F[A] <: C` or `F[B] <: C`.
However, in case of covariant `F[+_]`, it is possible to distribute the
type arguments when performing the `&` operation: `F[A] & F[B] ~> F[A & B]`.
Hence there is one more case to be considered when checking `<:<`
relationship. This commit adds such a check to the `<:<` logic. Now,
`F[A] & F[B] <:< C` is true (for covariant `F`) if either of the following
is true:
- F[A] <: C
- F[B] <: C
- F[A & B] <: C

@smarter smarter closed this in 7cdab92 Mar 19, 2019

smarter added a commit that referenced this issue Mar 19, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.