Re: Brain bug or GNAT bug?

[Ludovic Brenta <ludovic@ludovic-brenta.org>]

(see below) writes:
> Ludovic Brenta writes:
>> Per ARM 3.7(15), the types of DT1.the_size and DT2.the_size must be
>> statically compatible.  In other words, you must guarantee at compile
>> time that "the_size" is in the range of type "modular".  Because
>> modular's range is not known at compile time but bounded's is, no such
>> guarantee exists.
>> 
>> If you remove the "range" constraint on subtype "bounded", then the
>> range for "bounded" and the range of "modular" are known at compile
>> time to be identical, so all is well.
>
> But if the declaration of bounded compiles,
> the range of bounded must be a subset of the range of modular,

The compiler doesn't know that, so inserts run-time checks as aptly
illustrated by Jeffrey Carter.

> so DT2.the_size must be in the range of modular.
> The rule at ARM 3.7(15) seems overly restrictive.

The rule implies there must be no run-time checks.  I don't think this
is overly restrictive, since this is exactly what you want as you
explained below.

>> What are ou trying to achieve?
>
> Implement DT2 as a derivation of DT1 with guaranteed bounds on its
> size (in the actual s/w, the bounds are also generic parameters, and
> DT1 is actually declared in a distinct, with-ed package).

Consider that it must be possible to convert explicitly between
related types, i.e. from DT1 to DT2 and back.  What happens if you
want to convert from a DT1 object with unknown bounds to a DT2 with
"guaranteed" but different bounds?  Remember that generic formal
objects are never considered static inside the generic, even if the
actuals for some instantiations happen to be static.

> At the moment bounds checking for DT2 has to be done by a runtime
> check on use of DT2 objects.

Yes, but even with your solution, this is still a run-time check, and
that's illegal for a discriminant used to constrain a parent type.

> I can't help feeling the type system should be able to catch a
> misuse, at the point of declaration of a DT2 object, but there does
> not seem any way to do that, thanks to ARM 3.7(15).

So long as the bounds of DT1 are unknown at compile time, there will
be a run-time check somewhere.  You can make that implicit or
explicit.

I think a possible solution is to not declare DT2 as derived from DT1.
Make the two types independent, and write a conversion function that
takes into account the possible difference in bounds.  For example, it
would convert a DT1 object with unknown bounds into one *or more* DT2
objects with guaranteed bounds.  Actually, make that *zero* or more
DT2 objects.

-- 
Ludovic Brenta.