Skip to content

Commit c5415cb

Browse files
committed
Fix #4031: Check arguments of dependent methods for realizability
- Skolemize if not realizable, but use an approximating map that avoids using such skolems as paths (because that would be unsound).
1 parent 3a3b5e0 commit c5415cb

File tree

9 files changed

+119
-16
lines changed

9 files changed

+119
-16
lines changed

compiler/src/dotty/tools/dotc/core/Types.scala

+25-2
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import Denotations._
1818
import Periods._
1919
import util.Stats._
2020
import util.SimpleIdentitySet
21+
import CheckRealizable.{realizability, Realizable}
2122
import reporting.diagnostic.Message
2223
import ast.tpd._
2324
import ast.TreeTypeMap
@@ -149,14 +150,20 @@ object Types {
149150

150151
/** Does this type denote a stable reference (i.e. singleton type)? */
151152
final def isStable(implicit ctx: Context): Boolean = stripTypeVar match {
152-
case tp: TermRef => tp.termSymbol.isStable && tp.prefix.isStable || tp.info.isStable
153+
case tp: TermRef => tp.symbol.isStable && tp.prefix.isStable || tp.info.isStable
153154
case _: SingletonType | NoPrefix => true
154155
case tp: RefinedOrRecType => tp.parent.isStable
155156
case tp: ExprType => tp.resultType.isStable
156157
case tp: AnnotatedType => tp.parent.isStable
157158
case _ => false
158159
}
159160

161+
/** Does this type denote a realizable stable reference? Much more expensive to check
162+
* than isStable, that's why some of the checks are done later in PostTyper.
163+
*/
164+
final def isStableRealizable(implicit ctx: Context): Boolean =
165+
isStable && realizability(this) == Realizable
166+
160167
/** Is this type a (possibly refined or applied or aliased) type reference
161168
* to the given type symbol?
162169
* @sym The symbol to compare to. It must be a class symbol or abstract type.
@@ -3573,6 +3580,17 @@ object Types {
35733580

35743581
def withName(name: Name): this.type = { myRepr = name; this }
35753582

3583+
private[this] var isRealizableKnown = false
3584+
private[this] var isRealizableCache: Boolean = _
3585+
3586+
def isRealizable(implicit ctx: Context) = {
3587+
if (!isRealizableKnown) {
3588+
isRealizableCache = realizability(info) == Realizable
3589+
isRealizableKnown = true
3590+
}
3591+
isRealizableCache
3592+
}
3593+
35763594
private[this] var myRepr: Name = null
35773595
def repr(implicit ctx: Context): Name = {
35783596
if (myRepr == null) myRepr = SkolemName.fresh()
@@ -4506,6 +4524,8 @@ object Types {
45064524
else if (lo `eq` hi) lo
45074525
else Range(lower(lo), upper(hi))
45084526

4527+
protected def emptyRange = range(defn.NothingType, defn.AnyType)
4528+
45094529
protected def isRange(tp: Type): Boolean = tp.isInstanceOf[Range]
45104530

45114531
protected def lower(tp: Type): Type = tp match {
@@ -4578,6 +4598,9 @@ object Types {
45784598
else tryWiden(tp, preHi)
45794599
forwarded.orElse(
45804600
range(super.derivedSelect(tp, preLo).loBound, super.derivedSelect(tp, preHi).hiBound))
4601+
case pre: SkolemType if !pre.isRealizable =>
4602+
// If `pre` is not realizable it could would be in general unsound to use it as a path
4603+
emptyRange
45814604
case _ =>
45824605
super.derivedSelect(tp, pre) match {
45834606
case TypeBounds(lo, hi) => range(lo, hi)
@@ -4630,7 +4653,7 @@ object Types {
46304653
else tp.derivedTypeBounds(lo, hi)
46314654

46324655
override protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type): Type =
4633-
if (isRange(thistp) || isRange(supertp)) range(defn.NothingType, defn.AnyType)
4656+
if (isRange(thistp) || isRange(supertp)) emptyRange
46344657
else tp.derivedSuperType(thistp, supertp)
46354658

46364659
override protected def derivedAppliedType(tp: AppliedType, tycon: Type, args: List[Type]): Type =

compiler/src/dotty/tools/dotc/typer/Applications.scala

+3-2
Original file line numberDiff line numberDiff line change
@@ -478,8 +478,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
478478
addArg(typedArg(arg, formal), formal)
479479
if (methodType.isParamDependent && typeOfArg(arg).exists)
480480
// `typeOfArg(arg)` could be missing because the evaluation of `arg` produced type errors
481-
safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg))
482-
else identity
481+
safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg), initVariance = -1)
482+
else
483+
identity
483484
}
484485

485486
def missingArg(n: Int): Unit = {

compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala

+14-5
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ trait TypeAssigner {
105105
case info: ClassInfo =>
106106
range(defn.NothingType, apply(classBound(info)))
107107
case _ =>
108-
range(defn.NothingType, defn.AnyType) // should happen only in error cases
108+
emptyRange // should happen only in error cases
109109
}
110110
case tp: ThisType if toAvoid(tp.cls) =>
111111
range(defn.NothingType, apply(classBound(tp.cls.classInfo)))
@@ -340,13 +340,22 @@ trait TypeAssigner {
340340
}
341341
}
342342

343-
/** Substitute argument type `argType` for parameter `pref` in type `tp`,
343+
/** Substitute argument type `argType` for parameter `pref` in type `tp`
344344
* skolemizing the argument type if it is not stable and `pref` occurs in `tp`.
345+
* Skolemization has to be done in an approximating type map since the underlying
346+
* type might not be realizable, in which case the skolem cannot be used as a path.
345347
*/
346-
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type)(implicit ctx: Context): Type = {
348+
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type, initVariance: Int = 1)(implicit ctx: Context): Type = {
347349
val tp1 = tp.substParam(pref, argType)
348-
if ((tp1 eq tp) || argType.isStable) tp1
349-
else tp.substParam(pref, SkolemType(argType.widen))
350+
if ((tp1 eq tp) || argType.isStableRealizable) tp1
351+
else {
352+
val avoidParam = new ApproximatingTypeMap {
353+
val skolem = SkolemType(argType.widen)
354+
variance = initVariance
355+
def apply(t: Type) = if (t `eq` pref) skolem else mapOver(t)
356+
}
357+
avoidParam(tp)
358+
}
350359
}
351360

352361
/** Substitute types of all arguments `args` for corresponding `params` in `tp`.

tests/neg/i4031-posttyper.scala

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
object App {
2+
trait A { type L >: Any}
3+
def upcast(a: A, x: Any): a.L = x
4+
lazy val p: A { type L <: Nothing } = p
5+
val q = new A { type L = Any }
6+
def coerce2(x: Any): Int = upcast(p, x): p.L // error: not a legal path
7+
}

tests/neg/i4031.scala

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// originlly reported in #4031
2+
object Test {
3+
trait A { type L >: Any}
4+
def upcast(a: A, x: Any): a.L = x
5+
lazy val p: A { type L <: Nothing } = p
6+
def coerce(x: Any): Int = upcast(p, x) // error: found Any required: Int
7+
8+
def main(args: Array[String]): Unit = {
9+
println(coerce("Uh oh!"))
10+
}
11+
}
12+
// variations
13+
object App {
14+
trait A { type L >: Any}
15+
def upcast(a: A, x: Any): a.L = x
16+
lazy val p: A { type L <: Nothing } = p
17+
val q = new A { type L = Any }
18+
def coerce(x: Any): Int = upcast(p, x) // error: found Any required: Int
19+
def compare(x: A, y: x.L) = assert(x == y)
20+
def compare2(x: A)(y: x.type) = assert(x == y)
21+
def main(args: Array[String]): Unit = {
22+
println(coerce("Uh oh!"))
23+
compare(p, p) // error: found App.A{L <: Nothing}(App.p) required: Nothing
24+
compare2(p)(p) // error: found App.A{L <: Nothing}(App.p) required: App.A{L <: Nothing}(?1)
25+
}
26+
}

tests/neg/i4060.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@ object App {
66
trait X { type R >: U }
77
trait Y { type R = V }
88

9-
class T[A <: X](erased val a: A)(val value: a.R) // error
9+
class T[A <: X](erased val a: A)(val value: a.R)
1010

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

13-
val a = new T[Y & X](O.x)(u)
13+
val a = new T[Y & X](O.x)(u) // error
1414
a.value
1515
}
1616

tests/neg/i50-volatile.scala

+12-5
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,23 @@ class Test {
1010
}
1111
lazy val o: A & B = ???
1212

13-
class Client extends o.Inner // old-error // old-error
13+
class Client extends o.Inner // error
1414

15-
def xToString(x: o.X): String = x // old-error
15+
def xToString(x: o.X): String = x // error
1616

1717
def intToString(i: Int): String = xToString(i)
1818
}
19-
object Test2 {
2019

21-
import Test.o._ // error
20+
object Test2 {
21+
trait A {
22+
type X = String
23+
}
24+
trait B {
25+
type X = Int
26+
}
27+
lazy val o: A & B = ???
2228

23-
def xToString(x: X): String = x
29+
def xToString(x: o.X): String = x // error
2430

31+
def intToString(i: Int): String = xToString(i)
2532
}

tests/neg/realizability.scala

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
class C { type T }
2+
3+
class Test {
4+
5+
type D <: C
6+
7+
lazy val a: C = ???
8+
final lazy val b: C = ???
9+
val c: D = ???
10+
final lazy val d: D = ???
11+
12+
val x1: a.T = ??? // error: not a legal path, since a is lazy & non-final
13+
val x2: b.T = ??? // OK, b is lazy but concrete
14+
val x3: c.T = ??? // OK, c is abstract but strict
15+
val x4: d.T = ??? // error: not a legal path since d is abstract and lazy
16+
17+
val y1: Singleton = a
18+
val y2: Singleton = a
19+
val y3: Singleton = a
20+
val y4: Singleton = a
21+
22+
}

tests/pos/i4031.scala

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
object App {
2+
trait A { type L >: Any}
3+
def upcast(a: A, x: Any): a.L = x
4+
lazy val p: A { type L <: Nothing } = p
5+
val q = new A { type L = Any }
6+
def coerce1(x: Any): Any = upcast(q, x) // ok
7+
def coerce3(x: Any): Any = upcast(p, x) // ok, since dependent result type is not needed
8+
}

0 commit comments

Comments
 (0)