Skip to content

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

Merged
merged 7 commits into from
Mar 1, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
6 changes: 6 additions & 0 deletions compiler/src/dotty/tools/dotc/config/Config.scala
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,12 @@ object Config {
*/
final val checkUnerased = false

/** Check that atoms-based comparisons match regular comparisons that do not
* take atoms into account. The two have to give the same results, since
* atoms comparison is intended to be just an optimization.
*/
final val checkAtomsComparisons = false

/** In `derivedSelect`, rewrite
*
* (S & T)#A --> S#A & T#A
Expand Down
33 changes: 33 additions & 0 deletions compiler/src/dotty/tools/dotc/core/Atoms.scala
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
98 changes: 62 additions & 36 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =>
Expand All @@ -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
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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.
*/
Copy link
Member

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.

def canCompare(atoms: Set[Type]): Boolean =
ctx.phase.isTyper || {
def compareAtoms(tp1: Type, tp2: Type): Option[Boolean] =
Copy link
Member

Choose a reason for hiding this comment

The 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.

Copy link
Contributor Author

Choose a reason for hiding this comment

The 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 None. You get a Some only if both compared sides are consist of atoms.


/** 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`.
Expand Down Expand Up @@ -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

Expand Down
60 changes: 27 additions & 33 deletions compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1167,35 +1167,37 @@ object Types {
this
}

/** If this type is an alias of a disjunction of stable singleton types,
* these types as a set, otherwise the empty set.
/** The singleton types that must or may be in this type. @see Atoms.
* Overridden and cached in OrType.
* @param widenOK If type proxies that are upperbounded by types with atoms
* have the same atoms.
*/
def atoms(widenOK: Boolean = false)(implicit ctx: Context): Set[Type] = dealias match {
def atoms(using Context): Atoms = dealias match
case tp: SingletonType =>
def normalize(tp: Type): Type = tp match {
def normalize(tp: Type): Type = tp match
case tp: SingletonType =>
tp.underlying.dealias match {
tp.underlying.dealias match
case tp1: SingletonType => normalize(tp1)
case _ =>
tp match {
tp match
case tp: TermRef => tp.derivedSelect(normalize(tp.prefix))
case _ => tp
}
}
case _ => tp
}
val underlyingAtoms = tp.underlying.atoms(widenOK)
if (underlyingAtoms.isEmpty && tp.isStable) Set.empty + normalize(tp)
else underlyingAtoms
case tp: ExprType => tp.resType.atoms(widenOK)
case tp: OrType => tp.atoms(widenOK) // `atoms` overridden in OrType
case tp: AndType => tp.tp1.atoms(widenOK) & tp.tp2.atoms(widenOK)
case tp: TypeProxy if widenOK => tp.underlying.atoms(widenOK)
case _ => Set.empty
}
tp.underlying.atoms match
case as @ Atoms.Range(lo, hi) =>
if hi.size == 1 then as // if there's just one atom, there's no uncertainty which one it is
else Atoms.Range(Set.empty, hi)
case Atoms.Unknown =>
if tp.isStable then
val single = Set.empty + normalize(tp)
Atoms.Range(single, single)
else Atoms.Unknown
case tp: ExprType => tp.resType.atoms
case tp: OrType => tp.atoms // `atoms` overridden in OrType
case tp: AndType => tp.tp1.atoms & tp.tp2.atoms
case tp: TypeProxy =>
tp.underlying.atoms match
case Atoms.Range(_, hi) => Atoms.Range(Set.empty, hi)
case Atoms.Unknown => Atoms.Unknown
case _ => Atoms.Unknown

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

private var atomsRunId: RunId = NoRunId
private var myAtoms: Set[Type] = _
private var myWidenedAtoms: Set[Type] = _
private var myAtoms: Atoms = _
private var myWidened: Type = _

private def ensureAtomsComputed()(implicit ctx: Context): Unit =
if (atomsRunId != ctx.runId) {
val atoms1 = tp1.atoms()
val atoms2 = tp2.atoms()
myAtoms = if (atoms1.nonEmpty && atoms2.nonEmpty) atoms1 | atoms2 else Set.empty
val widenedAtoms1 = tp1.atoms(widenOK = true)
val widenedAtoms2 = tp2.atoms(widenOK = true)
myWidenedAtoms = if (widenedAtoms1.nonEmpty && widenedAtoms2.nonEmpty) widenedAtoms1 | widenedAtoms2 else Set.empty
if atomsRunId != ctx.runId then
myAtoms = tp1.atoms | tp2.atoms
val tp1w = tp1.widenSingletons
val tp2w = tp2.widenSingletons
myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
atomsRunId = ctx.runId
}

override def atoms(widenOK: Boolean)(implicit ctx: Context): Set[Type] = {
override def atoms(using Context): Atoms =
ensureAtomsComputed()
if widenOK then myAtoms else myWidenedAtoms
}
myAtoms

override def widenSingletons(implicit ctx: Context): Type = {
ensureAtomsComputed()
Expand Down
9 changes: 5 additions & 4 deletions compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -146,7 +146,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
else
toTextPrefix(tp.prefix) ~ selectionString(tp)
case tp: TermParamRef =>
ParamRefNameString(tp) ~ ".type"
ParamRefNameString(tp) ~ lambdaHash(tp.binder) ~ ".type"
case tp: TypeParamRef =>
ParamRefNameString(tp) ~ lambdaHash(tp.binder)
case tp: SingletonType =>
Expand Down Expand Up @@ -237,9 +237,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
def toTextSingleton(tp: SingletonType): Text =
"(" ~ toTextRef(tp) ~ " : " ~ toTextGlobal(tp.underlying) ~ ")"

protected def paramsText(tp: LambdaType): Text = {
def paramText(name: Name, tp: Type) = toText(name) ~ toTextRHS(tp)
Text(tp.paramNames.lazyZip(tp.paramInfos).map(paramText), ", ")
protected def paramsText(lam: LambdaType): Text = {
def paramText(name: Name, tp: Type) =
toText(name) ~ lambdaHash(lam) ~ toTextRHS(tp)
Text(lam.paramNames.lazyZip(lam.paramInfos).map(paramText), ", ")
}

protected def ParamRefNameString(name: Name): String = name.toString
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +212,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
toTextInfixType(tpnme.raw.BAR, tp1, tp2) { toText(tpnme.raw.BAR) }
case EtaExpansion(tycon) if !printDebug =>
toText(tycon)
case tp: RefinedType if defn.isFunctionType(tp) =>
case tp: RefinedType if defn.isFunctionType(tp) && !printDebug =>
toTextDependentFunction(tp.refinedInfo.asInstanceOf[MethodType])
case tp: TypeRef =>
if (tp.symbol.isAnonymousClass && !ctx.settings.uniqid.value)
Expand Down
26 changes: 10 additions & 16 deletions compiler/src/dotty/tools/dotc/typer/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -926,27 +926,21 @@ class Typer extends Namer
isContextual = funFlags.is(Given), isErased = funFlags.is(Erased))

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

args match {
case ValDef(_, _, _) :: _ =>
Expand Down
19 changes: 19 additions & 0 deletions tests/pos/i8128.scala
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
}