scala / scala-dev

Scala 2 team issues. Not for user-facing bugs or directly actionable user-facing improvements. For build/test/infra and for longer-term planning and idea tracking. Our bug tracker is at https://github.com/scala/bug/issues
Apache License 2.0
130 stars 15 forks source link

(tp1 =:= tp2) != (tp1 <:< tp2) && (tp2 <:< tp1) #530

Open adriaanm opened 6 years ago

adriaanm commented 6 years ago

isSameType does not correspond to isSubtype the way you'd expected. Specifically, the case for refined types looks wrong (though compact):

case (RefinedType(ps1, ds1), RefinedType(ps2, ds2)) => 
  (ps1 corresponds ps2)(_ =:= _) && (ds1 isSameScope ds2)

Inlining the case for refined types of the definition of subtyping (in both directions), you'd expect something equivalent to:

    ps1.forall(p1 => ps2.exists(p2 => p2 <:< p1)) &&
    ps2.forall(p2 => ps1.exists(p1 => p1 <:< p2)) &&
    ds1.forall(d1 => specializesSym(tp2, d1)) &&
    ds2.forall(d2 => specializesSym(tp1, d2))

The above uses a more restricted form of scope equality:

    def isSameScope(other: Scope) = (
         (size == other.size)     // optimization - size is cached
      && (this isSubScope other)
      && (other isSubScope this)
    )

    def isSubScope(other: Scope) = {
      def scopeContainsSym(sym: Symbol): Boolean = {
        @tailrec def entryContainsSym(e: ScopeEntry): Boolean = e match {
          case null => false
          case _    =>
            val comparableInfo = sym.info.substThis(sym.owner, e.sym.owner)
            (e.sym.info =:= comparableInfo) || entryContainsSym(lookupNextEntry(e))
        }
        entryContainsSym(this lookupEntry sym.name)
      }
      other.toList forall scopeContainsSym
    }
adriaanm commented 6 years ago

The comment is just one example of how isSameType is wrong. Here's a simpler one: typeOf[String with AnyRef] =:= typeOf[String] is false...

Blaisorblade commented 6 years ago

Here's a simpler one: typeOf[String with AnyRef] =:= typeOf[String] is false...

That's according to the spec, tho it's most clearly not defensible — it follows from SLS 3.5.1 (same quote as in https://github.com/lampepfl/dotty/issues/4781#issuecomment-404156017):

Two compound types are equivalent if the sequences of their component are pairwise equivalent, and occur in the same order, and their refinements are equivalent. Two refinements are equivalent if they bind the same names and the modifiers, types and bounds of every declared entity are equivalent in both refinements.

adriaanm commented 6 years ago

You're right -- good point, but I don't think that's a very intuitive definition of type equality. Witness the implementation in dotty :-)

EDIT: yes, I realize compound types and intersection types are not the same thing, and I guess we may be stuck with this in Scala 2, but I don't see why type equality should encode properties related to member selection (linearisation). Especially for the original example: String and String with AnyRef are completely indistinguishable, except with respect to type equality :-D

Blaisorblade commented 6 years ago

You're right -- good point, but I don't think that's a very intuitive definition of type equality. Witness the implementation in dotty :-)

Oh sure, I'm not defending the spec — I'm happy for every change that can be imported in Scala 2, I just dunno how easy that is. I already decided that point must change for Scala 3 — and I already filed a couple of issues on scala/bug on trickier points. I'm just less sure how to best proceed (and working on the DOT formalization first).