Specifications can be terser through more type trickery

[OlivierNicole]

As I was writing an STM specification for Dynarrays, I was a bit frustrated to have to add a catch-all assert false at the end of postcond. So I went into an over-engineering rabbit hole and found that it can be avoided by making the cmd type of specifications a GADT, which allows to specify the result type for commands. The typechecker is then able to deduce the result type when pattern matching on commands.

As an example, I have rewritten src/atomic/stm_tests.ml to match the new Spec signature.

This has a number of benefits and some drawbacks.

Benefits

• When writing the run function, results no longer need to be wrappend into the Res constructor. However, it is still necessary to also return an instance of 'a ty_show; I have not found a simpler way to make the results printable.
• When writing the postcond function, it is no longer necessary to match on patterns like Res ((Result (Int, Exn), _), v) for the typechecker to deduce the right type for v: the command name suffices. It is also no longer necessary to add a catch-all _ -> assert false at the end.
• Functions like run are safer because the result type is checked.

Drawbacks

Defining a GADT in the specification adds its own boilerplate: most functions now need explicit type annotations with universal quantifiers; the user must also define an existential type packed_cmd and wrap the command generators in it. Such STM tests are harder to write when one is not familiar with qcheck-stm.

And of course, another big drawback is that it changes the signature of STM specifications.

For these reasons, I open this PR as a draft, mostly to share the idea.