Type projection is unsound

[odersky]

The following program compiles and throws a ClassCastException when executed. One might be tempted to try to rule out the obviously bad intersection T & U but we know from our work on DOT that there are ways to engineer bad bounds that cannot be detected locally. So the culprit is the projection
X#A.

object Test {

  trait C { type A }

  type T = C { type A >: Any }
  type U = C { type A <: Nothing }
  type X = T & U

  def main(args: Array[String]) = {
    val y: X#A = 1
    val z: String = y
  }
}

[smarter]

this looks very similar to #50

[adriaanm]

it kind of looks like an existential whose skolem is used outside of the existential scope -- when you open X#A to admit 1, there's this unknown type that we assume for it, and then we carry that over and make another assumption on it for z = y.

[smarter]

I don't want to insist too much on this since I haven't done any more work to convince anyone except @sstucki that this makes sense, but my type projection proposal side-steps this: X#A is always considered to be a subtype and a supertype of its upper-bound, so you can never use it to do unsound casts.

[odersky]

@smarter Yes, but we plan to address #50 tightening the isVolatile check. We have not contemplated volatile checking for prefixes of projections. One could try that, but I fear it would throw out many interesting use cases of projections.

[odersky]

@smarter Here is the same example with aliases:

object Test {

  trait C { type A }

  type T = C { type A = Any }
  type U = C { type A = Nothing }
  type X = T & U

  def main(args: Array[String]) = {
    val y: X#A = 1
    val z: String = y
  }
}

Same ClassCastException. The way I interpret your proposal it means I map the first program to the second one, no?

[adriaanm]

Can you rewrite this using existential types and still get away with it?

val y: T forSome { type T >: Int} = 1
val z: String = y: T forSome { type T <: String } // not allowed to reinterpret the bounds

val y: T forSome { type T >: Int <: String } = 1 //  `1`  is not a subtype of String
val z: String = y: T forSome { type T >: Int <: String }

[odersky]

We don't have existentials anymore.

[smarter]

@odersky :

Same ClassCastException

This shouldn't happen and looks like a separate bug. I expect A in X = T & U to have type >: (Any | Nothing) <: (Any & Nothing), which means that val x: X#A = 1 should not compile because Int is not a subtype of Any & Nothing in my system. It compiles currently since Int is a subtype of the lower bound Any | Nothing.

[adriaanm]

Sure, it was a thought experiment to see how they relate.

[adriaanm]

EDIT: nevermind (my thinking was that the bounds should be considered together, as if they were one type, but the resulting thought was not fully formed -- I'll leave it for the record :-)).

How about saying that val z: String = y only type checks if all of y's bounds (lower and upper) are a subtype of String?

[odersky]

@smarter No, in the example Int needs to be a subtype of the lower bound, Any | Nothing, which it is, obviously.

[smarter]

It looks like we have three possible set of rules, which look a bit like this (very approximately):

• current:

------------------------------
G |- {L: X..Y, ...}#L <: Y

------------------------------
G |- X <: {L: X..Y, ...}#L

• @adriaanm's proposal above, which I find interesting:

------------------------------
G |- {L: X..Y, ...}#L <: Y

G |- T <: X     G |- T <: Y
------------------------------
G |- T <: {L: X..Y, ...}#L

• my proposal: see https://gist.github.com/smarter/831a8b6f8641bd857bfa

[smarter]

@smarter No, in the example Int needs to be a subtype of the lower bound, Any | Nothing, which it is, obviously.

Right, that's different from what would happen in my proposal where Int needs to be a subtype of the upper bound.

[adriaanm]

(Note that I withdrew my proposal ;-) T <: X doesn't make sense in general, since X defaults to Nothing. It could work out better to flip it: X <: T.)

[smarter]

T <: X doesn't make sense in general, since X defaults to Nothing

How is that different from what we're doing now? In both scalac and dotty, if you write trait A { type X <: Any}, then the only subtype of A#X is Nothing.