CODEWITHSUNDEEP
scalaexistential-type
Alex Archambault
Alex Archambault

Reputation: 985

Checking the equality of types involving existentials in Scala

I'm writing a function of the form

def test[A,B](a: A, b: B)(implicit eq: A =:= B): Unit = ...

where I require an evidence that types A and B are the same.

I would expect calls of the form test(a,a) to compile for any a, but it seems not to be the case when a's type involves existentials, like in

case class Foo[T](c: T)
val l = List(Foo(1), Foo(1.0F), Foo(0.0)) // Inferred type: List[Foo[_ >: Double with Float with Int <: AnyVal]]

test(l.head, l.head) // Does not compile, error like: Cannot prove that Foo[_7] =:= Foo[_7].

So my question is: am I mis-using =:=? Or could it be a bug? Or a fundamental limitation of existentials? Or a limitation of their implementation?

Context

I'm testing the return type of a function f involving dependent types. I expect it to return the same type for a and b in val a = f(...); val b = f(...), thus I call test(a, b). If a and b's types involve existentials, even test(a,a) and test(b,b) don't compile, as described above.

Upvotes: 6

Views: 234

Answers (1)

dk14
dk14

Reputation: 22374

Implicit =:= works fine for existential types

scala> implicitly[Foo[_ <: Int] =:= Foo[_ <: Int]]
res0: =:=[Foo[_ <: Int],Foo[_ <: Int]] = <function1>

scala> implicitly[Foo[_ <: Int] =:= Foo[_]]
<console>:10: error: Cannot prove that Foo[_ <: Int] =:= Foo[_].
              implicitly[Foo[_ <: Int] =:= Foo[_]]
                        ^

The problem is scala loses existential type when resolving implicit for function call - A and B are not inferred here (that's why you see _7 denotation and no implicits are found).

def test[A,B](a: A, b: B)(implicit eq: A =:= B)

It can be solved with type alias:

scala> case class Foo[A](a: A) {type X = A}
defined class Foo

scala> val l = List(Foo(1), Foo(1.0F), Foo(0.0)) // Inferred type: List[Foo[_ >: Double with Float with Int <: AnyVal]]
l: List[Foo[_ >: Double with Float with Int <: AnyVal]] = List(Foo(1), Foo(1.0), Foo(0.0)) 

scala> val k = l.head
k: Foo[_ >: Double with Float with Int <: AnyVal] = Foo(1)

scala> implicitly[k.X =:= k.X]
res15: =:=[_ >: Double with Float with Int <: AnyVal, _ >: Double with Float with Int <: AnyVal] = <function1>

scala> implicitly[k.X =:= _ >: Double with Float with Int <: AnyVal]
res16: =:=[_ >: Double with Float with Int <: AnyVal, _ >: Double with Float with Int <: AnyVal] = <function1>

But keep in mind that even types with similar signature, but from different Foo's will be different (because it's path-dependent types) - existential types are so existential!

Upvotes: 3

Related Questions