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]
3
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?