diff --git a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala index b1fc0515392b..c47022be10af 100644 --- a/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala +++ b/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 diff --git a/tests/patmat/gadt2.scala b/tests/patmat/gadt2.scala new file mode 100644 index 000000000000..f6a3978c773c --- /dev/null +++ b/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 + } +} diff --git a/tests/patmat/gadt4.check b/tests/patmat/gadt4.check new file mode 100644 index 000000000000..3b9e89f171e8 --- /dev/null +++ b/tests/patmat/gadt4.check @@ -0,0 +1 @@ +12: Pattern Match Exhaustivity: (VC(_, _), VN()), (VN(), VC(_, _)) \ No newline at end of file diff --git a/tests/patmat/gadt2.scala.ignore b/tests/patmat/gadt4.scala similarity index 75% rename from tests/patmat/gadt2.scala.ignore rename to tests/patmat/gadt4.scala index 80ba72c70884..d5212be2d406 100644 --- a/tests/patmat/gadt2.scala.ignore +++ b/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] diff --git a/tests/patmat/gadt5.check b/tests/patmat/gadt5.check new file mode 100644 index 000000000000..3709cbf15fa8 --- /dev/null +++ b/tests/patmat/gadt5.check @@ -0,0 +1 @@ +63: Pattern Match Exhaustivity: (Try3.VC(_, _), Try3.VN()), (Try3.VN(), Try3.VC(_, _)) diff --git a/tests/patmat/gadt5.scala b/tests/patmat/gadt5.scala new file mode 100644 index 000000000000..8cc9e77f1cdd --- /dev/null +++ b/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 + } + } +}