Existence of types associated with existential values ​​in Scala

Question

I am writing a form function

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

where I need confirmation that types A and B same.

I would expect the calls of the form test(a,a) to compile for any A , but it does not seem to be the case when type A includes existences, for example, 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 using =:= incorrectly? Or could it be a mistake? Or a fundamental limitation of existentiality? Or a restriction on their implementation?

Context

I am testing the return type of a function f with dependent types. I expect it to return the same type for A and B in val a = f(...); val b = f(...) val a = f(...); val b = f(...) , so I call test(a, b) . If types A and B include existences, even test(a,a) and test(b,b) not compiled as described above.

Answer 1

Implicit =: = works great 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 that scala loses its existential type when resolving an implicit function call - A and B are not displayed here (what you see is a _7-notation and no implications found).

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

It can be solved using an alias like:

 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[kX =:= kX] res15: =:=[_ >: Double with Float with Int <: AnyVal, _ >: Double with Float with Int <: AnyVal] = <function1> scala> implicitly[kX =:= _ >: 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 a similar signature, but from different Foo will be different (because they depend on the type) - the existential types are so existential!