In the latest release of scala (2.12.x), is the implementation of path-dependent type incomplete?

Question

I did a quick experiment to understand the nature of path-dependent type feature of scala:

  trait SS {

    type II
  }

  class SS1() extends SS {}

  def sameType[T1, T2](implicit ev: T1 =:= T2): Unit = {}

// experiments start here

    val a = new SS1()

    val b = new SS1()

    val c = a

    sameType[a.II, a.II]

    assertDoesNotCompile(
      """
        |sameType[a.II, b.II]
        |""".stripMargin
    ) // of course it happens

So far so good? Until I type in the next line:

    sameType[a.II, c.II] 

At which point the compiler gave the following error:

[Error] .../PathDependentType/ProveSameType.scala:32: Cannot prove that a.II =:= c.II.
one error found

despite that constant a & c always refer to 2 completely identical objects. So why scala compiler choose not to prove it? Does this implies that a & c refers to 2 different 'paths', and such behaviour is expected for practicality?

Answer 1

It's absolutely correct behavior. Reference equality of a and c is irrelevant. Path-dependent types a.II and c.II are different.

a.II, c.II are shorthands for types a.type#II, c.type#II and singleton types a.type, c.type are different too.

Paths https://scala-lang.org/files/archive/spec/2.13/03-types.html#paths

Equivalence of types https://scala-lang.org/files/archive/spec/2.13/03-types.html#equivalence