- Notifications
You must be signed in to change notification settings - Fork 1.1k
Description
@namin and me had a look at the isVolatile method in Types/TypeOps.
If we try the following example:
objectTest{traitA{typeX=String } traitB{typeX=Int } lazyvalo:A&B=???defxToString(x: o.X):String= x defintToString(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:
caseAndType(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
defneedsChecking(tp: Type, isPart: Boolean):Boolean=truewe get a java.util.NoSuchElementException: head of empty list, so it's not just an optimization...