Generic formals and Aspects

[Simon Wright <simon@pushface.org>]

Recently on StackOverflow there was a question[1] about clamping a value
to a range.

The answer, so far, suggests a generic:

   generic
      type Source_Type is range <>;
      type Destination_Type is range <>;
   function Saturate (X : Source_Type) return Destination_Type;

with discussion about what happens if Destination_Type'Range is not a
subset of Source_Type'Range.

I see in AARM 13.1.1(4.b)[2] that a formal_type_declaration is allowed to
include an aspect specification, so tried

   generic
      type Source_Type is range <>
        with Static_Predicate =>
          Long_Long_Integer (Destination_Type'First)
            >= Long_Long_Integer (Source_Type'First)
          and Long_Long_Integer (Destination_Type'Last)
            <= Long_Long_Integer (Source_Type'Last);
      type Destination_Type is range <>;
   function Saturate (X : Source_Type) return Destination_Type;

but GNAT (4.9.1, GPL 2014) said that Static_Predicate wasn't allowed
(nor was Dynamic_Predicate).

Predicate (GNAT-special?) was allowed, but had no effect: I was able to
instantiate with

   type Source is new Integer range 10 .. 20;
   type Destination is new Integer range 30 .. 40;


(a) what aspects are/should be allowed in a formal_type_declaration?

(b) how to write the generic to prevent this sort of mistake at compile
    time? (easy enough to get a runtime CE).

[1] http://stackoverflow.com/questions/26390135/can-i-clamp-a-value-into-a-range-in-ada
[2] http://www.ada-auth.org/standards/12aarm/html/AA-13-1-1.html#p4.b