Skip to content

Commit 1b2a16e

Browse files
sjrdsjrd
committed
New implementation of provablyDisjoint to match SIP-56.
1 parent ec94ff5 commit 1b2a16e

15 files changed

+430
-167
lines changed

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

+209-143
Large diffs are not rendered by default.

‎tests/neg/6314-1.scala

+5-4
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
object G {
2-
final class X
3-
final class Y
2+
trait X
3+
class Y
4+
class Z
45

56
trait FooSig {
67
type Type
@@ -13,14 +14,14 @@ object G {
1314
type Foo = Foo.Type
1415

1516
type Bar[A] = A match {
16-
case X & Y => String
17+
case X & Z => String
1718
case Y => Int
1819
}
1920

2021
def main(args: Array[String]): Unit = {
2122
val a: Bar[X & Y] = "hello" // error
2223
val i: Bar[Y & Foo] = Foo.apply[Bar](a)
23-
val b: Int = i // error
24+
val b: Int = i
2425
println(b + 1)
2526
}
2627
}

‎tests/neg/6314-6.check

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
-- Error: tests/neg/6314-6.scala:26:3 ----------------------------------------------------------------------------------
2+
26 | (new YY {}).boom // error: object creation impossible
3+
| ^
4+
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test3 is not defined
5+
|(Note that
6+
| parameter String in def apply(fa: String): Int in trait XX in object Test3 does not match
7+
| 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
8+
| )
9+
-- Error: tests/neg/6314-6.scala:52:3 ----------------------------------------------------------------------------------
10+
52 | (new YY {}).boom // error: object creation impossible
11+
| ^
12+
|object creation impossible, since def apply(fa: String): Int in trait XX in object Test4 is not defined
13+
|(Note that
14+
| parameter String in def apply(fa: String): Int in trait XX in object Test4 does not match
15+
| 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
16+
| )

‎tests/neg/6314-6.scala

+4-8
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,9 @@ object Test3 {
2121
trait YY extends XX {
2222
type Foo = X & Y
2323

24-
def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa // error
25-
// overriding method apply in trait XX of type (fa: String): Int;
26-
// method apply of type (fa: String): String has incompatible type
24+
def apply(fa: Bar[X & Foo]): Bar[Y & Foo] = fa
2725
}
28-
(new YY {}).boom
26+
(new YY {}).boom // error: object creation impossible
2927
}
3028

3129
object Test4 {
@@ -49,9 +47,7 @@ object Test4 {
4947
trait YY extends XX {
5048
type Foo = X & Y
5149

52-
def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa // error
53-
// overriding method apply in trait XX of type (fa: String): Int;
54-
// method apply of type (fa: String): String has incompatible type
50+
def apply(fa: Bar[X & FooAlias]): Bar[Y & FooAlias] = fa
5551
}
56-
(new YY {}).boom
52+
(new YY {}).boom // error: object creation impossible
5753
}

‎tests/neg/6314.check

+44
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
-- [E007] Type Mismatch Error: tests/neg/6314.scala:28:27 --------------------------------------------------------------
2+
28 | val i: Bar[Y | Type] = 1 // error
3+
| ^
4+
| Found: (1 : Int)
5+
| Required: Test1Bis.Bar[Test1Bis.Y | Test.this.Type]
6+
|
7+
| Note: a match type could not be fully reduced:
8+
|
9+
| trying to reduce Test1Bis.Bar[Test1Bis.Y | Test.this.Type]
10+
| failed since selector Test1Bis.Y | Test.this.Type
11+
| does not match case Test1Bis.X & Test1Bis.Y => String
12+
| and cannot be shown to be disjoint from it either.
13+
| Therefore, reduction cannot advance to the remaining case
14+
|
15+
| case Any => Int
16+
|
17+
| longer explanation available when compiling with `-explain`
18+
-- [E007] Type Mismatch Error: tests/neg/6314.scala:45:33 --------------------------------------------------------------
19+
45 | def right(fa: Bar[L]): Int = fa // error
20+
| ^^
21+
| Found: (fa : Wizzle.this.Bar[L])
22+
| Required: Int
23+
|
24+
| where: L is a type in trait Wizzle with bounds <: Int & Singleton
25+
|
26+
| longer explanation available when compiling with `-explain`
27+
-- [E007] Type Mismatch Error: tests/neg/6314.scala:55:33 --------------------------------------------------------------
28+
55 | def right(fa: Bar[L]): Int = fa // error
29+
| ^^
30+
| Found: (fa : Wazzlo.this.Bar[L])
31+
| Required: Int
32+
|
33+
| where: L is a type in trait Wazzlo with bounds <: Int & AnyVal
34+
|
35+
| longer explanation available when compiling with `-explain`
36+
-- [E007] Type Mismatch Error: tests/neg/6314.scala:65:33 --------------------------------------------------------------
37+
65 | def right(fa: Bar[L]): Int = fa // error
38+
| ^^
39+
| Found: (fa : Wuzzlu.this.Bar[L])
40+
| Required: Int
41+
|
42+
| where: L is a type in trait Wuzzlu with bounds <: String & AnyRef
43+
|
44+
| longer explanation available when compiling with `-explain`

‎tests/neg/6314.scala

+28-9
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,41 @@
1-
final class X
2-
final class Y
3-
41
object Test1 {
2+
// X, Y and Z are unrelated, Y is provably disjoint from Z, but X is not provably disjoint with either
3+
trait X
4+
class Y
5+
class Z
6+
57
trait Test {
68
type Type
79
// This is testing that both permutations of the types in a &
8-
// are taken into account by the intersection test
9-
val i: Bar[Y & Type] = 1 // error
10+
// are taken into account by the provablyDisjoint test
11+
val i: Bar[Y & Type] = 1 // ok, disjoint from X & Z because Y and Z are disjoint
1012
}
1113

1214
type Bar[A] = A match {
13-
case X & Y => String
15+
case X & Z => String
1416
case Y => Int
1517
}
1618
}
1719

20+
object Test1Bis {
21+
final class X
22+
final class Y
23+
24+
trait Test {
25+
type Type
26+
// This is testing that both permutations of the types in a |
27+
// are taken into account by the provablyDisjoint test
28+
val i: Bar[Y | Type] = 1 // error
29+
}
30+
31+
type Bar[A] = A match {
32+
case X & Y => String
33+
case Any => Int
34+
}
35+
}
36+
1837
object Test2 {
19-
trait Wizzle[L <: Int with Singleton] {
38+
trait Wizzle[L <: Int & Singleton] {
2039
type Bar[A] = A match {
2140
case 0 => String
2241
case L => Int
@@ -26,7 +45,7 @@ object Test2 {
2645
def right(fa: Bar[L]): Int = fa // error
2746
}
2847

29-
trait Wazzlo[L <: Int with AnyVal] {
48+
trait Wazzlo[L <: Int & AnyVal] {
3049
type Bar[A] = A match {
3150
case 0 => String
3251
case L => Int
@@ -36,7 +55,7 @@ object Test2 {
3655
def right(fa: Bar[L]): Int = fa // error
3756
}
3857

39-
trait Wuzzlu[L <: String with AnyRef] {
58+
trait Wuzzlu[L <: String & AnyRef] {
4059
type Bar[A] = A match {
4160
case "" => String
4261
case L => Int

‎tests/neg/i13190.check

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
2+
-- [E172] Type Error: tests/neg/i13190/B_2.scala:14:38 -----------------------------------------------------------------
3+
14 | summon[FindField[R, "B"] =:= Double] // error
4+
| ^
5+
| Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double.
6+
|
7+
| Note: a match type could not be fully reduced:
8+
|
9+
| trying to reduce Test.FindField[Test.R, ("B" : String)]
10+
| failed since selector Test.R
11+
| does not match case Opaque.FieldType[("B" : String), f] *: t => f
12+
| and cannot be shown to be disjoint from it either.
13+
| Therefore, reduction cannot advance to the remaining case
14+
|
15+
| case _ *: t => Test.FindField[t, ("B" : String)]

‎tests/pos/i13190/A_1.scala renamed to ‎tests/neg/i13190/A_1.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
object Opaque {
22
opaque type FieldType[K, +V] <: V = V
3-
}
3+
}

‎tests/pos/i13190/B_2.scala renamed to ‎tests/neg/i13190/B_2.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,5 @@ object Test {
1111
//val f2: Int = f
1212

1313
type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple
14-
summon[FindField[R, "B"] =:= Double]
14+
summon[FindField[R, "B"] =:= Double] // error
1515
}

‎tests/neg/i13190b.check

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- [E172] Type Error: tests/neg/i13190b.scala:18:38 --------------------------------------------------------------------
2+
18 | summon[FindField[R, "B"] =:= Double] // error
3+
| ^
4+
| Cannot prove that Test.FindField[Test.R, ("B" : String)] =:= Double.
5+
|
6+
| Note: a match type could not be fully reduced:
7+
|
8+
| trying to reduce Test.FindField[Test.R, ("B" : String)]
9+
| failed since selector Test.R
10+
| does not match case Opaque.FieldType[("B" : String), f] *: t => f
11+
| and cannot be shown to be disjoint from it either.
12+
| Therefore, reduction cannot advance to the remaining case
13+
|
14+
| case _ *: t => Test.FindField[t, ("B" : String)]

‎tests/neg/i13190b.scala

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
object Opaque {
2+
opaque type FieldType[K, +V] <: V = V
3+
}
4+
5+
import Opaque.*
6+
7+
object Test {
8+
type FindField[R <: scala.Tuple, K] = R match {
9+
case FieldType[K, f] *: t => f
10+
case _ *: t => FindField[t, K]
11+
}
12+
13+
val f: FieldType["A", Int] = ???
14+
val f1: Int = f
15+
//val f2: Int = f
16+
17+
type R = FieldType["A", Int] *: FieldType["B", Double] *: FieldType["C", String] *: FieldType["D", Boolean] *: EmptyTuple
18+
summon[FindField[R, "B"] =:= Double] // error
19+
}

‎tests/neg/i15312.check

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
-- [E007] Type Mismatch Error: tests/neg/i15312.scala:7:27 -------------------------------------------------------------
2+
7 |val b: F[{type A = Int}] = "asd" // error
3+
| ^^^^^
4+
| Found: ("asd" : String)
5+
| Required: F[Object{type A = Int}]
6+
|
7+
| Note: a match type could not be fully reduced:
8+
|
9+
| trying to reduce F[Object{type A = Int}]
10+
| failed since selector Object{type A = Int}
11+
| does not match case Object{type A = Float} => Int
12+
| and cannot be shown to be disjoint from it either.
13+
| Therefore, reduction cannot advance to the remaining case
14+
|
15+
| case Object{type A = Int} => String
16+
|
17+
| longer explanation available when compiling with `-explain`

‎tests/pos/i15312.scala renamed to ‎tests/neg/i15312.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ type F[t] =
44
case {type A = Int} => String
55

66
val a: F[{type A = Float}] = 10
7-
val b: F[{type A = Int}] = "asd" // Found:("asd" : String) Required: F[Object{A = Int}]
7+
val b: F[{type A = Int}] = "asd" // error

‎tests/pos/i15677.scala renamed to ‎tests/pos-deep-subtype/i15677.scala

File renamed without changes.

‎tests/pos/match-type-disjoint-transitivity.scala

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
/* Tests that the following property holds for a chosen set of types (S, T, U):
2+
*
3+
* If S <: T and T provably disjoint from U, then S provably disjoint from U.
4+
*/
5+
6+
class Parent[T]
7+
class Child[T] extends Parent[T]
8+
trait ChildTrait[T] extends Parent[T]
9+
10+
class OtherClass
11+
12+
trait Common[A]
13+
trait Left[A] extends Common[A]
14+
trait Right[A] extends Common[A]
15+
16+
// Since Parent[Boolean] disjoint from Parent[Int], we must have Child[Boolean] also disjoint from Parent[Int]
17+
object Test1:
18+
type MT[X] = X match
19+
case Parent[Int] => Int
20+
case Parent[Boolean] => Boolean
21+
22+
def test(): Unit =
23+
summon[MT[Parent[Int]] =:= Int]
24+
summon[MT[Parent[Boolean]] =:= Boolean]
25+
26+
summon[MT[Child[Int]] =:= Int]
27+
summon[MT[Child[Boolean]] =:= Boolean]
28+
end test
29+
end Test1
30+
31+
// Since Parent[Int] disjoint from OtherClass, we must have Child[Int] and ChildTrait[T] also disjoint from OtherClass
32+
object Test2:
33+
type MT[X] = X match
34+
case OtherClass => Int
35+
case Parent[Int] => Boolean
36+
37+
def test(): Unit =
38+
summon[MT[OtherClass] =:= Int]
39+
summon[MT[Parent[Int]] =:= Boolean]
40+
41+
summon[MT[Child[Int]] =:= Boolean]
42+
summon[MT[ChildTrait[Int]] =:= Boolean]
43+
end test
44+
end Test2
45+
46+
// Since Common[Int] is disjoint from Right[Boolean], we must have Left[Int] disjoint from Right[Boolean]
47+
object Test3:
48+
type MT[X] = X match
49+
case Right[Boolean] => Int
50+
case Any => Boolean
51+
52+
def test(): Unit =
53+
summon[MT[Common[Int]] =:= Boolean]
54+
summon[MT[Left[Int]] =:= Boolean]
55+
end test
56+
end Test3

0 commit comments

Comments
 (0)