Skip to content

Commit c89e85c

Browse files
committed
Merge pull request #599 from dotty-staging/add/existential-skolemization
Tighten comparison of skolem types
2 parents 2ce159f + 310615e commit c89e85c

23 files changed

+364
-242
lines changed

src/dotty/tools/dotc/config/Config.scala

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,11 @@ object Config {
3232
*/
3333
final val checkConstraintsPropagated = false
3434

35+
/** Check that no type appearing as the info of a SymDenotation contains
36+
* skolem types.
37+
*/
38+
final val checkNoSkolemsInInfo = false
39+
3540
/** Type comparer will fail with an assert if the upper bound
3641
* of a constrained parameter becomes Nothing. This should be turned
3742
* on only for specific debugging as normally instantiation to Nothing

src/dotty/tools/dotc/core/Phases.scala

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -285,6 +285,9 @@ object Phases {
285285
*/
286286
def relaxedTyping: Boolean = false
287287

288+
/** Overridden by FrontEnd */
289+
def isTyper = false
290+
288291
def exists: Boolean = true
289292

290293
private var myPeriod: Period = Periods.InvalidPeriod

src/dotty/tools/dotc/core/Skolemization.scala

Lines changed: 0 additions & 126 deletions
This file was deleted.

src/dotty/tools/dotc/core/Substituters.scala

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -179,21 +179,21 @@ trait Substituters { this: Context =>
179179
.mapOver(tp)
180180
}
181181

182-
final def substSkolem(tp: Type, from: Type, to: Type, theMap: SubstSkolemMap): Type =
182+
final def substRefinedThis(tp: Type, from: Type, to: Type, theMap: SubstRefinedThisMap): Type =
183183
tp match {
184-
case tp @ SkolemType(binder) =>
184+
case tp @ RefinedThis(binder) =>
185185
if (binder eq from) to else tp
186186
case tp: NamedType =>
187187
if (tp.currentSymbol.isStatic) tp
188-
else tp.derivedSelect(substSkolem(tp.prefix, from, to, theMap))
188+
else tp.derivedSelect(substRefinedThis(tp.prefix, from, to, theMap))
189189
case _: ThisType | _: BoundType | NoPrefix =>
190190
tp
191191
case tp: RefinedType =>
192-
tp.derivedRefinedType(substSkolem(tp.parent, from, to, theMap), tp.refinedName, substSkolem(tp.refinedInfo, from, to, theMap))
192+
tp.derivedRefinedType(substRefinedThis(tp.parent, from, to, theMap), tp.refinedName, substRefinedThis(tp.refinedInfo, from, to, theMap))
193193
case tp: TypeAlias =>
194-
tp.derivedTypeAlias(substSkolem(tp.alias, from, to, theMap))
194+
tp.derivedTypeAlias(substRefinedThis(tp.alias, from, to, theMap))
195195
case _ =>
196-
(if (theMap != null) theMap else new SubstSkolemMap(from, to))
196+
(if (theMap != null) theMap else new SubstRefinedThisMap(from, to))
197197
.mapOver(tp)
198198
}
199199

@@ -222,7 +222,7 @@ trait Substituters { this: Context =>
222222
case tp: NamedType =>
223223
if (tp.currentSymbol.isStatic) tp
224224
else tp.derivedSelect(substParams(tp.prefix, from, to, theMap))
225-
case _: ThisType | NoPrefix | _: SkolemType =>
225+
case _: ThisType | NoPrefix =>
226226
tp
227227
case tp: RefinedType =>
228228
tp.derivedRefinedType(substParams(tp.parent, from, to, theMap), tp.refinedName, substParams(tp.refinedInfo, from, to, theMap))
@@ -266,8 +266,8 @@ trait Substituters { this: Context =>
266266
def apply(tp: Type): Type = substThis(tp, from, to, this)
267267
}
268268

269-
final class SubstSkolemMap(from: Type, to: Type) extends DeepTypeMap {
270-
def apply(tp: Type): Type = substSkolem(tp, from, to, this)
269+
final class SubstRefinedThisMap(from: Type, to: Type) extends DeepTypeMap {
270+
def apply(tp: Type): Type = substRefinedThis(tp, from, to, this)
271271
}
272272

273273
final class SubstParamMap(from: ParamType, to: Type) extends DeepTypeMap {

src/dotty/tools/dotc/core/SymDenotations.scala

Lines changed: 24 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ object SymDenotations {
7979
super.validFor_=(p)
8080
}
8181
*/
82+
if (Config.checkNoSkolemsInInfo) assertNoSkolems(initInfo)
8283

8384
// ------ Getting and setting fields -----------------------------
8485

@@ -168,8 +169,8 @@ object SymDenotations {
168169
}
169170

170171
protected[dotc] final def info_=(tp: Type) = {
171-
/*
172-
def illegal: String = s"illegal type for $this: $tp"
172+
/* // DEBUG
173+
def illegal: String = s"illegal type for $this: $tp"
173174
if (this is Module) // make sure module invariants that allow moduleClass and sourceModule to work are kept.
174175
tp match {
175176
case tp: ClassInfo => assert(tp.selfInfo.isInstanceOf[TermRefBySym], illegal)
@@ -178,6 +179,7 @@ object SymDenotations {
178179
case _ =>
179180
}
180181
*/
182+
if (Config.checkNoSkolemsInInfo) assertNoSkolems(initInfo)
181183
myInfo = tp
182184
}
183185

@@ -1049,8 +1051,28 @@ object SymDenotations {
10491051
s"$kindString $name"
10501052
}
10511053

1054+
// ----- Sanity checks and debugging */
1055+
10521056
def debugString = toString + "#" + symbol.id // !!! DEBUG
10531057

1058+
def hasSkolems(tp: Type): Boolean = tp match {
1059+
case tp: SkolemType => true
1060+
case tp: NamedType => hasSkolems(tp.prefix)
1061+
case tp: RefinedType => hasSkolems(tp.parent) || hasSkolems(tp.refinedInfo)
1062+
case tp: PolyType => tp.paramBounds.exists(hasSkolems) || hasSkolems(tp.resType)
1063+
case tp: MethodType => tp.paramTypes.exists(hasSkolems) || hasSkolems(tp.resType)
1064+
case tp: ExprType => hasSkolems(tp.resType)
1065+
case tp: AndOrType => hasSkolems(tp.tp1) || hasSkolems(tp.tp2)
1066+
case tp: TypeBounds => hasSkolems(tp.lo) || hasSkolems(tp.hi)
1067+
case tp: AnnotatedType => hasSkolems(tp.tpe)
1068+
case tp: TypeVar => hasSkolems(tp.inst)
1069+
case _ => false
1070+
}
1071+
1072+
def assertNoSkolems(tp: Type) =
1073+
if (!this.isSkolem)
1074+
assert(!hasSkolems(tp), s"assigning type $tp containing skolems to $this")
1075+
10541076
// ----- copies and transforms ----------------------------------------
10551077

10561078
protected def newLikeThis(s: Symbol, i: Type): SingleDenotation = new UniqueRefDenotation(s, i, validFor)

src/dotty/tools/dotc/core/TypeApplications.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -387,9 +387,9 @@ class TypeApplications(val self: Type) extends AnyVal {
387387
case _ => firstBaseArgInfo(defn.SeqClass)
388388
}
389389

390-
def containsSkolemType(target: Type)(implicit ctx: Context): Boolean = {
390+
def containsRefinedThis(target: Type)(implicit ctx: Context): Boolean = {
391391
def recur(tp: Type): Boolean = tp.stripTypeVar match {
392-
case SkolemType(tp) =>
392+
case RefinedThis(tp) =>
393393
tp eq target
394394
case tp: NamedType =>
395395
tp.info match {
@@ -446,7 +446,7 @@ class TypeApplications(val self: Type) extends AnyVal {
446446

447447
def replacements(rt: RefinedType): List[Type] =
448448
for (sym <- boundSyms)
449-
yield TypeRef(SkolemType(rt), correspondingParamName(sym))
449+
yield TypeRef(RefinedThis(rt), correspondingParamName(sym))
450450

451451
def rewrite(tp: Type): Type = tp match {
452452
case tp @ RefinedType(parent, name: TypeName) =>
@@ -489,7 +489,7 @@ class TypeApplications(val self: Type) extends AnyVal {
489489
val lambda = defn.lambdaTrait(boundSyms.map(_.variance))
490490
val substitutedRHS = (rt: RefinedType) => {
491491
val argRefs = boundSyms.indices.toList.map(i =>
492-
SkolemType(rt).select(tpnme.lambdaArgName(i)))
492+
RefinedThis(rt).select(tpnme.lambdaArgName(i)))
493493
tp.subst(boundSyms, argRefs).bounds.withVariance(1)
494494
}
495495
val res = RefinedType(lambda.typeRef, tpnme.Apply, substitutedRHS)

src/dotty/tools/dotc/core/TypeComparer.scala

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ import scala.util.control.NonFatal
1616

1717
/** Provides methods to compare types.
1818
*/
19-
class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling with Skolemization {
19+
class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
2020
implicit val ctx: Context = initctx
2121

2222
val state = ctx.typerState
@@ -276,7 +276,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
276276
}
277277
case tp1: SkolemType =>
278278
tp2 match {
279-
case tp2: SkolemType if tp1 == tp2 => true
279+
case tp2: SkolemType if !ctx.phase.isTyper && tp1.info <:< tp2.info => true
280280
case _ => thirdTry(tp1, tp2)
281281
}
282282
case tp1: TypeVar =>
@@ -536,18 +536,16 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
536536
* rebase both itself and the member info of `tp` on a freshly created skolem type.
537537
*/
538538
protected def hasMatchingMember(name: Name, tp1: Type, tp2: RefinedType): Boolean = {
539-
val saved = skolemsOutstanding
540-
try {
541-
val rebindNeeded = tp2.refinementRefersToThis
542-
val base = if (rebindNeeded) ensureStableSingleton(tp1) else tp1
543-
val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substSkolem(tp2, base) else tp2.refinedInfo
544-
def qualifies(m: SingleDenotation) = isSubType(m.info, rinfo2)
545-
def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
546-
case mbr: SingleDenotation => qualifies(mbr)
547-
case _ => mbr hasAltWith qualifies
548-
}
549-
/*>|>*/ ctx.traceIndented(i"hasMatchingMember($base . $name :? ${tp2.refinedInfo}) ${base.member(name).info.show} $rinfo2", subtyping) /*<|<*/ {
550-
memberMatches(base member name) ||
539+
val rebindNeeded = tp2.refinementRefersToThis
540+
val base = if (rebindNeeded) ensureStableSingleton(tp1) else tp1
541+
val rinfo2 = if (rebindNeeded) tp2.refinedInfo.substRefinedThis(tp2, base) else tp2.refinedInfo
542+
def qualifies(m: SingleDenotation) = isSubType(m.info, rinfo2)
543+
def memberMatches(mbr: Denotation): Boolean = mbr match { // inlined hasAltWith for performance
544+
case mbr: SingleDenotation => qualifies(mbr)
545+
case _ => mbr hasAltWith qualifies
546+
}
547+
/*>|>*/ ctx.traceIndented(i"hasMatchingMember($base . $name :? ${tp2.refinedInfo}) ${base.member(name).info.show} $rinfo2", subtyping) /*<|<*/ {
548+
memberMatches(base member name) ||
551549
tp1.isInstanceOf[SingletonType] &&
552550
{ // special case for situations like:
553551
// class C { type T }
@@ -558,9 +556,13 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
558556
case _ => false
559557
}
560558
}
561-
}
562559
}
563-
finally skolemsOutstanding = saved
560+
}
561+
562+
final def ensureStableSingleton(tp: Type): SingletonType = tp.stripTypeVar match {
563+
case tp: SingletonType if tp.isStable => tp
564+
case tp: ValueType => SkolemType(tp)
565+
case tp: TypeProxy => ensureStableSingleton(tp.underlying)
564566
}
565567

566568
/** Skip refinements in `tp2` which match corresponding refinements in `tp1`.
@@ -645,13 +647,12 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling wi
645647
private def narrowGADTBounds(tr: NamedType, bound: Type, isUpper: Boolean): Boolean =
646648
ctx.mode.is(Mode.GADTflexible) && {
647649
val tparam = tr.symbol
648-
val bound1 = deSkolemize(bound, toSuper = !isUpper)
649-
typr.println(s"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound1 ${bound1.isRef(tparam)}")
650-
!bound1.isRef(tparam) && {
650+
typr.println(s"narrow gadt bound of $tparam: ${tparam.info} from ${if (isUpper) "above" else "below"} to $bound ${bound.isRef(tparam)}")
651+
!bound.isRef(tparam) && {
651652
val oldBounds = ctx.gadt.bounds(tparam)
652653
val newBounds =
653-
if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound1)
654-
else TypeBounds(oldBounds.lo | bound1, oldBounds.hi)
654+
if (isUpper) TypeBounds(oldBounds.lo, oldBounds.hi & bound)
655+
else TypeBounds(oldBounds.lo | bound, oldBounds.hi)
655656
isSubType(newBounds.lo, newBounds.hi) &&
656657
{ ctx.gadt.setBounds(tparam, newBounds); true }
657658
}

0 commit comments

Comments
 (0)