Is there a way to expand the scope of an existential type quantifier in Scala to convince the type checker that two variables have the same type?

Question

Consider the following code snippet:

case class Foo[A](a:A)
case class Bar[A](a:A)

def f[B](foo:Foo[Seq[B]], bar:Bar[Seq[B]]) = foo.a ++ bar.a

val s : Seq[T] forSome {type T} = Seq(1, 2, 3)

f(Foo(s), Bar(s))

The last line fails to type check, because Foo(s) has type Foo[Seq[T]] forSome {type T} and Bar(s) has type Bar[Seq[T]] forSome {type T}, i.e. each has its own existential quantifier.

Is there any way around this? In reality all I know about s at compile time is that it has such an existential type. How can I force Foo(s) and Bar(s) to fall under the scope of a single existential quantifier?

Does this make sense? I'm pretty new to Scala and fancy types in general.

Answer 1

To be clear,

val s : Seq[T] forSome {type T} = Seq(1, 2, 3)

is equivalent to

val s: Seq[_] = Seq(1, 2, 3)

I think the answer is no for this question. You'll either need to use a type parameter/type member that's in scope or a concrete type.

One way you can do this is with tagged types: http://etorreborre.blogspot.com/2011/11/practical-uses-for-unboxed-tagged-types.html

type Tagged[U] = { type Tag = U }
type @@[T, U] = T with Tagged[U]
def tag[A, B](a: A): @@[A, B] = a.asInstanceOf[@@[A, B]]
trait ThisExistsAtCompileTime

case class Foo[A](a:A)
case class Bar[A](a:A)

def f[B](foo:Foo[Seq[B]], bar:Bar[Seq[B]]) = foo.a ++ bar.a

val s : Seq[@@[T, ThisExistsAtCompileTime] forSome {type T}] = Seq(1, 2, 3) map { x => tag[Any, ThisExistsAtCompileTime](x) }

f(Foo(s), Bar(s))

Answer 2

I realized it's possible to make this work with a little bit of refactoring:

case class Foo[A](a:A)
case class Bar[A](a:A)

def f[B](foo:Foo[Seq[B]], bar:Bar[Seq[B]]) = foo.a ++ bar.a
def g[B](s1:Seq[B], s2:Seq[B]) = f(Foo(s1), Bar(s2))

val s : Seq[T] forSome {type T} = Seq(1, 2, 3)

g(s)

Essentially I wrap the call to f in another function g that guarantees that the two sequences have the same type.