AI22-0010-1
!standard 7.3(13) 22-01-14 AI22-0010-1/04
!class binding interpretation 21-11-11
!status Amendment 1-2022 22-01-14
!status WG9 Approved 22-10-18
!status ARG Approved 12-0-0 21-11-18
!status work item 21-11-11
!status received 21-10-14
!submitter Stephen Baird
!priority Medium
!difficulty Easy
!qualifier Error
!subject Predicates on private extensions
Predicates that apply to a private extension shall also apply to the full view.
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?
The completion of a partial view should be required to honor all of the "contracts" associated with the partial view. Therefore, we need some sort of matching requirement that the full type has all of the predicates that apply to 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.
Add after 7.3(13):
Each predicate specification that applies to some ancestor of a private extension shall also apply to some ancestor of 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.)
This is incompatible, but allowing such cases is worse. In the example above, if this was legal, one would have a constant C 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.
@dinsa
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.
@dinst
Each predicate specification that applies to some ancestor of a private
extension shall also apply to some ancestor of the full view.
An ACATS B-Test is needed to check this rule.
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.
****************************************************************
From: Steve Baird
Sent: Tuesday, November 16, 2021 5:36 PM [Privately]
Another point crossed my mind about the proposed new rule:
All predicate specifications that apply to a private extension shall also
apply to the full view.
Is it clear how this rule interacts with privacy?
Consider the following example:
procedure Foo is
package Pkg1 is
type T1 is tagged record
Int : Integer;
end record;
subtype S1 is T1 with
Dynamic_Predicate => S1.Int /= 0;
end Pkg1;
package Pkg2 is
type T2 is new Pkg1.T1 with private;
private
type T2 is new Pkg1.S1 with null record;
end Pkg2;
package Pkg3 is
type T3 is new Pkg1.S1 with private;
private
type T3 is new Pkg2.T2 with null record;
end Pkg3;
begin
null;
end Foo;
The one-and-only Dynamic_Predicate aspect specification in this example
certainly applies to the partial view of Pkg3.T3, a private extension.
So this AI adds a requirement that it must also apply to the full view.
Is that requirement met?
That depends on whether we peek into the private part of Pkg2 when
we are checking the legality of the full view of Pkg3.T3.
So do we ignore privacy here? One would hope not.
I think we'd all agree that we want this example to be illegal.
What do you think?
****************************************************************
From: Randy Brukardt
Sent: Tuesday, November 16, 2021 10:34 PM [Privately]
...
> That depends on whether we peek into the private part of Pkg2 when
> we are checking the legality of the full view of Pkg3.T3.
And that depends on whether "apply" is really statically or dynamically
defined. Since it is statically defined in 3.2.4, views do matter. And
since views matter, the predicate does not apply to the full T3, since
it is not visible.
OTOH, the predicates checked do not depend on visibility, since there is an
explicit rule checking the predicates of the parent/progenitors. So:
package Pkg4 is
type T4 is new Pkg2.T2 with private;
private
type T4 is new Pkg2.T2 with null record;
V : T4 := 0; -- Still raises Assertion_Error here.
end Pkg3;
The predicate does NOT apply to type T4 (since it is not visible to it), but
the check is still made when the predicates of T2 are checked (first).
...
> What do you think?
No problem here, "apply" is a static semantics term, and that is always
view-specific. The predicate does not apply to Pkg2.T2 outside of Pkg2.
I would have said the public subtype Pkg2.T2 does not have a predicate
applying to it, while the private subtype Pkg2.T2 does. I know you guys
hate that description, but it is what happens here, regardless of how you
describe it.
The predicates checked explicitly include checking the predicates of parents,
etc., so the predicate gets checked anyway when hidden (dynamic rules don't
care about views).
****************************************************************
From: Randy Brukardt
Sent: Wednesday, November 17, 2021 12:38 AM
I've reposted AI22-0010-1. None of the real meat has changed (including the
actual RM wording), but Tucker suggested rewriting the question and the
recommendation to make the problem and the solution clearer, and I removed
some of the discussion that was more confusing than helpful. I also added a
couple of sentences clarifying why the proposed rule will not violate
privacy. Hopefully this version will be more understandable than the original
version. As always, sorry for any inconvenience.
****************************************************************