Derived types, private parts, abstract subprograms

[adam@irvine.com (Adam Beneschan)]

We believe we have found an error in some Ada source code that is
publicly available on the Internet, that isn't supposed to compile but
that some compilers apparently let slip through.  However, I wanted to
ask to make sure my interpretation of the RM is correct.

package pak1 is
   type T1 is abstract tagged null record;
   procedure Operation (X : T1) is abstract;
end pak1;

with pak1;
package pak2 is
   type T2 is new pak1.T1 with null record;
private
   procedure Operation (X : T2);
end pak2;

package pak3 is
   procedure Foo;
end pak3;

with pak2;
package body pak3 is
   type T3 is new pak2.T2 with null record;

   procedure Foo is
       X : T3;
   begin
      Operation (X);      --legal?
   end Foo;

end pak3;


As I interpret the RM: When T2 is declared, Operaton is inherited, but
the inherited subprogram is still abstract.  3.9.3(6) says that
Operation must be overridden with a nonabstract procedure, but that
the overriding may be done in the private part, which is what's done
here.

When T3 is declared, T2's primitive subprograms are inherited.  As I
understand it, this includes primitive subprograms of T2 that are
overridden, since those would reemerge in places where the overriding
subprogram isn't visible.  Is this correct in general for derived
types?  Thus, it would seem that T3 would inherit both the abstract
and the nonabstract versions of Operation from T2; but by 7.3.1(6),
the nonabstract version is not visible in places where pak2's private
part is not visible.  In this instance, the nonabstract inherited
version of Operation that operates on T3 is, in the language of
7.3.1(6), "not declared at all" and thus "cannot be named in a call"
(but still could be called indirectly with a dispatching call).  This
would seem to mean that the call with the "--legal?" comment cannot
name the nonabstract inherited Operation; however, the *abstract*
inherited Operation is still visible (reemerges?), and thus Operation
in this statement names this subprogram, but this makes the call
illegal because it's a nondispatching call on an abstract subprogram
(3.9.3(7)).

Is this all correct?

Is this the intent of the language?  It seems like it should be,
because declaring pak2.Operation in the private part of pak2 should
mean that you can't call it directly when the private part of pak2
isn't visible, even via a derived type.  But I want to make sure there
isn't any subtlety I've missed before I make a bug report.

Thanks in advance for any help,

                                      -- Adam