Skip to content

Commit 7d9ae5f

Browse files
authored
Merge pull request #8139 from dotty-staging/fix-#8128
Fix #8128: Fix atoms computations
2 parents 4ac8511 + 8a5ca00 commit 7d9ae5f

File tree

8 files changed

+163
-90
lines changed

8 files changed

+163
-90
lines changed

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,12 @@ object Config {
141141
*/
142142
final val checkUnerased = false
143143

144+
/** Check that atoms-based comparisons match regular comparisons that do not
145+
* take atoms into account. The two have to give the same results, since
146+
* atoms comparison is intended to be just an optimization.
147+
*/
148+
final val checkAtomsComparisons = false
149+
144150
/** In `derivedSelect`, rewrite
145151
*
146152
* (S & T)#A --> S#A & T#A
Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
package dotty.tools
2+
package dotc
3+
package core
4+
5+
import Types._
6+
7+
/** Indicates the singleton types that a type must or may consist of.
8+
* @param lo The lower bound: singleton types in this set are guaranteed
9+
* to be in the carrier type.
10+
* @param hi The upper bound: all singleton types in the carrier type are
11+
* guaranteed to be in this set
12+
* If the underlying type of a singleton type is another singleton type,
13+
* only the latter type ends up in the sets.
14+
*/
15+
enum Atoms:
16+
case Range(lo: Set[Type], hi: Set[Type])
17+
case Unknown
18+
19+
def & (that: Atoms): Atoms = this match
20+
case Range(lo1, hi1) =>
21+
that match
22+
case Range(lo2, hi2) => Range(lo1 & lo2, hi1 & hi2)
23+
case Unknown => this
24+
case Unknown => that
25+
26+
def | (that: Atoms): Atoms = this match
27+
case Range(lo1, hi1) =>
28+
that match
29+
case Range(lo2, hi2) => Range(lo1 | lo2, hi1 | hi2)
30+
case Unknown => Unknown
31+
case Unknown => Unknown
32+
33+
end Atoms

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

Lines changed: 62 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
4242

4343
private var needsGc = false
4444

45+
private var canCompareAtoms: Boolean = true // used for internal consistency checking
46+
4547
/** Is a subtype check in progress? In that case we may not
4648
* permanently instantiate type variables, because the corresponding
4749
* constraint might still be retracted and the instantiation should
@@ -418,6 +420,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
418420
if (tp11.stripTypeVar eq tp12.stripTypeVar) recur(tp11, tp2)
419421
else thirdTry
420422
case tp1 @ OrType(tp11, tp12) =>
423+
compareAtoms(tp1, tp2) match
424+
case Some(b) => return b
425+
case None =>
421426

422427
def joinOK = tp2.dealiasKeepRefiningAnnots match {
423428
case tp2: AppliedType if !tp2.tycon.typeSymbol.isClass =>
@@ -440,19 +445,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
440445
(tp1.widenSingletons ne tp1) &&
441446
recur(tp1.widenSingletons, tp2)
442447

443-
if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
444-
val atoms1 = tp1.atoms(widenOK = true)
445-
atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms())
446-
else
447-
widenOK
448-
|| joinOK
449-
|| recur(tp11, tp2) && recur(tp12, tp2)
450-
|| containsAnd(tp1) && recur(tp1.join, tp2)
451-
// An & on the left side loses information. Compensate by also trying the join.
452-
// This is less ad-hoc than it looks since we produce joins in type inference,
453-
// and then need to check that they are indeed supertypes of the original types
454-
// under -Ycheck. Test case is i7965.scala.
455-
448+
widenOK
449+
|| joinOK
450+
|| recur(tp11, tp2) && recur(tp12, tp2)
451+
|| containsAnd(tp1) && recur(tp1.join, tp2)
452+
// An & on the left side loses information. Compensate by also trying the join.
453+
// This is less ad-hoc than it looks since we produce joins in type inference,
454+
// and then need to check that they are indeed supertypes of the original types
455+
// under -Ycheck. Test case is i7965.scala.
456456
case tp1: MatchType =>
457457
val reduced = tp1.reduced
458458
if (reduced.exists) recur(reduced, tp2) else thirdTry
@@ -613,9 +613,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
613613
}
614614
compareTypeLambda
615615
case OrType(tp21, tp22) =>
616-
if (tp2.atoms().nonEmpty && canCompare(tp2.atoms()))
617-
val atoms1 = tp1.atoms(widenOK = true)
618-
return atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms()) || isSubType(tp1, NothingType)
616+
compareAtoms(tp1, tp2) match
617+
case Some(b) => return b
618+
case _ =>
619619

620620
// The next clause handles a situation like the one encountered in i2745.scala.
621621
// We have:
@@ -1172,22 +1172,48 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
11721172
else None
11731173
}
11741174

1175-
/** Check whether we can compare the given set of atoms with another to determine
1176-
* a subtype test between OrTypes. There is one situation where this is not
1177-
* the case, which has to do with SkolemTypes. TreeChecker sometimes expects two
1178-
* types to be equal that have different skolems. To account for this, we identify
1179-
* two different skolems in all phases `p`, where `p.isTyper` is false.
1180-
* But in that case comparing two sets of atoms that contain skolems
1181-
* for equality would give the wrong result, so we should not use the sets
1182-
* for comparisons.
1175+
/** If both `tp1` and `tp2` have atoms information, compare the atoms
1176+
* in a Some, otherwise None.
11831177
*/
1184-
def canCompare(atoms: Set[Type]): Boolean =
1185-
ctx.phase.isTyper || {
1178+
def compareAtoms(tp1: Type, tp2: Type): Option[Boolean] =
1179+
1180+
/** Check whether we can compare the given set of atoms with another to determine
1181+
* a subtype test between OrTypes. There is one situation where this is not
1182+
* the case, which has to do with SkolemTypes. TreeChecker sometimes expects two
1183+
* types to be equal that have different skolems. To account for this, we identify
1184+
* two different skolems in all phases `p`, where `p.isTyper` is false.
1185+
* But in that case comparing two sets of atoms that contain skolems
1186+
* for equality would give the wrong result, so we should not use the sets
1187+
* for comparisons.
1188+
*/
1189+
def canCompare(ts: Set[Type]) = ctx.phase.isTyper || {
11861190
val hasSkolems = new ExistsAccumulator(_.isInstanceOf[SkolemType]) {
11871191
override def stopAtStatic = true
11881192
}
1189-
!atoms.exists(hasSkolems(false, _))
1193+
!ts.exists(hasSkolems(false, _))
11901194
}
1195+
def verified(result: Boolean): Boolean =
1196+
if Config.checkAtomsComparisons then
1197+
try
1198+
canCompareAtoms = false
1199+
val regular = recur(tp1, tp2)
1200+
assert(result == regular,
1201+
i"""Atoms inconsistency for $tp1 <:< $tp2
1202+
|atoms predicted $result
1203+
|atoms1 = ${tp1.atoms}
1204+
|atoms2 = ${tp2.atoms}""")
1205+
finally canCompareAtoms = true
1206+
result
1207+
1208+
tp2.atoms match
1209+
case Atoms.Range(lo2, hi2) if canCompareAtoms && canCompare(hi2) =>
1210+
tp1.atoms match
1211+
case Atoms.Range(lo1, hi1) =>
1212+
if hi1.subsetOf(lo2) then Some(verified(true))
1213+
else if !lo1.subsetOf(hi2) then Some(verified(false))
1214+
else None
1215+
case _ => Some(verified(recur(tp1, NothingType)))
1216+
case _ => None
11911217

11921218
/** Subtype test for corresponding arguments in `args1`, `args2` according to
11931219
* variances in type parameters `tparams2`.
@@ -1787,15 +1813,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
17871813
else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp2
17881814
else
17891815
def mergedLub(tp1: Type, tp2: Type): Type = {
1790-
val atoms1 = tp1.atoms(widenOK = true)
1791-
if (atoms1.nonEmpty && !widenInUnions) {
1792-
val atoms2 = tp2.atoms(widenOK = true)
1793-
if (atoms2.nonEmpty) {
1794-
if (atoms1.subsetOf(atoms2)) return tp2
1795-
if (atoms2.subsetOf(atoms1)) return tp1
1796-
if ((atoms1 & atoms2).isEmpty) return orType(tp1, tp2)
1797-
}
1798-
}
1816+
tp1.atoms match
1817+
case Atoms.Range(lo1, hi1) if !widenInUnions =>
1818+
tp2.atoms match
1819+
case Atoms.Range(lo2, hi2) =>
1820+
if hi1.subsetOf(lo2) then return tp2
1821+
if hi2.subsetOf(lo1) then return tp1
1822+
if (hi1 & hi2).isEmpty then return orType(tp1, tp2)
1823+
case none =>
1824+
case none =>
17991825
val t1 = mergeIfSuper(tp1, tp2, canConstrain)
18001826
if (t1.exists) return t1
18011827

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

Lines changed: 27 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1167,35 +1167,37 @@ object Types {
11671167
this
11681168
}
11691169

1170-
/** If this type is an alias of a disjunction of stable singleton types,
1171-
* these types as a set, otherwise the empty set.
1170+
/** The singleton types that must or may be in this type. @see Atoms.
11721171
* Overridden and cached in OrType.
1173-
* @param widenOK If type proxies that are upperbounded by types with atoms
1174-
* have the same atoms.
11751172
*/
1176-
def atoms(widenOK: Boolean = false)(implicit ctx: Context): Set[Type] = dealias match {
1173+
def atoms(using Context): Atoms = dealias match
11771174
case tp: SingletonType =>
1178-
def normalize(tp: Type): Type = tp match {
1175+
def normalize(tp: Type): Type = tp match
11791176
case tp: SingletonType =>
1180-
tp.underlying.dealias match {
1177+
tp.underlying.dealias match
11811178
case tp1: SingletonType => normalize(tp1)
11821179
case _ =>
1183-
tp match {
1180+
tp match
11841181
case tp: TermRef => tp.derivedSelect(normalize(tp.prefix))
11851182
case _ => tp
1186-
}
1187-
}
11881183
case _ => tp
1189-
}
1190-
val underlyingAtoms = tp.underlying.atoms(widenOK)
1191-
if (underlyingAtoms.isEmpty && tp.isStable) Set.empty + normalize(tp)
1192-
else underlyingAtoms
1193-
case tp: ExprType => tp.resType.atoms(widenOK)
1194-
case tp: OrType => tp.atoms(widenOK) // `atoms` overridden in OrType
1195-
case tp: AndType => tp.tp1.atoms(widenOK) & tp.tp2.atoms(widenOK)
1196-
case tp: TypeProxy if widenOK => tp.underlying.atoms(widenOK)
1197-
case _ => Set.empty
1198-
}
1184+
tp.underlying.atoms match
1185+
case as @ Atoms.Range(lo, hi) =>
1186+
if hi.size == 1 then as // if there's just one atom, there's no uncertainty which one it is
1187+
else Atoms.Range(Set.empty, hi)
1188+
case Atoms.Unknown =>
1189+
if tp.isStable then
1190+
val single = Set.empty + normalize(tp)
1191+
Atoms.Range(single, single)
1192+
else Atoms.Unknown
1193+
case tp: ExprType => tp.resType.atoms
1194+
case tp: OrType => tp.atoms // `atoms` overridden in OrType
1195+
case tp: AndType => tp.tp1.atoms & tp.tp2.atoms
1196+
case tp: TypeProxy =>
1197+
tp.underlying.atoms match
1198+
case Atoms.Range(_, hi) => Atoms.Range(Set.empty, hi)
1199+
case Atoms.Unknown => Atoms.Unknown
1200+
case _ => Atoms.Unknown
11991201

12001202
private def dealias1(keep: AnnotatedType => Context => Boolean)(implicit ctx: Context): Type = this match {
12011203
case tp: TypeRef =>
@@ -2919,28 +2921,20 @@ object Types {
29192921
}
29202922

29212923
private var atomsRunId: RunId = NoRunId
2922-
private var myAtoms: Set[Type] = _
2923-
private var myWidenedAtoms: Set[Type] = _
2924+
private var myAtoms: Atoms = _
29242925
private var myWidened: Type = _
29252926

29262927
private def ensureAtomsComputed()(implicit ctx: Context): Unit =
2927-
if (atomsRunId != ctx.runId) {
2928-
val atoms1 = tp1.atoms()
2929-
val atoms2 = tp2.atoms()
2930-
myAtoms = if (atoms1.nonEmpty && atoms2.nonEmpty) atoms1 | atoms2 else Set.empty
2931-
val widenedAtoms1 = tp1.atoms(widenOK = true)
2932-
val widenedAtoms2 = tp2.atoms(widenOK = true)
2933-
myWidenedAtoms = if (widenedAtoms1.nonEmpty && widenedAtoms2.nonEmpty) widenedAtoms1 | widenedAtoms2 else Set.empty
2928+
if atomsRunId != ctx.runId then
2929+
myAtoms = tp1.atoms | tp2.atoms
29342930
val tp1w = tp1.widenSingletons
29352931
val tp2w = tp2.widenSingletons
29362932
myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
29372933
atomsRunId = ctx.runId
2938-
}
29392934

2940-
override def atoms(widenOK: Boolean)(implicit ctx: Context): Set[Type] = {
2935+
override def atoms(using Context): Atoms =
29412936
ensureAtomsComputed()
2942-
if widenOK then myAtoms else myWidenedAtoms
2943-
}
2937+
myAtoms
29442938

29452939
override def widenSingletons(implicit ctx: Context): Type = {
29462940
ensureAtomsComputed()

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -146,7 +146,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
146146
else
147147
toTextPrefix(tp.prefix) ~ selectionString(tp)
148148
case tp: TermParamRef =>
149-
ParamRefNameString(tp) ~ ".type"
149+
ParamRefNameString(tp) ~ lambdaHash(tp.binder) ~ ".type"
150150
case tp: TypeParamRef =>
151151
ParamRefNameString(tp) ~ lambdaHash(tp.binder)
152152
case tp: SingletonType =>
@@ -237,9 +237,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
237237
def toTextSingleton(tp: SingletonType): Text =
238238
"(" ~ toTextRef(tp) ~ " : " ~ toTextGlobal(tp.underlying) ~ ")"
239239

240-
protected def paramsText(tp: LambdaType): Text = {
241-
def paramText(name: Name, tp: Type) = toText(name) ~ toTextRHS(tp)
242-
Text(tp.paramNames.lazyZip(tp.paramInfos).map(paramText), ", ")
240+
protected def paramsText(lam: LambdaType): Text = {
241+
def paramText(name: Name, tp: Type) =
242+
toText(name) ~ lambdaHash(lam) ~ toTextRHS(tp)
243+
Text(lam.paramNames.lazyZip(lam.paramInfos).map(paramText), ", ")
243244
}
244245

245246
protected def ParamRefNameString(name: Name): String = name.toString

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -212,7 +212,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
212212
toTextInfixType(tpnme.raw.BAR, tp1, tp2) { toText(tpnme.raw.BAR) }
213213
case EtaExpansion(tycon) if !printDebug =>
214214
toText(tycon)
215-
case tp: RefinedType if defn.isFunctionType(tp) =>
215+
case tp: RefinedType if defn.isFunctionType(tp) && !printDebug =>
216216
toTextDependentFunction(tp.refinedInfo.asInstanceOf[MethodType])
217217
case tp: TypeRef =>
218218
if (tp.symbol.isAnonymousClass && !ctx.settings.uniqid.value)

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

Lines changed: 10 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -932,27 +932,21 @@ class Typer extends Namer
932932
isContextual = funFlags.is(Given), isErased = funFlags.is(Erased))
933933

934934
/** Typechecks dependent function type with given parameters `params` */
935-
def typedDependent(params: List[ValDef])(implicit ctx: Context): Tree = {
936-
completeParams(params)
937-
val params1 = params.map(typedExpr(_).asInstanceOf[ValDef])
938-
if (!funFlags.isEmpty)
939-
params1.foreach(_.symbol.setFlag(funFlags))
940-
val resultTpt = typed(body)
941-
val companion = MethodType.companion(
942-
isContextual = funFlags.is(Given), isErased = funFlags.is(Erased))
943-
val mt = companion.fromSymbols(params1.map(_.symbol), resultTpt.tpe)
935+
def typedDependent(params: List[ValDef])(implicit ctx: Context): Tree =
936+
val params1 =
937+
if funFlags.is(Given) then params.map(_.withAddedFlags(Given))
938+
else params
939+
val appDef0 = untpd.DefDef(nme.apply, Nil, List(params1), body, EmptyTree).withSpan(tree.span)
940+
index(appDef0 :: Nil)
941+
val appDef = typed(appDef0).asInstanceOf[DefDef]
942+
val mt = appDef.symbol.info.asInstanceOf[MethodType]
944943
if (mt.isParamDependent)
945944
ctx.error(i"$mt is an illegal function type because it has inter-parameter dependencies", tree.sourcePos)
946945
val resTpt = TypeTree(mt.nonDependentResultApprox).withSpan(body.span)
947-
val typeArgs = params1.map(_.tpt) :+ resTpt
946+
val typeArgs = appDef.vparamss.head.map(_.tpt) :+ resTpt
948947
val tycon = TypeTree(funCls.typeRef)
949-
val core = assignType(cpy.AppliedTypeTree(tree)(tycon, typeArgs), tycon, typeArgs)
950-
val appMeth = ctx.newSymbol(ctx.owner, nme.apply, Synthetic | Method | Deferred, mt, coord = body.span)
951-
val appDef = assignType(
952-
untpd.DefDef(appMeth.name, Nil, List(params1), resultTpt, EmptyTree),
953-
appMeth).withSpan(body.span)
948+
val core = AppliedTypeTree(tycon, typeArgs)
954949
RefinedTypeTree(core, List(appDef), ctx.owner.asClass)
955-
}
956950

957951
args match {
958952
case ValDef(_, _, _) :: _ =>

tests/pos/i8128.scala

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
object Test {
2+
def id: (x: 1 | 0) => x.type = x => x
3+
id(0): 0 // ok
4+
5+
def id2: Function1[1 | 0, 1 | 0] {
6+
def apply(x: 1 | 0): x.type
7+
} = ???
8+
id2(0): 0 // ok
9+
10+
def id3: Function1[1 | 0, Int] {
11+
def apply(x: 1 | 0): x.type
12+
} = ???
13+
id3(0): 0 // ok
14+
15+
var x: 0 = 0
16+
var y: (1 & 0) | 0 = 0
17+
x = y
18+
y = x
19+
}

0 commit comments

Comments
 (0)