isVolatile incorrect for intersection types about scala3 HOT 57 CLOSED

I just checked with the changes from #47 , but this problem remains (which is not surprising because #47 does not change isVolatile...)

from scala3.

Reopening to keep the test case around for the time we have refchecks written.

from scala3.

@smarter In this example, if we remove lazy, the program will crash when evaluating ???, so if we can cast Int to String afterwards, no one cares. However, if o is lazy (but never forced), we can cast Int to String, which is a typesafety breach.

from scala3.

@odersky : does this still need to be kept open?

from scala3.

Yes, the error is not detected. I'll put a test in pending/neg.

from scala3.

Note that instead of an unimplemented lazy val, we could also have a null val.
We can also interchange with and &.

@RossTate and I found a similar issue that also affects scalac:
https://issues.scala-lang.org/browse/SI-9633

from scala3.

Good point. I think this would have a fix analogous to lazy vals: We need a
predicate that a type is guaranteed
to have good bounds under all possible refinements (i.e. the opposite of
the isVolatile, after that is fixed). It can be a conservative
approximation. Let's call it "alwaysGoodBounds" (agp).

Then for

lazy val x: T = ...
val x: T = null
T # A

T must in each case be agp.

Wdyt?

On Fri, Jan 29, 2016 at 7:12 AM, Nada Amin [email protected] wrote:

Note that instead of an unimplemented lazy val, we could also have a null
val.
We can also interchange with and &.

@RossTate https://github.com/RossTate and I found a similar issue that
also affects scalac:
https://issues.scala-lang.org/browse/SI-9633

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

Not sure I understand how the proposal would work.

1. For val x: T = null, how would you enforce T agp for val x: T = <arbitrary expression that evaluates to null>?
2. Also, how would you handle the case below? It seems like you'd need to consider every parameter type as well?

  trait A { type L <: Nothing }
  trait B { type L >: Any}
  def id1(b: B, x: Any): b.L = x
  def id2(p: B with A)(x: Any): Nothing = id1(p, x)
  def id3(x: Any): Nothing =  id2(null)(x)
  println(id3("oh"))

from scala3.

One option would be to make Null a subtype only of (agp) types?

On Fri, Jan 29, 2016 at 9:41 AM, Nada Amin [email protected] wrote:

Not sure I understand how the proposal would work.

For val x: T = null, how would you enforce T agp for val x: T =
?
2.

Also, how would you handle the case below? It seems like you'd need to
consider every parameter type as well?

trait A { type L <: Nothing }
trait B { type L >: Any}
def id1(b: B, x: Any): b.L = x
def id2(p: B with A)(x: Any): Nothing = id1(p, x)
def id3(x: Any): Nothing = id2(null)(x)
println(id3("oh"))

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

Note that you can also have expression evaluate to null due to initialization order:

class C {
  val a: T = method
  def method = b
  val b: T = a
}

(new C).a#A

This code is type correct for any T, a and b are always initialized to null, there is no particular place to issue a warning(method could be implemented in a subclass).

from scala3.

@DarkDimius Yes, I know. We need to fix initialization separately. One thing after another. Right now, we need to classify programs that access uninitialized data as potentially unsound.

from scala3.

@odersky -- to enforce Null <: agp, you'd also have to enforce agp <: non-agp, otherwise you could circumvent the check through a chain of casts? I don't see how you'd get agp <: non-agp, e.g. Any <: x.L, but then I don't know what exactly you have in mind for agp.

from scala3.

@namin I think if you have Null <: agp <: non-agp then non-agp cannot constitute a soundness hole, because the bounds are known to be good through the agp <: non-agp relationship.

But on second thought we should wait until we address the problem at the root with the null-safe type system we planned. Then null would be its own type, anything nullable would be represented as T | Null , and we can decree that if x: T | Null then x is not a path.

from scala3.

@odersky -- maybe you're right about agp <: non-agp

The second proposal feels right long-term...

from scala3.

Yet another variation (relevant to agp proposal), showing interaction with polymorphism and subtyping constraints.

  trait A { type L <: Nothing }
  trait B { type L >: Any}
  def id1(b: B, x: Any): b.L = x
  def id2[C, A1 >: C <: A, B1 >: C <: B](c: C, x: Any): Nothing = {
    val c1: B1 with A1 = c
    id1(c1, x)
  }
  def id3(x: Any): Nothing = id2[Null, A, B](null, x)
  println(id3("oh"))

from scala3.

@odersky what is the proposed definition of 'always good bounds'? We know that previous definitions of realizability are not preserved through narrowing, which (I believe) is the problem we're observing here.

Another variation (with either null or lazy, both of which are not supported by the theory):

    trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      val p: B
      // or: lazy val p: B
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      val p: A & B = null
      // or: lazy val p: A & B = ???
    }
    val v = new V {}
    v.brand("boom!")

from scala3.

@TiarkRompf -- cool example. In scalac (with B with A instead of A & B), it's a compile time error because any refined val p is checked for incompatible bounds.

from scala3.

@namin Well, slight variations break in scalac as well:

    trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      type X <: B
      val p: X
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      type X = B with A
      val p: X = null
      // or: lazy val p: X = ???
    }
    val v = new V {}
    v.brand("boom!"): Nothing

from scala3.

@namin Does scalacs checking also work if the bad bounds arise from an intersection somewhere deeper?

It looks to me we also have to enforce that val's used in paths are final.

from scala3.

@TiarkRompf Thanks for the example! So it seems our only option is to
demand path vals to be effectively final.

On Sun, Jan 31, 2016 at 2:33 AM, Tiark Rompf [email protected]
wrote:

@namin https://github.com/namin Well, slight variations break in scalac
as well:

trait A { type L <: Nothing }
trait B { type L >: Any}
trait U {
  type X <: B
  val p: X
  def brand(x: Any): p.L = x
}
trait V extends U {
  type X = B with A
  val p: X = null
  // or: lazy val p: X = ???
}
val v = new V {}
v.brand("boom!"): Nothing

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

@odersky, here's a slightly modified example by @TiarkRompf that shows that finality of the val is not enough:

 trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      type X <: B
      val p2: X                  // <<-- added
      final val p: X = p2        // <<-- changed
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      type X = B with A
      val p2: X = null           // <<-- changed
      // or: lazy val p: X = ???
    }
    val v = new V {}
    v.brand("boom!"): Nothing

from scala3.

@DarkDimius I think this example is not like the others, in the sense that
it is falls into the class of initialization errors. p will be
initialized with the val of p2 which at this point is undefined.

On Sun, Jan 31, 2016 at 3:27 AM, Dmitry Petrashko [email protected]
wrote:

@odersky https://github.com/odersky, here's a slightly modified example
by @TiarkRompf https://github.com/TiarkRompf that shows that finality
of the val is not enough:

trait A { type L <: Nothing }
trait B { type L >: Any}
trait U {
type X <: B
val p2: X // <<-- added
final val p: X = p2 // <<-- changed
def brand(x: Any): p.L = x
}
trait V extends U {
type X = B with A
val p2: X = null // <<-- changed
// or: lazy val p: X = ???
}
val v = new V {}
v.brand("boom!"): Nothing

``

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

@odersky, ok, a small restructuring and second field is not needed:

 trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      type X <: B
      def p2: X                  // <<-- added
      final val p: X = p2        // <<-- changed
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      type X = B with A
      def p2: X = null           // <<-- changed
      // or: lazy val p: X = ???
    }
    val v = new V {}
    v.brand("boom!"): Nothing

from scala3.

@DarkDimius Now you have a null-safety issue (which we will handle separately). If you change the null initialization to a lazy val p2 = ??? you get an initialization issue because you will hit the ??? when initializing p.

from scala3.

I have found a less invasive way to deal with the root case: We need to demand that lazy vals can only override lazy vals, and enforce in addition that lazy vals in paths must be final. That is much less invasive than demanding finality for all vals that appear in paths. #1051 contains an implementation of this with adapted tests.

from scala3.

I'm confused -- how would this help?

    trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      type X <: B
      def p2: X
      final lazy val p: X = p2
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      type X = B with A
      def p2: X = ???
    }
    val v = new V {}
    v.brand("boom!"): Nothing

from scala3.

@DarkDimius (note that I changed p to be lazy)

from scala3.

@TiarkRompf With #1051 the example is rejected:

i1050.scala:73: error: U.this.X(U.this.p) is not a legal path since its underlying type U.this.X it is not a concrete type
      def brand(x: Any): p.L = x

from scala3.

Ah, missed that bit! But here's one that still fails (with commit efe1bf2):

    trait U { 
      type Y
      trait X { type L = Y }
      def compute: X
      final lazy val p: X = compute
      def brand(x: Y): p.L = x 
    }
    trait V extends U { 
      type Y >: Any <: Nothing
      def compute: X = ???
    }
    val v = new V {}
    v.brand("boom!")

from scala3.

Wow, this gets more and more insidious. Any suggestions how we should formulate "good bounds" to avoid this?

from scala3.

@odersky that's what I was trying to suggest.
I do not see how this can be done without either analysis based on call graph or requiring that all methods used in rhs of (lazy) vals are final, and bodies of those final methods themselves only refer to final methods and so on... some kind of transitive finality.

from scala3.

@DarkDimius Do you want to try it out on our codebase? Check whether this would be workable?

from scala3.

Btw the last one is not even related to lazy vals (is there no check to require good bounds at object construction?):

    trait V { 
      type Y >: Any <: Nothing
      def id(x: Y): Y = x 
    }
    val v = new V {}
    v.id("boom!"): Nothing

from scala3.

@TiarkRompf Looks like it's still missing (but should be easy to add).

On Sun, Jan 31, 2016 at 11:23 PM, Tiark Rompf [email protected]
wrote:

Btw the last one is not even related to lazy vals (is there no check to
require good bounds in traits?):

trait V {
  type Y >: Any <: Nothing
  def id(x: Y): Y = x
}
val v = new V {}
v.id("boom!"): Nothing

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

@odersky I want to discuss this idea in details with you and Sandro to see if its sufficient before implementing it.

from scala3.

@TiarkRompf OK we should have a test in now for this. The latest example is rejected with:

i1050.scala:94: error: Object with Tiark4.V{...} cannot be instantiated since it has a member type Y with possibly conflicting bounds Any <: ... <: Nothing
    val v = new V {} // error: cannot be instantiated
                ^

On Sun, Jan 31, 2016 at 11:36 PM, Dmitry Petrashko <[email protected]

wrote:

@odersky https://github.com/odersky I want to discuss this idea in
details with you and Sandro to see if its sufficient before trying to
implement it.

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

All tests in test/pos/i1050.scala of #1051.

from scala3.

Here are two more that look like easy fixes. One:

    trait A { type L <: Nothing }
    trait B { type L >: Any }
    def f(x: => A & B)(y: Any):Nothing = (y:x.L)
    f(???)("boom!")

And two:

    trait B { type L >: Any }
    trait A { type L <: Nothing }
    trait U { 
      trait X { 
        val q: A & B = ???
      }
      final lazy val p: X = ???
      def brand(x: Any): p.q.L = x 
    }
    val v = new U {}
    v.brand("boom!"): Nothing

from scala3.

Good examples. One is easy. Two is more interesting. It shows that we need
to test in general laziness and realizability on different parts of a path.

On Mon, Feb 1, 2016 at 4:18 AM, Tiark Rompf [email protected]
wrote:

Here are two more that look like easy fixes. One:

trait A { type L <: Nothing }
trait B { type L >: Any }
def f(x: => A & B)(y: Any):Nothing = (y:x.L)
f(???)("boom!")

And two:

trait B { type L >: Any }
trait A { type L <: Nothing }
trait U {
  trait X {
    val q: A & B = ???
  }
  final lazy val p: X = ???
  def brand(x: Any): p.q.L = x
}
val v = new U {}
v.brand("boom!"): Nothing

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

Y'all aren't the only ones with a problem. I can recreate this in Java using implicit constraints on wildcards:

class Unsound {
    static class Bound<A, B extends A> {}
    static class Bind<A> {
        <B extends A> A bad(Bound<A,B> bound, B b) {return b;}
    }
    public static <T,U> U coerce(T t) {
        Bound<U,? super T> bound = null;
        Bind<U> bind = new Bind<U>();
        return bind.bad(bound, t);
    }
}

This problem seems fundamental to virtual types and inhabitability. In short, it seems you should only be able to use a virtual type if you can guarantee that its context object actually exists.

from scala3.

Great example, @RossTate!

from scala3.

I added more tests in #1051 which also check

• deep paths
• imports
• types that are unrealizable because they contain unrealizable fields.

These files are neg/i1050.scala i1050a.scala i1050c.scala

from scala3.

@RossTate I tried to convert your example to Scala but it does not pass:

object unsound {
  trait Bound[A, B <: A]
  trait Bind[A] {
    def bad[B <: A](bound: Bound[A, B], b: B) = b
  }
  def coerce[T, U](t: T): U = {
    lazy val bound: Bound[U, _ >: T] = ???
    def bind = new Bind[U] {}
    bind.bad(bound, t)
  }
}

Compiling this gives:

error: Type argument  >: T does not conform to upper bound U 
    lazy val bound: Bound[U, _ >: T] = ???
                             ^

one error found

from scala3.

It wouldn't translate to Scala. Java's wildcards generate implicit constraints, whereas Scala's do not. Here's a simpler example:

class Numbers<N extends Number> extends List<N> {...}
Numbers<? extends Number> foo(Numbers<?> n) { return n; }

This type checks in Java because Java infers that the wildcard in Numbers<?> must be a subtyping of Number because whatever type it is abstracting must be a valid type argument for Numbers. Scala, on the other hand, is unable to recognize that every Numbers[_] is also a Numbers[_<:Number].

But the high-level strategy of this example is that same as what @namin and I came up with for Scala: rather than writing the inconsistent bounds directly, where the compiler would check for consistency, instead figure out some way to have inconsistent bounds be generated, where the compiler would not check for consistency. In my Java example, I do this using implicit constraints (and use the Bind class to get around some hack in the compiler). In @namin's and my Scala example, we do this using trait intersection. Both compilers have ad-hoc methods for preventing these, but adding enough layers of indirection seems to always eventually get around those hacks.

from scala3.

Good observations, @RossTate, and interesting to see how this plays out in Java.

I think one important bit we've learnt from the DOT proofs is that most static predicates (like realizability of types) are not preserved by narrowing. So whenever we want to use realizability as a safeguard (instead of knowing that a type must be inhabited through evaluation) we're on thin ice, and we have to be very careful that narrowing (through function calls or inheritance) is ruled out.

For top-level lazy vals the restrictions we have now look reasonable to me (non-overridable definition of the lazy val, non-overridable definition of its type).

But for the other bits I don't the fix is quite there yet (cc @odersky). The length > 1 path example seems to be unchanged (?), and the by-name one blows up with a little more indirection:

    trait A { type L <: Nothing }
    trait B { type L >: Any }
    def f(x: => B)(y: Any):x.L = y
    def f1(x: => A & B)(y: Any):Nothing = f(x)(y)
    f1(???)("boom!"): Nothing

When I said these issues were easy to fix I thought of a more conservative solution, i.e. of disallowing by-name values in paths, and restricting lazy vals to be endpoints in paths (but of course this doesn't rule out solutions based on more elaborate checks).

from scala3.

I agree. I think it's safe to say that you can't soundly have bounded virtual types, intersection types, and a (lazily) inhabitable bottom type.

from scala3.

@TiarkRompf You need to compile with -strict. We check fields for
realizability only under strict mode.
Because fields currently could be null (and therefore in the new typesystem
not eligible as paths),
we risk get false negatives if we make every unrealizable field as an
error.

Cheers

• Martin

On Tue, Feb 2, 2016 at 7:33 PM, Ross Tate [email protected] wrote:

I agree. I think it's safe to say that you can't soundly have bounded
virtual types, intersection types, and a (lazily) inhabitable bottom type.

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

@odersky ok, got it now. The nested path fails with -strict, but the second by-name example still goes through.

from scala3.

@TiarkRompf Which example did you mean?

On Tue, Feb 2, 2016 at 8:41 PM, Tiark Rompf [email protected]
wrote:

@odersky https://github.com/odersky ok, got it now. The nested path
fails with -strict, but the second by-name example still goes through.

—
Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

from scala3.

This one:

    trait A { type L <: Nothing }
    trait B { type L >: Any }
    def f(x: => B)(y: Any):x.L = y
    def f1(x: => A & B)(y: Any):Nothing = f(x)(y)
    f1(???)("boom!"): Nothing

from scala3.

@TiarkRompf Ah I overlooked that. But it seems anyway we should reject all cbn parameters as paths because they can have different values on each call. Do you agree?

from scala3.

Yes, agreed.

from scala3.

I just thought I'd mention this here. I tried running the unsound null example in earlier versions of Scala (<=2.9.3) but interestingly, it doesn't compile due to restrictions on dependent method types. Does that suggest a static null containment strategy only for arguments of dependent methods, or am I missing something?

When I try to convert to OO in order to avoid dependent methods, I get the usual checks for good bounds in objects.

from scala3.

Ah, nevermind. As @odersky hinted, the dependent method type is just one more restriction rather than essential. @TiarkRompf already had some earlier examples with no dependent methods: #50 (comment)

Here's an example that compiles with all major Scala releases listed in the download page, including 2.5 to 2.9.

object unsound_legacy {
  trait LowerBound[T] {
    type M >: T;
  }
  trait UpperBound[U] {
    type M <: U;
  }
  trait Upcast[T] {
    type X <: LowerBound[T]
    def compute: X
    final val ub: X = compute
    def upcast(t: T): ub.M = t
  }
  class Coerce[T,U] extends Upcast[T] {
    type X = LowerBound[T] with UpperBound[U]
    override def compute = null
    def coerce(t: T): U = upcast(t)
  }
  def main(args : Array[String]) : Unit = {
    val zero : String = (new Coerce[Int,String]).coerce(0)
    println("...")
  }
}

from scala3.

Current dotty master (9f3005c) still fails to reject the example from SI-9633.

from scala3.

Yes, @olhotak -- Scala and Dotty have deferred any fixes for null paths. In Dotty, the fixes have focused on lazy paths.

from scala3.

@olhotak I think you need -strict
EDIT: ah nevermind, this example uses null which we don't deal with yet as Nada said (waiting on non-nullable types)

from scala3.