Ensure erased vals pass CheckRealizable (#16111)

Fix #4060.

Per @odersky's [comment](#4060 (comment)),
we wish to add realizability checks to all erased vals.

- [x] Add realization check to erased definitions typer
- [x] Add note about realizibility in the spec
- [x] Add tests for #4060

Author: natsukagami

compiler/src/dotty/tools/dotc/transform/PostTyper.scala

@@ -302,12 +302,14 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
             checkNoConstructorProxy(tree)
             transformSelect(tree, Nil)
         case tree: Apply =>
-          val methType = tree.fun.tpe.widen
+          val methType = tree.fun.tpe.widen.asInstanceOf[MethodType]
           val app =
             if (methType.isErasedMethod)
               tpd.cpy.Apply(tree)(
                 tree.fun,
                 tree.args.mapConserve(arg =>
+                  if methType.isResultDependent then
+                    Checking.checkRealizable(arg.tpe, arg.srcPos, "erased argument")
                   if (methType.isImplicitMethod && arg.span.isSynthetic)
                     arg match
                       case _: RefTree | _: Apply | _: TypeApply if arg.symbol.is(Erased) =>

docs/_docs/reference/experimental/erased-defs-spec.md

@@ -62,3 +62,9 @@ TODO: complete
 7. Overriding
    * Member definitions overriding each other must both be `erased` or not be `erased`
    * `def foo(x: T): U` cannot be overridden by `def foo(erased x: T): U` and vice-versa
+   *
+
+
+8. Type Restrictions
+   * For dependent functions, `erased` parameters are limited to realizable types, that is, types that are inhabited by non-null values.
+     This restriction stops us from using a bad bound introduced by an erased value, which leads to unsoundness (see #4060).

tests/neg-custom-args/erased/i4060.scala

@@ -0,0 +1,21 @@
+// See https://github.com/lampepfl/dotty/issues/4060#issuecomment-445808377
+
+object App {
+  trait A { type L >: Any}
+  def upcast(erased a: A)(x: Any): a.L = x
+  erased val p: A { type L <: Nothing } = p
+  def coerce(x: Any): Int = upcast(p)(x) // error
+
+  def coerceInline(x: Any): Int = upcast(compiletime.erasedValue[A {type L <: Nothing}])(x) // error
+
+  trait B { type L <: Nothing }
+  def upcast_dep_parameter(erased a: B)(x: a.L) : Int = x
+  erased val q : B { type L >: Any } = compiletime.erasedValue
+
+  def coerceInlineWithB(x: Any): Int = upcast_dep_parameter(q)(x) // error
+
+  def main(args: Array[String]): Unit = {
+    println(coerce("Uh oh!"))
+    println(coerceInlineWithB("Uh oh!"))
+  }
+}