Using sequence in refinement results in error

[senier]

The following specification is rejected:

package Seq_In_Ref is

   type Byte is mod 2 ** 8;

   type M1 is
      message
         Length : Byte;
         Data : Opaque
            with Size => 8 * Length;
      end message;

   type M2 is
      message
         Value : Byte;
      end message;

   type M2s is sequence of M2;
   for M1 use (Data => M2s);
end Seq_In_Ref;

Parsing seq_in_ref.rflx
Processing Seq_In_Ref
seq_in_ref.rflx:19:24: parser: error: undefined type "Seq_In_Ref::M2s" in refinement of "Seq_In_Ref::M1"

At least, the error message is misleading and should be improved. Ideally we should support using sequences in refinements directly.

A workaround is to wrap the sequence into a message with a single element:

   type M2s_Message is
      message
         Data : M2
            with Size => Message'Size;
      end message;
   for M1 use (Data => M2s_Message);