Coherence constraints for Choose

[ebfull]

None of these have safety implications, but there are a number of coherence constraints ideal for Choose:

• We don't want types like Choose<A, Choose<B, Finally<A>>> to be expressible. That is, there exists no Chooser<A, B> such that Chooser<A, B>: Chooser<S> and B: Chooser<S>.
• We should ensure that Choose<P, Q> only allows Choose and Finally to exist as Q.
• Finally should not exist outside of Choose, if possible.

As a bonus, it may not be necessary to use Finally at all, but I am doubtful.