Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
adriaanm opened this issue Jul 11, 2018 · 4 comments
Open

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

adriaanm opened this issue Jul 11, 2018 · 4 comments

Comments

@adriaanm
Copy link
Contributor

adriaanm commented Jul 11, 2018

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
Copy link
Contributor Author

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
Copy link

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 scala/scala3#4781 (comment)):

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
Copy link
Contributor Author

adriaanm commented Jul 11, 2018

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
Copy link

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).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants