Is there a way to verify two generic formals are the same type if one is incomplete?

The previous version of this answer missed the fact that Jere needs it to work for formal incomplete types, which were introduced with AI05-0213.

One of the (main?) use cases for that AI was to make it easier to create signature packages (see the Ada 2012 Rationale, section 4.3) in some circumstances. So, here’s an offering using a signature package - no idea whether it meets the desired use case.

generic
   type T is tagged;
package Signature is
end Signature;

with Signature;
generic
   type T is tagged private;
   with package Sig is new Signature (T);
package Parent is
   subtype Parent_T is T;
   Instance : T;
end Parent;

generic
   type T is new Parent.Parent_T with private;
   with package Sig is new Signature (T);
package Parent.Child is
end Parent.Child;

with Signature;
with Parent.Child;
package User is
   type Base is tagged null record;
   procedure Proc (Param : Base);

   package Sig_For_Parent is new Signature (T => Base);
   package For_Parent is new Parent (T => Base, Sig => Sig_For_Parent);

   --  this is OK
   type Extension is new Base with null record;
   procedure Proc (Param : Extension);
   package Sig_For_Child is new Signature (T => Extension);
   package For_Child
   is new For_Parent.Child (T => Extension, Sig => Sig_For_Child);

   --  this fails
   type Wrong is tagged null record;  -- not in Base'Class
   package Sig_For_Wrong is new Signature (T => Wrong);
   package For_Wrong
   is new For_Parent.Child (T => Wrong, Sig => Sig_For_Wrong);

end User;

with Ada.Text_IO;
package body User is

   procedure Proc (Param : Base) is
   begin
      Ada.Text_IO.Put_Line ("Base_P's Proc called.");
   end Proc;

   procedure Proc (Param : Extension) is
   begin
      Ada.Text_IO.Put_Line ("Extension_P's Proc called.");
   end Proc;

end User;

with User;
procedure Test is
   Var : User.Extension;
begin
   Var.Proc;
end Test;

At the end of the Rationale chapter, the line

(If this is all too confusing, do not worry, the compiler will moan at you if you make a mistake.)

is certainly true. What I found while playing around with this code is that it’s not very good at telling you what the mistake is.

If you don't need the parent/child relationship of the generics, you can do something like this:

foo.ads

generic
   type T(<>) is tagged;
package Foo is

end Foo;

bar.ads

with Foo;

generic
   type T(<>) is tagged private;
   with package Foo_Instance is new Foo(T); --package parameter
package Bar is
 
end Bar;

This way, the complete type must exactly match the incomplete type, ie. it cannot be a type extension, thus:

with Foo;
with Bar;

package Baz is

   type Base is tagged;
   package Base_Foo is new Foo(Base);
   
   
   type Base is tagged null record;
   package Base_Bar is new Bar(Base, Base_Foo);
   
   
   type Extension is new Base with null record;
   package Extension_Bar is new Bar(Extension, Base_Foo); -- fails!

end Baz;

So I got some inspiration from Simon Wright's answer which included a Signature package. That by itself wasn't enough, but it was a necessary building block for the ultimate solution. Basically, since Ada doesn't provide a means to verify two generic formal types are the same, I used a separate package to provide that functionality at run time by generating a unique ID for the given type, passing that package to both the Parent and Parent.Child packages, and, inside the Parent.Child body, verify that both instances of the package had the same ID (and thus were the same package). An example is provided below:

The idea of the signature package led to the following ID package:

package Type_ID is

   type ID is limited private;
   function "="(L,R : ID) return Boolean;

   generic
      type Item_Type(<>);
   package Unique_ID is
      function Get_ID return ID;
   end Unique_ID;
   
private
   
   -- Implement ID however you wish, just needs to be a unique ID for
   -- each package instantiation

end Type_ID;

Then I changed the parent specification to:

with Type_ID;

generic
   with package ID is new Type_ID.Unique_ID(<>);
package Parent is
   type Instance is tagged private;
private
    -- private stuff
end Parent;

And the Parent.Child package spec was updated to:

with Base;

generic
   type T(<>) is new Base.Instance with private;
   with package ID is new Type_ID.Unique_ID(T);
package Parent.Child is
   
   type T_Access is access T;

   function Make(Ref : not null T_Access) return Parent.Instance;
   
end Parent.Child;

Finally, the part where the types are verified to be the same. Since both Parent and Parent.Child take an instance of Type_ID.Unique_ID(<>), we just need to make sure they are both the same instance by comparing the output of the Get_ID function within the package body of Parent.Child:

package body Parent.Child is

   -- Other implementation stuff

   use all type Type_ID.ID;
begin
   if Parent.ID.Get_ID /= Parent.Child.ID.Get_ID then
      raise Program_Error with "Invalid type passed to child package";
   end if;
end Parent.Child;

Basically adding my own run time type information.

Instantiation of the package then becomes:

with Ada.Text_IO;
with Type_ID;
with Base;
with Parent;
with Parent.Child;

procedure Main is

   type Test is tagged;

   package ID is new Type_ID.Unique_ID(Test);
   package P is new Parent(ID);

   type Test is new Base.Instance with record
      Thing :  P.Instance;
   end record;

   package PC is new P.Child(Test,ID);

   Thing : P.Instance := PC.Make(new Test);

begin
   Ada.Text_IO.Put_Line("Hello");
end Main;

is there a way in a child package to ensure a type passed into the child as a generic formal is the same type as (or even a descendant of) Parent.T?

Yes.

Generic
   Type Parent(<>) is tagged private;
Package Example is
End Example;

...and...

Generic
   Type Descendant(<>) is new Parent with private;
Package Example.Child is
End Example.Child;