Skip to content

Improve handling of disjunctions when comparing types #11083

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 3 commits into from
Jan 18, 2021
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
16 changes: 6 additions & 10 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,9 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
try op finally frozenGadt = savedFrozenGadt
}

private inline def inFrozenGadtAndConstraint[T](inline op: T): T =
inFrozenGadtIf(true)(inFrozenConstraint(op))

protected def isSubType(tp1: Type, tp2: Type, a: ApproxState): Boolean = {
val savedApprox = approx
val savedLeftRoot = leftRoot
Expand Down Expand Up @@ -431,25 +434,18 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case Some(b) => return b
case None =>

/** `recur` shouldn't normally be used with approximated types, according to its
* documentation. In the specific examples where this function is
* called, it is sound to do so as long as we freeze GADTs.
*/
def recurInFrozenGadt(tp1: Type, tp2: Type) =
inFrozenGadt { recur(tp1, tp2) }

def widenOK =
(tp2.widenSingletons eq tp2)
&& (tp1.widenSingletons ne tp1)
&& recurInFrozenGadt(tp1.widenSingletons, tp2)
&& inFrozenGadtAndConstraint(recur(tp1.widenSingletons, tp2))

def joinOK = tp2.dealiasKeepRefiningAnnots match {
case tp2: AppliedType if !tp2.tycon.typeSymbol.isClass =>
// If we apply the default algorithm for `A[X] | B[Y] <: C[Z]` where `C` is a
// type parameter, we will instantiate `C` to `A` and then fail when comparing
// with `B[Y]`. To do the right thing, we need to instantiate `C` to the
// common superclass of `A` and `B`.
recurInFrozenGadt(tp1.join, tp2)
inFrozenGadtAndConstraint(recur(tp1.join, tp2))
case _ =>
false
}
Expand All @@ -476,7 +472,7 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
widenOK
|| joinOK
|| (tp1.isSoft || constrainRHSVars(tp2)) && recur(tp11, tp2) && recur(tp12, tp2)
|| containsAnd(tp1) && recurInFrozenGadt(tp1.join, tp2)
|| containsAnd(tp1) && inFrozenGadt(recur(tp1.join, tp2))
case tp1: MatchType =>
val reduced = tp1.reduced
if (reduced.exists) recur(reduced, tp2) else thirdTry
Expand Down
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3104,7 +3104,10 @@ object Types {

private def ensureAtomsComputed()(using Context): Unit =
if atomsRunId != ctx.runId then
myAtoms = tp1.atoms | tp2.atoms
myAtoms =
if tp1.hasClassSymbol(defn.NothingClass) then tp2.atoms
else if tp2.hasClassSymbol(defn.NothingClass) then tp1.atoms
else tp1.atoms | tp2.atoms
val tp1w = tp1.widenSingletons
val tp2w = tp2.widenSingletons
myWidened = if ((tp1 eq tp1w) && (tp2 eq tp2w)) this else tp1w | tp2w
Expand Down
1 change: 0 additions & 1 deletion scala3doc/test/dotty/dokka/SourceLinksTests.scala
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,6 @@ class SourceLinksTest:
case (path: String, line: Int) => links.pathTo(projectRoot.resolve(path), line = Some(line))
case (path: String, operation: Operation) => links.pathTo(projectRoot.resolve(path), operation = operation)
case (path: String, line: Int, operation: Operation) => links.pathTo(projectRoot.resolve(path), operation = operation, line = Some(line))
case _ => ??? // needed due to handling of singleton types inside union types

val expectedRes = expected match
case s: String => Some(s)
Expand Down
2 changes: 1 addition & 1 deletion tests/neg/singletonOrs.scala
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ object Get2As1 {
def get2as11X:V = tuToV()(2) // error
}
class Or11Nothing extends Or11X[Nothing]
def get2as1:1 = new Or11Nothing().get2as11X // error
def get2as1:1 = new Or11Nothing().get2as11X // ok

def main(a:Array[String]) = {
println(get2as1) // prints 2
Expand Down
20 changes: 20 additions & 0 deletions tests/pos/i11003.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
object Foo

val x: Foo.type = Foo
val y: Foo.type | Nothing = x
val z: Foo.type = y
val a: 1 | Nothing = 1
val b: 1 = a

val intSuper = summon[(Int | Nothing) <:< Int]
val intSub = summon[Int <:< (Int | Nothing)]
val intEq = summon[Int =:= (Int | Nothing)]

val fooSuper = summon[(Foo.type | Nothing) <:< Foo.type]
val fooSub = summon[Foo.type <:< (Foo.type | Nothing)]
val fooEq = summon[Foo.type =:= (Foo.type | Nothing)]

val oneSuper = summon[(1 | Nothing) <:< 1]
val oneSub = summon[1 <:< (1 | Nothing)]
val oneEq = summon[1 =:= (1 | Nothing)]