GADT pattern matching issue

[sir-wabbit]

sealed trait Foo[A]
final case class Bar[X]() extends Foo[List[X]]

def foo[A](foo: Foo[A], a: A): Int = foo match {
    case Bar() => a.length
}

-- [E008] Member Not Found Error: test.scala:7:24 ------------------------------
7 |        case Bar() => a.length
  |                      ^^^^^^^^
  |        value length is not a member of A
  |
  |        where:    A is a type in method foo which is an alias of List[A$1]
one error found

Possibly already part of #4076. Notice that the error message actually says that A = List[a]!

[sir-wabbit]

sealed trait Foo[A, B]
final case class Bar[X]() extends Foo[X, X => Int]

def foo[A, B](value: Foo[A, B], a: A, b: B): Int = value match {
    case Bar() => b(a)
}

-- [E050] Reference Error: test.scala:8:22 -------------------------------------
8 |        case Bar() => b(a)
  |                      ^
  |                      value b does not take parameters

longer explanation available when compiling with `-explain`
one error found

[sir-wabbit]

✅Both

sealed trait Foo[A, B]
final case class Bar[X]() extends Foo[X, X]

def foo[A, B](value: Foo[A, B], a: A): B = value match {
    case Bar() => a
}

and

sealed trait Foo[A, B]
final case class Bar[X](x: X) extends Foo[X, X]

def foo[A, B](value: Foo[A, B], a: A => Int): B = value match {
    case Bar(x) => a(x); x
}

work but give what I think is a spurious warning

-- Warning: test.scala:8:9 -----------------------------------------------------
8 |    case Bar() => a
  |         ^^^^^
  |         the type test for G.Bar[A] cannot be checked at runtime
one warning found

[sir-wabbit]

sealed trait Foo[F[_]]
case object Bar extends Foo[Option]

def foo[F[_]](value: Foo[F], a: F[Int]): Option[Int] = value match {
    case Bar => a.map(_ + 1)
}

doesn't work

-- [E008] Member Not Found Error: test.scala:8:18 ------------------------------
8 |    case Bar => a.map(_ + 1)
  |                ^^^^^
  |           value map is not a member of F[Int] - did you mean a.==?
  |
  |           where:    F is a type in method foo which is an alias of Option
one error found

Notice that the error message actually says that F = Option!

[sir-wabbit]

✅Both

sealed trait Foo[F[_], G[_]]
final case class Bar[R[_]]() extends Foo[R, R]

def foo[F[_], G[_]](value: Foo[F, G], a: F[Int]): G[Int] = value match {
    case Bar() => a
}

and

sealed trait Foo[F[_], A]
final case class Bar[R[_]]() extends Foo[R, R[Int]]

def foo[F[_], A](value: Foo[F, A], a: A): F[Int] = value match {
    case Bar() => a
}

work but give 2 spurious warnings:

-- [E029] Pattern Match Exhaustivity Warning: test.scala:7:59 ------------------
7 |def foo[F[_], G[_]](value: Foo[F, G], a: F[Int]): G[Int] = value match {
  |                                                           ^^^^^
  |                                      match may not be exhaustive.
  |
  |                                      It would fail on pattern case: Bar()

longer explanation available when compiling with `-explain`
-- Warning: test.scala:8:9 -----------------------------------------------------
8 |    case Bar() => a
  |         ^^^^^
  |         the type test for G.Bar[F] cannot be checked at runtime
two warnings found

[abgruszecki]

Note that the following do compile:

    sealed trait Foo[A]
    final case class Bar[X]() extends Foo[List[X]]

    def foo[A](foo: Foo[A], a: A): Int = foo match {
      case Bar() => (a : List[_]).length
    }

    sealed trait Foo[A, B]
    final case class Bar[X]() extends Foo[X, X => Int]

    def foo[A, B](value: Foo[A, B], a: A, b: B): Int = value match {
      case _: Bar[x] => (b : x => Int)(a)
    }

This is, I think, exactly the same problem that one of previous versions of opaque types had - member lookup simply does not check GADT constraints due to caching etc.

In all cases, this should be possible to manually circumvent by ascribing a correct type.

[abgruszecki]

Assigning low prio: ideally we'd like to have this fixed and we have an idea of how to fix it (use the "magic" TermRefs like in #6344), but the fix is finicky, potentially performance-costly and it's unclear whether this is a significant problem since there is a clear workaround.

[wdanilo]

@AleksanderBG I don't agree that there is a clear workaround. Sure, manual typing can make this code compile, but makes it very tedious to write, much more error prone, harder to refactor and breaks a lot of power of GADTs. I encountered this problem several times already and it's a high-priority for me - until its fixed, I would not consider GADTs in Dotty to be "working properly".

[abgruszecki]

@wdanilo Right now I'd agree with you - by now I've seen multiple examples of this issue actually manifesting in practice and I think it should be fixed. I'll see to fixing it when I'll have the time.

Removing low prio and opening #7044 in favour of this one, since it explains the problem much clearer.

[wdanilo]

@AleksanderBG Thank you, highly appreciated!