From 55861e964a1e1bcdb0ef0d1f640d7393080b7f79 Mon Sep 17 00:00:00 2001
From: Wojciech Mazur <wmazur@virtuslab.com>
Date: Mon, 2 Dec 2024 20:03:53 +0100
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][modified]
---
 .../src/dotty/tools/dotc/core/TypeComparer.scala     | 12 ++++++++++++
 compiler/test/dotc/pos-test-pickling.blacklist       |  2 +-
 tests/pos/i20897.scala                               | 10 ++++++++++
 3 files changed, 23 insertions(+), 1 deletion(-)
 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 ca5059c944c6..fa84b914a561 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -2881,6 +2881,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
         true
       case (_, _: HKLambda) =>
         true
+      /* 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
       case (tp1: OrType, _)  =>
         provablyDisjoint(tp1.tp1, tp2) && provablyDisjoint(tp1.tp2, tp2)
       case (_, tp2: OrType)  =>
@@ -2891,6 +2897,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
       case (_, tp2: AndType) =>
         !(tp2 <:< tp1)
         && (provablyDisjoint(tp1, tp2.tp2) || provablyDisjoint(tp1, tp2.tp1))
+      /* 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
       case (tp1: NamedType, _) if gadtBounds(tp1.symbol) != null =>
         provablyDisjoint(gadtBounds(tp1.symbol).uncheckedNN.hi, tp2)
         || provablyDisjoint(tp1.superTypeNormalized, tp2)
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index fd40d8b3577a..8293d0a69d79 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -57,6 +57,7 @@ i15158.scala
 i15155.scala
 i15827.scala
 i18211.scala
+i20897.scala
 
 # Opaque type
 i5720.scala
@@ -112,4 +113,3 @@ i15525.scala
 i19955a.scala
 i19955b.scala
 i20053b.scala
-
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