Looks like a lot of people don't like to talk about the inconsistencies and unsound assumptions they snuck into their formal systems or wish to sneak in, including Agda. This rare exception says:

> The grammar of possible size expressions [...] is usually restricted to size variables and addition by constants, so that sizes are nicely inferrable and don’t require complex solvers. However, this does restrict the number of things we can express. This is why most sized type theories (and Agda) also has an infinite size ∞. Just as Nat [s] represents a natural no larger than s, Nat [∞] then represents any possible natural, also referred to as a full natural, in contrast to sized naturals.

> Notice that all sizes are strictly smaller than ∞, including itself. This is how both the size parameter and the size argument of succ are ∞; if not, this function wouldn’t be implementable. This poses a problem for Agda in particular, because we simultaneous expect < to be a well-behaved strict order, but ∞ clearly violates this expectation. These two simple facts yield an inconsistency, as described by this Agda issue.

> There are a few proposed solutions to this problem, most of them centered around removing the ∞ < ∞ property of the infinite size. [...] The key insight is that it’s not that an unsized natural inherently has no possible size to it, but rather that it has some unknown size. We can express this in the type theory using an existentially-quantified inductive type, ∃α. Nat [α].

> Existential Size Quantification is Still Insufficient. You can imagine extending this technique for circumventing the infinite size for more inductive types than just the naturals. However, it only works for simple inductive types; when we extend to general inductive types, where the recursive argument of constructors can be a function that returns the inductive, it starts to break down.

> We now essentially have a new constructor for sizes. [...] Given that we’ve been freely using fst and snd on existential size pairs, it seems that we should promote sizes to being proper terms. (Incidentally, in Agda they are.) Assuming we have some type Size, we can write down the typing rules for the introduction forms.

> Notice that we have an unbound universe level ℓ. This suggests that we need to pass ℓ as an argument to either lim itself or to Size. Since we’d like to treat sizes uniformly and be able to pass them around without worrying about the level, we’ll adopt the former solution. If we think of Size as an inductive type in Agda, this forces us to put it in Setω. This is a problem because inductive types contain a size as a parameter, meaning that they, too, all need to live in Setω.

> Take the naturals, for example: morally, they should be in Set, but [defining them in Agda using the above Sizes] would require data Nat (α : Size) : Setω where ... The problem would be solved if we could put Size in Set instead. In Agda, this requires Set to be impredicative, in a sense, which when combined with large elimination of types in Set in general would be inconsistent. It’s yet unclear to me whether only allowing Size to be in Set as a primitive formation rule would be consistent.

> Summary: Having a consistent, reasonable, and useable sized dependent type system is still an open problem.

Oh and I finally found the github issue on Agda: Equality is incompatible with sized types #2820. It was opened on 2017/10/27 and has lasted 3.5 years before it was finally 'resolved' on 2021/05/29 by simply blindly making it 'unsafe' (Sized types are no longer safe #5354). Clearly, almost nobody really cares about correctness of their formal systems. Very disappointing.

LOL. Everyone seems to be working blindly with impredicative stuff: Coq Issue #9458: Future of -impredicative-set, F* Issue #360: Paradoxes from impredicative polymorphism + excluded middle + large elimination, ...