Validity checking for sessions

[plaidfinch]

Consider the following:

type S = Send<bool, Recv<bool, Done>>;
let Chan<S, (), ()> = S::wrap((), ());

This code currently typechecks in Dialectic, even though the unit type () has no implementation of Transmit or Receive, making it such that enacting the session on this channel is impossible. It is only when we try to invoke the send or recv methods on the Chan that the error about Transmit or Receive would be thrown. Although in this case, it's clear that () is a silly channel type, we could imagine other scenarios with complex session types and/or channel backends with complex invariants about what can be sent (i.e. serialization constraints), which would make it non-trivial to tell at a glance whether a given session is possible to fulfill on a given backend.

Proposal:

pub trait ValidFor<Tx, Rx>: Session {}

We could then require this bound on Chan, so that all Chans are known to be statically valid for the whole session, and can't get stuck.

Issues/complications:

• The calling-convention polymorphism means there is more than one way to send a value, and it's not possible to know even from the combination of the backend and the session type which calling convention will be used. Only one of them might be valid, or multiple, or none. How can we handle this?
• We will need to correctly handle Split, where it must be disallowed to send/choose from the receive-only end, and recv/offer from the send-only end.
• Lack of constraint kinds means we can't prove that ValidFor<Tx, Rx> implies any particular other constraint. In particular, in contexts polymorphic over Tx and Rx, we'll have to always add ValidFor<Tx, Rx>... and then go on to list precisely the constraints that this entails on Tx and Rx, despite ValidFor implying them already.