Skip to content

Commit 1763131

Browse files
committed
Test for creative GADT constraint usage
1 parent fe93ddc commit 1763131

File tree

1 file changed

+66
-0
lines changed

1 file changed

+66
-0
lines changed
+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
object buffer {
2+
object EssaInt {
3+
def unapply(i: Int): Some[Int] = Some(i)
4+
}
5+
6+
case class Inv[T](t: T)
7+
8+
enum EQ[A, B] { case Refl[T]() extends EQ[T, T] }
9+
enum SUB[A, +B] { case Refl[T]() extends SUB[T, T] } // A <: B
10+
11+
def test_eq1[A, B](eq: EQ[A, B], a: A, b: B): B =
12+
Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
13+
Inv(a) match { case Inv(_: Int) => // a >: Sko(Int) | Sko(Int)
14+
eq match { case EQ.Refl() => // a = b
15+
val success: A = b
16+
val fail: A = 0 // error
17+
0 // error
18+
}
19+
}
20+
}
21+
22+
def test_eq2[A, B](eq: EQ[A, B], a: A, b: B): B =
23+
Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
24+
Inv(b) match { case Inv(_: Int) => // b >: Sko(Int)
25+
eq match { case EQ.Refl() => // a = b
26+
val success: A = b
27+
val fail: A = 0 // error
28+
0 // error
29+
}
30+
}
31+
}
32+
33+
def test_sub1[A, B](sub: SUB[A, B], a: A, b: B): B =
34+
Inv(b) match { case Inv(_: Int) => // b >: Sko(Int)
35+
Inv(b) match { case Inv(_: Int) => // b >: Sko(Int) | Sko(Int)
36+
sub match { case SUB.Refl() => // b >: a
37+
val success: B = a
38+
val fail: A = 0 // error
39+
0 // error
40+
}
41+
}
42+
}
43+
44+
def test_sub2[A, B](sub: SUB[A, B], a: A, b: B): B =
45+
Inv(a) match { case Inv(_: Int) => // a >: Sko(Int)
46+
Inv(b) match { case Inv(_: Int) => // b >: Sko(Int) | Sko(Int)
47+
sub match { case SUB.Refl() => // b >: a
48+
val success: B = a
49+
val fail: A = 0 // error
50+
0 // error
51+
}
52+
}
53+
}
54+
55+
56+
def test_sub_eq[A, B, C](sub: SUB[A|B, C], eqA: EQ[A, 5], eqB: EQ[B, 6]): C =
57+
sub match { case SUB.Refl() => // C >: A | B
58+
eqA match { case EQ.Refl() => // A = 5
59+
eqB match { case EQ.Refl() => // B = 6
60+
val fail1: A = 0 // error
61+
val fail2: B = 0 // error
62+
0 // error
63+
}
64+
}
65+
}
66+
}

0 commit comments

Comments
 (0)