[Class Modifiers] Specification of Disallowing Implementation seems unnecessarily complex

[leafpetersen]

The section on disallowing implementation in the class modifiers spec is quite hard to read, and I think unnecessarily so. As best I can tell, it is entirely equivalent to the following two sentence specification:

It is a compile-time error to implement an interface I in library L unless all super-interfaces of I (including I) which are marked `base` or `final` are also defined in L.

It is a compile-time error if a sub-interface of a declaration marked `base` or `final` is not marked `base`, `final`, or `sealed`.

Am I missing something? This seems much clearer and easier to understand. It might be reasonable to present the "cannot be implemented locally" algorithm as commentary on a possible implementation, but as best I can tell it is equivalent, and seems much harder to reason through.

cc @dart-lang/language-team

[lrhn]

That does look mostly correct.

There is one extra clause, for a mixin declaration in a different library with a sealed declaration as on type.
That case causes the mixin's interface to prevent implementation too, even if there is no supertype marked final or base.
We can't just say "has a sealed declaration's interface from another library as superinterface" because sealed isn't transitive, and the other library can have an open subclass of a sealed declaration.

(I'd probably also cross some t's and dot some i's wrt. the distinction between an interface and its declaration.)

The sealed class thing is why I ended up with the current definition:

• You cannot implement an interface which has a base/final declared superinterface outside of the same library as all such superintefaces' declarations.
• But you also cannot implement the interface of this mixin declaration, even inside its own library, even if it has no base/final superinterfaces, and that goes for all its subtypes too.

Maybe trying to unify those two was the mistake.

Written separately, it can be:

• It's a compile-time error to implement an interface I in library L unless all superinterfaces of I
  are either declared in L or not marked final or base.
• It's a compile-time error if a declaration D has an interface with superinterface S,
  the declaration of S is marked final or base and D is not marked final, base or sealed.

Plus:

• A mixin declaration D in library L is said to be mixin-on-sealed (strawman name)
  if it has an on clause type denoting a declaration S in a different library than L,
  and S is marked sealed.
• It's a compile-time error to implement any interface I which has the interface of a mixin-on-sealed
  declaration as superinterface.
• It's a compile-time error if a declaration D has an interface with a superinterface which is
  the interface of a mixin-on-sealed declaration as superinterface, and D is not marked base, final or sealed.

That's an option.

I do like a more unified approach better, but it can still be made more declarative than the iterative algorithm we have now:

An interface I prevents implementation in library L if

• The declaration of I is in a library other than L and is marked base or `final.
• The declaration of I is a mixin declaration in a library K,
  it has an on type denoting a declaration M in a library other than K, and M is marked sealed.

It's a compile-time error if a declaration in library L implements an interface whose declaration prevents
implementation in L.

It's a compile-time error if a declaration D has a superinterface which prevents
implementation (in any library), and D is not marked base, final or sealed.

[leafpetersen]

There is one extra clause, for a mixin declaration in a different library with a sealed declaration as on type.
That case causes the mixin's interface to prevent implementation too, even if there is no supertype marked final or base.

I don't know exactly what you mean here - do you mean that the mixin declaration is in a different library from the sealed declaration, or that the mixin and sealed declaration are in one library and the class trying to implement it is in a separate library. Either way:

1. This doesn't seem to be implemented (and hence probably isn't tested)
2. I don't think this is enough to close a soundness hole that is induced by mixins.

For 1), I currently see the following code as having no errors:

// lib1.dart
import "lib2.dart";
sealed class A {}
mixin M1 on A {}
class C implements M2 {}

//lib2.dart
import "lib1.dart";
mixin M2 on A {}
class ImplementsBoth implements M1, M2 {}

For 2), I think that nothing we have specified makes the declaration of M2 or class C an error, but I think that this breaks the soundness of sealed (at least for modular compilation) since if you look at lib1.dart you only see one direct subtype of A, but M2 is a direct subtype of A defined in a different library, which has inhabitants from C. Am I missing an error somewhere which catches this? If so it is currently not implemented.

[lrhn]

I mean that if a mixin declaration is mixin Id on S1, S2 ...., and one of the Sis denote a sealed declaration of another library, then that mixin's interface must not be be implementable, and nor must any subinterface of it.
The mixin declaration itself prevents local implementation, in the current specification's terms.

The example of usage is:

library l1;
sealed class Widget { ... }
class StatefulWidget extends Widget { ... }
class StatelessWidget extends Widget { ... }

and

library l2;
/// Applies to both [StatefulWidget] and [StatelessWidget].
base mixin SpecialWidget on Widget { ... }

Here SpecialWidget must be marked base, final or sealed, and it prevents local implementation.
I do believe it prevents any mixin soundness issues, and it allows defining mixins that can be used
on the entire family of subclasses of a sealed class.

In your example, M2 must be marked base, final or sealed (because it prevents local implementation).
That prevents class C implements M2 {} from being valid.
Also since M2 prevents local implementation, that prevents class ImplementsBoth implements M1, M2 as well.

The only way to subclass a mixin which prevents local (and therefore global) implementation is to apply it. The only thing you can apply it to is an extensible subclass of A (can't apply it to A itself, it's sealed so not a valid superclass outside of its library). All extensible subclasses of A are subtypes of a subtype of A declared in in lib.dart`. And that's enough for exhaustiveness.

You can do class C = A with M2; in lib1.dart. That is a subclass of A in C with no other intermediate subclasses between them, so it should be counted towards the "immediate subclasses" of A used for exhaustivness.
(Which classes that is is something we do need to define precisely.)

Or in other words, the only way you can ever create an instance whose runtime type implements M2 is by applying M2 to an extensible superclass which implements A. By property of A being sealed, all such classes are subclasses of M1 or another subclass of A in the same library, or it's A itself and the mixin application happens inside lib1.dart and can be counted towards exhaustiveness.
You cannot use M2 to create an instance which would break exhaustiveness.

[leafpetersen]

Here SpecialWidget must be marked base, final or sealed, and it prevents local implementation.
I do believe it prevents any mixin soundness issues, and it allows defining mixins that can be used
on the entire family of subclasses of a sealed class.

I haven't had time to work through this in detail, but two quick comments:

1. The implementation does not enforce this, and I see no failing tests around this, so I think this is unimplemented and untested behavior. If we want this behavior we should fix both of those things ASAP! :)

2. This is really weird behavior. It's highly non-intuitive to me that SpecialWidget would be allowed, but be required to be marked base. There are no other places that I'm aware of where having a superclass marked sealed induces a transitive modifier requirement. It seems to me that it would be better to just make SpecialWidget an error. It directly subtypes Widget.

[eernstg]

It seems to me that it would be better to just make SpecialWidget an error. It directly subtypes Widget.

That's what I proposed already long ago (by treating on and implements identically in the rules about class modifiers). I thought @lrhn had actually sorted out the details such that we could allow it, but it could be a safer bet to make this case an error. We are then in a position where we can generalize and allow it later on, without breakage.

[leafpetersen]

We decided in the meeting this morning that the SpecialWidget example above should be an error. That is, we add an error saying that:

• It is a compile-time error to use an interface I as the on type of mixin declaration D if I is in a different library from D and I is marked sealed.

This eliminates the need for the additional cases. We can then reduce the specification of the transitivity requirements to the following (based on my original wording, adjusted to use some of the formulation from @lrhn above):

• It is a compile-time error if a declaration in library L implements an interface I whose declaration is in a library other than L and I is marked base or final
• It is a compile-time error if a declaration D has a super-interface which is marked base or final and D is not marked base, final, or sealed.

Does this seem reasonable and correct?

[lrhn]

Close for the "local implementation restriction". Let me try:

• It's a compile-time error if a declaration in library L implements an interface I, and I has a superinterface S whose declaration is in another library than L and is marked base or final.

We need the two steps: The declaration D with an implements clause (what we want to prevent) pointing to an interface I, but I can be declared in the same library as D and just be (validly) extending S, so we need to link it to an other-library base or final declaration.

This is what I normally call "I prevents implementation in L", and then it's a compile-time error to implement, in L, an interface which prevents implementation in L.
The extra definition is probably not necessary. Unlike "prevents implementation" it's not used anywhere else.

[leafpetersen]

PR from @lrhn with proposed updates here.

[leafpetersen]

This has been resolved.