GADT pattern matching fails to infer type equations

[TomasMikula]

Compiler version

3.0.0

Minimized code

enum Foo[T] {
  case Bar[F[_]](fu: List[F[Unit]]) extends Foo[F[Unit]]
}

def some1[T](foo: Foo[T]): Foo[Option[T]] =
  foo match {
    case Foo.Bar(fu) =>
      Foo.Bar(fu.map(Option(_)))
  }

// the same thing, but with type annotations and comments
def some2[T](foo: Foo[T]): Foo[Option[T]] =
  foo match {
    // capturing the type parameter of Bar into a type variale `f`
    case Foo.Bar(fu) : Foo.Bar[f] =>
      // now it is known that T = f[Unit]

      val fu1: List[Option[f[Unit]]] =
        fu.map(Option(_))

      val res: Foo[Option[f[Unit]]] =
        Foo.Bar[[x] =>> Option[f[x]]](fu1)

      // given that f[Unit] = T,
      // `res` should pass as a return value of type Foo[Option[T]]
      res
  }

Output

-- [E007] Type Mismatch Error: gadt.scala:8:28 ---------------------------------
8 |      Foo.Bar(fu.map(Option(_)))
  |                            ^
  |      Found:    (_$2 : F$1[Unit])
  |      Required: Unit
  |
  |      where:    F$1 is a type in method some1 with bounds <: [_$1] =>> Any

longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: gadt.scala:26:6 ---------------------------------
26 |      res
   |      ^^^
   |      Found:    (res : Foo[Option[f[Unit]]])
   |      Required: Foo[Option[T]]
   |
   |      where:    f is a type in method some2 with bounds <: [_$1] =>> Any

longer explanation available when compiling with `-explain`
2 errors found

Expectation

The code should compile, the comments in the some2 method explain why.

[LPTK]

Here is a weird workaround:

def some1[T](foo: Foo[T]): Foo[Option[T]] =
  foo match {
    case foo: (foo.type & Foo.Bar[f]) =>
      Foo.Bar[[x] =>> Option[f[x]]](foo.fu.map(Option(_)))
  }

It does give off a spurious exhaustivity warning, probably for the same reason as in #12475 (comment)

[TomasMikula]

@LPTK Thanks for the workaround.

[dwijnand]

def some2 now compiles, provided you drop the unapply and just use the type test. Then you need the type variable to call the constructor.

[TomasMikula]

@dwijnand what version is "now", and what's the compiling code?

[dwijnand]

enum Foo[T] {
  case Bar[F[_]](fu: List[F[Unit]]) extends Foo[F[Unit]]
}

// the same thing, but with type annotations and comments
def some2[T](foo: Foo[T]): Foo[Option[T]] =
  foo match {
    // capturing the type parameter of Bar into a type variale `f`
    case bar : Foo.Bar[f] =>
      // now it is known that T = f[Unit]

      val fu = bar.fu

      val fu1: List[Option[f[Unit]]] =
        fu.map(Option(_))

      val res: Foo[Option[f[Unit]]] =
        Foo.Bar[[x] =>> Option[f[x]]](fu1)

      // given that f[Unit] = T,
      // `res` should pass as a return value of type Foo[Option[T]]
      res
  }

I just tested with 3.2.2.

[TomasMikula]

I just checked and your version compiles already in 3.0.0, so that doesn't show any improvement compared to when this issue was raised, just another workaround.

[dwijnand]

Then is the bug you're having that this minimisation doesn't compile?

enum Foo[T] {
  case Bar[F[_]](fu: List[F[Unit]]) extends Foo[F[Unit]]
}

def wrap[F[_]](fu2: List[Option[F[Unit]]]): Foo[Option[F[Unit]]] =
  Foo.Bar(fu2)