Skip to content

Fix #4031, v2: Check arguments of dependent methods for realizability (WIP) #5557

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 13 commits into from
Closed
26 changes: 15 additions & 11 deletions compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ import collection.mutable
/** Realizability status */
object CheckRealizable {

abstract class Realizability(val msg: String) {
sealed abstract class Realizability(val msg: String) {
def andAlso(other: => Realizability): Realizability =
if (this == Realizable) other else this
def mapError(f: Realizability => Realizability): Realizability =
Expand Down Expand Up @@ -70,16 +70,20 @@ class CheckRealizable(implicit ctx: Context) {
def realizability(tp: Type): Realizability = tp.dealias match {
case tp: TermRef =>
val sym = tp.symbol
if (sym.is(Stable)) realizability(tp.prefix)
else {
val r =
if (!sym.isStable) NotStable
else if (!isLateInitialized(sym)) realizability(tp.prefix)
else if (!sym.isEffectivelyFinal) new NotFinal(sym)
else realizability(tp.info).mapError(r => new ProblemInUnderlying(tp.info, r))
if (r == Realizable) sym.setFlag(Stable)
r
}
val r =
if (sym.is(Stable)) realizability(tp.prefix)
else {
val r =
if (!sym.isStable) NotStable
else if (!isLateInitialized(sym)) Realizable
else if (!sym.isEffectivelyFinal) new NotFinal(sym)
else realizability(tp.info).mapError(r => new ProblemInUnderlying(tp.info, r))
r andAlso {
sym.setFlag(Stable)
realizability(tp.prefix)
}
}
if (r == Realizable || tp.info.isStableRealizable) Realizable else r
case _: SingletonType | NoPrefix =>
Realizable
case tp =>
Expand Down
14 changes: 7 additions & 7 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -319,7 +319,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
thirdTry
case tp1: TypeParamRef =>
def flagNothingBound = {
if (!frozenConstraint && tp2.isRef(defn.NothingClass) && state.isGlobalCommittable) {
if (!frozenConstraint && tp2.isRef(NothingClass) && state.isGlobalCommittable) {
def msg = s"!!! instantiated to Nothing: $tp1, constraint = ${constraint.show}"
if (Config.failOnInstantiationToNothing) assert(false, msg)
else ctx.log(msg)
Expand Down Expand Up @@ -404,8 +404,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
if (cls2.isClass) {
if (cls2.typeParams.isEmpty) {
if (cls2 eq AnyKindClass) return true
if (tp1.isRef(defn.NothingClass)) return true
if (tp1.isRef(NothingClass)) return true
if (tp1.isLambdaSub) return false
if (cls2 eq AnyClass) return true
// Note: We would like to replace this by `if (tp1.hasHigherKind)`
// but right now we cannot since some parts of the standard library rely on the
// idiom that e.g. `List <: Any`. We have to bootstrap without scalac first.
Expand All @@ -417,7 +418,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
val base = tp1.baseType(cls2)
if (base.typeSymbol == cls2) return true
}
else if (tp1.isLambdaSub && !tp1.isRef(defn.AnyKindClass))
else if (tp1.isLambdaSub && !tp1.isRef(AnyKindClass))
return recur(tp1, EtaExpansion(cls2.typeRef))
}
fourthTry
Expand Down Expand Up @@ -1382,7 +1383,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
// at run time. It would not work to replace that with `Nothing`.
// However, maybe we can still apply the replacement to
// types which are not explicitly written.
defn.NothingType
NothingType
case _ => andType(tp1, tp2)
}
case _ => andType(tp1, tp2)
Expand All @@ -1393,8 +1394,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {
}

/** The greatest lower bound of a list types */
final def glb(tps: List[Type]): Type =
((defn.AnyType: Type) /: tps)(glb)
final def glb(tps: List[Type]): Type = ((AnyType: Type) /: tps)(glb)

/** The least upper bound of two types
* @param canConstrain If true, new constraints might be added to simplify the lub.
Expand Down Expand Up @@ -1424,7 +1424,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling {

/** The least upper bound of a list of types */
final def lub(tps: List[Type]): Type =
((defn.NothingType: Type) /: tps)(lub(_,_, canConstrain = false))
((NothingType: Type) /: tps)(lub(_,_, canConstrain = false))

/** Try to produce joint arguments for a lub `A[T_1, ..., T_n] | A[T_1', ..., T_n']` using
* the following strategies:
Expand Down
11 changes: 10 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ import Denotations._
import Periods._
import util.Stats._
import util.SimpleIdentitySet
import CheckRealizable._
import reporting.diagnostic.Message
import ast.tpd._
import ast.TreeTypeMap
Expand Down Expand Up @@ -157,6 +158,12 @@ object Types {
case _ => false
}

/** Does this type denote a realizable stable reference? Much more expensive to check
* than isStable, that's why some of the checks are done later in PostTyper.
*/
final def isStableRealizable(implicit ctx: Context): Boolean =
isStable && realizability(this) == Realizable

/** Is this type a (possibly refined or applied or aliased) type reference
* to the given type symbol?
* @sym The symbol to compare to. It must be a class symbol or abstract type.
Expand Down Expand Up @@ -4506,6 +4513,8 @@ object Types {
else if (lo `eq` hi) lo
else Range(lower(lo), upper(hi))

protected def emptyRange: Type = range(defn.NothingType, defn.AnyType)

protected def isRange(tp: Type): Boolean = tp.isInstanceOf[Range]

protected def lower(tp: Type): Type = tp match {
Expand Down Expand Up @@ -4630,7 +4639,7 @@ object Types {
else tp.derivedTypeBounds(lo, hi)

override protected def derivedSuperType(tp: SuperType, thistp: Type, supertp: Type): Type =
if (isRange(thistp) || isRange(supertp)) range(defn.NothingType, defn.AnyType)
if (isRange(thistp) || isRange(supertp)) emptyRange
else tp.derivedSuperType(thistp, supertp)

override protected def derivedAppliedType(tp: AppliedType, tycon: Type, args: List[Type]): Type =
Expand Down
5 changes: 3 additions & 2 deletions compiler/src/dotty/tools/dotc/typer/Applications.scala
Original file line number Diff line number Diff line change
Expand Up @@ -478,8 +478,9 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
addArg(typedArg(arg, formal), formal)
if (methodType.isParamDependent && typeOfArg(arg).exists)
// `typeOfArg(arg)` could be missing because the evaluation of `arg` produced type errors
safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg))
else identity
safeSubstParam(_, methodType.paramRefs(n), typeOfArg(arg), initVariance = -1)
else
identity
}

def missingArg(n: Int): Unit = {
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/RefChecks.scala
Original file line number Diff line number Diff line change
Expand Up @@ -979,7 +979,7 @@ class RefChecks extends MiniPhase { thisPhase =>
checkAllOverrides(cls)
tree
} catch {
case ex: MergeError =>
case ex: TypeError =>
ctx.error(ex.getMessage, tree.pos)
tree
}
Expand Down
31 changes: 25 additions & 6 deletions compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import NameOps._
import collection.mutable
import reporting.diagnostic.messages._
import Checking.checkNoPrivateLeaks
import CheckRealizable._

trait TypeAssigner {
import tpd._
Expand Down Expand Up @@ -105,7 +106,7 @@ trait TypeAssigner {
case info: ClassInfo =>
range(defn.NothingType, apply(classBound(info)))
case _ =>
range(defn.NothingType, defn.AnyType) // should happen only in error cases
emptyRange // should happen only in error cases
}
case tp: ThisType if toAvoid(tp.cls) =>
range(defn.NothingType, apply(classBound(tp.cls.classInfo)))
Expand Down Expand Up @@ -340,13 +341,31 @@ trait TypeAssigner {
}
}

/** Substitute argument type `argType` for parameter `pref` in type `tp`,
* skolemizing the argument type if it is not stable and `pref` occurs in `tp`.
/** Substitute argument type `argType` for parameter `pref` in type `tp`, but
* take special measures if the argument is not realizable:
* 1. If the widened argument type is known to have good bounds,
* substitute the skolemized argument type.
* 2. If the widened argument type is not known to have good bounds, eliminate all references
* to the parameter in `tp`.
* (2) is necessary since even with a skolemized type we might break subtyping if
* bounds are bad. This could lead to errors not being detected. A test case is the second
* failure in neg/i4031.scala
*/
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type)(implicit ctx: Context): Type = {
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type, initVariance: Int = 1)(implicit ctx: Context): Type = {
val tp1 = tp.substParam(pref, argType)
if ((tp1 eq tp) || argType.isStable) tp1
else tp.substParam(pref, SkolemType(argType.widen))
if ((tp1 eq tp) || argType.isStableRealizable) tp1
else {
val widenedArgType = argType.widen
if (realizability(widenedArgType) == Realizable)
tp.substParam(pref, SkolemType(widenedArgType))
else {
val avoidParam = new ApproximatingTypeMap {
variance = initVariance
def apply(t: Type) = if (t `eq` pref) emptyRange else mapOver(t)
}
avoidParam(tp)
}
}
}

/** Substitute types of all arguments `args` for corresponding `params` in `tp`.
Expand Down
3 changes: 3 additions & 0 deletions tests/neg/i4031-anysel.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
object Test {
val v: Any = 1: Any#L // error
}
7 changes: 7 additions & 0 deletions tests/neg/i4031-posttyper.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
object App {
trait A { type L >: Any}
def upcast(a: A, x: Any): a.L = x
lazy val p: A { type L <: Nothing } = p
val q = new A { type L = Any }
def coerce2(x: Any): Int = upcast(p, x): p.L // error: not a legal path
}
17 changes: 17 additions & 0 deletions tests/neg/i4031.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
object App {
trait A { type L >: Any}
def upcast(a: A, x: Any): a.L = x
lazy val p: A { type L <: Nothing } = p
val q = new A { type L = Any }
def coerce(x: Any): Int = upcast(p, x) // error: not a legal path

def compare(x: A, y: x.L) = assert(x == y)
def compare2(x: A)(y: x.type) = assert(x == y)


def main(args: Array[String]): Unit = {
println(coerce("Uh oh!"))
compare(p, p) // error: not a legal path
compare2(p)(p) // error: not a legal path
}
}
17 changes: 12 additions & 5 deletions tests/neg/i50-volatile.scala
Original file line number Diff line number Diff line change
Expand Up @@ -10,16 +10,23 @@ class Test {
}
lazy val o: A & B = ???

class Client extends o.Inner // old-error // old-error
class Client extends o.Inner // error // old-error

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

def intToString(i: Int): String = xToString(i)
}
object Test2 {

import Test.o._ // error
object Test2 {
trait A {
type X = String
}
trait B {
type X = Int
}
lazy val o: A & B = ???

def xToString(x: X): String = x
def xToString(x: o.X): String = x // error

def intToString(i: Int): String = xToString(i)
}
12 changes: 12 additions & 0 deletions tests/neg/i5521.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
class Hello {
class Foo {
class Bar
final lazy val s: Bar = ???
}

lazy val foo: Foo = ???

val x: foo.s.type = ??? // error: `foo` must be final since it's a lazy val
val x2: foo.s.type = ??? // error: `foo` must be final since it's a lazy val
}

22 changes: 22 additions & 0 deletions tests/neg/realizability.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
class C { type T }

class Test {

type D <: C

lazy val a: C = ???
final lazy val b: C = ???
val c: D = ???
final lazy val d: D = ???

val x1: a.T = ??? // error: not a legal path, since a is lazy & non-final
val x2: b.T = ??? // OK, b is lazy but concrete
val x3: c.T = ??? // OK, c is abstract but strict
val x4: d.T = ??? // error: not a legal path since d is abstract and lazy

val y1: Singleton = a
val y2: Singleton = a
val y3: Singleton = a
val y4: Singleton = a

}
64 changes: 64 additions & 0 deletions tests/pos-deep-subtype/i4036.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
trait A { def x: this.type = this; type T }
trait B { def y: this.type = this; def x: y.type = y; type T }
object A {
val v = new A { type T = Int }
v: v.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.type

1: v.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.T

val u = new B { type T = Int }
u: u.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.x.
x.type

val z = new B { type T = this.type }
z: z.T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#
T#T#T#T#T#T#T#T#T#T#T#T#T#T#T#T
}
8 changes: 8 additions & 0 deletions tests/pos/i4031.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
object App {
trait A { type L >: Any}
def upcast(a: A, x: Any): a.L = x
lazy val p: A { type L <: Nothing } = p
val q = new A { type L = Any }
def coerce1(x: Any): Any = upcast(q, x) // ok
def coerce3(x: Any): Any = upcast(p, x) // ok, since dependent result type is not needed
}