!standard 4.5.2(28.1/4)                                    19-04-10  AI12-0328-1/02
!standard 4.5.2(4.1/4)
!class binding interpretation 19-04-10
!status work item 19-04-05
!status received 19-03-28
!priority Low
!difficulty Easy
!subject Meaning of limited type and record type in 4.5.2(28.1/4)
!summary

Membership test on a type with a limited partial view with a 
user-defined primitive "=" is illegal in the scope of the full type,
if the full type is nonlimited.

!question

RM 4.5.2(28-28.1/4) (A Dynamic Semantics rule) reads:

An individual membership test yields the result True if: 

* The membership_choice is a choice_simple_expression, and the 
  tested_simple_expression is equal to the value of the membership_choice. 
  If the tested type is a record type or a limited type, the test uses the 
  primitive equality for the type; otherwise, the test uses predefined 
  equality.

How does this work if the tested type is private? Does it depend on the
view of the type? (No.)

!wording

Modify RM 4.5.2(4.1/4):

  If a membership test includes one or more choice_simple_expressions
  and the tested type of the membership test is limited, then the tested
  type of the membership test shall have a visible primitive equality
  operator[.]{; if the tested type of the membership test is nonlimited
  with a limited partial view, the tested type shall be a record type or
  the limited partial view shall not have a visible primitive equality
  operator}.

    AARM Reason: We make the membership test on the full view of a type
    illegal if it would use a different equality operator than what
    would be used on its (limited) partial view.

!discussion

We want to be sure that you get the same result from a membership test applied
to the full view and the partial view, if both are legal. For the case of a 
limited partial view, the membership test is legal so long as there is a 
primitive equality operator. But if the full view is nonlimited, and not a 
record type, then the dynamic semantics say we use the predefined equality.
Making the dynamic semantics view dependent is frowned upon, especially for an
expression that could conceivably be used in a default expression, where the 
default expression in the body would see the full view, while the default 
expression in the spec would see the partial view.

For this special case, we make such a membership test illegal when the full 
view is in scope. The membership test can easily be replaced by a use of one 
or more equality tests, in which case the same (primitive) equality operator 
would be used independent of view, so there is an easy workaround in a case 
where the membership test is made illegal by this change.

!ASIS

No ASIS effect.

!ACATS test

ACATS tests C452004, C452005, and C452006 test various cases like these.

!appendix

From: Randy Brukardt
Sent: Thursday, march 28, 2019  10:32 PM

I'm spending a couple of days working on ACATS tests.

RM 4.5.2(28-28.1/4) (A Dynamic Semantics rule) reads:

An individual membership test yields the result True if: 

* The membership_choice is a choice_simple_expression, and the 
  tested_simple_expression is equal to the value of the membership_choice. 
  If the tested type is a record type or a limited type, the test uses the 
  primitive equality for the type; otherwise, the test uses predefined 
  equality.

AARM 3.1(7.d/3) says: "On the other hand, run-time rules can work either way, 
so "view of" should not be assumed in Dynamic Semantics rules." The above 
rule does not say "view of", so I presume that it ignores privacy.

This makes sense for records, as we want memberships to use the same "="
that is used for composition of equality. So in a case like:

   package P1 is
      type P is private;

      function "=" (Left, Right : P) return Boolean;

   private
      type P is record ...
   end P1;

We want the membership operation to use the primitive (user-defined) "=", not 
the predefined one. (The version of GNAT I have gets this wrong on the new 
ACATS test. Hope that's already been fixed.)

It's a bit weird that which equality is used for an array depends on whether 
the array type is limited, but of course there's no choice in the limited case 
(there's no predefined "=" to use), and the nonlimited case is consistent with 
composition and generic formal private types. And user-defined equality on 
array types isn't used that much.

Which brings us to my question. Consider (as in my new C452006 test):

   package P2 is
      type LP is private;

      function "=" (Left, Right : LP) return Boolean;

   private
      type LP is access ...
   end P2;

Here we have a type that is limited at the point of the membership, but the 
full view is nonlimited (and elementary).

The rule as written seems to imply that we ignore privacy and use the full 
view. In that case, the user-defined "=" is ignored by a membership operation, 
and the (hidden) predefined equality is used.

However, that is mighty strange; the programmer may have declared the type 
limited in the first place to ensure that the predefined equality wasn't used. 
They're not likely to be happy that it reappeared.

Note that there isn't any such existing case that's not pathological (unlike 
the array case): generic formal limited private types do not have "=", and 
there is no predefined equality for limited types, so there is no composition 
case to worry about. This sort of thing could happen only if a nested package 
declared a composite type with a component of the limited private type; in 
that case, the full view of the that type would have "="
and it would use the predefined "=" of the type -- but that "=" could only be 
used in the body of the (outer) package -- clients could never see it. (I 
consider this sort of case a pathology; Ada 83 should have banned it somehow 
rather than adopting a bunch of messy rules to make it work in an unexpected 
way, but of course it's way too late for that now.)

Also note that in the case where there is no visible "=", the membership is 
illegal. So we don't have to worry about *that* case.

I suspect that it would make more sense for the rule to be written in terms of 
whether the view of the type is visible. Of course, in that case, a membership 
in the body of P2 would act differently than the same membership elsewhere. 
Which I guess means we can't win. :-)

An alternative would be to write the rule in terms of immutably limited types 
to make it clearer that privacy is ignored. But in that case, we'd probably 
have to disallow writing a membership on a type whose full type is limited but 
not immutably limited. (Which would be incompatible.)

<Some time passes> I just read all of the discussion and minutes on the 
original AI, and didn't find anything about limited types other than Steve's 
"obvious" observation that we shouldn't be using "=" that doesn't exist or 
isn't visible (associated with adding the Legality Rule mentioned above).
Nothing about the Dynamic Semantics and views.

Thoughts on all of this?

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