[sealed] Changes to type system

[Jonathan Gibbons]

I'd be curious to see how the proposed rules interact (if at all) with 
the accessibility of the subtypes, and accessibility of sealed subtypes 
in particular.

-- Jon


On 2/18/20 7:47 AM, Gavin Bierman wrote:
> Dear Experts:
>
> One aspect of sealed types that we have not discussed before, is that it
> suggests a change in the type system.
>
> This change regards conversions used in casting contexts. For example, in Java
> right now:
>
>     interface I {}
>     class C {} // does not implement I
>
>     void test (C c) {
>         if (c instanceof I)
>             System.out.println("It's an I");
>     }
>
> This compiles even though it is *currently* not possible for a C object to
> implement the interface I. Of course, it might be, for example:
>
>     class B extends C implements I {}
>
>     test(new B());
>     // Prints "It's an I"
>
> So, the conversion rules capture "open extensibility"; i.e. the Java type system
> does not assume a closed world, classes and interfaces could be extended, and
> casting conversions compile to runtime tests, so we can safely be flexible.
>
> However, at the other end of the spectrum the conversion rules do address
> the case where a class can *not* be extended, i.e. when it is a *final* class.
>
>     final class C {}
>
>     void test (C c) {
>         if (c instanceof I)
>             System.out.println("It's an I");
>     }
>
> The method test fails to compile, as the compiler knows that there can be no
> subclass of C, so as C does not implement I then it is never possible for a C
> value to implement I. This is a compile-time error.
>
> But what about if C is not final, but *sealed*? Given that its direct subclasses
> are explicitly enumerated, and - by the definition of being sealed - in the same
> module, we would surely expect the compiler to look to see if it can spot a
> similar compile-time error. Consider the following code:
>
>     interface I {}
>     sealed class C permits D {}
>     final class D extends C {}
>     
>     void test (C c) {
>         if (c instanceof I)
>             System.out.println("It's an I");
>     }
>
> Class C does not implement I, and is not final - so by the old rules we might
> conclude that there is a conversion - but it is sealed. There is one permitted
> direct subclass of C: D. By definition of sealed types, D must be either final,
> sealed or non-sealed. In this example, all the direct subclasses of C are final
> and do not implement I, so in fact we can safely reject this program, as there
> cannot be a subtype of C that implements I.
>
> In contrast, consider a similar program where one of the direct subclasses of
> the sealed class is non-sealed:
>
>     interface I {}
>     sealed class C permits D, E {}
>     non-sealed class D extends C {}
>     final class E extends C {}
>
>     void test (C c) {
>         if (c instanceof I)
>             System.out.println("It's an I");
>     }
>
> This is type correct as it is possible for a subtype of the non-sealed type D to
> implement I.
>
> The trick is to extend the notion of allowed narrowing reference conversion (JLS
> 5.1.6.1) to follow the sealed type declarations. I'll spare you the gory details
> in this email - they will appear in the JLS draft appearing soon (!) - but I
> wanted to check that this extension to the type system seems reasonable.
> Obviously it will be putting more strain on the type checker. Is everyone happy
> with this extension?
>
> Thanks,
> Gavin
>
>
> PS: Some further examples for your amusement:
>
> Example 1:
> ----------
>
> non-sealed interface I {}
> non-sealed interface J {}
>
> I i;
> if (i instanceof J) {} // Yes!
>
> Example 2:
> ----------
>
> sealed interface I permits C {}
> final class C implements I {}
> non-sealed interface J {}
>
> I i;
> if (i instanceof J) {} // Error, only instance of I is C
>                         // Which doesn’t implement J
>
> Example 3:
> ----------
>
> non-sealed interface I {}
> sealed interface J permits C {}
> final class C implements J {}
>
> I i;
> if (i instanceof J) {} // Error, only instance of J is C
>                         // which doesn’t implement I
>
> Example 4:
> ----------
>
> sealed interface I permits A {}
> sealed interface J permits B {}
> final class A implements I {}
> final class B implements J {}
>
> I i;
> if (i instanceof J) {} // Error, similar to above
>
>
> Example 5:
> ----------
>
> non-sealed class C {}
> non-sealed interface I {}
>
> C c;
> if (c instanceof I) {} // Yes!
>
> Example 6:
> ----------
>
> non-sealed class C {}
> sealed interface I permits A {}
> final class A implements I {}
>
> C c;
> if (c instanceof I) {} // Error
>
> Example 7:
> ----------
>
> final class C {}
> non-sealed interface I {}
>
> C c;
> if (c instanceof I) {} // Error
>
> Example 8:
> ----------
>
> final class C {}
> sealed interface I permits D {}
> final class D implements I {}
>
> C c;
> if (c instanceof I) {} // Error
>
> Example 9:
> ----------
>
> sealed class C permits D {}
> final class D extends C {}
> non-sealed interface I {}
>
> C c;
> if (c instanceof I) {} // Error
>
> Example 10:
> -----------
>
> sealed class C permits D {}
> final class D {}
> sealed interface I permits E {}
> final class E {}
>
> C c;
> if (c instanceof I) {} // Error
>
> Example 11:
> -----------
>
> non-sealed interface I {}
> non-sealed class C {}
>
> I i;
> if (i instanceof C) {} // Yes!
>
> Example 12:
> -----------
>
> non-sealed interface I {}
> final class C {}
>
> I i;
> if (i instanceof C) {} // Error
>
> Example 13:
> -----------
>
> non-sealed interface I {}
> sealed class C permits D {}
> final class D {}
>
> I i;
> if (i instanceof C) {} // Error
>
> Example 14:
> -----------
>
> sealed interface I permits D {}
> final class D {}
> non-sealed class C {}
>
> I i;
> if (i instanceof C) {} // Error
>
> Example 15:
> -----------
>
> sealed interface I permits D {}
> final class D implements I {}
> final class C {}
>
> I i;
> if (i instanceof C) {} // Error
>
> Example 16:
> -----------
>
> sealed interface I permits D {}
> final class D implements I {}
> sealed class C permits E {}
> final class E extends C {}
>
> I i;
> if (i instanceof C) {} // Error
>