New implementation of provablyDisjoint to match SIP-56.

scala · Dec 18, 2023 · 1b2a16e · 1b2a16e
1 parent ec94ff5
commit 1b2a16e
Show file tree

Hide file tree

Showing 15 changed files with 430 additions and 167 deletions.
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
diff --git a/tests/neg/6314-1.scala b/tests/neg/6314-1.scala
@@ -1,6 +1,7 @@
 object G {
-  final class X
-  final class Y
+  trait X
+  class Y
+  class Z
 
   trait FooSig {
     type Type
@@ -13,14 +14,14 @@ object G {
   type Foo = Foo.Type
 
   type Bar[A] = A match {
-    case X & Y => String
+    case X & Z => String
     case Y => Int
   }
 
   def main(args: Array[String]): Unit = {
     val a: Bar[X & Y] = "hello" // error
     val i: Bar[Y & Foo] = Foo.apply[Bar](a)
-    val b: Int = i // error
+    val b: Int = i
     println(b + 1)
   }
 }
diff --git a/tests/neg/6314-6.check b/tests/neg/6314-6.check
@@ -0,0 +1,16 @@
+-- Error: tests/neg/6314-6.scala:26:3 ----------------------------------------------------------------------------------
+26 |  (new YY {}).boom // error: object creation impossible
+   |   ^
+   |object creation impossible, since def apply(fa: String): Int in trait XX in object Test3 is not defined 
+   |(Note that
+   | parameter String in def apply(fa: String): Int in trait XX in object Test3 does not match
+   | parameter Test3.Bar[X & Object with Test3.YY {...}#Foo] in def apply(fa: Test3.Bar[X & YY.this.Foo]): Test3.Bar[Y & YY.this.Foo] in trait YY in object Test3
+   | )
+-- Error: tests/neg/6314-6.scala:52:3 ----------------------------------------------------------------------------------
+52 |  (new YY {}).boom // error: object creation impossible
+   |   ^
+   |object creation impossible, since def apply(fa: String): Int in trait XX in object Test4 is not defined 
+   |(Note that
+   | parameter String in def apply(fa: String): Int in trait XX in object Test4 does not match
+   | parameter Test4.Bar[X & Object with Test4.YY {...}#FooAlias] in def apply(fa: Test4.Bar[X & YY.this.FooAlias]): Test4.Bar[Y & YY.this.FooAlias] in trait YY in object Test4
+   | )
diff --git a/tests/neg/6314-6.scala b/tests/neg/6314-6.scala
@@ -21,11 +21,9 @@ object Test3 {
   trait YY extends XX {
     type Foo = X & Y
 
-    def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error
-        // overriding method apply in trait XX of type (fa: String): Int;
-        //   method apply of type (fa: String): String has incompatible type
+    def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
   }
-  (new YY {}).boom
+  (new YY {}).boom // error: object creation impossible
 }
 
 object Test4 {
@@ -49,9 +47,7 @@ object Test4 {
   trait YY extends XX {
     type Foo = X & Y
 
-    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error
-        // overriding method apply in trait XX of type (fa: String): Int;
-        //   method apply of type (fa: String): String has incompatible type
+    def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa
   }
-  (new YY {}).boom
+  (new YY {}).boom // error: object creation impossible
 }
diff --git a/tests/neg/6314.check b/tests/neg/6314.check
@@ -0,0 +1,44 @@
+-- [E007] Type Mismatch Error: tests/neg/6314.scala:28:27 --------------------------------------------------------------
+28 |    val i: Bar[Y | Type] = 1 // error
+   |                           ^
+   |                           Found:    (1 : Int)
+   |                           Required: Test1Bis.Bar[Test1Bis.Y | Test.this.Type]
+   |
+   |                           Note: a match type could not be fully reduced:
+   |
+   |                             trying to reduce  Test1Bis.Bar[Test1Bis.Y | Test.this.Type]
+   |                             failed since selector Test1Bis.Y | Test.this.Type
+   |                             does not match  case Test1Bis.X & Test1Bis.Y => String
+   |                             and cannot be shown to be disjoint from it either.
+   |                             Therefore, reduction cannot advance to the remaining case
+   |
+   |                               case Any => Int
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/6314.scala:45:33 --------------------------------------------------------------
+45 |    def right(fa: Bar[L]): Int = fa // error
+   |                                 ^^
+   |                                 Found:    (fa : Wizzle.this.Bar[L])
+   |                                 Required: Int
+   |
+   |                                 where:    L is a type in trait Wizzle with bounds <: Int & Singleton
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/6314.scala:55:33 --------------------------------------------------------------
+55 |    def right(fa: Bar[L]): Int = fa // error
+   |                                 ^^
+   |                                 Found:    (fa : Wazzlo.this.Bar[L])
+   |                                 Required: Int
+   |
+   |                                 where:    L is a type in trait Wazzlo with bounds <: Int & AnyVal
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg/6314.scala:65:33 --------------------------------------------------------------
+65 |    def right(fa: Bar[L]): Int = fa // error
+   |                                 ^^
+   |                                 Found:    (fa : Wuzzlu.this.Bar[L])
+   |                                 Required: Int
+   |
+   |                                 where:    L is a type in trait Wuzzlu with bounds <: String & AnyRef
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/6314.scala b/tests/neg/6314.scala
@@ -1,22 +1,41 @@
-final class X
-final class Y
-
 object Test1 {
+  // X, Y and Z are unrelated, Y is provably disjoint from Z, but X is not provably disjoint with either
+  trait X
+  class Y
+  class Z
+
   trait Test {
     type Type
     // This is testing that both permutations of the types in a &
-    // are taken into account by the intersection test
-    val i: Bar[Y & Type] = 1 // error
+    // are taken into account by the provablyDisjoint test
+    val i: Bar[Y & Type] = 1 // ok, disjoint from X & Z because Y and Z are disjoint
   }
 
   type Bar[A] = A match {
-    case X & Y => String
+    case X & Z => String
     case Y => Int
   }
 }
 
+object Test1Bis {
+  final class X
+  final class Y
+
+  trait Test {
+    type Type
+    // This is testing that both permutations of the types in a |
+    // are taken into account by the provablyDisjoint test
+    val i: Bar[Y | Type] = 1 // error
+  }
+
+  type Bar[A] = A match {
+    case X & Y => String
+    case Any => Int
+  }
+}
+
 object Test2 {
-  trait Wizzle[L <: Int with Singleton] {
+  trait Wizzle[L <: Int & Singleton] {
     type Bar[A] = A match {
       case 0 => String
       case L => Int
@@ -26,7 +45,7 @@ object Test2 {
     def right(fa: Bar[L]): Int = fa // error
   }
 
-  trait Wazzlo[L <: Int with AnyVal] {
+  trait Wazzlo[L <: Int & AnyVal] {
     type Bar[A] = A match {
       case 0 => String
       case L => Int
@@ -36,7 +55,7 @@ object Test2 {
     def right(fa: Bar[L]): Int = fa // error
   }
 
-  trait Wuzzlu[L <: String with AnyRef] {
+  trait Wuzzlu[L <: String & AnyRef] {
     type Bar[A] = A match {
       case "" => String
       case L => Int

diff --git a/tests/neg/i13190.check b/tests/neg/i13190.check
@@ -0,0 +1,15 @@
+
+-- [E172] Type Error: tests/neg/i13190/B_2.scala:14:38 -----------------------------------------------------------------
+14 |  summon[FindField[R, "B"] =:= Double] // error
+   |                                      ^
+   |                                      Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double.
+   |
+   |                                      Note: a match type could not be fully reduced:
+   |
+   |                                        trying to reduce  Test.FindField[Test.R, ("B" : String)]
+   |                                        failed since selector Test.R
+   |                                        does not match  case Opaque.FieldType[("B" : String), f] *: t => f
+   |                                        and cannot be shown to be disjoint from it either.
+   |                                        Therefore, reduction cannot advance to the remaining case
+   |
+   |                                          case _ *: t => Test.FindField[t, ("B" : String)]
diff --git a/tests/pos/i13190/A_1.scala → tests/neg/i13190/A_1.scala b/tests/pos/i13190/A_1.scala → tests/neg/i13190/A_1.scala
@@ -1,3 +1,3 @@
 object Opaque {
   opaque type FieldType[K, +V] <: V = V
-}
+}
diff --git a/tests/pos/i13190/B_2.scala → tests/neg/i13190/B_2.scala b/tests/pos/i13190/B_2.scala → tests/neg/i13190/B_2.scala
@@ -11,5 +11,5 @@ object Test {
   //val f2: Int = f
 
   type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple
-  summon[FindField[R, "B"] =:= Double]
+  summon[FindField[R, "B"] =:= Double] // error
 }
diff --git a/tests/neg/i13190b.check b/tests/neg/i13190b.check
@@ -0,0 +1,14 @@
+-- [E172] Type Error: tests/neg/i13190b.scala:18:38 --------------------------------------------------------------------
+18 |  summon[FindField[R, "B"] =:= Double] // error
+   |                                      ^
+   |                                      Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double.
+   |
+   |                                      Note: a match type could not be fully reduced:
+   |
+   |                                        trying to reduce  Test.FindField[Test.R, ("B" : String)]
+   |                                        failed since selector Test.R
+   |                                        does not match  case Opaque.FieldType[("B" : String), f] *: t => f
+   |                                        and cannot be shown to be disjoint from it either.
+   |                                        Therefore, reduction cannot advance to the remaining case
+   |
+   |                                          case _ *: t => Test.FindField[t, ("B" : String)]
diff --git a/tests/neg/i13190b.scala b/tests/neg/i13190b.scala
@@ -0,0 +1,19 @@
+object Opaque {
+  opaque type FieldType[K, +V] <: V = V
+}
+
+import Opaque.*
+
+object Test {
+  type FindField[R <: scala.Tuple, K] = R match {
+    case FieldType[K, f] *: t => f
+    case _ *: t => FindField[t, K]
+  }
+
+  val f: FieldType["A", Int] = ???
+  val f1: Int = f
+  //val f2: Int = f
+
+  type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple
+  summon[FindField[R, "B"] =:= Double] // error
+}
diff --git a/tests/neg/i15312.check b/tests/neg/i15312.check
@@ -0,0 +1,17 @@
+-- [E007] Type Mismatch Error: tests/neg/i15312.scala:7:27 -------------------------------------------------------------
+7 |val b: F[{type A = Int}] = "asd" // error
+  |                           ^^^^^
+  |                           Found:    ("asd" : String)
+  |                           Required: F[Object{type A = Int}]
+  |
+  |                           Note: a match type could not be fully reduced:
+  |
+  |                             trying to reduce  F[Object{type A = Int}]
+  |                             failed since selector Object{type A = Int}
+  |                             does not match  case Object{type A = Float} => Int
+  |                             and cannot be shown to be disjoint from it either.
+  |                             Therefore, reduction cannot advance to the remaining case
+  |
+  |                               case Object{type A = Int} => String
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/pos/i15312.scala → tests/neg/i15312.scala b/tests/pos/i15312.scala → tests/neg/i15312.scala
@@ -4,4 +4,4 @@ type F[t] =
     case {type A = Int} => String
 
 val a: F[{type A = Float}] = 10
-val b: F[{type A = Int}] = "asd" // Found:("asd" : String) Required: F[Object{A = Int}]
+val b: F[{type A = Int}] = "asd" // error
diff --git a/tests/pos/i15677.scala → tests/pos-deep-subtype/i15677.scala b/tests/pos/i15677.scala → tests/pos-deep-subtype/i15677.scala
diff --git a/tests/pos/match-type-disjoint-transitivity.scala b/tests/pos/match-type-disjoint-transitivity.scala
@@ -0,0 +1,56 @@
+/* Tests that the following property holds for a chosen set of types (S, T, U):
+ *
+ *   If S <: T and T provably disjoint from U, then S provably disjoint from U.
+ */
+
+class Parent[T]
+class Child[T] extends Parent[T]
+trait ChildTrait[T] extends Parent[T]
+
+class OtherClass
+
+trait Common[A]
+trait Left[A] extends Common[A]
+trait Right[A] extends Common[A]
+
+// Since Parent[Boolean] disjoint from Parent[Int], we must have Child[Boolean] also disjoint from Parent[Int]
+object Test1:
+  type MT[X] = X match
+    case Parent[Int]     => Int
+    case Parent[Boolean] => Boolean
+
+  def test(): Unit =
+    summon[MT[Parent[Int]] =:= Int]
+    summon[MT[Parent[Boolean]] =:= Boolean]
+
+    summon[MT[Child[Int]] =:= Int]
+    summon[MT[Child[Boolean]] =:= Boolean]
+  end test
+end Test1
+
+// Since Parent[Int] disjoint from OtherClass, we must have Child[Int] and ChildTrait[T] also disjoint from OtherClass
+object Test2:
+  type MT[X] = X match
+    case OtherClass  => Int
+    case Parent[Int] => Boolean
+
+  def test(): Unit =
+    summon[MT[OtherClass] =:= Int]
+    summon[MT[Parent[Int]] =:= Boolean]
+
+    summon[MT[Child[Int]] =:= Boolean]
+    summon[MT[ChildTrait[Int]] =:= Boolean]
+  end test
+end Test2
+
+// Since Common[Int] is disjoint from Right[Boolean], we must have Left[Int] disjoint from Right[Boolean]
+object Test3:
+  type MT[X] = X match
+    case Right[Boolean] => Int
+    case Any            => Boolean
+
+  def test(): Unit =
+    summon[MT[Common[Int]] =:= Boolean]
+    summon[MT[Left[Int]] =:= Boolean]
+  end test
+end Test3