[pyjarrett]

> However, existing programming languages have little or no subtyping

Every "type" you use in Ada is actually a subtype.

In Ada, "A subtype of a given type is a combination of the type, a constraint on values of the type, and certain attributes specific to the subtype".

You don't ever refer to actual types in Ada, since creating a type with "type" actually creates an anonymous type and the name refers to the first subtype.[1]

    type Token_Kind is (
       Identifier,
       String_Literal,
       --  many more ...
    
       -- These are character symbols and will be part of Token_Character_Symbol.
       Ampersand,
       --  ...
       Vertical_Bar,
    );
    
    --  A subtype with a compile-time checked predicate.
    subtype Subprogram_Kind is Token_Kind
    with Static_Predicate => Subprogram_Kind in RW_Function | RW_Procedure;
    
    subtype Token_Character_Symbol is Token_Kind range Ampersand .. Vertical_Bar;

> If you have a pointer with more permissions, it should still be usable in a place that only requires a pointer with fewer permissions

This is exactly how "accessibility" of access types works in Ada[2]. If you have a pointer ("access type") to something on the heap, you can use it wherever an anonymous access type can be used. You can also create subtypes of access types which have the constraint of a "null exclusion".

[1]: https://ada-lang.io/docs/arm/AA-3/AA-3.2#p1_3.2.1

[2]: https://ada-lang.io/docs/arm/AA-3/AA-3.10