!standard 12.5.1(7)                                       20-01-10  AI12-0351-1/01
!standard 12.5.1(8)
!class binding interpretation 20-01-10
!status work item 20-01-10
!status received 19-11-23
!priority Low
!difficulty Easy
!qualifier Error
!subject Matching for actuals for formal derived types
!summary


!question

In 12.5.1, actual type matching for formal derived types that do not have
discriminants include a number of bullets which attempt to ensure that any 
value of the actual subtype can be successfully converted to the ancestor 
subtype.

One of the rules is:

   - If the ancestor subtype is constrained, the actual subtype
     shall be constrained, and shall be statically compatible
     with the ancestor;

This prevents something like:

     generic
        type T is new Natural;
     package G1 is
     end G1;

    package I1 is new G1 (Integer); -- Illegal.


Static compability includes constraints, null exclusions, and predicates.
So, the check 

    subtype Nonzero_Integer is Integer
      with Static_Predicate => Nonzero_Integer /= 0;

    generic
       type T is new Nonzero_Integer;
    package G2 is
    end G2;

    package I2 is new G2 (Integer); -- Illegal.

However, one can have a null exclusion or predicate on an unconstrained type.
The above rule doesn't cover such cases. This is easy to see for a floating 
point type:

    subtype Nonzero_Float is Float
       with Static_Predicate => Nonzero_Float /= 0.0;

    generic
       type T is new Nonzero_Float;
    package G3 is
    end G3;

    package I3 is new G3 (Float); -- OK? (No.)

Should this be fixed? (Yes.)

!recommendation

(See Summary.)

!wording

Modify 12.5.1(7):

For a generic formal derived type with no discriminant_part{, the actual subtype
shall be statically compatible with the ancestor subtype. Furthermore}: 

Modify 12.5.1(8):

If the ancestor subtype is constrained, the actual subtype shall be 
constrained[, and shall be statically compatible with the ancestor]; 

!discussion

Static compatibility allows "null constraints", which despite their name have
nothing to do with null exclusions. Rather this is a name for the constraints
of an unconstrained type. Beyond the "nothing is something" factor, this means
that static compatibility can be applied to any type. Therefore, it is OK to
apply it to all of the bullets in this set of rules.

It might seem that such a change would be incompatible, but we have not been
able to identify any incompatibilities due to applying static compatibility
to formal derived type matching of unconstrained types.

Note that the original bullets are mutually exclusive, so we preserve that
property by putting the static compatibility requirement into the lead-in 
text.

!ASIS

No ASIS effect.

!ACATS test

An ACATS B-Test should check cases involving predicates like the ones in the
question. It also should try null exclusions on otherwise unconstrained access 
types.

!appendix

From: Steve Baird
Sent: Saturday, November 23, 2019  1:22 PM

In RM 12.5.1, the rules for formal derived types include
    For a generic formal derived type with no discriminant_part:
       - If the ancestor subtype is constrained, the actual subtype
         shall be constrained, and shall be statically compatible
         with the ancestor;

Roughly speaking, the design goal here is to ensure that any value of the 
actual subtype can be successfully converted to the ancestor subtype.

To illustrate:

     generic
        type T is new Natural;
     package G is
     end G;

     type New_Positive is new Positive;
     type New_Integer is new Integer;
     package Ok is new G (New_Positive); -- legal
     package Not_Ok is new G (New_Integer); -- illegal

The wording of this rule makes sense if all we are thinking about is 
constraints, but static compatibility also includes rules about predicates 
and null exclusions. We want not just the constraints but also the predicates 
and null exclusions of the ancestor subtype to be part of the contract that 
the actual parameter must satisfy.

Recall that Standard.Integer is a constrained subtype (3.5.4) and 
Standard.Float is not (3.5.7).

This all means that the following instance is illegal (which is what we want, 
as per the aforementioned design goal)

    subtype Nonzero_Integer is Integer
      with Static_Predicate => Nonzero_Integer /= 0;

    generic
       type D1 is new Nonzero_Integer;
    package G1 is
    end G1;

    package I1 is new G1 (Integer);

but, unfortunately, the following very similar instance is legal (despite the 
fact that it violates that design principle):

    subtype Nonzero_Float is Float
      with Static_Predicate => Nonzero_Float /= 0.0;

    generic
       type D2 is new Nonzero_Float;
    package G2 is
    end G2;

    package I2 is new G2 (Float);

IMO, the clause above
       - If the ancestor subtype is constrained, the actual subtype
         shall be constrained, and shall be statically compatible
         with the ancestor;
should be split into two clauses
       - If the ancestor subtype is constrained, the actual subtype
         shall be constrained;
       - the ancestor subtype shall be statically compatible
         with the ancestor subtype;

so that the static compatibility requirement applies even if the ancestor 
subtype is unconstrained. This change would also address similar problems 
involving null exclusions.

Opinions?

****************************************************************

From: Tucker Taft
Sent: Sunday, November 24, 2019  9:37 AM

...
> should be split into two clauses
>      - If the ancestor subtype is constrained, the actual subtype
>        shall be constrained;
>      - the ancestor subtype shall be statically compatible
>        with the ancestor subtype;

I'll bet you meant something closer to:

  - the actual subtype shall be statically compatible with the ancestor 
    subtype.

> so that the static compatibility requirement applies even if the 
> ancestor subtype is unconstrained. This change would also address 
> similar problems involving null exclusions.

In any case, I agree this is an appropriate direction.

****************************************************************

From: Randy Brukardt
Sent: Sunday, November 24, 2019  6:24 PM

> I'll bet you meant something closer to:
> 
>   - the actual subtype shall be statically compatible with the 
> ancestor subtype.

Yeah, comparing the ancestor to itself seems uninteresting. ;-)
 
> > so that the static compatibility requirement applies even if the 
> > ancestor subtype is unconstrained. This change would also address 
> > similar problems involving null exclusions.
> 
> In any case, I agree this is an appropriate direction.

I was concerned that such a check would either be undefined or prevent some 
expected cases (such as a constrained actual subtype for an unconstrained 
record type with discriminants). I haven't been able to construct a problem 
so far. The key is that an unconstrained type is defined to have a "null 
constraint", so we can talk about the constraint of a unconstrained type 
without falling into a black hole. This terminology is confusing these days 
(it sounds like it has something to do with null exclusions), and it is 
annoying in that it defines nothing (no constraint) to be something (a null 
constraint). Still, it seems to work logically (at least if you can get over 
the "nothing is something" factor).

As such, one can talk about comparing the constraint of an unconstrained type,
which is an important part of the definition of static compatibility.

I guess in the end I don't care enough if there is any incompatibility to 
worry about this further. (If the rule was "no actual subtype matches an 
untagged formal derived type", we wouldn't lose much useful capability, or 
one that is used much in practice. As such, this is a corner case of a corner 
case, hard to imagine it matters to anyone either way.)

****************************************************************

From: Steve Baird
Sent: Monday, November 25, 2019  9:55 AM

> I'll bet you meant something closer to:
> 
>    - the actual subtype shall be statically compatible with the ancestor 
>      subtype.

Good point.

****************************************************************