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

Type projection is unsound #1050

Closed
odersky opened this Issue Jan 28, 2016 · 16 comments

Comments

Projects
None yet
3 participants
@odersky
Copy link
Contributor

odersky commented Jan 28, 2016

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 comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

this looks very similar to #50

@adriaanm

This comment has been minimized.

Copy link
Contributor

adriaanm commented Jan 28, 2016

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

This comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

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

This comment has been minimized.

Copy link
Contributor Author

odersky commented Jan 28, 2016

@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

This comment has been minimized.

Copy link
Contributor Author

odersky commented Jan 28, 2016

@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

This comment has been minimized.

Copy link
Contributor

adriaanm commented Jan 28, 2016

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

This comment has been minimized.

Copy link
Contributor Author

odersky commented Jan 28, 2016

We don't have existentials anymore.

@smarter

This comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

@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

This comment has been minimized.

Copy link
Contributor

adriaanm commented Jan 28, 2016

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

@adriaanm

This comment has been minimized.

Copy link
Contributor

adriaanm commented Jan 28, 2016

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

This comment has been minimized.

Copy link
Contributor Author

odersky commented Jan 28, 2016

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

@smarter

This comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

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
@smarter

This comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

@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

This comment has been minimized.

Copy link
Contributor

adriaanm commented Jan 28, 2016

(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

This comment has been minimized.

Copy link
Member

smarter commented Jan 28, 2016

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.

@odersky

This comment has been minimized.

Copy link
Contributor Author

odersky commented Feb 10, 2016

Closed by way of #1051

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment