[Class Modifiers] Overlap in lint and base/final subtyping restriction

[kallentu]

In the spec, it mentions in the "Disallowing implementation" section:
It is a compile-time error if a subtype of a declaration marked base or final is not marked base, final, or sealed. This restriction applies to both direct and indirect subtypes and along all paths that introduce subtypes: implements clauses, extends clauses, with clauses, and on clauses. This restriction applies even to types within the same library.

Then in the "reopen lint" section it states:
Extends or mixes in a class, mixin, or mixin class marked interface or final and is not itself marked interface or final.

Doesn't the error cover the final case in the lint already?
Is the lint supposed to only cover interface types? And if so, do we want a lint or annotation at all for just this one scenario?

cc @pq @bwilkerson @dart-lang/language-team

[lrhn]

No, not entirely. The error case allows a base class which has a final supertype. (And maybe even an interface superclass.)

The lint "interface" warnings are given for for super/sub-class modifier combinations: final/none, final/base, interface/none, and interface/base.

Of these, only final/none is an error, and that lint warning should be omitted in favor of the error.
The remaining three, including one with final, should be reported.

The 5x5x4 table of superclass, subclass, relation and its effect (within the same library) would be:

subclass	superclass	extends	with	implements	on	(comment)
none	none
none	interface	lint	lint			(Don't allow inheriting implementation)
none	base	error	error	error	error
none	final	error	error	error	error
none	sealed	see supers	see supers	see supers	see supers
interface	none
interface	interface
interface	base	error	error	error	error
interface	final	error	error	error	error
interface	sealed	see supers	see supers	see supers	see supers
base	none
base	interface	lint	lint
base	base
base	final	lint	lint			(Not completely sure about implements)
base	sealed	see supers	see supers
final	none
final	interface
final	base
final	final
final	sealed
sealed	none
sealed	interface
sealed	base
sealed	final
sealed	sealed

In general, the errors and lints are all about inheriting implementation.

• An interface or final class suggests that a subclass must not inherit its implementation.
• A base or final class enforces that you must inherit its implementation. There cannot be a fresh implementation in another library which is not inheriting the implementation (or some implementation from the same library).

These restrictions are strongly enforced outside of the library.
Inside the library we enforce some and suggest others through the lint.

• If superclass is base or final, subclass must be base, final, sealed, otherwise it's an error. This enforces the "must inherit implementation" rule. It allows a base subclass of a final superclass, so it's not entirely monotonic.
• Otherwise, if superclass is interface or final (doesn't allow inheriting implementation), and the subclass extends or mixes in the superclass (inherits implementation) and is not itself interface, final or sealed (allows others to inherit that inherited implementation), give a lint. (Silence lint with @reopen or // ignore.)
• And if superclass is final, subclass extends or mixes it in and subclass is base, also give a lint. That also allows inheriting the implementation of the final superclass. (Even if the class is private, because we don't want to decide whether it escapes somehow.)
• A sealed subtype doesn't introduce new restrictions, but propagates base and final of its superclasses, and the interface of its extended or mixed-in superclasses. (That is, for these purposes, treat a sealed class as having the LUB of its supertypes in the diamond none < base < final/none < interface < final partial order.)
• The extends and with relations both inherit implementation from the superclass, so they behave the same
• And on types are mostly like implements relations, not carrying the implementation of the supertype, so they behave the same as implements.

Abbreviated and reordered, that would be:

subclass	superclass	extends	with	implements	on	(comment)
*	none					(Always safe)
final	*
sealed	*
base	base
interface	interface
none	interface	lint	lint			(Don't allow inheriting implementation)
base	interface	lint	lint
base	final	lint	lint
base	sealed	see supers	see supers
none	base	error	error	error	error	(Don't allow implementing)
none	final	error	error	error	error	(replaces lint)
interface	base	error	error	error	error
interface	final	error	error	error	error
none	sealed	see supers	see supers	see supers	see supers	(Inherit behavior)
interface	sealed	see supers	see supers	see supers	see supers

@eernstg Am I missing anything?

[eernstg]

[Edit Mar 2: Adjusted the terminology in the rule about implicitly induced class modifiers for a sealed declaration: The precise terminology is that class A extends S with M1 .. Mk implements S1 .. Sm {} has direct superinterfaces S with M1 .. Mk, plus S1, S2 .. Sm. That is, the superclass, including all mixins, is one superinterface, not k+1 superinterfaces. Each mixin application (S with M1, S with M1, M2 and so on) has its own implicitly induced class modifiers, cf. #2830.]

Big tables is hard work. ;-)

I think the 'see supers' classification is a little bit non-obvious, and I'd still like to treat sealed as a completely orthogonal property (now at the semantic level, because we won't do it at the syntactic level). This does reduce your last table somewhat.

So we consider the sealed modifier to give rise to implicitly induced modifiers as follows:

1. A sealed declaration D is considered final if it has a direct superclass which is final, or it has a direct superclass which is interface and it has a direct superinterface which is base.
2. Otherwise, D is considered base if it has a direct superinterface which is base or final.
3. Otherwise, D is considered interface if it has a direct superclass which is interface.
4. Otherwise, D does not have any implicitly induced class modifiers.

In particular, a sealed mixin can never be implicitly final or interface, because it never has a superclass. It can be implicitly base, though.

Other than this, sealed is handled by one simple rule: It is a compile-time error for a declaration in a library L to have a sealed direct superinterface which is declared in a different library than L.

Here's your table again, simplified a little bit because we never mention sealed explicitly, and because identical columns have been merged:

subtype	supertype	extends/with	implements/on	Comment
*	none			Always safe
final	*
base	base
interface	interface
base	final	lint		Don't allow inheriting implementation
base	interface	lint
none	interface	lint
interface	final	error	error	Don't allow implementing
interface	base	error	error
none	final	error	error	(and the lint is suppressed)
none	base	error	error

@lrhn, does that capture your intentions around 'see supers'?

[lrhn]

I think so.

Let me try my own words:

• A sealed class or mixin prevents implementation if it has an immediate superinterface which is marked base or final.
• A sealed class or mixin prevents inheritance if it extends or mixes in a declaration which is marked interface or final.
• A sealed class or mixin is implicitly marked:
  • final if it prevents implementation and prevents inheritance.
  • base if it prevents implementation, but not inheritance.
  • interface if it prevents inheritance, but not implementation.
  • nothing, if it prevents neither.

Not sure it's the same thing.

[eernstg]

I think it's the same thing: The properties 'prevents implementation and prevents inheritance' are sufficient to ensure that we're in the first bullet in my rule; 'prevents implementations, but not inheritance' ensure that we are not in the first bullet, but we are indeed in the second bullet; and so on.

Nice! This also serves as a double check on the sanity of the rules.

[kallentu]

I'd like to take another look at this and clarify my understanding with the specification.

@eernstg @lrhn How does the base/final subtype restriction come into play with induced modifiers? It seems like any class/mixin with a supertype that is base or final would be induced either base or final.

Does this example induce any modifiers? From the two comments above, I'm a little confused on what happens here.

base class A {}
sealed class B extends A {} // Does not induce any modifiers?

Same with this example:

final class A {}
sealed mixin B implements A {} // should produce error that B must be base or final because A is final, but induces base?

Could you help me clarify how the sealed induced modifiers that you've specified above work with the base/final errors with induced modifiers on sealed? Are the base/final subtyping errors separate to the induced modifier definition?
Maybe I'm missing something!

[eernstg]

How does the base/final subtype restriction come into play with induced modifiers?

The implicitly induced modifiers are just as good as the explicitly written ones.

I'd prefer to say that we have a program with modifiers base, interface, final, sealed; we check the sealedness separately (it's an error to have a direct subinterface in a different library); next, we compute the implicitly induced modifiers on every sealed declaration and every mixin application; going ahead, sealed is ignored; finally, we check 'It is a compile-time error if a subtype of a declaration marked base or final is not marked base or final', and 'it's a lint if a subtype extends or mixes in a class, mixin, or mixin class marked interface or final, and is not itself marked interface or final.

This means that we apply a very simple local check, which is possible because we have changed the program such that it has interface, base, and final modifiers on every class that semantically needs to satisfy the associated constraints. I find this approach simpler to understand than an approach where we compute the missing modifiers on sealed classes and mixin applications on the fly, based on traversals of part of the superinterface graph.

It seems like any class/mixin with a supertype that is base or final would be induced either base or final.

Yes. The implicitly induced modifiers should be exactly sufficient to avoid the error and the lint (where sealed is ignored, because it has already done its job in terms of implicitly inducing some modifiers). So that base or final modifier is required if a supertype has base or final.

base class A {}
sealed /*base*/ class B extends A {}

final class C {}
sealed /*base*/ mixin M implements C {} 

The reason why we must implicitly induce base on class B is that otherwise it would have a compile-time error (again: because we're ignoring sealed): A has base and is a direct superinterface of B. The reason why we must implicitly induce base on mixin M is that it has a direct superinterface which is final.

We do not induce final on M for the following reason: The base part of final is required because C is a superinterface with final; but the interface part of final isn't required for M, because M does not inherit any instance member implementations from C. So in the traversal from C to M we drop the interface part of the final modifier, and hence base is exactly what we need on M in order to avoid re-opening anything.

Are the base/final subtyping errors separate to the induced modifier definition?

The implicitly induced interface, base, and final modifiers on sealed declarations and on mixin applications are intended to ensure that there is no re-opening, and also that the modifiers are most permissive ones we can possibly have while still ensuring that there is no re-opening. This implies that the induced modifiers won't have any errors and they won't have any lints. In that sense they are separate.

But there is no need to make them an exception, they just happen to be non-re-opening by construction, they can be checked according to the standard rules (actually, that's the whole point ;-).

[munificent]

There's a lot in these comments. :) Is this all sorted out now, or is there more to do here?

[kallentu]

Lint and error are now completed, we can close this out now.