Unsoundness due to erased

[sir-wabbit]

Related to #50 #4042 #4031.

object App {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    class T[A <: X](ghost val a: A)(val value: a.R)

    object O { lazy val x : Y & X = ??? }

    val a = new T[Y & X](O.x)(u)
    a.value
  }

  def main(args: Array[String]): Unit = {
    val x: Int = coerce[String, Int]("a")
    println(x + 1)
  }
}

//////////////////////////////////////////////////////////////

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(HelloWorld.scala:15)
	at App.main(HelloWorld.scala)

[Blaisorblade]

In a hurry, but since #4031 is open, is ghost needed to get the unsoundness here? In fact, I suspect ghost should mask this bug. I’d expect two errors:

• a lazy val is not stable, so can’t instantiate params with mentioned in path-dependent types (WIP in Fix #4031: Check arguments of dependent methods for realizability #4036);
• a lazy val is not stable, so it can’t instantiate ghost arguments — if they’re supposed to be used as proofs, the language of unused arguments need to be pure and strongly normalizing. None of this is mentioned by the documentation for ghost, but it seems to be a loophole in the implied guarantees.

@nicolasstucki @odersky what do you think? We should probably have a chat about this.

[sir-wabbit]

ghost is necessary because otherwise O.x will get evaluated. You can pass ??? directly to ghost instead with the same result:

object App {
  def coerce[U, V](u: U): V = {
    trait X { type R >: U }
    trait Y { type R = V }

    class T[A <: X](ghost val a: A)(val value: a.R)

    val a = new T[Y & X]( ??? : Y & X )(u)
    a.value
  }

  def main(args: Array[String]): Unit = {
    val x: Int = coerce[String, Int]("a")
    println(x + 1)
  }
}

[Blaisorblade]

OK. I suppose already isStable in Typer could recognize ghost definitions as unstable, since figuring this out requires no forcing.

[Blaisorblade]

@alexknvl I renamed unused to ghost throughout the issue because of #4061.

[Blaisorblade]

Thinking again:

• currently ghost only promises that values are erased, so we should mark everything ghost as unstable;
• if someday we finally get a good effect analysis, we might use it to check statically that ghost constructs are strongly normalizing (which we'd want for proofs as I suggested), but that's a major improvement. When that's done, it might be possible to allow treating ghost values as stable, but I'd want to think it through first (if not sketch an extension of the soundness proofs). Significantly, we barely know a Scala subset which is strongly normalizing (status in http://drops.dagstuhl.de/opus/volltexte/2017/7276/).

[Blaisorblade]

Implemented it through isStable in SymDenotations, not Typer, since it was easier to access the flag there (as IIUC it's a flag on symbols, not types themselves).

[odersky]

Unfortunately, this makes erased vals practically useless. We should backout this fix and mark erased vals as unrealizable instead. erased is really the same as lazy in this respect. Either implies that the right-hand side will be constructed.

[Blaisorblade]

Reopening given the resolution to #4031 in #5568. When applying a dependent method/function to a dependent argument a, we realized that we need not check a's realizability because a will be a value; but we must if a is erased. Concretely, we get a CCE from:

object App {
  trait A { type L >: Any}
  //def upcast(a: A, x: Any): a.L = x
  def upcast(erased a: A)(x: Any): a.L = x
  //lazy val p: A { type L <: Nothing } = p
  erased val p: A { type L <: Nothing } = p
  def coerce(x: Any): Int = upcast(p)(x)

  def main(args: Array[String]): Unit = {
    println(coerce("Uh oh!"))
  }
}

[Blaisorblade]

Martin today suggested we might want to just require all erased arguments to be realizable, to make this simpler to implement.
But there are open questions on erased itself; until they are resolved, this should be put on hold.

[bishabosha]

most recent example from @Blaisorblade does still compile and lead to a class cast exception

[odersky]

I think we should check that all erased definitions are realizable. See CheckRealizability.scala. Spec needs to be updated as well.