-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Fix #8128: Fix atoms computations #8139
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
Changes from all commits
b2646d5
6f5e760
898bc84
53df90a
ce9cd39
d2b01d0
8a5ca00
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
package dotty.tools | ||
package dotc | ||
package core | ||
|
||
import Types._ | ||
|
||
/** Indicates the singleton types that a type must or may consist of. | ||
* @param lo The lower bound: singleton types in this set are guaranteed | ||
* to be in the carrier type. | ||
* @param hi The upper bound: all singleton types in the carrier type are | ||
* guaranteed to be in this set | ||
* If the underlying type of a singleton type is another singleton type, | ||
* only the latter type ends up in the sets. | ||
*/ | ||
enum Atoms: | ||
case Range(lo: Set[Type], hi: Set[Type]) | ||
case Unknown | ||
|
||
def & (that: Atoms): Atoms = this match | ||
case Range(lo1, hi1) => | ||
that match | ||
case Range(lo2, hi2) => Range(lo1 & lo2, hi1 & hi2) | ||
case Unknown => this | ||
case Unknown => that | ||
|
||
def | (that: Atoms): Atoms = this match | ||
case Range(lo1, hi1) => | ||
that match | ||
case Range(lo2, hi2) => Range(lo1 | lo2, hi1 | hi2) | ||
case Unknown => Unknown | ||
case Unknown => Unknown | ||
|
||
end Atoms |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -42,6 +42,8 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
|
||
private var needsGc = false | ||
|
||
private var canCompareAtoms: Boolean = true // used for internal consistency checking | ||
|
||
/** Is a subtype check in progress? In that case we may not | ||
* permanently instantiate type variables, because the corresponding | ||
* constraint might still be retracted and the instantiation should | ||
|
@@ -418,6 +420,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
if (tp11.stripTypeVar eq tp12.stripTypeVar) recur(tp11, tp2) | ||
else thirdTry | ||
case tp1 @ OrType(tp11, tp12) => | ||
compareAtoms(tp1, tp2) match | ||
case Some(b) => return b | ||
case None => | ||
|
||
def joinOK = tp2.dealiasKeepRefiningAnnots match { | ||
case tp2: AppliedType if !tp2.tycon.typeSymbol.isClass => | ||
|
@@ -440,19 +445,14 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
(tp1.widenSingletons ne tp1) && | ||
recur(tp1.widenSingletons, tp2) | ||
|
||
if (tp2.atoms().nonEmpty && canCompare(tp2.atoms())) | ||
val atoms1 = tp1.atoms(widenOK = true) | ||
atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms()) | ||
else | ||
widenOK | ||
|| joinOK | ||
|| recur(tp11, tp2) && recur(tp12, tp2) | ||
|| containsAnd(tp1) && recur(tp1.join, tp2) | ||
// An & on the left side loses information. Compensate by also trying the join. | ||
// This is less ad-hoc than it looks since we produce joins in type inference, | ||
// and then need to check that they are indeed supertypes of the original types | ||
// under -Ycheck. Test case is i7965.scala. | ||
|
||
widenOK | ||
|| joinOK | ||
|| recur(tp11, tp2) && recur(tp12, tp2) | ||
|| containsAnd(tp1) && recur(tp1.join, tp2) | ||
// An & on the left side loses information. Compensate by also trying the join. | ||
// This is less ad-hoc than it looks since we produce joins in type inference, | ||
// and then need to check that they are indeed supertypes of the original types | ||
// under -Ycheck. Test case is i7965.scala. | ||
case tp1: MatchType => | ||
val reduced = tp1.reduced | ||
if (reduced.exists) recur(reduced, tp2) else thirdTry | ||
|
@@ -613,9 +613,9 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
} | ||
compareTypeLambda | ||
case OrType(tp21, tp22) => | ||
if (tp2.atoms().nonEmpty && canCompare(tp2.atoms())) | ||
val atoms1 = tp1.atoms(widenOK = true) | ||
return atoms1.nonEmpty && atoms1.subsetOf(tp2.atoms()) || isSubType(tp1, NothingType) | ||
compareAtoms(tp1, tp2) match | ||
case Some(b) => return b | ||
case _ => | ||
|
||
// The next clause handles a situation like the one encountered in i2745.scala. | ||
// We have: | ||
|
@@ -1172,22 +1172,48 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
else None | ||
} | ||
|
||
/** Check whether we can compare the given set of atoms with another to determine | ||
* a subtype test between OrTypes. There is one situation where this is not | ||
* the case, which has to do with SkolemTypes. TreeChecker sometimes expects two | ||
* types to be equal that have different skolems. To account for this, we identify | ||
* two different skolems in all phases `p`, where `p.isTyper` is false. | ||
* But in that case comparing two sets of atoms that contain skolems | ||
* for equality would give the wrong result, so we should not use the sets | ||
* for comparisons. | ||
/** If both `tp1` and `tp2` have atoms information, compare the atoms | ||
* in a Some, otherwise None. | ||
*/ | ||
def canCompare(atoms: Set[Type]): Boolean = | ||
ctx.phase.isTyper || { | ||
def compareAtoms(tp1: Type, tp2: Type): Option[Boolean] = | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The use of an Option here might noticeably increase our allocation rate, a tri-state enum could be used instead. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I don't think so, since the overwhelming majority of calls should give |
||
|
||
/** Check whether we can compare the given set of atoms with another to determine | ||
* a subtype test between OrTypes. There is one situation where this is not | ||
* the case, which has to do with SkolemTypes. TreeChecker sometimes expects two | ||
* types to be equal that have different skolems. To account for this, we identify | ||
* two different skolems in all phases `p`, where `p.isTyper` is false. | ||
* But in that case comparing two sets of atoms that contain skolems | ||
* for equality would give the wrong result, so we should not use the sets | ||
* for comparisons. | ||
*/ | ||
def canCompare(ts: Set[Type]) = ctx.phase.isTyper || { | ||
val hasSkolems = new ExistsAccumulator(_.isInstanceOf[SkolemType]) { | ||
override def stopAtStatic = true | ||
} | ||
!atoms.exists(hasSkolems(false, _)) | ||
!ts.exists(hasSkolems(false, _)) | ||
} | ||
def verified(result: Boolean): Boolean = | ||
if Config.checkAtomsComparisons then | ||
try | ||
canCompareAtoms = false | ||
val regular = recur(tp1, tp2) | ||
assert(result == regular, | ||
i"""Atoms inconsistency for $tp1 <:< $tp2 | ||
|atoms predicted $result | ||
|atoms1 = ${tp1.atoms} | ||
|atoms2 = ${tp2.atoms}""") | ||
finally canCompareAtoms = true | ||
result | ||
|
||
tp2.atoms match | ||
case Atoms.Range(lo2, hi2) if canCompareAtoms && canCompare(hi2) => | ||
tp1.atoms match | ||
case Atoms.Range(lo1, hi1) => | ||
if hi1.subsetOf(lo2) then Some(verified(true)) | ||
else if !lo1.subsetOf(hi2) then Some(verified(false)) | ||
else None | ||
case _ => Some(verified(recur(tp1, NothingType))) | ||
case _ => None | ||
|
||
/** Subtype test for corresponding arguments in `args1`, `args2` according to | ||
* variances in type parameters `tparams2`. | ||
|
@@ -1787,15 +1813,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w | |
else if tp2.isAny && !tp1.isLambdaSub || tp2.isAnyKind || tp1.isRef(NothingClass) then tp2 | ||
else | ||
def mergedLub(tp1: Type, tp2: Type): Type = { | ||
val atoms1 = tp1.atoms(widenOK = true) | ||
if (atoms1.nonEmpty && !widenInUnions) { | ||
val atoms2 = tp2.atoms(widenOK = true) | ||
if (atoms2.nonEmpty) { | ||
if (atoms1.subsetOf(atoms2)) return tp2 | ||
if (atoms2.subsetOf(atoms1)) return tp1 | ||
if ((atoms1 & atoms2).isEmpty) return orType(tp1, tp2) | ||
} | ||
} | ||
tp1.atoms match | ||
case Atoms.Range(lo1, hi1) if !widenInUnions => | ||
tp2.atoms match | ||
case Atoms.Range(lo2, hi2) => | ||
if hi1.subsetOf(lo2) then return tp2 | ||
if hi2.subsetOf(lo1) then return tp1 | ||
if (hi1 & hi2).isEmpty then return orType(tp1, tp2) | ||
case none => | ||
case none => | ||
val t1 = mergeIfSuper(tp1, tp2, canConstrain) | ||
if (t1.exists) return t1 | ||
|
||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
object Test { | ||
def id: (x: 1 | 0) => x.type = x => x | ||
id(0): 0 // ok | ||
|
||
def id2: Function1[1 | 0, 1 | 0] { | ||
def apply(x: 1 | 0): x.type | ||
} = ??? | ||
id2(0): 0 // ok | ||
|
||
def id3: Function1[1 | 0, Int] { | ||
def apply(x: 1 | 0): x.type | ||
} = ??? | ||
id3(0): 0 // ok | ||
|
||
var x: 0 = 0 | ||
var y: (1 & 0) | 0 = 0 | ||
x = y | ||
y = x | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The comment above applies to the
canCompare
method so it should be moved down.