Private (or "abstract") types should not be allowed to be marshalled

[ejgallego]

Quite a few types in the codebase are declared "private", however it turns out that this doesn't reflect usage as the abstraction is later broken, usually by using Marshall.

This inconsistency puts a huge barrier to developers willing to experiment with alternative serialization formats, and makes impossible to properly ask many basic questions about the system without indeed, having to mess with core APIs.

[ejgallego]

cc: ocaml/ocaml#5797 ocaml/ocaml#6338

[Alizter]

@ejgallego What should be done to resolve this?

[ejgallego]

@ejgallego What should be done to resolve this?

That requires developer discussion; usually you would expect types that can be saved to disk to implement a Serializable.S interface that Coq would provide, but there are non-trivial issues to overcome. Maybe we could introduce a Marshall.S interface?

I dunno, there are many use cases here, including differential computation.