In scala, how to instruct the compiler to realise the equivalence of two abstract types?

user_1732418 0
Viewed 122

I have a simple case to test the type inference capability of scala:

    trait Super1[S] {

      final type Out = this.type
      final val out: Out = this
    }

    trait Super2[S] extends Super1[S] {

      final type SS = S
    }

    case class A[S](k: S) extends Super2[S] {}

    val a = A("abc")

    implicitly[a.type =:= a.out.type]
    // success

    implicitly[a.Out =:= a.out.Out]
    // success

    implicitly[a.SS =:= a.out.SS]
    implicitly[a.SS <:< a.out.SS]
    implicitly[a.out.SS <:< a.SS]
    // oops

The error for the last 4 lines looks like this:

[Error] /home/peng/git-spike/scalaspike/common/src/test/scala/com/tribbloids/spike/scala_spike/AbstractType/InferInheritance.scala:28: Cannot prove that a.SS =:= Super2.this.SS.
[Error] /home/peng/git-spike/scalaspike/common/src/test/scala/com/tribbloids/spike/scala_spike/AbstractType/InferInheritance.scala:29: Cannot prove that a.SS <:< Super2.this.SS.
[Error] /home/peng/git-spike/scalaspike/common/src/test/scala/com/tribbloids/spike/scala_spike/AbstractType/InferInheritance.scala:30: Cannot prove that Super2.this.SS <:< a.SS.
three errors found

Clearly scala compiler screwed up on these cases: if I move:

      final type Out = this.type
      final val out: Out = this

to be under Super2 it will compile successfully. My question is that: why the status quo inference algorithm won't work in this case? and how can I rewrite my code to circumvent this problem of the compiler?

path-dependent-type dependent-type type-inference abstract-type scala
1 Answers

If a.SS =:= a.out.SS then we should be able to use one in place of the other. Is that the case?

No.

val x: a.SS = "hello"
val y: a.out.SS = "hello"

Compiling this I get:

ScalaFiddle.scala:29: error: type mismatch;
 found   : lang.this.String("hello")
 required: Super2.this.SS
    (which expands to)  S
  val y: a.out.SS = "hello"

It looks like Scala understands that a.SS is really String, which isn't surprising.

But clearly a.out.SS isn't String but rather... S.

Strangely this works even though it's clearly wrong:

val b = A(1)
implicitly[a.out.SS =:= b.out.SS]

If you just define out to be of type this.type then your code works.

The best I can come up with is that when defining the type of out, Scala fails to associate the actual type represented by S with out and so the type SS as viewed through out just has the generic type S.

The type Out does seem to understand the actual type represented by S, so this works:

implicitly[a.SS =:= a.Out#SS]
implicitly[a.SS <:< a.Out#SS]
implicitly[a.Out#SS <:< a.SS]

and this correctly fails to compile:

val b = A(1)
implicitly[a.Out#SS =:= b.Out#SS]
user_26841960
Related