Why does universe level restriction behave differently between inductive family and parameterized inductive type without axiom K in agda

Question

An observation when defining List in agda with --without-K enabled:

The following parameterized inductive definition is accepted:

data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

but not the equivalent inductive family definition:

data List' : Set → Set where 
    []'  : {A : Set} → List' A
    _::'_ : {A : Set} → A → List' A → List' A

The error message is Set₁ is not less or equal than Set, so I have to change the type from List' : Set → Set to List' : Set → Set₁ in order for it to type-check. If I disable --without-K, then agda also correctly type-checks.

I tried to look up why this is the case, e.g., on the page https://agda.readthedocs.io/en/latest/language/without-k.html it says "When --without-K is enabled, some indexed datatypes must be defined in a higher universe level. In particular, the types of all indices should fit in the sort of the datatype." But it doesn't say the reason for such difference between inductive family (indexed datatypes) definition and the parameterized inductive definition. I guess it has something to do with the homotopy model interpretation of the underlying type theory. However I want to know what sort of "bad" thing will happen if the inductive family lives in a smaller universe (syntax and semantics). And how would parameterized inductive definition avoids such issue?

Answer 1

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.