From f18465b60fbc08c9e87500d9a188871d9ab71853 Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Tue, 27 Sep 2022 11:18:27 +0200 Subject: [PATCH 1/4] Add realization check to erased definitions typer --- .../dotty/tools/dotc/transform/PostTyper.scala | 8 ++++++++ tests/neg-custom-args/erased/i4060.scala | 17 +++++++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 tests/neg-custom-args/erased/i4060.scala diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala index 7873124d84bd..27586c986e1c 100644 --- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala +++ b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala @@ -350,6 +350,11 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase if (fn.symbol != defn.ChildAnnot.primaryConstructor) // Make an exception for ChildAnnot, which should really have AnyKind bounds Checking.checkBounds(args, fn.tpe.widen.asInstanceOf[PolyType]) + if fn.symbol eq defn.Compiletime_erasedValue then + // Check the instantiated type of erasedValue for realizibility + for arg <- args do + Checking.checkRealizable(arg.tpe, arg.srcPos, "type application of erasedValue") + fn match { case sel: Select => val args1 = transform(args) @@ -484,6 +489,9 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase private def checkErasedDef(tree: ValOrDefDef)(using Context): Unit = if tree.symbol.is(Erased, butNot = Macro) then val tpe = tree.rhs.tpe + if !tree.symbol.isOneOf(TermParamOrAccessor) && !tree.symbol.eq(defn.Compiletime_erasedValue) then // Only need to check non-parameters, since parameters have their own path checks. + // We want all erased definitions to have a realizable type + Checking.checkRealizable(tree.tpt.tpe, tree.srcPos, "erased type") if tpe.derivesFrom(defn.NothingClass) then report.error("`erased` definition cannot be implemented with en expression of type Nothing", tree.srcPos) else if tpe.derivesFrom(defn.NullClass) then diff --git a/tests/neg-custom-args/erased/i4060.scala b/tests/neg-custom-args/erased/i4060.scala new file mode 100644 index 000000000000..9fdca4cfdfc7 --- /dev/null +++ b/tests/neg-custom-args/erased/i4060.scala @@ -0,0 +1,17 @@ +// See https://github.com/lampepfl/dotty/issues/4060#issuecomment-445808377 +import scala.language.experimental.erasedDefinitions + +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 // error + def coerce(x: Any): Int = upcast(p)(x) + + def coerceInline(x: Any): Int = upcast(compiletime.erasedValue[A {type L <: Nothing}])(x) // error + + def main(args: Array[String]): Unit = { + println(coerce("Uh oh!")) + } +} From b429e6b8a76e57c1570ed93d874cf63b1f9e3a88 Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Wed, 28 Sep 2022 15:22:20 +0200 Subject: [PATCH 2/4] Check realizability of parameters of an erased function ... instead of checking every instantiated instance of erasedValue[T]. I think this is the better solution, since erasedValue have uses outside of erasedDefinitions (i.e. in inlining) which has their own realizability checks as well. We don't have to be pessimistic in those cases. - Only check for realizability for erased parameters of result-dependent functions. Per talk with @odersky, it seems that it is enough to check for realizability of parameters of a dependent function in order to avoid unsoundness. Note that the following actions have already been checked for, with erased parameters: - Using them as a dependent path in casting / variable definitions - Using them as the input to an `inline match` The check previously performed on `val`/`def` definitions are also removed, so we are as liberal as possible, to avoid too much restriction. I think with this, we can also remove the special case for `compiletime.erasedValue`. --- .../src/dotty/tools/dotc/transform/PostTyper.scala | 12 +++--------- tests/neg-custom-args/erased/i4060.scala | 2 +- 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala b/compiler/src/dotty/tools/dotc/transform/PostTyper.scala index 27586c986e1c..05aaa745bb18 100644 --- a/compiler/src/dotty/tools/dotc/transform/PostTyper.scala +++ b/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) => @@ -350,11 +352,6 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase if (fn.symbol != defn.ChildAnnot.primaryConstructor) // Make an exception for ChildAnnot, which should really have AnyKind bounds Checking.checkBounds(args, fn.tpe.widen.asInstanceOf[PolyType]) - if fn.symbol eq defn.Compiletime_erasedValue then - // Check the instantiated type of erasedValue for realizibility - for arg <- args do - Checking.checkRealizable(arg.tpe, arg.srcPos, "type application of erasedValue") - fn match { case sel: Select => val args1 = transform(args) @@ -489,9 +486,6 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase private def checkErasedDef(tree: ValOrDefDef)(using Context): Unit = if tree.symbol.is(Erased, butNot = Macro) then val tpe = tree.rhs.tpe - if !tree.symbol.isOneOf(TermParamOrAccessor) && !tree.symbol.eq(defn.Compiletime_erasedValue) then // Only need to check non-parameters, since parameters have their own path checks. - // We want all erased definitions to have a realizable type - Checking.checkRealizable(tree.tpt.tpe, tree.srcPos, "erased type") if tpe.derivesFrom(defn.NothingClass) then report.error("`erased` definition cannot be implemented with en expression of type Nothing", tree.srcPos) else if tpe.derivesFrom(defn.NullClass) then diff --git a/tests/neg-custom-args/erased/i4060.scala b/tests/neg-custom-args/erased/i4060.scala index 9fdca4cfdfc7..dabf9a746ef1 100644 --- a/tests/neg-custom-args/erased/i4060.scala +++ b/tests/neg-custom-args/erased/i4060.scala @@ -7,7 +7,7 @@ object App { 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 // error - def coerce(x: Any): Int = upcast(p)(x) + def coerce(x: Any): Int = upcast(p)(x) // error def coerceInline(x: Any): Int = upcast(compiletime.erasedValue[A {type L <: Nothing}])(x) // error From 11ace0f494986d7cefc650407f305a37d10ff52f Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Tue, 27 Sep 2022 12:51:38 +0200 Subject: [PATCH 3/4] Add tests for #4060 --- tests/neg-custom-args/erased/i4060.scala | 12 ++++++++---- tests/neg-custom-args/i4060.scala | 22 ---------------------- 2 files changed, 8 insertions(+), 26 deletions(-) delete mode 100644 tests/neg-custom-args/i4060.scala diff --git a/tests/neg-custom-args/erased/i4060.scala b/tests/neg-custom-args/erased/i4060.scala index dabf9a746ef1..a1a2eee68dc0 100644 --- a/tests/neg-custom-args/erased/i4060.scala +++ b/tests/neg-custom-args/erased/i4060.scala @@ -1,17 +1,21 @@ // See https://github.com/lampepfl/dotty/issues/4060#issuecomment-445808377 -import scala.language.experimental.erasedDefinitions 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 // error + 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!")) } } diff --git a/tests/neg-custom-args/i4060.scala b/tests/neg-custom-args/i4060.scala deleted file mode 100644 index 3d5c180b5d7b..000000000000 --- a/tests/neg-custom-args/i4060.scala +++ /dev/null @@ -1,22 +0,0 @@ -class X { type R } -class T(erased val a: X)(val value: a.R) - -object App { - def coerce[U, V](u: U): V = { - trait X { type R >: U } - trait Y { type R = V } - - class T[A <: X](erased val a: A)(val value: a.R) // error - - 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) - - } -} From e770df3c1e7d59f4eac77344bdf066f68792cfdb Mon Sep 17 00:00:00 2001 From: Natsu Kagami Date: Tue, 27 Sep 2022 11:27:22 +0200 Subject: [PATCH 4/4] Add note about realizibility in the spec --- docs/_docs/reference/experimental/erased-defs-spec.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/docs/_docs/reference/experimental/erased-defs-spec.md b/docs/_docs/reference/experimental/erased-defs-spec.md index 5395a8468399..24ae89c7e28b 100644 --- a/docs/_docs/reference/experimental/erased-defs-spec.md +++ b/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).