Why am I allowed to rename subprogram subtypes?

I have been reading about Ada’s renaming declarations and started playing with what can and cannot be changed in a subprogram renaming declaration.

As it turns out, the formal parameter types and the return type can be narrowed to a subtype (here IntegerPositive).

with Ada.Text_IO;

procedure Renaming_Subprogram_Types is

   function Incr(Value : Integer; By : Integer := 1) return Integer is
   begin
      return Value + By;
   end Incr;

   function Pos_Incr(V : Integer; I : Positive := 2) return Positive
      renames Incr;

   Pos : constant Integer := Pos_Incr (-3);

begin

   -- Ada.Text_IO.Put_Line(Pos_Incr(-3, 0)'Image); -- Constraint_Error on `0`
   Ada.Text_IO.Put_Line(Pos'Image);

end Renaming_Subprogram_Types;

ARM 2022’s 8.5.4 Subprogram Renaming Declarations says:

Static Semantics
A renaming-as-declaration declares a new view of the renamed entity. The profile of this new view takes its subtypes, parameter modes, and calling convention from the original profile of the callable entity, while taking the formal parameter names and default_expressions from the profile given in the subprogram_renaming_declaration. The new view is a function or procedure, never an entry.

I assume I am dealing with renaming-as-declaration and not the other one.
Am I understanding this correctly that what’s happening is that I get something ARM calls a view and no subtypes are changed.
My function Pos_Incr could take two Integers and it still returns an Integer.
However, by changing the parameter subtype(s) I leave the compiler no option but to intervene when it sees an invocation that violates the renaming declaration.

Any help? Am I completely out of my depth?

Compiler: GNATMAKE 14.2.1 20250110 (Red Hat 14.2.1-7):
Command: gnatmake -gnat2022 -gnatwae renaming_subprogram_types.adb

You want to rename subprogram subtypes to preserve logical distinctions and avoid category errors like mixing units or using functions in unintended contexts. Renaming lets you constrain usage without redefining the logic of the subprogram itself.

The subtypes you specify in a subprogram renaming-as-declaration are only used to select which particular subprogram you are renaming, in case there is overloading. In particular, the constraints of the subtypes you specify in such a subprogram renaming are ignored, so it is best not to specify a subtype with a constraint of any sort, as that might be misleading.

Note that renaming-as-body requires subtypes to match exactly.

It looks like from their post though it is enforcing the subtypes of the renaming:

-- Ada.Text_IO.Put_Line(Pos_Incr(-3, 0)'Image); -- Constraint_Error on `0

So maybe a compiler bug there then?

Yes, this appears to be a GNAT bug. The Positive for the return subtype is being correctly ignored, but apparently the Positive for the second parameter is not being properly ignored. I was able to reproduce it on two different versions of GNAT.

Thanks everyone for your clarifications.

Indeed, @jere caught the gist of what I wanted to say but as I read that now I realise I didn’t make that clear.
I suppose spending a Sunday evening trying to come up with an explanation for why the compiler is acting against the reference and stress-testing this feature has impaired my clarity.

Should I report this to GNAT?

If you aren’t a direct Adacore customer, you’ll want to send the report here:

I would include the pertinent RM section discussed.

Side note, I don’t know if it falls into the “intended” reasons to allow it, but there isn’t normally a way to rename a type locally like you can packages and subprograms. The only thing you can do is a subtype of the original type, so if you use a local subtype to rename a type from another package you can still do your subprogram renaming using those local subtypes rather the orginal long type names:


-- Not actual ada since these are keywords, but just for example.
with Some.Package.Path.That.Is.Long;
package My_Package is
   subtype Some_Type is Some.Package.Path.That.Is.Long.Some_Type;
   procedure Do_Something(Value : Some_Type)
      renames Some.Package.Path.That.Is.Long.Do_Something;
end My_Package;