Fix #21295: Restrict provablyDisjoint with Nothings in invariant …

…type params. (#21891)

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.

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -3232,6 +3232,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.
@@ -3240,9 +3246,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) =>

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