Monday, June 3, 2013

Proving type equality in a Scala pattern match

Finally got this to work. Here's the infuriating code:

  1  sealed trait Two[A,B]
  2  case class One[A]() extends Two[A,A]
  4  def convert[A,B](x: A, t: Two[A,B]): B = t match {
  5    case One() => x
  6  }

which of course gives:

type mismatch;
 found   : x.type (with underlying type A)
 required: B
    case One() => x

You would think that Scala might introduce a constraint that A =:= B, but apparently not. Of course you could just make the =:= yourself

  7  sealed trait Two[A,B]
  8  case class One[A,B](pf: A =:= B) extends Two[A,B]

except that that is much more cluttered and not how people usually write and use case classes.

It turns out that the working solution is to use a matched (lower-case) type variable:

  9    def convert[A,B](x: A, t: Two[A,B]): B = t match {
 10      case o: One[a] =>
 11        x: a
 12    }

So, the match is not as pretty as it could be, but the case class definition is clean and we never explicitly mentioned =:=, which is always a good thing.

(What's going on is that Scala is introducing two implicit =:= s, one linking a to A and one linking a to B, but doesn't chain implicits).

1 comment:

  1. Thanks for posting this. I've been wondering about a solution to this for a while. Just a note: How would you use the `pf` variable on line 8 in a pattern match for the containing case class?