Pattern matching does not appropriately refine types as expected for GADTs

[scabug]

An important part of GADT support is that pattern matching should recover / refine type information. I posted some examples here: https://gist.github.com/1369239 Here's a smaller snippet:

/** GADTs for stream transforming functions */
trait F[A,B] { 
  def eval: List[A] => List[B]
  def pipe[C](f: F[B,C]): F[A,C] = Pipe(this, f) 
}
case class Flip[A,B]() extends F[(A,B),(B,A)] {
  def eval = _ map { case (a,b) => (b,a) }
}
case class Pipe[A,B,C](f: F[A,B], g: F[B,C]) extends F[A,C] {
  def eval = f.eval andThen g.eval
}
case class MapF[A,B](f: A => B) extends F[A,B] { 
  def eval = _ map f
  override def pipe[C](g: F[B,C]) = g match {
    case MapF(g) => MapF(f andThen g)
    /** Commented out lines do not compile, the pattern match does not refine
     *  the type B to a (x,y) for some types, x, y */
    // case g2: Flip[a,b] => MapF(f andThen (_.swap))
    // case Flip() => MapF(f andThen (_.swap))
    case _ => Pipe(this,g)
  }
}

Note the commented out line - pattern matching on Flip does not refine the existing type parameters. In comparison, this Haskell code compiles as expected. The pattern match on Flip refines the type of the function f, so you can call swap on its result without any cast.

-- provides swap :: (a,b) -> (b,a)
import Data.Tuple

data F a b where
  MapF :: (a -> b) -> F a b
  Pipe :: F a b -> F b c -> F a c
  Flip :: F (a,b) (b,a)

-- smart constructor for pipe, which does optimization
pipe (MapF f) Flip = MapF (swap . f)  
pipe f g           = Pipe f g

In addition to the type refinement issue, I get spurious "constructor cannot be instantiated to expected type" problems which are probably related to the same underlying problem. The commented out line below does not compile - I've tried a few other variations of it that also don't compile.

case class Par[A,B,C,D](f: F[A,B], g: F[C,D]) extends F[(A,C), (B,D)] {
  def eval = l => f.eval(l.map(_._1)) zip g.eval(l.map(_._2))
  override def pipe[E](h: F[(B,D),E]) = h match { 
    case Par(f2, g2) => Par(f pipe f2, g pipe g2)
    /** This code does not compile  */
    // case Pipe(Flip(), Par(g2,f2)) => Par(f pipe f2, g pipe g2) pipe Flip()
    case _ => Pipe(this, h)
  }
}

It seems like most pattern matches that would result in type refinement of any existing type parameters are considered compile errors ("constructor cannot be instantiated to expected type"). There also seem to be some cases where Scala does the right thing, like the line above {noformat}case Par(f2, g2) => Par(f pipe f2, g pipe g2){noformat}. I don't have a clear model for why it works in some cases but not others.

It would be great if Scala included better GADT support. As a personal anecdote - I was working on a library for describing distributed computations and decided to try encoding it as a GADT. The description of the distributed computation could then be examined by multiple distribution strategies, which could optimize the descriptions via (well-typed) pattern matching before actually doing the distributed execution. I ran into so many problems with getting this to work properly that I eventually gave up and resorted to making everything untyped.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-5195?orig=1 Reporter: @pchiusano

[scabug]

@pchiusano said: This might be caused by the same thing as #127. That issue seems to be a bit different - that class is not really a GADT since has no type parameters - but the behavior is similar in that a type parameter is not being properly refined by a pattern match, so maybe it's the same thing.

In the case I reported, it is an invariant type parameter to a data constructor that is not being refined - in #127, it is just a type parameter to the function.

[scabug]

@SethTisue said: has anyone checked Dotty?

[scabug]

@SethTisue said: @pchiusano I notice the "affects version" field here is blank. curious if this regressed in the new pattern matcher, or if it never worked.

[aaronlevin]

I was working on type-aligned lists and encountered this bug (or a related bug). @snoble and I put together a small example with various variants, as well as compilation status from Scala 2.11, Scala 2.12, and Dotty (which @SethTisue was interested in). The results are interesting and not so consistent even in Dotty. https://gist.github.com/snoble/0385b32e8699843e0b2034b749f66734#gistcomment-2318457

sealed trait TList[X, Z]
case class TCons[X, Y, Z](head: X => Y, tail: TList[Y,Z]) extends TList[X, Z]
case class TEnd[X,Z](f: X => Z) extends TList[X, Z]

object Evaluators {
  def safe1[X,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case TCons(head, tail) => safe1(head(x), tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Warning
  // scala 2.11.8: Fine
  // scala 2.12.4: Fine

  def unsafe1[X,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case TCons(head, tail) => safe1("WTF", tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Warning
  // scala 2.11.8: Fine
  // scala 2.12.4: Fine

  def safe2[X,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case tCons: TCons[X, _, Z] => safe2(tCons.head(x), tCons.tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Error
  // scala 2.11.8: Fine
  // scala 2.12.4: Fine

  def unsafe2[X,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case tCons: TCons[X, _, Z] => unsafe2("WTF", tCons.tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Error
  // scala 2.11.8: Error
  // scala 2.12.4: Error

  def safe3[X,Y,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case tCons: TCons[X, Y, Z] => safe3(tCons.head(x), tCons.tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Fine
  // scala 2.11.8: Warning (Erasure)
  // scala 2.12.4: Warning (Erasure)

  def unsafe3[X,Y,Z](x: X, tList: TList[X, Z]): Z = tList match {
    case tCons: TCons[X, Y, Z] => unsafe3("WTF", tCons.tail)
    case TEnd(f) => f(x)
  }
  // dotty 0.5   : Error
  // scala 2.11.8: Error
  // scala 2.12.4: Error
}