> decide that the ID should be genericized so it can be anything
You say that, but you probably don't actually do it. If it truly could "be anything" then you would not be able to do anything to it. This is the nature of polymorphism.
So instead, your algorithm constrains the polymorphism based on what you need. If you make use of the properties {small, bit-shiftable, sized, bounded, copy-safe} then you must prove (exactly and only) that whatever the generic variable gets instantiated to satisfies {small, bit-shiftable, sized, bounded, copy-safe}.
Indeed, this is part of how such a system prevents bugs---it forces you to express exactly how much information about the types involved is needed. You can thus reflect better on the kinds of contracts/laws things must uphold and are prevented from accidentally making use of a property of your concrete type which you do not demarcate.
In a truly expressive language you might write
foo : forall id n .
(Bits id, Size id = n, n <= 1024)
=> id -> {Copy id} id
to indicate all of those properties needed (bounded being subsumed by constraining the size)
Today, you can get promises very similar to the above by using a language like Cryptol[0].
You say that, but you probably don't actually do it. If it truly could "be anything" then you would not be able to do anything to it. This is the nature of polymorphism.
So instead, your algorithm constrains the polymorphism based on what you need. If you make use of the properties {small, bit-shiftable, sized, bounded, copy-safe} then you must prove (exactly and only) that whatever the generic variable gets instantiated to satisfies {small, bit-shiftable, sized, bounded, copy-safe}.
Indeed, this is part of how such a system prevents bugs---it forces you to express exactly how much information about the types involved is needed. You can thus reflect better on the kinds of contracts/laws things must uphold and are prevented from accidentally making use of a property of your concrete type which you do not demarcate.
In a truly expressive language you might write
to indicate all of those properties needed (bounded being subsumed by constraining the size)Today, you can get promises very similar to the above by using a language like Cryptol[0].
[0] https://galois.com/project/cryptol/