Skip to content

Commit

Permalink
Fix #20897: Make Nothing ⋔ Nothing, as per spec.
Browse files Browse the repository at this point in the history
`derivesFrom`, used in `provablyDisjointClasses`, normally returns
`false` when the receiver is `Nothing`. However, it returns `true`
if the right-hand-side happens to be exactly `Nothing` as well.
For the purpose of computing `provablyDisjoint`, that is not what
we want.

The root issue was that we let the previous algorithm handle
`Nothing` like a class type, which it *is* in dotc but not in the
spec. That led to this mistake.

`AnyKind` suffers a similar issue, but already had special-cases in
various places to mitigate it.

Instead of adding a new special-case for `Nothing` inside
`provablyDisjointClasses`, we address the root issue. Now we deal
with `Nothing` and `AnyKind` early, before trying any of the code
paths that handle (real) class types.

[Cherry-picked b7846c4]
  • Loading branch information
sjrd authored and WojciechMazur committed Aug 27, 2024
1 parent 30cff00 commit 2baefd5
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 8 deletions.
24 changes: 17 additions & 7 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2929,6 +2929,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case pair if pending != null && pending.contains(pair) =>
false

/* Nothing is not a class type in the spec but dotc represents it as if it were one.
* Get it out of the way early to avoid mistakes (see for example #20897).
* Nothing ⋔ T and T ⋔ Nothing for all T.
*/
case (tp1, tp2) if tp1.isExactlyNothing || tp2.isExactlyNothing =>
true

// Cases where there is an intersection or union on the right
case (tp1, tp2: OrType) =>
provablyDisjoint(tp1, tp2.tp1, pending) && provablyDisjoint(tp1, tp2.tp2, pending)
Expand All @@ -2941,14 +2948,21 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
case (tp1: AndType, tp2) =>
provablyDisjoint(tp1.tp1, tp2, pending) || provablyDisjoint(tp1.tp2, tp2, pending)

/* Handle AnyKind now for the same reason as Nothing above: it is not a real class type.
* Other than the rules with Nothing, unions and intersections, there is structurally
* no rule such that AnyKind ⋔ T or T ⋔ AnyKind for any T.
*/
case (tp1, tp2) if tp1.isDirectRef(AnyKindClass) || tp2.isDirectRef(AnyKindClass) =>
false

// Cases involving type lambdas
case (tp1: HKTypeLambda, tp2: HKTypeLambda) =>
tp1.paramNames.sizeCompare(tp2.paramNames) != 0
|| provablyDisjoint(tp1.resultType, tp2.resultType, pending)
case (tp1: HKTypeLambda, tp2) =>
!tp2.isDirectRef(defn.AnyKindClass)
true
case (tp1, tp2: HKTypeLambda) =>
!tp1.isDirectRef(defn.AnyKindClass)
true

/* Cases where both are unique values (enum cases or constant types)
*
Expand Down Expand Up @@ -3052,17 +3066,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
else child
}.filter(child => child.exists && child != cls)

// TODO? Special-case for Nothing and Null? We probably need Nothing/Null disjoint from Nothing/Null
def eitherDerivesFromOther(cls1: Symbol, cls2: Symbol): Boolean =
cls1.derivesFrom(cls2) || cls2.derivesFrom(cls1)

def smallestNonTraitBase(cls: Symbol): Symbol =
cls.asClass.baseClasses.find(!_.is(Trait)).get

if cls1 == defn.AnyKindClass || cls2 == defn.AnyKindClass then
// For some reason, A.derivesFrom(AnyKind) returns false, so we have to handle it specially
false
else if (eitherDerivesFromOther(cls1, cls2))
if (eitherDerivesFromOther(cls1, cls2))
false
else
if (cls1.is(Final) || cls2.is(Final))
Expand Down
2 changes: 1 addition & 1 deletion compiler/test/dotc/pos-test-pickling.blacklist
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ mt-redux-norm.perspective.scala
i18211.scala
10867.scala
named-tuples1.scala
i20897.scala

# Opaque type
i5720.scala
Expand Down Expand Up @@ -134,4 +135,3 @@ parsercombinators-new-syntax.scala
hylolib-deferred-given
hylolib-cb
hylolib

10 changes: 10 additions & 0 deletions tests/pos/i20897.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
object Test:
type Disj[A, B] =
A match
case B => true
case _ => false

def f(a: Disj[1 | Nothing, 2 | Nothing]): Unit = ()

val t = f(false)
end Test

0 comments on commit 2baefd5

Please sign in to comment.