Coq provides payload to our layer via two different mechanisms:
feedback messages
error exceptions
In both cases, the payload is the same, and it comes via different ways due to historical reasons. We abstract the payload as to better handle the common paths.