Re: Ada2012 Invariants and obaque types

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

Martin Dowie wrote on comp.lang.ada:
> A fairly common Ada idiom is to define the full view of a private type
> using an incomplete declaration. Thus leaving the actual
> implementation to the package spec. Trying this out with the public
> view defined with an invariant lead to a compiler error - is this:
>
> a) expected?
> b) an unexpected consequence? or
> c) a compiler bug?
>
> Example:
> package P1 is
>    type T1 is tagged private
>       with Invariant => Is_Valid (T1);
>    function Create               return T1;
>    function Is_Valid (This : T1) return Boolean;
> private
>    type Imp;
>    type T1 is
>       record
>          I : Imp;
>       end record;
> end P1;
>
> gnatmake -ws -c -u -PH:\Ada\test_invariants\test_invariants.gpr p1.ads
> gcc -c -g -g -gnatE -gnatVn -gnato -fstack-check -gnat12 -gnatf -I- -
> gnatA H:\Ada\test_invariants\src\p1.ads
> p1.ads:11:04: type "Imp" is frozen at line 3 before its full
> declaration
> p1.ads:13:09: full declaration of private type "T1" defined at line 3
> must be a tagged type
> p1.ads:15:14: invalid use of type before its full declaration
> gnatmake: "H:\Ada\test_invariants\src\p1.ads" compilation error
>
> [2011-06-21 09:46:55] process exited with status 4 (elapsed time:
> 00.26s)

This looks like a consequence of 13.14(8.2/1): "If an expression is
implicitly converted to a type or subtype T, then at the place where
the expression causes freezing, T is frozen." (where in this case the
expression is T1, which stands for the current instance of the type,
and the type T is also T1).

This subclause however seems to contradict 13.14(7.2/3): "At the
freezing point of the entity associated with an aspect_specification,
any expressions or names within the aspect_specification cause
freezing."; this subclause would defer the freezing point of T1 until
the end of the enclosing package spec or the declaration of a constant
of the type, whichever comes first (as is normal for tagged types).

Another possible interpretation is that Is_Valid must be called as
part of the elaboration of type T1, in which case the
aspect_specification is a function call, which freezes the types of
its parameters (per 13.14(10.1/3)).  But I doubt this is true.

So, this looks like an area of the language definition that needs
clarifying (but then again, freezing rules have always been difficult
to understand). The behavior of the compiler definitely looks
undesirable to me.  So I vote for b) an unexpected (and undesirable)
consequence (of existing rules).

--
Ludovic Brenta.