Unified Errors, a non-proliferation treaty, and extensible types