I've been reading and understand the design choices behind Agda not having a cumulative universe hierarchy by default. However, while tinkering with the language, I've noticed that, at least for Agda 2.6.3,
--cumulativity as a pragma is marked as incompatible with the
This didn't sound unreasonable, but I've not found any reference in either the documentation or any other question as to why this is the case.
I know that this pragma is quite new (from version 2.6.1, if I'm not mistaken), and it would be reasonable to me that this is due to it still being considered experimental; but it would also seem plausible to me that something in the type system of the language made this feature, (although less radical than stuff like
--type-in-type), intrinsically unsafe.
I would like to know which one of these two options (or maybe a secret third one!) is behind the decision, in a way to know if it would be expected for this feature to be "safely" available at some point in the future of the development of the language.