Skip to content

Commit 54047ba

Browse files
abgruszeckiabgruszecki
committed
Add type-member-based GADT test suite
These tests were meant to test inferring GADT constraints based on type members, which we backed out of. They are still useful to see if we don't do anything unsound when type members are present.
1 parent d25f03c commit 54047ba

File tree

5 files changed

+394
-0
lines changed

5 files changed

+394
-0
lines changed

‎tests/neg/structural-gadt.scala‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
// This file is part of tests for inferring GADT constraints from type members,
2+
// which needed to be reverted because of soundness issues.
3+
//
4+
// Lines with "// limitation" are the ones that we could soundly allow.
5+
object Test {
6+
7+
trait Expr { type T }
8+
trait IntLit extends Expr { type T <: Int }
9+
trait IntExpr extends Expr { type T = Int }
10+
11+
def foo[A](e: Expr { type T = A }) = e match {
12+
case _: IntLit =>
13+
val a: A = 0 // error
14+
val i: Int = ??? : A // limitation // error
15+
16+
case _: Expr { type T <: Int } =>
17+
val a: A = 0 // error
18+
val i: Int = ??? : A // limitation // error
19+
20+
case _: IntExpr =>
21+
val a: A = 0 // limitation // error
22+
val i: Int = ??? : A // limitation // error
23+
24+
case _: Expr { type T = Int } =>
25+
val a: A = 0 // limitation // error
26+
val i: Int = ??? : A // limitation // error
27+
}
28+
29+
def bar[A](e: Expr { type T <: A }) = e match {
30+
case _: IntLit =>
31+
val a: A = 0 // error
32+
val i: Int = ??? : A // error
33+
34+
case _: Expr { type T <: Int } =>
35+
val a: A = 0 // error
36+
val i: Int = ??? : A // error
37+
38+
case _: IntExpr =>
39+
val a: A = 0 // limitation // error
40+
val i: Int = ??? : A // error
41+
42+
case _: Expr { type T = Int } =>
43+
val a: A = 0 // limitation // error
44+
val i: Int = ??? : A // error
45+
}
46+
47+
trait IndirectExprOfIntList extends Expr {
48+
type T = U
49+
type U <: List[Int]
50+
}
51+
def baz[A](e: Expr { type T <: List[A] }) = e match {
52+
case _: IndirectExprOfIntList =>
53+
val a: A = 0 // error
54+
val i: Int = ??? : A // error
55+
}
56+
}

‎tests/neg/structural-recursive-both1-gadt.scala‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
// This file is part of tests for inferring GADT constraints from type members,
2+
// which needed to be reverted because of soundness issues.
3+
//
4+
// Lines with "// limitation" are the ones that we could soundly allow.
5+
object Test {
6+
7+
trait Expr { type T }
8+
trait IntLit extends Expr { type T <: Int }
9+
trait IntExpr extends Expr { type T = Int }
10+
11+
type ExprSub[+A] = Expr { type T <: A }
12+
type ExprExact[A] = Expr { type T = A }
13+
14+
trait IndirectIntLit extends Expr { type S <: Int; type T = S }
15+
trait IndirectIntExpr extends Expr { type S = Int; type T = S }
16+
17+
type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
18+
type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
19+
type IndirectExprExact[A] = Expr { type S = A; type T = S }
20+
21+
trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
22+
trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
23+
24+
type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
25+
type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
26+
type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
27+
28+
def foo[A](e: IndirectExprExact[A]) = e match {
29+
case _: AltIndirectIntLit =>
30+
val a: A = 0 // error
31+
val i: Int = ??? : A // limitation // error
32+
33+
case _: AltIndirectExprSub[Int] =>
34+
val a: A = 0 // error
35+
val i: Int = ??? : A // limitation // error
36+
37+
case _: AltIndirectExprSub2[Int] =>
38+
val a: A = 0 // error
39+
val i: Int = ??? : A // limitation // error
40+
41+
case _: AltIndirectIntExpr =>
42+
val a: A = 0 // limitation // error
43+
val i: Int = ??? : A // limitation // error
44+
45+
case _: AltIndirectExprExact[Int] =>
46+
val a: A = 0 // limitation // error
47+
val i: Int = ??? : A // limitation // error
48+
}
49+
50+
def bar[A](e: IndirectExprSub[A]) = e match {
51+
case _: AltIndirectIntLit =>
52+
val a: A = 0 // error
53+
val i: Int = ??? : A // error
54+
55+
case _: AltIndirectExprSub[Int] =>
56+
val a: A = 0 // error
57+
val i: Int = ??? : A // error
58+
59+
case _: AltIndirectExprSub2[Int] =>
60+
val a: A = 0 // error
61+
val i: Int = ??? : A // error
62+
63+
case _: AltIndirectIntExpr =>
64+
val a: A = 0 // limitation // error
65+
val i: Int = ??? : A // error
66+
67+
case _: AltIndirectExprExact[Int] =>
68+
val a: A = 0 // limitation // error
69+
val i: Int = ??? : A // error
70+
}
71+
72+
def baz[A](e: IndirectExprSub2[A]) = e match {
73+
case _: AltIndirectIntLit =>
74+
val a: A = 0 // error
75+
val i: Int = ??? : A // error
76+
77+
case _: AltIndirectExprSub[Int] =>
78+
val a: A = 0 // error
79+
val i: Int = ??? : A // error
80+
81+
case _: AltIndirectExprSub2[Int] =>
82+
val a: A = 0 // error
83+
val i: Int = ??? : A // error
84+
85+
case _: AltIndirectIntExpr =>
86+
val a: A = 0 // limitation // error
87+
val i: Int = ??? : A // error
88+
89+
case _: AltIndirectExprExact[Int] =>
90+
val a: A = 0 // limitation // error
91+
val i: Int = ??? : A // error
92+
}
93+
}

‎tests/neg/structural-recursive-both2-gadt.scala‎

Lines changed: 93 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,93 @@
1+
// This file is part of tests for inferring GADT constraints from type members,
2+
// which needed to be reverted because of soundness issues.
3+
//
4+
// Lines with "// limitation" are the ones that we could soundly allow.
5+
object Test {
6+
7+
trait Expr { type T }
8+
trait IntLit extends Expr { type T <: Int }
9+
trait IntExpr extends Expr { type T = Int }
10+
11+
type ExprSub[+A] = Expr { type T <: A }
12+
type ExprExact[A] = Expr { type T = A }
13+
14+
trait IndirectIntLit extends Expr { type S <: Int; type T = S }
15+
trait IndirectIntExpr extends Expr { type S = Int; type T = S }
16+
17+
type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
18+
type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
19+
type IndirectExprExact[A] = Expr { type S = A; type T = S }
20+
21+
trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
22+
trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
23+
24+
type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
25+
type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
26+
type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
27+
28+
def foo[A](e: AltIndirectExprExact[A]) = e match {
29+
case _: IndirectIntLit =>
30+
val a: A = 0 // error
31+
val i: Int = ??? : A // limitation // error
32+
33+
case _: IndirectExprSub[Int] =>
34+
val a: A = 0 // error
35+
val i: Int = ??? : A // limitation // error
36+
37+
case _: IndirectExprSub2[Int] =>
38+
val a: A = 0 // error
39+
val i: Int = ??? : A // limitation // error
40+
41+
case _: IndirectIntExpr =>
42+
val a: A = 0 // limitation // error
43+
val i: Int = ??? : A // limitation // error
44+
45+
case _: IndirectExprExact[Int] =>
46+
val a: A = 0 // limitation // error
47+
val i: Int = ??? : A // limitation // error
48+
}
49+
50+
def bar[A](e: AltIndirectExprSub[A]) = e match {
51+
case _: IndirectIntLit =>
52+
val a: A = 0 // error
53+
val i: Int = ??? : A // error
54+
55+
case _: IndirectExprSub[Int] =>
56+
val a: A = 0 // error
57+
val i: Int = ??? : A // error
58+
59+
case _: IndirectExprSub2[Int] =>
60+
val a: A = 0 // error
61+
val i: Int = ??? : A // error
62+
63+
case _: IndirectIntExpr =>
64+
val a: A = 0 // limitation // error
65+
val i: Int = ??? : A // error
66+
67+
case _: IndirectExprExact[Int] =>
68+
val a: A = 0 // limitation // error
69+
val i: Int = ??? : A // error
70+
}
71+
72+
def baz[A](e: AltIndirectExprSub2[A]) = e match {
73+
case _: IndirectIntLit =>
74+
val a: A = 0 // error
75+
val i: Int = ??? : A // error
76+
77+
case _: IndirectExprSub[Int] =>
78+
val a: A = 0 // error
79+
val i: Int = ??? : A // error
80+
81+
case _: IndirectExprSub2[Int] =>
82+
val a: A = 0 // error
83+
val i: Int = ??? : A // error
84+
85+
case _: IndirectIntExpr =>
86+
val a: A = 0 // limitation // error
87+
val i: Int = ??? : A // error
88+
89+
case _: IndirectExprExact[Int] =>
90+
val a: A = 0 // limitation // error
91+
val i: Int = ??? : A // error
92+
}
93+
}

‎tests/neg/structural-recursive-pattern-gadt.scala‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
// This file is part of tests for inferring GADT constraints from type members,
2+
// which needed to be reverted because of soundness issues.
3+
//
4+
// Lines with "// limitation" are the ones that we could soundly allow.
5+
object Test {
6+
7+
trait Expr { type T }
8+
trait IntLit extends Expr { type T <: Int }
9+
trait IntExpr extends Expr { type T = Int }
10+
11+
type ExprSub[+A] = Expr { type T <: A }
12+
type ExprExact[A] = Expr { type T = A }
13+
14+
trait IndirectIntLit extends Expr { type S <: Int; type T = S }
15+
trait IndirectIntExpr extends Expr { type S = Int; type T = S }
16+
17+
type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
18+
type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
19+
type IndirectExprExact[A] = Expr { type S = A; type T = S }
20+
21+
trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
22+
trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
23+
24+
type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
25+
type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
26+
type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
27+
28+
def foo[A](e: ExprExact[A]) = e match {
29+
case _: IndirectIntLit =>
30+
val a: A = 0 // error
31+
val i: Int = ??? : A // limitation // error
32+
33+
case _: IndirectExprSub[Int] =>
34+
val a: A = 0 // error
35+
val i: Int = ??? : A // limitation // error
36+
37+
case _: IndirectExprSub2[Int] =>
38+
val a: A = 0 // error
39+
val i: Int = ??? : A // limitation // error
40+
41+
case _: IndirectIntExpr =>
42+
val a: A = 0 // limitation // error
43+
val i: Int = ??? : A // limitation // error
44+
45+
case _: IndirectExprExact[Int] =>
46+
val a: A = 0 // limitation // error
47+
val i: Int = ??? : A // limitation // error
48+
}
49+
50+
def bar[A](e: ExprSub[A]) = e match {
51+
case _: IndirectIntLit =>
52+
val a: A = 0 // error
53+
val i: Int = ??? : A // error
54+
55+
case _: IndirectExprSub[Int] =>
56+
val a: A = 0 // error
57+
val i: Int = ??? : A // error
58+
59+
case _: IndirectExprSub2[Int] =>
60+
val a: A = 0 // error
61+
val i: Int = ??? : A // error
62+
63+
case _: IndirectIntExpr =>
64+
val a: A = 0 // limitation // error
65+
val i: Int = ??? : A // error
66+
67+
case _: IndirectExprExact[Int] =>
68+
val a: A = 0 // limitation // error
69+
val i: Int = ??? : A // error
70+
}
71+
}

‎tests/neg/structural-recursive-scrutinee-gadt.scala‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
// This file is part of tests for inferring GADT constraints from type members,
2+
// which needed to be reverted because of soundness issues.
3+
//
4+
// Lines with "// limitation" are the ones that we could soundly allow.
5+
object Test {
6+
7+
trait Expr { type T }
8+
trait IntLit extends Expr { type T <: Int }
9+
trait IntExpr extends Expr { type T = Int }
10+
11+
type ExprSub[+A] = Expr { type T <: A }
12+
type ExprExact[A] = Expr { type T = A }
13+
14+
trait IndirectIntLit extends Expr { type S <: Int; type T = S }
15+
trait IndirectIntExpr extends Expr { type S = Int; type T = S }
16+
17+
type IndirectExprSub[+A] = Expr { type S <: A; type T = S }
18+
type IndirectExprSub2[A] = Expr { type S = A; type T <: S }
19+
type IndirectExprExact[A] = Expr { type S = A; type T = S }
20+
21+
trait AltIndirectIntLit extends Expr { type U <: Int; type T = U }
22+
trait AltIndirectIntExpr extends Expr { type U = Int; type T = U }
23+
24+
type AltIndirectExprSub[+A] = Expr { type U <: A; type T = U }
25+
type AltIndirectExprSub2[A] = Expr { type U = A; type T <: U }
26+
type AltIndirectExprExact[A] = Expr { type U = A; type T = U }
27+
28+
def foo[A](e: IndirectExprExact[A]) = e match {
29+
case _: IntLit =>
30+
val a: A = 0 // error
31+
val i: Int = ??? : A // limitation // error
32+
33+
case _: ExprSub[Int] =>
34+
val a: A = 0 // error
35+
val i: Int = ??? : A // limitation // error
36+
37+
case _: IntExpr =>
38+
val a: A = 0 // limitation // error
39+
val i: Int = ??? : A // limitation // error
40+
41+
case _: ExprExact[Int] =>
42+
val a: A = 0 // limitation // error
43+
val i: Int = ??? : A // limitation // error
44+
}
45+
46+
def bar[A](e: IndirectExprSub[A]) = e match {
47+
case _: IntLit =>
48+
val a: A = 0 // error
49+
val i: Int = ??? : A // error
50+
51+
case _: ExprSub[Int] =>
52+
val a: A = 0 // error
53+
val i: Int = ??? : A // error
54+
55+
case _: IntExpr =>
56+
val a: A = 0 // limitation // error
57+
val i: Int = ??? : A // error
58+
59+
case _: ExprExact[Int] =>
60+
val a: A = 0 // limitation // error
61+
val i: Int = ??? : A // error
62+
}
63+
64+
def baz[A](e: IndirectExprSub2[A]) = e match {
65+
case _: IntLit =>
66+
val a: A = 0 // error
67+
val i: Int = ??? : A // error
68+
69+
case _: ExprSub[Int] =>
70+
val a: A = 0 // error
71+
val i: Int = ??? : A // error
72+
73+
case _: IntExpr =>
74+
val a: A = 0 // limitation // error
75+
val i: Int = ??? : A // error
76+
77+
case _: ExprExact[Int] =>
78+
val a: A = 0 // limitation // error
79+
val i: Int = ??? : A // error
80+
}
81+
}

0 commit comments

Comments
 (0)