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

Unsoundness due to projections from structural types #4098

Closed
Blaisorblade opened this issue Mar 9, 2018 · 1 comment
Closed

Unsoundness due to projections from structural types #4098

Blaisorblade opened this issue Mar 9, 2018 · 1 comment

Comments

@Blaisorblade
Copy link
Contributor

A new variant of #50 (re)surfacing, haven't checked yet among all the original examples, nor if this is fixed by the existing PRs (in particular, #4036). The issue is that (({ type R = A }) & ({ type R = B }))#R is allowed and shouldn't, so I adapted @alexknvl's code in #4060 to implement coerce.

object App {
  def coerce[U, V](u: U): V = {
    type X = { type R >: U }
    type Y = { type R = V }
    type Z = X & Y
    val u1: Z#R = u

    u1
  }

  def main(args: Array[String]): Unit = {
    val x: Int = coerce[String, Int]("a")
    println(x + 1)
  }
}
$ dotc -d out UnsoundProj.scala
$ dotr -classpath out App
Exception in thread "main" java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Integer
        at scala.runtime.BoxesRunTime.unboxToInt(BoxesRunTime.java:101)
        at App$.main(UnsoundProj.scala:11)
        at App.main(UnsoundProj.scala)

This was prompted by a question from @allanrenucci. He also pointed me to the documentation on type projections (http://dotty.epfl.ch/docs/reference/dropped/type-projection.html), which seems both unclear and misleading:

Scala so far allowed general type projection T#A where T is an arbitrary type and A names a type member of T.
Dotty disallows this if T is an abstract type (class types and type aliases are fine). This change was made because unrestricted type projection is unsound.

Projections should be illegal on lots of types T that aren't abstract types themselves — T must be a class type (or alias to such), and A should be a fully defined type member, but type operators like intersections, unions, structural refinements should be forbidden — probably all operators should (unless we have a very good reason for allowing some).

This way, type projections can only access global (type) constants:

class Defining {
  type TypeMember = ...
}
object Defining {
  val valueMember
}
// Here, Defining#T and Defining.valueMember are both references to known global constants, at value or type-level
@Blaisorblade
Copy link
Contributor Author

Assigning to @smarter for triage, feel free to reassign to Martin.

@smarter smarter removed their assignment Mar 13, 2018
odersky added a commit to dotty-staging/dotty that referenced this issue Mar 15, 2018
So far, we did the check only for member symbols. We have to do the same thing
for type refinements that do not refer to a member.
odersky added a commit to dotty-staging/dotty that referenced this issue Mar 19, 2018
So far, we did the check only for member symbols. We have to do the same thing
for type refinements that do not refer to a member.
odersky added a commit that referenced this issue Mar 28, 2018
Fix #4098: Check that refinements have good bounds
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants