Skip to content

Cleanup and improve realizability (reopen #5558) #5727

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.

Sign up for GitHub

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 9 commits into from
Closed

Cleanup and improve realizability (reopen #5558) #5727

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
224b2ac
Show that Any#L is still rejected when written by the user
Blaisorblade Dec 2, 2018
6a5f9da
Harden RefChecks
odersky Mar 28, 2018
d5d1d42
Drop stray comma
Blaisorblade Dec 2, 2018
11fffe0
Seal Realizability
Blaisorblade Apr 10, 2018
8475876
Cleanup: don't refer to members of defn directly
Blaisorblade Dec 2, 2018
58aabb4
Align isRealizable with isStable
odersky Mar 20, 2018
f435850
Use ProblemInUnderlying consistently
Blaisorblade May 30, 2018
6d063a4
Add stress-test for realizability checking
Blaisorblade Apr 10, 2018
72ea704
Refactor realizability to also cache result of isStableRealizable
Blaisorblade Dec 2, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
59 changes: 45 additions & 14 deletions compiler/src/dotty/tools/dotc/core/CheckRealizable.scala
View file
Open in desktop
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 @@ -49,7 +49,7 @@ object CheckRealizable {
def boundsRealizability(tp: Type)(implicit ctx: Context): Realizability =
new CheckRealizable().boundsRealizability(tp)

private val LateInitialized = Lazy | Erased,
private val LateInitialized = Lazy | Erased
}

/** Compute realizability status */
Expand All @@ -66,22 +66,53 @@ class CheckRealizable(implicit ctx: Context) {
*/
private def isLateInitialized(sym: Symbol) = sym.is(LateInitialized, butNot = Module)

/** The realizability status of given type `tp`*/
/** The realizability status of given type `tp`. Types can only project
* members from realizable types, that is, types having non-null values and
* not depending on mutable state.
* Beware that subtypes of realizable types might not be realizable; hence
* realizability checking restricts overriding. */
def realizability(tp: Type): Realizability = tp.dealias match {
case tp: TermRef =>
// Suppose tp is a.b.c.type, where c is declared with type T, then sym is c, tp.info is T and
// and tp.prefix is a.b.
val sym = tp.symbol
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)
}
// tp is realizable if it selects a stable member on a realizable prefix.

/** A member is always stable if tp.info is a realizable singleton type. We check this last
for performance, in all cases where some unrelated check might have failed. */
def patchRealizability(r: Realizability) =
r.mapError(if (tp.info.isStableRealizable) Realizable else _)

def computeStableMember(): Realizability = {
// Reject fields that are mutable, by-name, and similar.
if (!sym.isStable)
patchRealizability(NotStable)
// Accept non-lazy symbols "lazy"
else if (!isLateInitialized(sym))
patchRealizability(Realizable)
// Accept symbols that are lazy/erased, can't be overridden, and
// have a realizable type. We require finality because overrides
// of realizable fields might not be realizable.
else if (!sym.isEffectivelyFinal)
patchRealizability(new NotFinal(sym))
else
// Since patchRealizability checks realizability(tp.info) through
// isStableRealizable, using patchRealizability wouldn't make
// a difference. Calling it here again might introduce a slowdown
// exponential in the prefix length, so we avoid it at the cost of
// code complexity.
realizability(tp.info).mapError(r => new ProblemInUnderlying(tp.info, r))
}

val stableMember =
// 1. the symbol is flagged as stable.
if (sym.is(Stable)) Realizable
else {
val r = computeStableMember()
if (r == Realizable) sym.setFlag(Stable)
r
}
stableMember andAlso realizability(tp.prefix).mapError(r => new ProblemInUnderlying(tp.prefix, r))
case _: SingletonType | NoPrefix =>
Realizable
case tp =>
Expand Down
13 changes: 6 additions & 7 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
View file
Open in desktop
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,7 +404,7 @@ 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
// 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
Expand All @@ -417,7 +417,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 +1382,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 +1393,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 +1423,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
7 changes: 7 additions & 0 deletions compiler/src/dotty/tools/dotc/core/Types.scala
View file
Open in desktop
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
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/RefChecks.scala
View file
Open in desktop
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
3 changes: 3 additions & 0 deletions tests/neg/i4031-anysel.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
object Test {
val v: Any = 1: Any#L // error
}
64 changes: 64 additions & 0 deletions tests/pos-deep-subtype/i4036.scala
View file
Open in desktop
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
}