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