Verify HKT GADT code

[smarter]

Minimized code

sealed trait Test[+F[_], +A] extends Product with Serializable

object Test {

  implicit class Syntax[F[_], A](val self: Test[F, A]) extends AnyVal {

    def fold[B](completed: F[A] => B): B = self match {
      case Completed(fa) => completed(fa)
    }
  }


  final case class Completed[F[_], A](fa: F[A]) extends Test[F, A]
}

Output

Dotty 0.24.0-RC1:

[error] -- [E007] Type Mismatch Error: /Users/daniel/Development/Scala/cats-effect/core/src/main/scala/cats/effect/Test.scala:26:38 
[error] 26 |      case Completed(fa) => completed(fa)
[error]    |                                      ^^
[error]    |                 Found:    (fa : F$1[A$1])
[error]    |                 Required: F[A]
[error]    |
[error]    |                 where:    A$1 is a type in method fold with bounds <: A
[error]    |                           F$1 is a type in method fold with bounds <: F

Dotty master:

-- [E029] Pattern Match Exhaustivity Warning: try/dj.scala:7:43 ----------------
7 |    def fold[B](completed: F[A] => B): B = self match {
  |                                           ^^^^
  |                          match may not be exhaustive.
  |
  |                          It would fail on pattern case: Test.Completed(_)

longer explanation available when compiling with `-explain`
-- Warning: try/dj.scala:3:7 ---------------------------------------------------
3 |object Test {
  |       ^
  |       the type test for Test.Completed[?, ?] cannot be checked at runtime
2 warnings found

Expectation

I think 0.24.0-RC1 got it right, current master is missing the error and producing some weird warnings.

[smarter]

Hmm sorry, this is about GADT, not about exhaustivity checking, there might be some exhaustivity checking issue but they're not what's preventing the initial error.

[abgruszecki]

@smarter seems like letting GADT refinements be used for HKTs didn't go so well. Do you suppose there's anything I could read on how subtyping is supposed to work for HKTs in presence of variance before I fiddle with that code again?

[smarter]

Do you suppose there's anything I could read on how subtyping is supposed to work for HKTs in presence of variance before I fiddle with that code again?

Like a write-up or paper? I don't think that exists.

[LPTK]

I haven't read it yet, but maybe the closest thing is @sstucki's thesis.

[smarter]

I don't think variance was treated in Sandro's thesis (turns out things are already really complicated without it!)

[sstucki]

No, unfortunately I did not manage to include variances in my thesis. Adding them is WIP but turned out to be much harder than I thought. The issue is that having variances, currying and dependent types in the same calculus destroys some nice properties that one normally uses to model such theories. For the time being, it's an open problem to combine these, to the best of my knowledge.

For many instances, however, we don't need to worry about dependent kinds (in particular if no type bounds are involved). And for that case, we have a theory. See for example the following paper by Andreas Abel (you can safely ignore the bit about sized types if you're only interested in variances and HK types):

Andreas Abel, Polarized Subtyping for Sized Types. MSCS, vol. 18, pp. 797-822, special issue on subtyping. Cambridge University Press, 2008. PDF

[sstucki]

Hum, the interplay between variances and refinement here hurts my head. I'm honestly not sure how this would be desugared into any formal system I know of.

But I think @smarter is right that the 0.24.0-RC1 behavior is correct, because Test is covariant in it's arguments, we cannot assume that the F and A from the Complete instance are the same as the parameters passed to the Test type constructor.