GADTs and top-level type variables

[scabug]

Consider the common case of defining a transformation that preserves the structure of some type:

sealed abstract class Tree
final case class Program(str: String) extends Tree
final case class Literal(n: Int) extends Tree

object Foo {
  def transform[T <: Tree](t: T): T = t match {
    case Program(str) => Program(str + "_")
    case Literal(n)   => Literal(n + 1)
  }
}

This fails now with type errors:

transform.scala:7: error: type mismatch;
 found   : Program
 required: T
    case Program(str) => Program(str + "_")
                         ^
transform.scala:8: error: type mismatch;
 found   : Literal
 required: T
    case Literal(n)   => Literal(n + 1)
                         ^
two errors found

Could we do better? Given that {{T <: Program}} on branch 1, and {{Program}} is final, could we infer that {{T == Program}}? This looks like a common case, and a worthwhile ehancement.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-127?orig=1
Reporter: @dragos
Affected Versions: 2.10.0

[scabug]

Lauri Alanko (lealanko) said:

Given that T <: Program on branch 1, and Program is final, could we infer that T == Program?

No, since T could be a self-type of an instance of Program.

[scabug]

@Blaisorblade said:
I'm not sure if Lauri Alanko's comment is outdated or just not valid. Self-type are allowed on traits but must be satisfied by concrete instances; any instance would have to be a (forbidden) subclass of Program. The given example still gives the same failure on 2.10.0 HEAD.

[scabug]

@paulp said:
Paolo: he means it could be the singleton type of an instance, which finality does not preclude.

object Bar {
  val x = Program("bippy")
  Foo.transform[x.type](x)
}

[Blaisorblade]

Just looked at this again. As pointed out by Paul, Lauri Alanko is right, so this is not really a bug, unlike #5195 and #9879. It's not clear how one change the program to one which should work but exhibits this bug.

Instead, it's easy to use a proper GADT, which just works (though the type parameter looks a bit silly), even though it doesn't give the same guarantee. So I'm closing this to avoid confusion.

sealed abstract class Tree[T] -- Phantom type parameter. We could add more bounds, but this is enough.
final case class Program(str: String) extends Tree[Program]
final case class Literal(n: Int) extends Tree[Literal]

object Foo {
  def transform[T](t: Tree[T]): Tree[T] = t match {
    case Program(str) => Program(str + "_")
    case Literal(n)   => Literal(n + 1)
  }
}

Could the original program be made to work? Looking at ADTs in other languages, it's not clear there's an existing theory which helps.
In Haskell (or I guess ML) you can't write the pattern match of the original, you need proper GADTs (unlike this). This datatype isn't a GADT, though the program expects GADT-like type refinement, and this problem doesn't arise with GADTs.

[Blaisorblade]

So Cary Robbins at https://gitter.im/typelevel/cats?at=5a82340019147ac3231ccd3e has sketched a way to encode type refinement for a related issue. I’d love to take a closer look; meanwhile, this might help interested users.