Max_Size aspect RFC

Summary

The idea is to be able to annotate a tagged type declaration with a Max_Size aspect like so:

type Foo is tagged abstract null record 
with Max_Size => 16; --  I imagine the size would be in bytes

Then, any time a descendent would be declared, the compiler would verify that it satisfies the size constraints

type Bar is new Foo with record
   S : String (1 .. 128);
end record; --  ERROR: Record doesn't fit in 16 bytes

The usefulness of this is that the classwide type for Foo would be of a definite and known size, which would allow the users to use classwide instances as definite sized objects:

Inst : Foo'Class;
type Foo_Array is array (Positive range <>) of Foo'Class;

NOTE: Manually computing the size is tedious, so the idea would be to leverage the "final" feature explained here https://hackmd.io/6Au5wQ5HQ0G10wGGVii_nw to allow people that are OK with making the type final to let the compiler auto-compute the size.

type Foo is final tagged abstract null record
with Max_Size => Auto;
--  This type can only be derived inside the package it has been declared in.

type Bar is new Foo with record
    A, B : Integer;
end record;

type Baz is new Foo with record
    S : String (1 .. 128)
end record;

-- Size of Foo'Class automatically infered to be Max (Bar'Size, Baz'Size, ...)

Motivation

• Being able to use classwide types where definite types are required in Ada, which in turns allows to either use tagged types where they couldn't be used before, or remove a lot of dynamic allocations if tagged types were used already.

• The above will make tagged types much more usable in embedded contexts where dynamic allocation is prohibited, or discouraged.

Reference level explanation

A new aspect, Max_Size is added.

Syntax

No custom syntax

Static legality rules

• Max_Size can be specified only on tagged type definitions. Any use on other entities will raise an error.
• Max_Size can only be specified on the rootmost type of a tagged type hierarchy (excluding interfaces).
• Given a tagged type A which has a Max_Size aspect, the classwide type A'Class is a definite constrained type, as well as any classwide type for any of the types derived from A.
• When defining a type that is derived directly or indirectly from A, its computed size will be matched against the max-size. If it is bigger than the max size, an error will be raised.

Operational semantics

Objects with a max_size are stored by value in a memory zone that is the size of Max_Size.