Nullness Checker: unsoundness with unboxing UnknownInitialization types

[wmdietl]

This example:

import org.checkerframework.checker.initialization.qual.UnknownInitialization;

class Demo {
  @UnknownInitialization Integer n;
  
  Demo() {
    int y = n;
  }
  
  public static void main(String[] args) {
      new Demo();
  }
}

passes the Nullness Checker without an error or warning.
Executing it produces an NPE.

When the field n is not annotated, making it UnderInitialization in the constructor, the correct error is raised.

Neither version warns about the field not being initialized by the constructor, which is maybe OK when a different error is raised.