!standard 7.3(13)                                    21-11-16  AI22-0010-1/02
!class binding interpretation 21-11-11
!status work item 21-11-11
!status received 21-10-14
!priority Medium
!difficulty Easy
!qualifier Omission
!subject Predicates on private extensions
!summary

Predicates that apply to a private extension shall also apply to the full
view.

!question

A predicate might apply to a private extension because it applies to the 
ancestor subtype. But what happens if the full type is derived from a 
different subtype where there is no predicate? That sounds like trouble
as the predicate (of the partial view) would not be enforced on uses (since
it is the predicates of the full type that are checked). For example:

Consider:

   pragma Assertion_Policy (Check);

   type T1 is tagged record
      X, Y : Integer;
   end record;

   subtype S1 is T1 with Dynamic_Predicate => S1.X < S1.Y;

   Not_In_S1 : constant T1 := (1, 0);

   package Pkg is
      type T2 is new S1 with private;
      C : constant T2;
   private
      type T2 is new T1 with null record; -- (Now illegal.)

      C : constant T2 := (Not_In_S1 with null record); -- exception raised?
   end Pkg;

What is the intent here?

!recommendation

Disallow this case. The completion of a partial view should be required
to honor all of the "contracts" associated with the partial view.

With this change, the completion of type T2 in the example becomes illegal.

Note that similar problems can occur in cases involving interface type
progenitors.

!wording

Add after 7.3(13):

  All predicate specifications that apply to a private extension shall also
  apply to the full view.

  AARM Reason: The predicate specifications that are inherited by (formally,
  "apply to") a private extension have no effect on those that apply to the 
  full view. If we did not have the above rule, we could have types whose 
  partial view promises a predicate that is not actually enforced by the 
  full type. Note that this rule covers predicates that come from the 
  ancestor subtype or from any progenitor subtypes. (Predicates directly
  specified on the private extension always apply to the full type.)

!discussion

This is incompatible, but allowing such cases is worse. In the example above,
one would have a constant C2 which does not meet the predicate that applies
to the public view of type T2. That seems confusing to the user. This rule
is similar to the rules for discriminant constraints (7.3(13)) and interfaces
(7.3(7.3/2)) that apply to partial views.

---

Note that "applies" for a predicate specification is a Static Semantics term,
and thus is view-specific. Thus, a predicate specification that is given in
a private part does not apply to descendants of the partial view. Ergo, this
rule does not break privacy.

!ACATS test

An ACATS B-Test is needed to check this rule.

!appendix

From: Steve Baird
Sent: Thursday, October 14, 2021  1:21 PM [Privately]

We've got a rule in 7.3 that a partial tagged view of a type shall be a 
descendant of an interface type  if and only if the full type is a descendant
of the interface type.

That only talks about types, not subtypes.

Ada allows predicates to be specified for interface types.
That means that subtypes of a given interface type are not interchangeable.

So is the following example supposed to fail a predicate check at runtime when
the object X is declared?

  declare
     pragma Assertion_Policy (Check);

    package Pkg1 is
      type Ifc_Base is interface;
      function Pred (Arg : Ifc_Base) return Boolean is abstract;
      subtype Ifc is Ifc_Base with
           Dynamic_Predicate => Pred (Ifc_Base'Class (Ifc));
    end Pkg1;

    package Pkg2 is
      type T is new Pkg1.Ifc with private;
      -- partial view references Ifc
    private
      -- full view references Ifc_Base
      type T is new Pkg1.Ifc_Base with record
         Flag : Boolean := False;
      end record;
      overriding function Pred (Arg : T) return Boolean is (Arg.Flag);
    end Pkg2;

    X : Pkg2.T;

  begin ... end;

I think it comes down to a question of whether Pkg1.Ifc is a progenitor
subtype of Pkg2.T for purposes of dynamic semantics.

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

From: Randy Brukardt
Sent: Thursday, October 14, 2021  8:49 PM [Privately]

Dunno.
 
What happens in case when the ancestor (sub)type is different? Forgetting 
interfaces for a moment. (That would seem to have similar issues, with 
constraints as well.) 7.3.1(8) also only talks about types.
 
I suppose it would be hard/impossible to have the ancestor *more* constrained 
than the full type - generally, predicates come along in descendants.
 
Maybe you could play a game sort of like yours here?
 
declare 
     pragma Assertion_Policy (Check);


    package Pkg1 is
      type Root is tagged null record;
      function Pred (Arg : Root) return Boolean is (True);
      subtype Pred_OK is Root with
           Dynamic_Predicate => Pred (Root'Class (Ifc));
   end Pkg1;

   package Pkg2 is
      type T is new Pkg1.Pred_OK with private; 
      -- partial view references Pred_OK
   private
      -- full view references Root
      type T is new Pkg1.Root with record
         Flag : Boolean := False;
      end record;
      overriding function Pred (Arg : T) return Boolean is (Arg.Flag);
   end Pkg2;

   X : Pkg2.T;

  begin ... end;
 
This is your example, but with no interfaces in sight. 7.3(8) is satisfied 
because only types are discussed in that rule, and Pred_OK and Root are the
same type.
 
I think you could do something similar with discriminant constraints, but 
perhaps there is some rule elsewhere preventing that? I couldn't find it.
(That is, constrain the ancestor of the partial view, don't constrain the 
full view.) If there is, that is evidence that we need a similar rule for 
predicates.
 
I agree that something is wrong here, although if it is a real problem is 
unclear. Generally, dynamic semantics (like predicate checks) ignore privacy,
so the subtype on the partial view is irrelevant and only the full view is 
relevant. But that *is* confusing, and I'd guess that we'd want to ban 
something like these two examples where the partial subtype is more 
constrained than the full subtype.
 
****************************************************************

From: Steve Baird
Sent: Friday, October 15, 2021  11:54 AM [Privately]

I agree, this is a more general problem. I also agree with the general idea
that we want to require (at compile time) that a full view satisfies any 
promises that are implicit in the declaration of the partial view. So the 
solution to this problem is probably going to involve some new legality rules.
Like you, I do not want to silently ignore any such mismatch (e.g., by having
the dynamic semantics ignore the partial view).

That being said, I don't think there are any problems in this area with
discriminant constraints.

We've got this rule:
   If the ancestor subtype of a private extension has constrained 
   discriminants, then the parent subtype of the full view shall impose 
   a statically matching constraint on those discriminants.

I think that covers the case you were wondering about (i.e. "constrain the 
ancestor of the partial view, don't constrain the full view"). We just need
a similar rule for predicates, although I think we only want to require 
compatibility (as opposed to matching). Isn't it ok if the full view is
subject to some predicate that the partial view is not subject to?

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

From: Steve Baird
Sent: Friday, October 15, 2021  1:32 PM [Privately]

In the rules for static compatibility of two subtypes, we have this wording:
    all predicate specifications that apply to S2 apply also to S1, or


So how about adding the rule
    All predicate specifications that apply to the ancestor subtype of a 
    partial extension shall also apply to the parent subtype of the full view.
?

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

From: Steve Baird
Sent: Friday, October 15, 2021  1:35 PM [Privately]

I meant to also say something about where this new rule might be added.
I was thinking about adding it immediately after the existing rule
about statically matching discriminant constraints.

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

From: Steve Baird
Sent: Friday, October 15, 2021  6:58 PM [Privately]

> So how about adding the rule
>    All predicate specifications that apply to the ancestor subtype of a 
>    partial extension shall also apply to the parent subtype of the full
>    view.
> ?

In addition to saying "partial" when I meant "private", there is another 
problem: we need to worry about more than just the ancestor subtypes because
a private extension can have interface progenitors and they can have
predicates.

So something like
     type T2 is new T1 and Ifc_Subtype_With_Predicate with private;
  private
     type T2 is new T1 and Ifc_Basetype_Without_Predicate;

would not be addressed by the wording I proposed.

So perhaps make it even simpler:

     All predicate specifications that apply to a private extension shall also
     apply to the full view.

Does that work?

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

From: Randy Brukardt
Sent: Friday, October 15, 2021  7:37 PM [Privately]

I never got around to answering this earlier. I suppose this works:
 
  All predicate specifications that apply to a private extension shall also
  apply to the full view. 

But it seems a bit handwavey to me. The way it is written, it seems to be 
talking about predicates that apply directly to the private extension. OTOH,
perhaps we want that??
 
    type T2 is new T1 with private
       with Dynamic_Predicate => Foo(T2);
 
    type T2 is new T1 with null record; -- No predicate!
 
This has the same problem as the other cases: predicates of ancestors are 
evaluated, but there is nothing about those of partial views. So the 
predicate on the partial view would be ignored.
 
OT3H, we might just want to ban a predicate on a partial view, since it can 
never "apply" to the full view (even if the "same" predicate is given, it 
would be different, we're not trying to define matching for these guys). But
maybe that's overkill.
 
Looking at the definition of apply in 3.2.4, this is actually exactly the 
right rule, but I think we need an AARM note (or even user note) to make it
clear what this means for parents/progenitors. And the AI needs to mention
that if you want a predicate on a partial view, you need to give it on an 
ancestor. For instance, 
 
if you really wanted the above, you would need to write something like:
 
    subtype T1_w_Pred is T1 with Dynamic_Predicate => Foo(T1_w_Pred);
 
    type T2 is new T1_w_Pred with private;
 
    type T2 is new T1_w_Pred with null record;
 
Are you writing an AI for this (now that we know the format will be
unchanged)??

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

From: Steve Baird
Sent: Friday, October 15, 2021  8:39 PM [Privately]

I believe this is not a problem:

 >  type T2 is new T1 with private
 >      with Dynamic_Predicate => Foo(T2);
  > private
  >   type T2 is new T1 with null record; -- No predicate!

by 13.1.1(27):
    All other aspect_specifications are associated with the entity, and apply 
    to all views of the entity, unless otherwise specified in this document.

===

The notion of a predicate applying to a subtype is a well-defined technical term.
Without that, I might agree that the wording I suggested sounds hand-wavey;
but because it is a technical term, I think the meaning is clear.

We could have an AARM note emphasizing that this rule applies to "inherited"
(yes, I'm misusing that term here) predicates.

----

I'm certainly willing to take a stab at an AI. It seems like there are a 
couple of other post-Ada2022 issues that we've discussed that need AIs, but
I don't remember them off the top of my head.

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