Another GADT typechecking error

[TomasMikula]

Compiler version

3.0.2-RC1

Minimized code

class Module[*[_, _]] {
  sealed trait Box[A]

  case class Box2x2[A, B, C, D](value: (A * B) * (C * D)) extends Box[(A * B) * (C * D)]

  def unbox2[X, Y](box: Box[X * Y]): (X * Y) =
    box match {
      case Box2x2(v) => v // we know that v has type ((a * b) * (c * d))
                          // for some types a, b, c, d,
                          // and that ((a * b) * (c * d)) = (X * Y),
                          // so v does have the expected return type (X * Y)
    }
}

Output

% ~/scala3-3.0.2-RC1/bin/scalac boxes.scala 
-- [E007] Type Mismatch Error: boxes.scala:8:24 --------------------------------
8 |      case Box2x2(v) => v // we know that v has type ((a * b) * (c * d))
  |                        ^
  |       Found:    (v : A$1 * B$1 * (C$1 * D$1))
  |       Required: X * Y
  |
  |       where:    * is a type in class Module with bounds <: [_, _] =>> Any

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

Expectation

The code should typecheck, as per the explanation in the code comment.

[LPTK]

I don't think there is any logic in place to deal with constraints of the form ((a * b) * (c * d)) = (X * Y). Note that the constraint cannot be decomposed because * is abstract and may not be injective. Currently GADT reasoning only operates on constraints on type variables, for better or for worse.

Workaround:

  def unbox2[X, Y](box: Box[X * Y]): (X * Y) = unbox2Aux(box)
  def unbox2Aux[A](box: Box[A]): A =
    box match
      case Box2x2(v) => v

[TomasMikula]

Note that the constraint cannot be decomposed because * is abstract and may not be injective.

That's right, but:

• this example does not need injectivity;
• injectivity already seems to be falsely assumed elsewhere anyway, see Unsoundness in GADT pattern matching (falsely assumed injectivity) #13080.

Workaround:

This is a problem with minimized examples: workaround might exist and not even look too bad, while on a realistic example, workarounds, if they exist at all, have a tremendous cost.

[LPTK]

• this example does not need injectivity;

I did not say the example needs injectivity. I just remarked that injectivity cannot be assumed here. If it could (for example, through an annotation), the problem would go away, and injectivity is something some people may be expecting, since it's the default in languages like Haskell.

Another workaround, as usual, is to encode all equational reasoning in lower- and upper- bounded abstract type members, and use explicit type ascriptions. It's also not ideal, but at least it's more explicit in advanced cases like this.

[dwijnand]

#fixed-in-scala2 😛

$ pbpaste > boxes.scala
$ m boxes.scala
class Module[*[_, _]] {
  sealed trait Box[A]

  case class Box2x2[A, B, C, D](value: (A * B) * (C * D)) extends Box[(A * B) * (C * D)]

  def unbox2[X, Y](box: Box[X * Y]): (X * Y) =
    box match {
      case Box2x2(v) => v // we know that v has type ((a * b) * (c * d))
                          // for some types a, b, c, d,
                          // and that ((a * b) * (c * d)) = (X * Y),
                          // so v does have the expected return type (X * Y)
    }
}
$ scalac boxes.scala
$

[dwijnand]

Perhaps the two of you are already well aware, but in case it's useful, here's the explanation it gives:

I tried to show that
  (v : A$1 * B$1 * (C$1 * D$1))
conforms to
  X * Y
but the comparison trace ended with `false`:

  ==> (v : A$1 * B$1 * (C$1 * D$1))  <:  X * Y
    ==> (v : A$1 * B$1 * (C$1 * D$1))  <:  X * Y (recurring)
      ==> A$1 * B$1 * (C$1 * D$1)  <:  X * Y (left is approximated)
        ==> A$1 * B$1 * (C$1 * D$1)  <:  X * Y (recurring)
          ==> X  <:  A$1 * B$1
            ==> X  <:  A$1 * B$1 (recurring)
              ==> Any  <:  A$1 * B$1 (left is approximated)
                ==> Any  <:  A$1 * B$1 (recurring)
                <== Any  <:  A$1 * B$1 (recurring) = false
              <== Any  <:  A$1 * B$1 (left is approximated) = false
              ==> Any  <:  A$1 * B$1 in frozen constraint
                ==> Any  <:  A$1 * B$1 (recurring) in frozen constraint
                <== Any  <:  A$1 * B$1 (recurring) in frozen constraint = false
              <== Any  <:  A$1 * B$1 in frozen constraint = false
            <== X  <:  A$1 * B$1 (recurring) = false
          <== X  <:  A$1 * B$1 = false
          ==> Any  <:  X * Y (recurring)
          <== Any  <:  X * Y (recurring) = false
        <== A$1 * B$1 * (C$1 * D$1)  <:  X * Y (recurring) = false
      <== A$1 * B$1 * (C$1 * D$1)  <:  X * Y (left is approximated) = false
    <== (v : A$1 * B$1 * (C$1 * D$1))  <:  X * Y (recurring) = false
  <== (v : A$1 * B$1 * (C$1 * D$1))  <:  X * Y = false

The tests were made under the empty constraint

[TomasMikula]

I did not say the example needs injectivity. I just remarked that injectivity cannot be assumed here. If it could (for example, through an annotation), the problem would go away, and injectivity is something some people may be expecting, since it's the default in languages like Haskell.

👍 Passing some evidence of injectivity of an abstract type would be much wanted, especially for cases where injectivity is actually essential.

Another workaround, as usual, is to encode all equational reasoning in lower- and upper- bounded abstract type members, and use explicit type ascriptions. It's also not ideal, but at least it's more explicit in advanced cases like this.

Don't know about that. My usual workaround for non-working pattern matching is to give up pattern matching and do OO-style multiple dispatch through nested virtual method calls on the involved objects. Some of those methods need to take an explicit =:= and/or a witness of injectivity. I can tell you, it slows down development by at least 5x.

[LPTK]

Don't know about that.

To be clear, here is what I propose (it compiles):

abstract class Eq[A, B]:
  type Up   >: A <: B
  type Down >: B <: A

class Module[*[_, _]] {
  sealed trait Box[A]:
    type BoxA = A

  case class Box2x2[A, B, C, D](value: (A * B) * (C * D)) extends Box[(A * B) * (C * D)]:
    val ev: Eq[BoxA, (A * B) * (C * D)] = new{}

  def unbox2[X, Y](box: Box[X * Y]): (X * Y) =
    box match
      case b @ Box2x2(v) => v: b.ev.Down
}

[TomasMikula]

Could this approach be used to derive Eq[F[A], F[B]] from Eq[A, B]?

[LPTK]

Yes, though you actually need to phrase it in a way that's a bit of more general:

abstract class Eq[A, B]:
  type Ev >: B | A <: A & B

def toEqF[A, B, F[_]](eq: Eq[A, B]): Eq[F[A], F[B]] =
  new Eq[F[eq.Ev], F[eq.Ev]]{}

(This Ev member of course still works for the original problem in this issue.)