The rule preventing non-sendable params passed to an elevated-cap
constructor is there to prevent the possibility of the params becoming
entangled in the new object's fields. However, if the new object
has no fields, it is easily shown that there is no risk of such entanglement.
Hence, we can allow it.
When is it useful to have an iso object with no fields?
This pattern is used to create a non-replicable ticket,
such as the StdIn.Ticket used in the StdIn library.
The constructor for StdIn.Ticket takes the Env.Root.TicketIssuer'ref
as a parameter (which is not sendable), but as mentioned in this
ticket, it is safe to do so because it's not possible to become
entangled with it.
The rule preventing non-sendable params passed to an elevated-cap constructor is there to prevent the possibility of the params becoming entangled in the new object's fields. However, if the new object has no fields, it is easily shown that there is no risk of such entanglement. Hence, we can allow it.
When is it useful to have an
isoobject with no fields?This pattern is used to create a non-replicable ticket, such as the
StdIn.Ticketused in theStdInlibrary. The constructor forStdIn.Tickettakes theEnv.Root.TicketIssuer'refas a parameter (which is not sendable), but as mentioned in this ticket, it is safe to do so because it's not possible to become entangled with it.