Elaboration in generic package

[Simon Wright <simon@pushface.org>]

A StackOverflow user raises this problem
(http://stackoverflow.com/q/43349462/40851). The code:

   generic
      Top_M : Positive;
   package Mystic is
      type T is private;
      procedure Info;
   private
       type Table is array (Positive range <>) of Positive;
       function reallyComplicatedFunction(x : Positive) return Table;

       mytable : constant Table := reallyComplicatedFunction(top_m); --<<<<<
       -- I will need mytable for calculations later

       type T is array (mytable'Range) of Natural;
       -- T is very different from Table, except they share their Range
   end Mystic;

They wonder how the call to reallyComplicatedFunction at line 10
succeeds, given it looks like its body hasn't been seen yet (ARM
3.11(10)). Indeed, if I make Mystic non-generic (Top_M is a constant)
GNAT tells me

kryptozoon.ada:12:33: warning: cannot call "reallyComplicatedFunction" before body seen
kryptozoon.ada:12:33: warning: Program_Error will be raised at run time

and then, sure enough,

raised PROGRAM_ERROR : kryptozoon.ada:12 access before elaboration

Is it possible that the answer is ARM 3.11(13), "For the instantiation
of a generic unit that has a body, a check is made that this body is
already elaborated."? If so, this seems surprising.