Unsoundness from not-yet-initialized path without involving divergence

[mario-bucev]

Compiler version

Scala compiler version 3.0.0-RC2-bin-SNAPSHOT-nonbootstrapped-git-55da939 -- Copyright 2002-2021, LAMP/EPFL

Minimized code

@main def test: Unit = {
  trait Cov[+X] {
    def get: X
  }
  trait Bounded {
    type T >: Cov[Int] <: Cov[String]
  }
  val t: Bounded = new Bounded {
    // Note: using this instead of t produces an error (as expected)
    override type T >: t.T <: t.T
  }
  
  val covInt = new Cov[Int] {
    override def get: Int = 3
  }
  val str: String = ((covInt: t.T): Cov[String]).get // ClassCastException: class Integer cannot be cast to class String
}  

Output

Click to expand

Exception in thread "main" java.lang.ClassCastException: class java.lang.Integer cannot be cast to class java.lang.String (java.lang.Integer and java.lang.String are in module java.base of loader 'bootstrap')
	at Main$package$.test(Main.scala:16)
	at test.main(Main.scala:1)

Expectation

The above instantiation of t should be rejected, as it is using a not-yet-initialized t to construct non-sensical bounds using the assumption that Cov[Int] <: Cov[String].

This issue is similar to #5854 but does not involve divergence.

[liufengyun]

The initialization checker can be reused to catch such errors. Currently, type statements are ignored.

We can capture usage of terms in types and report an error if a field is not known to be initialized.

/cc: @olhotak @natsukagami

[odersky]

@liufengyun I think that would be worth a try.

[olhotak]

I should wait until after we discuss this with @liufengyun and @natsukagami, but one challenge we'll need to keep in mind is that initialization state is flow-sensitive while types are global, flow-insensitive.

For example, if some field has type T or the parameter or return type of some method is T, then that field can be accessed at any time and the method can be called at any time, independently of when a term that T depends on has been initialized.

Another way of saying this is that we can allow dependency on a term only if we can prove that the term will definitely be initialized "eventually", but how do we define when "eventually" will be? Many similar examples involve terms that would get initialized after the completion of some infinite loop.

Something to think about before our next initialization meeting.

[liufengyun]

As a memo for the meeting with @olhotak and @natsukagami , we believe theoretically it makes sense to perform this kind of check using the initialization checker. The intuitive reason is that we may imagine that Scala does not have type erasure semantics, therefore, a type selection on an uninitialized field is always a semantic error.

However, the initialization checker has some difficulty for the concrete case above, as it involves the initialization of local variables (not fields), which is governed by a forward reference check (not the initialization check). The same example wrapped in a class (instead of method) can be handled well by the initialization checker:

class A {
  trait Cov[+X] {
    def get: X
  }
  trait Bounded {
    type T >: Cov[Int] <: Cov[String]
  }
  val t: Bounded = new Bounded {
    // Note: using this instead of t produces an error (as expected)
    override type T >: t.T <: t.T
  }
  
  val covInt = new Cov[Int] {
    override def get: Int = 3
  }
  val str: String = ((covInt: t.T): Cov[String]).get // ClassCastException: class Integer cannot be cast to class String
}

[liufengyun]

The problem that involves fields of a class is now solved in #11716. For the version based on local variables, we need to enhance the forward reference check (use initialization checker for it?).