Skip to content

isVolatile incorrect for intersection types #50

Closed
@samuelgruetter

Description

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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions