isVolatile incorrect for intersection types

[samuelgruetter]

@namin and me had a look at the isVolatile method in Types/TypeOps.

If we try the following example:

object Test {
  trait A {
    type X = String
  }
  trait B {
    type X = Int
  }
  lazy val o: A & B = ???

  def xToString(x: o.X): String = x

  def intToString(i: Int): String = xToString(i)
}

It's accepted by dotty, which means that we can cast Int to String...

I added debug output for the results of isVolatile, and it prints

isVolatile(AndType(TypeRef(ThisType(module class Test$),A),TypeRef(ThisType(module class Test$),B)))=false

But as we understood isVolatile, it should return true for all types which are possibly uninhabited.

The and-case in needsChecking looks bad:

case AndType(l, r) =>
  needsChecking(l, true) || needsChecking(r, true)

because we cannot just look seperately at l and r, but we should check if there are conflicting members in l and r.

In Scala, this is not a problem, because we only have with, which is asymmetric, so the members of r override those of l and in our example, o.X is only Int.

From a theoretical point of view, we are bothered by the fact that !isVolatile is not preserved by weakening, i.e.

A <: B and !isVolatile(B) does not imply !isVolatile(A)

so we doubt if a !isVolatile judgment would be useful in a typesafety proof (needs more thinking...).

Additionally, if we replace the implementation of needsChecking (which seems to be just an optimization) by this

def needsChecking(tp: Type, isPart: Boolean): Boolean = true

we get a java.util.NoSuchElementException: head of empty list, so it's not just an optimization...

[samuelgruetter]

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

[odersky]

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

[samuelgruetter]

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

[smarter]

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

[odersky]

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

[namin]

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

[odersky]

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

[namin]

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

[odersky]

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

[DarkDimius]

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

[odersky]

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

[namin]

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

[odersky]

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

[namin]

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

The second proposal feels right long-term...

[namin]

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

[TiarkRompf]

@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!")

[namin]

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

[TiarkRompf]

@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

[odersky]

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

[RossTate]

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.

[TiarkRompf]

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

[RossTate]

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.

[odersky]

@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

[TiarkRompf]

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

[odersky]

@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

[TiarkRompf]

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

[odersky]

@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?

[TiarkRompf]

Yes, agreed.

[namin]

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.

[namin]

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("...")
  }
}

[olhotak]

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

[namin]

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

[smarter]

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