Teach provablyDisjoint to handle FromJavaObject

SpaceEngine makes use of provablyDisjoint, using its Empty space as a
result.  In the test case the scrutinee is of type xs.E, which has info
`>: Nothing <: <FromJavaObject>`, which isn't a subtype of Double and
Double isn't a subtype of it either.  But their intersection does exist,
in boxed Double.

The code here is exactly like FromJavaObject is handled in isSubType's
"firstTry".

Author: dwijnand

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

@@ -2597,6 +2597,10 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
     }.apply(true, tp)
 
     (tp1.dealias, tp2.dealias) match {
+      case _ if !ctx.erasedTypes && tp2.isFromJavaObject =>
+        provablyDisjoint(tp1, defn.AnyType)
+      case _ if !ctx.erasedTypes && tp1.isFromJavaObject =>
+        provablyDisjoint(defn.AnyType, tp2)
       case (tp1: TypeRef, _) if tp1.symbol == defn.SingletonClass =>
         false
       case (_, tp2: TypeRef) if tp2.symbol == defn.SingletonClass =>

tests/pos/i15717.scala

@@ -0,0 +1,16 @@
+// scalac: -Werror
+class Test:
+  def pmat(xs: java.util.Vector[_]): String = xs.get(0) match
+    case d: Double => d.toString() // was: error: unreachable case, which is spurious
+    case _         => "shrug"
+
+  def pmatR(xs: java.util.Vector[_]): String =
+    val scr = xs.get(0)
+    1.0 match
+      case `scr` => scr.toString() // for the reverse provablyDisjoint case
+      case _     => "shrug"
+
+  def test =
+    val x = new java.util.Vector[Double]()
+    x.add(1.0)
+    pmat(x)