Good old unsoundness, CCE

[sir-wabbit]

http://io.livecode.ch/learn/namin/unsound/scala

object App {
  trait A { type L >: Any}
  def upcast(a: A, x: Any): a.L = x
  lazy 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!"))
  }
}

lazy above is not necessary

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$.coerce(HelloWorld.scala:5)
	at App$.main(HelloWorld.scala:8)
	at App.main(HelloWorld.scala)

[Blaisorblade]

Without lazy you need null, right? Because otherwise you can't construct a value with p's type.

This looks related to #50 — in this example, it seems that what should be illegal is allowing dependent method upcast to be applied to non-stable argument p.

(If one really wanted it could be legal to allow upcast(p, x) with return type Any (the upper bound of a.L), in the spirit of typing rule (Tapp) in http://drops.dagstuhl.de/opus/volltexte/2017/7276/, but I'm not sure Scala intends to allow this).

[odersky]

I believe the lazy val

lazy val p: A { type L <: Nothing } = p

should not be realizable. We miss a check here.

[Blaisorblade]

Talked with Martin a lot about this and #4036. Turns out Dotty already switched to the refined logic — p is legal but unstable, so applying dependent methods/functions to it requires care.

(If one really wanted it could be legal to allow upcast(p, x) with return type Any (the upper bound of a.L), in the spirit of typing rule (Tapp) in http://drops.dagstuhl.de/opus/volltexte/2017/7276/, but I'm not sure Scala intends to allow this).

There is indeed some logic for it. If method f is dependent and argument e is unstable, f(e) could be rewritten in ANF, and typer produced the same result (a "more general" type). But typer can only approximate whether e is stable (PostTyper is more precise), yet the types it produces can't be refined later. We'll need to resume thinking about this.