add more gadt exhaustivity check tests

[liufengyun]

add more gadt exhaustivity check tests

[Blaisorblade]

This is not intended to be a correct representation of Peano numerals, right? Not only for the +T but also because T in Succ is completely unconstrained...

[liufengyun]

Yes, good catch, I forgot where I got the test case, I tried adding the bounds and remove the variance on Nat, it doesn't change the result. Le 14 févr. 2018 6:07 PM, "Paolo G. Giarrusso" <[email protected]> a écrit :

…

***@***.**** commented on this pull request. ------------------------------ In tests/patmat/gadt2.scala <#3999 (comment)>: > @@ -0,0 +1,16 @@ +sealed trait Nat[+T] +case class Zero() extends Nat[Nothing] +case class Succ[T]() extends Nat[T] This is not intended to be a correct representation of Peano numerals, right? Not only for the +T but also because T in Succ is completely unconstrained... — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#3999 (review)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAuDyevAMIsoYnG-kDA_kcm8CwdzyQ0rks5tUxLHgaJpZM4SFpXp> .

[Blaisorblade]

I should have spelled out the encoding I had in mind. Please take a look especially at the comments.

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 here!
      (v1, v2) match {
        case (VN(), VN())           => 1
        case (VC(x, xs), VC(y, ys)) => 2
      }
  }
}

[liufengyun]

@Blaisorblade Thanks for the encoding. If I were correct, as long as N is covariant in Vect, it's possible to have N = TZero | TSucc[_] in foo, thus it's correct to report the warnings.

[Blaisorblade]

@liufengyun IIUC, triggering N = TZero | TSucc[_] in Try3 requires extending VN or VC and refining the covariant type parameter ? If so, the warning can be avoided if both classes are final; IIRC Scalac manages to figure this out in some cases.

But if we forbid such covariant refinements as @smarter would like (see #3989), the warning becomes unnecessary.
And maybe case classes extending sealed should be final automatically, again making this warning unnecessary. In my 2013 paper I claimed I had use cases in SQuOpt for non-final children of sealed traits, I'll have to dig for them and see how crucial they are.

And to be sure: Even though all variants give the same warnings, we might want to add (with more priority) the encodings we want to keep supporting, more than the ones which might or might not work.

[liufengyun]

@Blaisorblade Triggering N = TZero | TSucc[_] doesn't require extending VN and VC, it's just normal type application with union types. Note that this behaviour only exists in Dotty because it support union types. In another word, in any theory that supports union types, we can not be sure that the same type parameter T in different positions always refer to the same type.

[Blaisorblade]

Triggering N = TZero | TSucc[_] doesn't require extending VN and VC, it's just normal type application with union types.

Ah, do you mean foo[TZero | TSucc[_], Int, String](VN(), VC("", VN()))? Ah, the crucial point is you can upcast Vec, I see! Very interesting and annoying.

In another word, in any theory that supports union types, we can not be sure that the same type parameter T in different positions always refer to the same type.

I see what you mean, but a type variable still is bound to one type at a time. We just have more type variables: due to covariance the argument for N to foo need not be the same as the one given to the Vec constructor, and union types give a surprising way to exploit that; intersection types and covariant type refinement give another.

[Blaisorblade]

@liufengyun Hope adding my commits here is OK

[liufengyun]

Sure, thanks a lot @Blaisorblade !

[Blaisorblade]

Also assigning myself so I come back to it.

[Blaisorblade]

But if we forbid such covariant refinements as @smarter would like (see #3989), the warning becomes unnecessary.

Discussion with Martin today suggested we should forbid "covariant refinement" from case classes only (since apparently next to nobody but the compilers inherit from case classes), while we need to keep allowing it for non-case classes (that's even used in 2.8 collections, not sure if that's the example Martin had in mind). See #4014 for details.

[Blaisorblade]

@liufengyun looks good to go, or do you want to add something? Seems mergeable!

[liufengyun]

Thanks @Blaisorblade , I've no more things on my side.