Skip to content

Type overriding does not result in type intersection #241

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

Closed
smarter opened this issue Nov 24, 2014 · 9 comments
Closed

Type overriding does not result in type intersection #241

smarter opened this issue Nov 24, 2014 · 9 comments

Comments

@smarter
Copy link
Member

smarter commented Nov 24, 2014

The following:

class A { type T = Int; val x: T = 1 }
class B extends A { override type T = String }

object O {
  val b: B = new B
  val s: String = b.x
}

Compiles without any error.
RefChecks.scala mentions:

        // types don't need to have their bounds in an overriding relationship
        // since we automatically form their intersection when selecting.

Should b.x have the type "Int | String" ?
CC @odersky @DarkDimius @namin .

@odersky
Copy link
Contributor

odersky commented Nov 24, 2014

No, it should be

 type T >: Int | String <: Int & String

which is an unsatisfiable type. The test that flags these as errors is still missing. This needs to be part of the "new refchecks" which is yet to be done.

@smarter
Copy link
Member Author

smarter commented Nov 24, 2014

Okay, related question:

class A { type T = Int; val x: T = 1 }
type B = A { override type T = String }

Should this fail for the same reason, or do we want to disallow refinement to all existing members?

@odersky
Copy link
Contributor

odersky commented Nov 24, 2014

Good question. According to DOT this would be correct. We check for satisfiable bounds only when creating an object. Whether we want to enforce the same in the compiler or something stronger is currently open.

@smarter
Copy link
Member Author

smarter commented Nov 24, 2014

Oh, so unsatisfiable types are allowed and are not a hole in the type system as long as you don't use something like null or ???, OK.

@samuelgruetter
Copy link
Contributor

@smarter yes, but it gets quite interesting when combined with lazy vals ;-) see #50

@smarter
Copy link
Member Author

smarter commented Nov 24, 2014

@samuelgruetter : What's the significance of the lazy? Your example compiles without it too.

@samuelgruetter
Copy link
Contributor

Here's something to keep in mind when doing the "new refchecks": The remark

    // types don't need to have their bounds in an overriding relationship
    // since we automatically form their intersection when selecting.

is somewhat incomplete: If we do not check that types have their bounds in an overriding relationship during refchecks, it's not sufficient to form their intersection when selecting, but we also have to do an additional test when creating new objects: When instantiating a class C, we have to check that whenever it overrides type members, it does so in a compatible way (i.e. we have to do exactly the check that current RefChecks tries to defer to later). An example:

trait A {
  type S <: T
  type T <: U
  type U
  def s2u(s: S): U = (s: T)
}

trait Converter {
  type S >: String
  type U <: Int
  def s2u(s: S): U
}

class B extends A with Converter

class C extends B {
  override type S = R
  override type T = R
  override type U = R
}

// a completely unrelated realizable class:
class R {}

object test2 {
  // Here it's not sufficient to check that the bounds given in C are satisfiable,
  // but we also have to check that they are compatible with all overridden bounds
  val c = new C

  val co: Converter = c
  val myStringAsInt: Int = co.s2u("hi")
}

@smarter
Copy link
Member Author

smarter commented Nov 24, 2014

@samuelgruetter: It seems to me that in #50 o.X should have type bounds (String | Int)..(String & Int) and intToString is invalid because Int is not a subtype of this type, so everything would be fine if the type of o.X was correct

@samuelgruetter
Copy link
Contributor

@smarter whether Int is a subtype of o.X (with bounds (String | Int)..(String & Int)) depends on whether the <:-SEL rule checks if the bounds of the path type are good, i.e. whether it checks that (String | Int) <: (String & Int). Some versions of DOT do this check, some don't, and dotty currently doesn't.

smarter referenced this issue in dotty-staging/dotty Dec 14, 2015
Comment explains why following aliases in general is incomplete and potentially unsound.
This makes Iter2 compile, but causes cyclic reference errors for pos/sets.scala.
DarkDimius pushed a commit to dotty-linker/dotty that referenced this issue May 9, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants