Certain types are not even intended for the executable code,
and we only need witnesses to ensure logical consistency.
In other words, even if we can only build a ghost witness,
we are still happy.

Thanks to Martin Clochard for this observation. Also, I relieve
him of any responsibility for the current syntax of the witnesses,
apart from the "by" keyword :)