From 531f29be3142f8163a4c99c625215be3d185c1d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= <sjrdoeraene@gmail.com>
Date: Tue, 5 Nov 2024 17:00:48 +0100
Subject: [PATCH] Fix #21295: Restrict `provablyDisjoint` with `Nothing`s in
 invariant type params.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

If `Foo[T]` is invariant in `T`, we previously concluded that
`Foo[A] ⋔ Foo[B]` from `A ⋔ B`. That is however wrong if both `A`
and `B` can be (instantiated to) `Nothing`.

We now rule out these occurrences in two ways:

* either we show that `T` corresponds to a field, like we do in the
  covariant case, or
* we show that `A` or `B` cannot possibly be `Nothing`.

The second condition is shaky at best. I would have preferred not
to include it. However, introducing the former without the fallback
on the latter breaks too many existing test cases.

[Cherry-picked 0dceb7fd16e5db4df1063a77018c604f6fe741b1]
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 21 +++++++++++++++++--
 tests/pos/i21295.scala                        |  8 +++++++
 2 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 tests/pos/i21295.scala

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 145a038dd856..79d43ade30ef 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -3231,6 +3231,12 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
   end provablyDisjointClasses
 
   private def provablyDisjointTypeArgs(cls: ClassSymbol, args1: List[Type], args2: List[Type], pending: util.HashSet[(Type, Type)])(using Context): Boolean =
+    // sjrd: I will not be surprised when this causes further issues in the future.
+    // This is a compromise to be able to fix #21295 without breaking the world.
+    def cannotBeNothing(tp: Type): Boolean = tp match
+      case tp: TypeParamRef => cannotBeNothing(tp.paramInfo)
+      case _                => !(tp.loBound.stripTypeVar <:< defn.NothingType)
+
     // It is possible to conclude that two types applied are disjoint by
     // looking at covariant type parameters if the said type parameters
     // are disjoint and correspond to fields.
@@ -3239,9 +3245,20 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     def covariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
       provablyDisjoint(tp1, tp2, pending) && typeparamCorrespondsToField(cls.appliedRef, tparam)
 
-    // In the invariant case, direct type parameter disjointness is enough.
+    // In the invariant case, we have more ways to prove disjointness:
+    // - either the type param corresponds to a field, like in the covariant case, or
+    // - one of the two actual args can never be `Nothing`.
+    // The latter condition, as tested by `cannotBeNothing`, is ad hoc and was
+    // not carefully evaluated to be sound. We have it because we had to
+    // reintroduce the former condition to fix #21295, and alone, that broke a
+    // lot of existing test cases.
+    // Having either one of the two conditions be true is better than not requiring
+    // any, which was the status quo before #21295.
     def invariantDisjoint(tp1: Type, tp2: Type, tparam: TypeParamInfo): Boolean =
-      provablyDisjoint(tp1, tp2, pending)
+      provablyDisjoint(tp1, tp2, pending) && {
+        typeparamCorrespondsToField(cls.appliedRef, tparam)
+          || (cannotBeNothing(tp1) || cannotBeNothing(tp2))
+      }
 
     args1.lazyZip(args2).lazyZip(cls.typeParams).exists {
       (arg1, arg2, tparam) =>
diff --git a/tests/pos/i21295.scala b/tests/pos/i21295.scala
new file mode 100644
index 000000000000..fc2db7c452d9
--- /dev/null
+++ b/tests/pos/i21295.scala
@@ -0,0 +1,8 @@
+sealed trait Foo[A]
+final class Bar extends Foo[Nothing]
+
+object Test:
+  type Extract[T] = T match
+    case Foo[_] => Int
+
+  val x: Extract[Bar] = 1