Interaction of partial unification and GADT pattern matching

[TomasMikula]

To reproduce, try to compile the following snippet by scalac 2.12.2 with -Ypartial-unification.

import scala.language.higherKinds

sealed abstract class Foo[F[_], A]
case class Bar[F[_]](fa: F[Int]) extends Foo[F, Unit]

class Fun[A, B]

object Main {

  def f[A, B](foo: Foo[({ type λ[b] = Fun[A, b] })#λ, B]): Unit = foo match {
    case Bar(_) => ()
  }
}

It results in

main.scala:11: error: constructor of type Bar[F] cannot be uniquely instantiated to expected type Foo[[b]Fun[?,b],?]
 --- because ---
undetermined type
    case Bar(_) => ()
         ^

Note that all of these three aspects are necessary to reproduce the bug:

1. Foo is a GADT. Changing Bar to

   case class Bar[F[_], A](fa: F[Int]) extends Foo[F, A]

   is sufficient to make it compile.

2. A is a type parameter of f. Pulling it out, as in

   object Main {
     class A
     def f[B](foo: Foo[({ type λ[b] = Fun[A, b] })#λ, B]): Unit = foo match {
       case Bar(_) => ()
     }
   }

   or in

   class Main[A] {
   
     def f[B](foo: Foo[({ type λ[b] = Fun[A, b] })#λ, B]): Unit = foo match {
       case Bar(_) => ()
     }
   }

   is sufficient to make it compile.

3. Partial unification is involved on the type of parameter foo. Changing f to

   def f[F[_], B](foo: Foo[F, B]): Unit = foo match {
     case Bar(_) => ()
   }

   is sufficient to make it compile.

[joroKr21]

When refining the GADT bounds, scalac replaces both A and B with wildcards (?). Then unifying Bar[?F] with Foo[[b]Fun[?,b],?] leads to the solution ?F = [b]Fun[?,b] which is not complete because it contains ?. If the compiler was smart enough to try replacing only B with a wildcard it would give the solution ?F = [b]Fun[A,b] but that may be too much to ask (combinatorial explosion?). I don't think this is fixable under the current GADT scheme.

The workaround is to specify the type of F explicitly:

def f[A, B](foo: Foo[({ type λ[b] = Fun[A, b] })#λ, B]): Unit = foo match {
  case bar: Bar[({ type λ[b] = Fun[A, b] })#λ] => ()
}

Relevant method:
https://github.com/scala/scala/blob/284a9c03c650c76e2b5295fee5c03565bcdf5246/src/compiler/scala/tools/nsc/typechecker/Infer.scala#L1043-L1122

[TomasMikula]

If the compiler was smart enough to try replacing only B with a wildcard [...]

I don't understand why it would replace type variables from outer scope with wildcards at all.

[joroKr21]

The method I linked does two tries. First is without wildcards and the second one is approximated with wildcards. The first try fails because Bar[?F] <:< Foo[[b]Fun[A,b],B] is false (B is not Unit) so we fallback to the second try.

[joroKr21]

It works in dotty, although it gives a warning:

scala> def f[A, B](foo: Foo[[b] => Fun[A, b], B]): Unit = foo match { case Bar(_) => () }
1 |def f[A, B](foo: Foo[[b] => Fun[A, b], B]): Unit = foo match { case Bar(_) => () }
  |                                                                    ^^^^^^
  |      the type test for Bar[[b] => Fun[A, b]] cannot be checked at runtime
def f[A, B](foo: Foo[[b] => Fun[A, b], B]): Unit

[TomasMikula]

The first try fails because Bar[?F] <:< Foo[[b]Fun[A,b],B] is false (B is not Unit)

Oh well, the compiler should infer that, locally inside that case Bar(_) clause, B is Unit.

[joroKr21]

But that's not how it works. Inside the method B is a skolem, not a type variable. There is some special handling of GADTs but it's limited.