add more gadt exhaustivity check tests

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

@@ -600,38 +600,28 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   def instantiate(tp1: NamedType, tp2: Type)(implicit ctx: Context): Type = {
     // expose abstract type references to their bounds or tvars according to variance
     class AbstractTypeMap(maximize: Boolean)(implicit ctx: Context) extends TypeMap {
-      def expose(tp: TypeRef): Type = {
-        val lo = this(tp.info.loBound)
-        val hi = this(tp.info.hiBound)
-        val exposed =
-          if (variance == 0)
-            newTypeVar(TypeBounds(lo, hi))
-          else if (variance == 1)
-            if (maximize) hi else lo
-          else
-            if (maximize) lo else hi
-
-        debug.println(s"$tp exposed to =====> $exposed")
-        exposed
-      }
+      def expose(lo: Type, hi: Type): Type =
+        if (variance == 0)
+          newTypeVar(TypeBounds(lo, hi))
+        else if (variance == 1)
+          if (maximize) hi else lo
+        else
+          if (maximize) lo else hi
 
       def apply(tp: Type): Type = tp match {
         case tp: TypeRef if tp.underlying.isInstanceOf[TypeBounds] =>
+          val lo = this(tp.info.loBound)
+          val hi = this(tp.info.hiBound)
           // See tests/patmat/gadt.scala  tests/patmat/exhausting.scala  tests/patmat/t9657.scala
-          expose(tp)
+          val exposed = expose(lo, hi)
+          debug.println(s"$tp exposed to =====> $exposed")
+          exposed
 
         case AppliedType(tycon: TypeRef, args) if tycon.underlying.isInstanceOf[TypeBounds] =>
           val args2 = args.map(this)
           val lo = this(tycon.info.loBound).applyIfParameterized(args2)
           val hi = this(tycon.info.hiBound).applyIfParameterized(args2)
-          val exposed =
-            if (variance == 0)
-              newTypeVar(TypeBounds(lo, hi))
-            else if (variance == 1)
-              if (maximize) hi else lo
-            else
-              if (maximize) lo else hi
-
+          val exposed = expose(lo, hi)
           debug.println(s"$tp exposed to =====> $exposed")
           exposed
 

tests/patmat/gadt2.scala

@@ -0,0 +1,16 @@
+sealed trait Nat[+T]
+case class Zero() extends Nat[Nothing]
+case class Succ[T]() extends Nat[T]
+
+// +N is incorrect, as in `foo` we can have `N = Zero | Succ[Zero]`,
+// then it's correct for exhaustivity check to produce two warnings.
+sealed trait Vect[N <: Nat[_], +T]
+case class VN[T]() extends Vect[Zero, T]
+case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]
+
+object Test {
+  def foo[N <: Nat[_], A, B](v1: Vect[N, A], v2: Vect[N, B]) = (v1, v2) match {
+    case (VN(), VN()) => 1
+    case (VC(x, xs), VC(y, ys)) => 2
+  }
+}

tests/patmat/gadt4.check

@@ -0,0 +1 @@
+12: Pattern Match Exhaustivity: (VC(_, _), VN()), (VN(), VC(_, _))

tests/patmat/gadt2.scala.ignore → tests/patmat/gadt4.scala

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

tests/patmat/gadt5.check

@@ -0,0 +1 @@
+63: Pattern Match Exhaustivity: (Try3.VC(_, _), Try3.VN()), (Try3.VN(), Try3.VC(_, _))

tests/patmat/gadt5.scala

@@ -0,0 +1,89 @@
+object Try1 {
+  // type-level naturals
+  sealed trait TNat
+  sealed trait TZero extends TNat
+  sealed trait TSucc[T] extends TNat
+
+  //reflect TNat at the value level; given n: Nat[T], n and T represent the same number.
+  //This is what Haskellers call "singleton types" and took from Omega.
+  // The point is that we can use such a number both at compile-time and at runtime,
+  // but of course the runtime representation is not erased.
+  //And this constrains the type argument of `Nat` to be of type `TNat` — though you could add bounds for it.
+
+  sealed trait Nat[+T]
+  case class Zero() extends Nat[TZero]
+  case class Succ[T](n: Nat[T]) extends Nat[TSucc[T]]
+
+  //We can index Vect with the types of value-level Nat, but this is a bit overkill. Still, no warnings.
+  sealed trait Vect[N <: Nat[_], +T]
+  case class VN[T]() extends Vect[Zero, T]
+  case class VC[T, N <: Nat[_]](x: T, xs: Vect[N, T]) extends Vect[Succ[N], T]
+
+  object Test {
+    def foo[N <: Nat[_], A, B](v1: Vect[N, A], v2: Vect[N, B]) =
+      (v1, v2) match {
+        case (VN(), VN())           => 1
+        case (VC(x, xs), VC(y, ys)) => 2
+      }
+  }
+}
+
+//Since we didn't need value-level numbers, let's drop them:
+object Try2 {
+  sealed trait TNat
+  sealed trait TZero extends TNat
+  sealed trait TSucc[T] extends TNat
+
+  sealed trait Vect[N <: TNat, +T]
+  case class VN[T]() extends Vect[TZero, T]
+  case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
+
+  object Test {
+    def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
+      (v1, v2) match {
+        case (VN(), VN())           => 1
+        case (VC(x, xs), VC(y, ys)) => 2
+      }
+  }
+}
+
+//Same as Try2, but now `Vect` is covariant in `N` so we get the warning you described.
+object Try3 {
+  sealed trait TNat
+  sealed trait TZero extends TNat
+  sealed trait TSucc[T] extends TNat
+
+  sealed trait Vect[+N <: TNat, +T]
+  case class VN[T]() extends Vect[TZero, T]
+  case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
+
+  object Test {
+    def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
+      //Warnings expected here!
+      (v1, v2) match {
+        case (VN(), VN())           => 1
+        case (VC(x, xs), VC(y, ys)) => 2
+      }
+    //a call-site which would cause a MatchError (maybe that error should be tested)
+    def bar = foo[TZero | TSucc[_], Int, String](VN(), VC("", VN()))
+  }
+}
+
+//Same as Try3, but now `Vect` is invariant
+object Try4 {
+  sealed trait TNat
+  sealed trait TZero extends TNat
+  sealed trait TSucc[T] extends TNat
+
+  sealed trait Vect[N <: TNat, +T]
+  case class VN[T]() extends Vect[TZero, T]
+  case class VC[T, N <: TNat](x: T, xs: Vect[N, T]) extends Vect[TSucc[N], T]
+
+  object Test {
+    def foo[N <: TNat, A, B](v1: Vect[N, A], v2: Vect[N, B]) =
+      (v1, v2) match {
+        case (VN(), VN())           => 1
+        case (VC(x, xs), VC(y, ys)) => 2
+      }
+  }
+}