Skip to content

Commit ce9cd39

Browse files
oderskyodersky
committed
Make atoms ranges
Fixes #8128
1 parent 53df90a commit ce9cd39

File tree

5 files changed

+115
-66
lines changed

5 files changed

+115
-66
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

‎compiler/src/dotty/tools/dotc/core/Atoms.scala‎

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: 50 additions & 32 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,21 +445,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
440445
(tp1.widenSingletons ne tp1) &&
441446
recur(tp1.widenSingletons, tp2)
442447

443-
tp2.atoms() match
444-
case Some(ts2) if canCompare(ts2) =>
445-
tp1.atoms(widenOK = true) match
446-
case Some(ts1) => ts1.subsetOf(ts2)
447-
case none => false
448-
case _ =>
449-
widenOK
450-
|| joinOK
451-
|| recur(tp11, tp2) && recur(tp12, tp2)
452-
|| containsAnd(tp1) && recur(tp1.join, tp2)
453-
// An & on the left side loses information. Compensate by also trying the join.
454-
// This is less ad-hoc than it looks since we produce joins in type inference,
455-
// and then need to check that they are indeed supertypes of the original types
456-
// under -Ycheck. Test case is i7965.scala.
457-
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.
458456
case tp1: MatchType =>
459457
val reduced = tp1.reduced
460458
if (reduced.exists) recur(reduced, tp2) else thirdTry
@@ -615,13 +613,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
615613
}
616614
compareTypeLambda
617615
case OrType(tp21, tp22) =>
618-
tp2.atoms() match
619-
case Some(ts2) if canCompare(ts2) =>
620-
val atomsFit = tp1.atoms(widenOK = true) match
621-
case Some(ts1) => ts1.subsetOf(ts2)
622-
case none => false
623-
return atomsFit || isSubType(tp1, NothingType)
624-
case none =>
616+
compareAtoms(tp1, tp2) match
617+
case Some(b) => return b
618+
case _ =>
625619

626620
// The next clause handles a situation like the one encountered in i2745.scala.
627621
// We have:
@@ -1187,13 +1181,37 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
11871181
* for equality would give the wrong result, so we should not use the sets
11881182
* for comparisons.
11891183
*/
1190-
def canCompare(atoms: Set[Type]): Boolean =
1191-
ctx.phase.isTyper || {
1184+
def compareAtoms(tp1: Type, tp2: Type): Option[Boolean] =
1185+
def canCompare(ts: Set[Type]) = ctx.phase.isTyper || {
11921186
val hasSkolems = new ExistsAccumulator(_.isInstanceOf[SkolemType]) {
11931187
override def stopAtStatic = true
11941188
}
1195-
!atoms.exists(hasSkolems(false, _))
1189+
!ts.exists(hasSkolems(false, _))
11961190
}
1191+
def verified(result: Boolean): Boolean =
1192+
if Config.checkAtomsComparisons && false then
1193+
try
1194+
canCompareAtoms = false
1195+
val regular = recur(tp1, tp2)
1196+
assert(result == regular,
1197+
i"""Atoms inconsistency for $tp1 <:< $tp2
1198+
|atoms predicted $result
1199+
|atoms1 = ${tp1.atoms}
1200+
|atoms2 = ${tp2.atoms}""")
1201+
finally canCompareAtoms = true
1202+
result
1203+
1204+
def falseUnlessBottom = Some(verified(recur(tp1, NothingType)))
1205+
1206+
tp2.atoms match
1207+
case Atoms.Range(lo2, hi2) if canCompareAtoms && canCompare(hi2) =>
1208+
tp1.atoms match
1209+
case Atoms.Range(lo1, hi1) =>
1210+
if hi1.subsetOf(lo2) then Some(verified(true))
1211+
else if !lo1.subsetOf(hi2) then falseUnlessBottom
1212+
else None
1213+
case _ => falseUnlessBottom
1214+
case _ => None
11971215

11981216
/** Subtype test for corresponding arguments in `args1`, `args2` according to
11991217
* variances in type parameters `tparams2`.
@@ -1793,13 +1811,13 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
17931811
else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp2
17941812
else
17951813
def mergedLub(tp1: Type, tp2: Type): Type = {
1796-
tp1.atoms(widenOK = true) match
1797-
case Some(ts1) if !widenInUnions =>
1798-
tp2.atoms(widenOK = true) match
1799-
case Some(ts2) =>
1800-
if ts1.subsetOf(ts2) then return tp2
1801-
if ts2.subsetOf(ts1) then return tp1
1802-
if (ts1 & ts2).isEmpty then return orType(tp1, tp2)
1814+
tp1.atoms match
1815+
case Atoms.Range(lo1, hi1) if !widenInUnions =>
1816+
tp2.atoms match
1817+
case Atoms.Range(lo2, hi2) =>
1818+
if hi1.subsetOf(lo2) then return tp2
1819+
if hi2.subsetOf(lo1) then return tp1
1820+
if (hi1 & hi2).isEmpty then return orType(tp1, tp2)
18031821
case none =>
18041822
case none =>
18051823
val t1 = mergeIfSuper(tp1, tp2, canConstrain)

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

Lines changed: 25 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -1167,38 +1167,36 @@ 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): Option[Set[Type]] =
1177-
dealias match
1173+
def atoms(using Context): Atoms = dealias match
11781174
case tp: SingletonType =>
1179-
def normalize(tp: Type): Type = tp match {
1175+
def normalize(tp: Type): Type = tp match
11801176
case tp: SingletonType =>
1181-
tp.underlying.dealias match {
1177+
tp.underlying.dealias match
11821178
case tp1: SingletonType => normalize(tp1)
11831179
case _ =>
1184-
tp match {
1180+
tp match
11851181
case tp: TermRef => tp.derivedSelect(normalize(tp.prefix))
11861182
case _ => tp
1187-
}
1188-
}
11891183
case _ => tp
1190-
}
1191-
tp.underlying.atoms(widenOK) match
1192-
case None if tp.isStable => Some(Set.empty + normalize(tp))
1193-
case s @ Some(ts) if ts.size == 1 || widenOK => s
1194-
case _ => None
1195-
case tp: ExprType => tp.resType.atoms(widenOK)
1196-
case tp: OrType => tp.atoms(widenOK) // `atoms` overridden in OrType
1197-
case tp: AndType =>
1198-
for ts1 <- tp.tp1.atoms(widenOK); ts2 <- tp.tp2.atoms(widenOK)
1199-
yield ts1 & ts2
1200-
case tp: TypeProxy if widenOK => tp.underlying.atoms(widenOK)
1201-
case _ => None
1184+
tp.underlying.atoms match
1185+
case as @ Atoms.Range(lo, hi) =>
1186+
if hi.size == 1 then as else Atoms.Range(Set.empty, hi)
1187+
case Atoms.Unknown =>
1188+
if tp.isStable then
1189+
val single = Set.empty + normalize(tp)
1190+
Atoms.Range(single, single)
1191+
else Atoms.Unknown
1192+
case tp: ExprType => tp.resType.atoms
1193+
case tp: OrType => tp.atoms // `atoms` overridden in OrType
1194+
case tp: AndType => tp.tp1.atoms & tp.tp2.atoms
1195+
case tp: TypeProxy =>
1196+
tp.underlying.atoms match
1197+
case Atoms.Range(_, hi) => Atoms.Range(Set.empty, hi)
1198+
case Atoms.Unknown => Atoms.Unknown
1199+
case _ => Atoms.Unknown
12021200

12031201
private def dealias1(keep: AnnotatedType => Context => Boolean)(implicit ctx: Context): Type = this match {
12041202
case tp: TypeRef =>
@@ -2922,26 +2920,20 @@ object Types {
29222920
}
29232921

29242922
private var atomsRunId: RunId = NoRunId
2925-
private var myAtoms: Option[Set[Type]] = _
2926-
private var myWidenedAtoms: Option[Set[Type]] = _
2923+
private var myAtoms: Atoms = _
29272924
private var myWidened: Type = _
29282925

29292926
private def ensureAtomsComputed()(implicit ctx: Context): Unit =
29302927
if atomsRunId != ctx.runId then
2931-
myAtoms =
2932-
for ts1 <- tp1.atoms(); ts2 <- tp2.atoms()
2933-
yield ts1 | ts2
2934-
myWidenedAtoms =
2935-
for ts1 <- tp1.atoms(widenOK = true); ts2 <- tp2.atoms(widenOK = true)
2936-
yield ts1 | ts2
2928+
myAtoms = tp1.atoms | tp2.atoms
29372929
val tp1w = tp1.widenSingletons
29382930
val tp2w = tp2.widenSingletons
29392931
myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
29402932
atomsRunId = ctx.runId
29412933

2942-
override def atoms(widenOK: Boolean)(implicit ctx: Context): Option[Set[Type]] =
2934+
override def atoms(using Context): Atoms =
29432935
ensureAtomsComputed()
2944-
if widenOK then myAtoms else myWidenedAtoms
2936+
myAtoms
29452937

29462938
override def widenSingletons(implicit ctx: Context): Type = {
29472939
ensureAtomsComputed()

‎tests/pos/i8128.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
object Test {
2-
def id: (x: 1 | 0) => x.type = ??? // x => x does not work yet
2+
def id: (x: 1 | 0) => x.type = x => x
33
id(0): 0 // ok
44

55
def id2: Function1[1 | 0, 1 | 0] {

0 commit comments

Comments
 (0)