Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda
Normally, Agda does an analysis to determine that your indexed type is equivalent to a parameterized type. Essentially, since A occurs in the result type, knowing that l : List A tells you what type A is 'stored' in the value l. The value is known, which means that tricks that involve embedding a universe into a small type within said universe to cause a paradox will not work.
However, the above reasoning basically presumes K for the universe. Really all we can say is that knowing the type List A lets us know that the stored type is equal to A, but without K, we don't know that there are no non-trivial equalities between types. I'm not sure if there is an example of how this extra degree of freedom would allow a paradox to be written, but even if no example is known, it is safer to require the larger size than to assume that the small size is consistent.