GNAT GPL 2013 bug?

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

ARM 3.9.2(10/2)

"... If the dispatching operation overrides an inherited subprogram, it
shall be subtype conformant with the inherited subprogram."

Does not-null constraint count? To me (I am not a language layer) it does.
But GNAT GPL 2013 (20130314) swallows this:

   type T is tagged null record;
   procedure P (X : access T) is null;

   type S is new T with null record;
   overriding procedure P (X : not null access S) is null;

Which is a bug to me.

P.S. Being subtype conformant to another type (T vs S) is a tricky part.
Presumably "the inherited subprogram" is

   procedure P (X : access T);

after T is replaced by S. Which gives

   procedure P (X : access S);

and this must be subtype conformant to

   overriding procedure P (X : not null access S);

which is not. Is it?

P.P.S. There is of course a deeper issue with any constraints put on or
lifted upon inheritance regarding LSP and substitutability. Because it
might be safe to weaken a constraint (precondition actually). E.g. turning
the example around:

   type T is tagged null record;
   procedure P (X : not null access T);

   type S is new T with null record;
   overriding procedure P (X : access S);

This might be safe as the clients are promised more.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de