Profile mismatch?

[Simon Wright <simon@pushface.org>]

Given the code below

   package Profile is
      type A1 is abstract tagged limited null record;
      procedure P (This : not null access A1);
      type A2 is abstract new A1 with null record;
      procedure P (This : access A2);              -- mismatch
      type T1 is new A1 with null record;
      procedure P (This : access T1);              -- mismatch
      type T2 is new A2 with null record;
      procedure P (This : not null access T2);     -- mismatch
      type T3 is new T2 with null record;
      procedure P (This : access T3);              -- mismatch
   end Profile;

should a compiler recognise the mismatches of the null exclusions where
indicated?

GNAT (4.8, 4.9, GPL 2013) accepts this code without comment. I've seen
very similar cases (structurally, but with many more subprograms) which
GNAT didn't accept, saying

   not subtype conformant with operation inherited at line 42
   type of "This" does not match

I've not yet tried to track this down.