From 2baefd5341f813f76017471c68940253953f926e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= <sjrdoeraene@gmail.com>
Date: Mon, 22 Jul 2024 11:22:49 +0200
Subject: [PATCH] =?UTF-8?q?Fix=20#20897:=20Make=20`Nothing=20=E2=8B=94=20N?=
 =?UTF-8?q?othing`,=20as=20per=20spec.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`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 b7846c497b4dae18b7a2484fe5ea1acf55a16487]
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 24 +++++++++++++------
 .../test/dotc/pos-test-pickling.blacklist     |  2 +-
 tests/pos/i20897.scala                        | 10 ++++++++
 3 files changed, 28 insertions(+), 8 deletions(-)
 create mode 100644 tests/pos/i20897.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index a732ee931b5d..fd9e02ca1cd6 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -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)
@@ -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)
        *
@@ -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))
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index d6f962176ecc..b68ac7fc3b6e 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -67,6 +67,7 @@ mt-redux-norm.perspective.scala
 i18211.scala
 10867.scala
 named-tuples1.scala
+i20897.scala
 
 # Opaque type
 i5720.scala
@@ -134,4 +135,3 @@ parsercombinators-new-syntax.scala
 hylolib-deferred-given
 hylolib-cb
 hylolib
-
diff --git a/tests/pos/i20897.scala b/tests/pos/i20897.scala
new file mode 100644
index 000000000000..ecfac5b1615e
--- /dev/null
+++ b/tests/pos/i20897.scala
@@ -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