⁴  This is also desirable from the viewpoint of consistency of the underlying type theory: we want types (here protocols) themselves guarantee basic safety properties.