GADT example fails to typecheck because it requires injectivity of type constructors

[Blaisorblade]

Found on Twitter, noting it here: https://gist.github.com/TomasMikula/ecdbde18f142ffda0a02219f0118d7ba

@TomasMikula correctly points out:

Note that for the typechecker to succeed, it will have to make use of the fact that Tuple2 is an injective type constructor, i.e. be able to derive A = C from (A, B) = (C, D).

Investigation status: Still poking at this, and even if I modify everything to avoid covariant ADTs from the stdlib (for simplicity) and make case classes final, the typechecker still seems to have problems with injectivity. Still need to fire up the debugger to see what happens inside.

case class Pair[A, B](a: A, b: B)

enum Maybe[A] {
  case None()
  case Just(a: A)
}

object WithInvTuple {
  // Shorter notation for it
  type ~[A, B] = Pair[A, B]

  sealed trait Shuffle[A1, A2] {
    def andThen[A3](that: Shuffle[A2, A3]) = Shuffle.AndThen(this, that)
  }
  object Shuffle {
    final case class Id[A]() extends Shuffle[A, A]
    final case class Swap[A, B]() extends Shuffle[A ~ B, B ~ A]
    final case class AssocLR[A, B, C]() extends Shuffle[(A ~ B) ~ C, A ~ (B ~ C)]
    final case class AssocRL[A, B, C]() extends Shuffle[A ~ (B ~ C), (A ~ B) ~ C]
    final case class Par[A1, B1, A2, B2](_1: Shuffle[A1, A2], _2: Shuffle[B1, B2]) extends Shuffle[(A1, A2), (B1, B2)]
    final case class AndThen[A1, A2, A3](_1: Shuffle[A1, A2], _2: Shuffle[A2, A3]) extends Shuffle[A1, A3]

    def rewrite3[A1, A2, A3, A4](
      op1: Shuffle[A1, A2],
      op2: Shuffle[A2, A3],
      op3: Shuffle[A3, A4]
    ): Maybe[Shuffle[A1, A4]] = (op1, op2, op3) match {
      // case (Swap(), _, _) =>
      //   Maybe.Just(
      //     AssocLR[A1, A2 ~ A3, A4]()
      //     )
      // case (_: Swap[a11 ~ a12, _]) =>
      //   Maybe.Just(
      //     // ???
      //     AssocLR[a11 ~ a12, A2 ~ A3, A4]()
      //     )
      case (Swap(), AssocRL(), _) => Some(AssocLR[A1, A2 ~ A3, A4]())
      //case (Swap(), AssocRL(), Par(Swap(), Id())) =>
        //Some(AssocLR() andThen Par(Pair(Id(), Swap())) andThen AssocRL())
      case _ =>
        Maybe.None()
    }
  }
}
//output:
[info] Compiling 2 Scala sources to /Users/pgiarrusso/git/dotty-example-project/target/scala-0.8/classes ...
[error] -- [E007] Type Mismatch Error: /Users/pgiarrusso/git/dotty-example-project/src/main/scala/playground/mikulaGADT.scala:65:41
[error] 65 |      case (Swap(), AssocRL(), _) => Some(AssocLR[A1, A2 ~ A3, A4]())
[error]    |                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
[error]    |found:    Some[mikulaGADT.WithInvTuple.Shuffle.AssocLR[A1, mikulaGADT.Pair[A2, A3], A4]]
[error]    |required: mikulaGADT.Maybe[mikulaGADT.WithInvTuple.Shuffle'[A1, A4]]
[error]    |
[error]    |where:    A1       is a type in method rewrite3 which is an alias of mikulaGADT.Pair[A$1, B$1]
[error]    |          A2       is a type in method rewrite3 with bounds >: mikulaGADT.Pair[B$1, A$1] and <: mikulaGADT.Pair[B$1, A$1] & mikulaGADT.Pair[B$1, mikulaGADT.Pair[B$2, C$1]]
[error]    |          A3       is a type in method rewrite3 which is an alias of mikulaGADT.Pair[mikulaGADT.Pair[B$1, B$2], C$1]
[error]    |          Shuffle  is a object in object WithInvTuple
[error]    |          Shuffle' is a trait in object WithInvTuple
[error] one error found
[error] (Compile / compileIncremental) Compilation failed
[error] Total time: 2 s, completed May 6, 2018 2:56:44 PM

[TomasMikula]

You copied the old version with a mistake in the Par constructor:

Also, your snippet mixes Pair and Tuple2 (your Par constructor uses Tuple2, whereas the other ones use Pair).

[abgruszecki]

A whole bunch of Nothing is inferred in the original example. Here's a version with all the type parameters explicitly annotated:

object i4471 {
  sealed trait Shuffle[A1, A2] {
    def andThen[A3](that: Shuffle[A2, A3]): Shuffle[A1, A3] = AndThen(this, that)
  }

  case class Id[A]() extends Shuffle[A, A]
  case class Swap[A, B]() extends Shuffle[(A, B), (B, A)]
  case class AssocLR[A, B, C]() extends Shuffle[((A, B), C), (A, (B, C))]
  case class AssocRL[A, B, C]() extends Shuffle[(A, (B, C)), ((A, B), C)]
  case class Par[A1, B1, A2, B2](_1: Shuffle[A1, B1], _2: Shuffle[A2, B2]) extends Shuffle[(A1, A2), (B1, B2)]
  case class AndThen[A1, A2, A3](_1: Shuffle[A1, A2], _2: Shuffle[A2, A3]) extends Shuffle[A1, A3]
  
  def rewrite3[A1, A2, A3, A4](
    op1: Shuffle[A1, A2],
    op2: Shuffle[A2, A3],
    op3: Shuffle[A3, A4]
  ): Option[Shuffle[A1, A4]] = (op1, op2, op3) match {
    case (
      _: Swap[x, y],
      _: AssocRL[u, v, w],
      op3_ : Par[p1, q1, p2, q2]
    ) => op3_ match {
      case Par(_: Swap[r, s], _: Id[p2_]) =>
        Some(
          AssocLR[v, w, u]() andThen Par(Id[v](), Swap[w, u]()) andThen AssocRL[v, u, w]()
        )
      case _ => None
    }
    case _ => None
  }
}

The GADT constraints that should be inferred are equiv to the following: (using parameter names from the above)

A1 := (x, y)
A2 := (y, x)
A2 := (u, (v, w))
A3 := ((u, v), w)
A3 := (p1, p2)
A4 := (q1, q2)
p1 := (r, s)
q1 := (s, r)
p2 := p2_
q2 := p2_

Gist can be further inspected to see how constraints which would allow the code to compile are derivable from the above.

[abgruszecki]

@TomasMikula any similar examples would be very welcome. The examples in this issue were the only ones to properly stress #5258. Haskell is OK, so is linking to a project which heavily uses GADTs.

[TomasMikula]

I'm glad that GADTs are being taken seriously.

Here is a more complex pattern on the same data type:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module Shuffle where

data Shuffle a1 a2 where
  Id      :: forall a.                                             Shuffle a         a
  Swap    :: forall a b.                                           Shuffle (a,b)     (b,a)
  AssocLR :: forall a b c.                                         Shuffle ((a,b),c) (a,(b,c))
  AssocRL :: forall a b c.                                         Shuffle (a,(b,c)) ((a,b),c)
  Par     :: forall a1 b1 a2 b2. Shuffle a1 b1 -> Shuffle a2 b2 -> Shuffle (a1,a2)   (b1,b2)
  AndThen :: forall a1 a2 a3.    Shuffle a1 a2 -> Shuffle a2 a3 -> Shuffle a1        a3

rewrite :: Shuffle a b -> Maybe (Shuffle a b)
rewrite (                               -- ((X, Y), (U, V))
          AssocLR
          `AndThen`                     -- (X, (Y, (U, V)))
          (Par Id ( AssocRL
                    `AndThen`           -- (X, ((Y, U), V))
                    (Par Swap Id)
                    `AndThen`           -- (X, ((U, Y), V))
                    AssocLR
                    `AndThen`           -- (X, (U, (Y, V)))
                    (Par Id Swap) ))
          `AndThen`                     -- (X, (U, (V, Y)))
          AssocRL
          `AndThen`                     -- ((X, U), (V, Y))
          (Par Swap Id)
          `AndThen`                     -- ((U, X), (V, Y))
          AssocLR
          `AndThen`                     -- (U, (X, (V, Y)))
          (Par Id ( AssocRL
                    `AndThen`           -- (U, ((X, V), Y))
                    (Par Swap Id)
                    `AndThen`           -- (U, ((V, X), Y))
                    AssocLR ))
          `AndThen`                     -- (U, (V, (X, Y)))
          AssocRL
        ) =                             -- ((U, V), (X, Y))
            Just Swap
rewrite _ = Nothing

Here, the data type is extended with Curry and Eval, so it tests that inference also works with function types:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module FreeCCC where

data FreeCCC a1 a2 where
  Id      :: forall a.                                               FreeCCC a         a
  Swap    :: forall a b.                                             FreeCCC (a,b)     (b,a)
  AssocLR :: forall a b c.                                           FreeCCC ((a,b),c) (a,(b,c))
  AssocRL :: forall a b c.                                           FreeCCC (a,(b,c)) ((a,b),c)
  Par     :: forall a1 b1 a2 b2. FreeCCC a1 b1 -> FreeCCC a2 b2   -> FreeCCC (a1,a2)   (b1,b2)
  AndThen :: forall a1 a2 a3.    FreeCCC a1 a2 -> FreeCCC a2 a3   -> FreeCCC a1        a3
  Curry   :: forall a b c.                        FreeCCC (a,b) c -> FreeCCC a         (b->c)
  Eval    :: forall a b.                                             FreeCCC (a->b, a) b

rewrite :: FreeCCC a b -> Maybe (FreeCCC a b)
rewrite ((Par (g `AndThen` (Curry h)) Id) `AndThen` Eval) = Just ((Par g Id) `AndThen` h)
rewrite _ = Nothing

Finally, I would like if such inferences worked not only for concrete types (Tuple2, Function), but also for abstract types, given some evidence that they are injective. Something like

sealed trait Shuffle[x[_,_], A1, A2] // abstract over Tuple2 with a generic product `x`
case class Swap[x[_,_], A, B]() extends Shuffle[x, A x B, B x A]
case class Par[x[_,_], A1, B1, A2, B2](_1: Shuffle[x, A1, B1], _2: Shuffle[x, A2, B2]) extends Shuffle[x, A1 x A2, B1 x B2]
// ...

def rewrite[x[_,_]: BiInjective, A, B](f: Shuffle[x, A, B]): Option[Shuffle[x, A, B]] =
  f match {
    // injectivity of `x` in both variables is taken into account by pattern matching
    case AndThen(Swap(), AndThen(Par(g, f), Swap())) => Par(f, g)

    case _ => None
  }

I don't know how to do this in Haskell, either.

[abgruszecki]

@TomasMikula - thank you for the examples. I've added some very similar examples on #5611, taken from Haskell test suite.

The exact examples from this issue do typecheck, so I'm closing the issue. We still have #5658 to deal with.