!standard 7.3.2(6.1/4)                                 20-06-10  AI12-0382-1/01
!class binding interpretation 20-06-10
!status work item 20-06-10
!status received 20-06-09
!priority Low
!difficulty Easy
!subject Loosen type-invariant overriding requirement of AI12-0042-1
!summary

The rule in RM 7.3.2(6.1/4), added by AI12-0042-1, should only apply
when a type extension occurs immediately within the visible part of
a package specification.

!question

RM 7.3.2(6.1/4):

  If a type extension occurs at a point where a private operation of
  some ancestor is visible and inherited, and a Type_Invariant'Class
  expression applies to that ancestor, then the inherited operation
  shall be abstract or shall be overridden.

This rules seems unnecessarily restrictive, and makes cases of type extensions
like the following illegal:

package Type_Invariant_Pkg is

   type T1 is tagged private with Type_Invariant'Class => Is_Ok (T1);

   function Is_Ok (X1 : T1) return Boolean;

   procedure Op (X : in out T1) is null; -- [1]

private

   type T1 is tagged record F1, F2 : Natural := 0; end record;

   procedure Priv_Op (X : in out T1) is null; -- [2]

   function Is_Ok (X1 : T1) return Boolean is (X1.F1 <= X1.F2);

   type T1_Priv_Deriv is new T1 with null record; -- Illegal by AI12-0042-1
   --
   -- Inherits procedure Op (X : in out T2);
   -- Inherits procedure Priv_Op (X : in out T2); -- Must override Priv_Op

end Type_Invariant_Pkg;

package Type_Invariant_Pkg.Child_Priv_Part is

   type T2 is new T1 with private;

private

   type T2 is new T1 with null record;             -- Illegal by AI12-0042-1
   --
   -- Inherits procedure Op (X : in out T2);
   -- Inherits procedure Priv_Op (X : in out T2);  -- Must override Priv_Op
end Type_Invariant_Pkg.Child_Priv_Part;

There seems to be no good reason to require that for such derivations that
inherit from a visible inherited private operation of the ancestor the
inherited operation must be overridden, since it won't be a boundary
entity of the derived type.

Should this rule be tightened up? (Yes.)

!recommendation

(See Summary.)

!wording

Modify 7.3.2(6.1/4) as follows:

  If a type extension occurs {immediately within the visible part of
  a package specification,} at a point where a private operation of
  some ancestor is visible and inherited, and a Type_Invariant'Class
  expression applies to that ancestor, then the inherited operation
  shall be abstract or shall be overridden.

!discussion

7.3.2(6.1/4) is basically a methodological rule to avoid surprises,
as stated in AI12-0042-1, and doesn't address any definitional problem.
The AI gives an example involving a private child package where in
its visible part a type extension inherits a private subprogram from
an ancestor declared in the parent package, and the subprogram is now
required to be overridden. Since the ancestor's private subprogram
is not a boundary entity, it would be surprising if the inherited
subprogram would be a boundary entity since calls to it will
effectively invoke the nonboundary version of the ancestor.

However, there seems to be no such rationale when the type extension
occurs within the private part of the package declaring the ancestor
of the type extension, or if it occurs in the private part of a child
package. In those cases, the inherited subprogram will not be a
boundary entity, so there's no real reason to require overriding.

In fact, there's good evidence that the intent was to have this rule
only apply to private operations that are inherited in a package's
visible part. The following is stated in 7.3.2, "Incompatibilities
with Ada 2012":

  41.h/4 {AI12-0042-1} Corrigendum: A private operation that is inherited
  in the visible part of a package to which a class-wide invariant applies
  now requires overriding. This is a very unlikely situation, and will
  prevent problems with invariant checks being added to routines that
  assume that they don't have them.

So it seems fairly clear that the rule wasn't written properly to reflect
that the overriding should only be required when the inheritance occurs
(immediately) within a visible part, and we correct the rule to say that.

!example

(See !problem.)

!corrigendum

!ACATS test

!appendix

****************************************************************