One possible problem is that we can end up with internal details like skolem constants leaking into the JSON representation. The core can probably be typed, but we don't have any documentation for what the types are, or how they correspond to the types the user wrote.

Thank you for looking at this and making the PR, but I would like to think about that problem first, which is why I put the issue under "Ideas".

Yeah, I thought so (i.e. WIP), I was just curious how a naive dump would look like. Feel free to close if you feel the PR is premature.

Thank you for the PR, but I think #3049 is more up to date at this point, so I'm going to close this. Apologies for letting this bitrot, especially since we might end up going a similar route.