Skip to content

Commit 6e3f188

Browse files
BlaisorbladeBlaisorblade
authored
Merge pull request #3999 from dotty-staging/gadt-test
add more gadt exhaustivity check tests
2 parents e6b6480 + 50d91c1 commit 6e3f188

File tree

6 files changed

+122
-23
lines changed

6 files changed

+122
-23
lines changed

‎compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

Lines changed: 13 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -600,38 +600,28 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
600600
def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
601601
// expose abstract type references to their bounds or tvars according to variance
602602
class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
603-
def expose(tp: TypeRef): Type = {
604-
val lo = this(tp.info.loBound)
605-
val hi = this(tp.info.hiBound)
606-
val exposed =
607-
if (variance == 0)
608-
newTypeVar(TypeBounds(lo, hi))
609-
else if (variance == 1)
610-
if (maximize) hi else lo
611-
else
612-
if (maximize) lo else hi
613-
614-
debug.println(s"$tp exposed to =====> $exposed")
615-
exposed
616-
}
603+
def expose(lo: Type, hi: Type): Type =
604+
if (variance == 0)
605+
newTypeVar(TypeBounds(lo, hi))
606+
else if (variance == 1)
607+
if (maximize) hi else lo
608+
else
609+
if (maximize) lo else hi
617610

618611
def apply(tp: Type): Type = tp match {
619612
case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
613+
val lo = this(tp.info.loBound)
614+
val hi = this(tp.info.hiBound)
620615
// See tests/patmat/gadt.scala tests/patmat/exhausting.scala tests/patmat/t9657.scala
621-
expose(tp)
616+
val exposed = expose(lo, hi)
617+
debug.println(s"$tp exposed to =====> $exposed")
618+
exposed
622619

623620
case AppliedType(tycon: TypeRef, args) if tycon.underlying.isInstanceOf[TypeBounds] =>
624621
val args2 = args.map(this)
625622
val lo = this(tycon.info.loBound).applyIfParameterized(args2)
626623
val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
627-
val exposed =
628-
if (variance == 0)
629-
newTypeVar(TypeBounds(lo, hi))
630-
else if (variance == 1)
631-
if (maximize) hi else lo
632-
else
633-
if (maximize) lo else hi
634-
624+
val exposed = expose(lo, hi)
635625
debug.println(s"$tp exposed to =====> $exposed")
636626
exposed
637627

‎tests/patmat/gadt2.scala

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
sealed trait Nat[+T]
2+
case class Zero() extends Nat[Nothing]
3+
case class Succ[T]() extends Nat[T]
4+
5+
// +N is incorrect, as in `foo` we can have `N = Zero | Succ[Zero]`,
6+
// then it's correct for exhaustivity check to produce two warnings.
7+
sealed trait Vect[N <: Nat[_], +T]
8+
case class VN[T]() extends Vect[Zero, T]
9+
case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]
10+
11+
object Test {
12+
def foo[N <: Nat[_], A, B](v1: Vect[N, A], v2: Vect[N, B]) = (v1, v2) match {
13+
case (VN(), VN()) => 1
14+
case (VC(x, xs), VC(y, ys)) => 2
15+
}
16+
}

‎tests/patmat/gadt4.check

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
12: Pattern Match Exhaustivity: (VC(_, _), VN()), (VN(), VC(_, _))

‎tests/patmat/gadt2.scala.ignore renamed to ‎tests/patmat/gadt4.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ sealed trait Nat[+T]
22
case class Zero() extends Nat[Nothing]
33
case class Succ[T]() extends Nat[T]
44

5+
// +N is incorrect, as in `foo` we can have `N = Zero | Succ[Zero]`,
6+
// then it's correct for exhaustivity check to produce two warnings.
57
sealed trait Vect[+N <: Nat[_], +T]
68
case class VN[T]() extends Vect[Zero, T]
79
case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]

‎tests/patmat/gadt5.check

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
63: Pattern Match Exhaustivity: (Try3.VC(_, _), Try3.VN()), (Try3.VN(), Try3.VC(_, _))

‎tests/patmat/gadt5.scala

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
object Try1 {
2+
// type-level naturals
3+
sealed trait TNat
4+
sealed trait TZero extends TNat
5+
sealed trait TSucc[T] extends TNat
6+
7+
//reflect TNat at the value level; given n: Nat[T], n and T represent the same number.
8+
//This is what Haskellers call "singleton types" and took from Omega.
9+
// The point is that we can use such a number both at compile-time and at runtime,
10+
// but of course the runtime representation is not erased.
11+
//And this constrains the type argument of `Nat` to be of type `TNat` — though you could add bounds for it.
12+
13+
sealed trait Nat[+T]
14+
case class Zero() extends Nat[TZero]
15+
case class Succ[T](n: Nat[T]) extends Nat[TSucc[T]]
16+
17+
//We can index Vect with the types of value-level Nat, but this is a bit overkill. Still, no warnings.
18+
sealed trait Vect[N <: Nat[_], +T]
19+
case class VN[T]() extends Vect[Zero, T]
20+
case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]
21+
22+
object Test {
23+
def foo[N <: Nat[_], A, B](v1: Vect[N, A], v2: Vect[N, B]) =
24+
(v1, v2) match {
25+
case (VN(), VN()) => 1
26+
case (VC(x, xs), VC(y, ys)) => 2
27+
}
28+
}
29+
}
30+
31+
//Since we didn't need value-level numbers, let's drop them:
32+
object Try2 {
33+
sealed trait TNat
34+
sealed trait TZero extends TNat
35+
sealed trait TSucc[T] extends TNat
36+
37+
sealed trait Vect[N <: TNat, +T]
38+
case class VN[T]() extends Vect[TZero, T]
39+
case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
40+
41+
object Test {
42+
def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
43+
(v1, v2) match {
44+
case (VN(), VN()) => 1
45+
case (VC(x, xs), VC(y, ys)) => 2
46+
}
47+
}
48+
}
49+
50+
//Same as Try2, but now `Vect` is covariant in `N` so we get the warning you described.
51+
object Try3 {
52+
sealed trait TNat
53+
sealed trait TZero extends TNat
54+
sealed trait TSucc[T] extends TNat
55+
56+
sealed trait Vect[+N <: TNat, +T]
57+
case class VN[T]() extends Vect[TZero, T]
58+
case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
59+
60+
object Test {
61+
def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
62+
//Warnings expected here!
63+
(v1, v2) match {
64+
case (VN(), VN()) => 1
65+
case (VC(x, xs), VC(y, ys)) => 2
66+
}
67+
//a call-site which would cause a MatchError (maybe that error should be tested)
68+
def bar = foo[TZero | TSucc[_], Int, String](VN(), VC("", VN()))
69+
}
70+
}
71+
72+
//Same as Try3, but now `Vect` is invariant
73+
object Try4 {
74+
sealed trait TNat
75+
sealed trait TZero extends TNat
76+
sealed trait TSucc[T] extends TNat
77+
78+
sealed trait Vect[N <: TNat, +T]
79+
case class VN[T]() extends Vect[TZero, T]
80+
case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
81+
82+
object Test {
83+
def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
84+
(v1, v2) match {
85+
case (VN(), VN()) => 1
86+
case (VC(x, xs), VC(y, ys)) => 2
87+
}
88+
}
89+
}

0 commit comments

Comments
 (0)