[sealed] Changes to type system

[Gavin Bierman]

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