Path-dependent types - what's wrong with the following code?

Question

The following code:

trait Foo {
  type T
  val x: T
}

trait Bar {
  type F <: Foo { type T <: F }
}

class C[B <: Bar](val f: B#F) {
  val x: f.T = f.x
}    

is rejected by the Scala compiler (2.11.5) with the following error message:

error: type mismatch;
found   : C.this.f.x.type (with underlying type C.this.f.T)
required: this.T
      val x: f.T = f.x
                  ^

If the explicit type declaration is omitted, the type is correctly inferred, according to the output from typer phase:

private[this] val x: C.this.f.T = C.this.f.x;
<stable> <accessor> def x: C.this.f.T = C.this.x

The problem also disappears if F inside the bound in Bar is changed to a type that is not a member of Bar, i.e.

type F <: Foo { type T <: Foo }

works correctly.

Is it a bug? Or some fundamental misunderstanding on my part? Or some arcane feature?

Answer 1

Not a definite answer, but some observations...

Let's first see what does work:

class C[B <: Foo](val f: B) {
  val x: f.T = f.x
}

so the compiler loses you when use a type projection for value f. If you "fix" that projection, it also seems to work:

class D[B <: Bar](val f: B#F) {
  val g: Foo = f
  val x: g.T = g.x
}

I have long struggled with F-bounded types until I got them "water-tight". There is something about type parameters versus type members that makes the former work. For example:

trait FooRec[F <: FooRec[F]] extends Foo {
  type T = F
}

class E[F <: FooRec[F]](val f: F) {
  val x: f.T = f.x
}

Finally, you could also fix Bar's type member by passing it in as a type parameter:

class G[F1 <: Foo { type T = F1 }, B <: Bar { type F = F1 }](val f: B#F) {
  val x: f.T = f.x
}

Similarily, if you fix the type already in the definition of Bar, it works:

trait Baz {
  type F <: Foo { type T = F }  // stable recursion
}

class H[B <: Baz](val f: B#F) {
  val x: f.T = f.x
}

So in your original definition and application having upper bounds seems not enough. Probably you can proof that the compiler is right about its rejection, but I don't know how...