Types inductifs paramétrés dans Agda

Question

Je lis juste Types dépendants au travail. Dans l'introduction de types paramétrisés, l'auteur mentionne que dans cette déclaration

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

le type de List est Set → Set et cela A devient un argument implicite pour les deux constructeurs, c'est-à-dire.

[]   : {A : Set} → List A
_::_ : {A : Set} → A → List A → List A

Eh bien, j'ai essayé de le réécrire un peu différemment

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

Ce qui ne fonctionne malheureusement pas (j'essaie d'apprendre Agda pendant environ deux jours, mais d'après ce que j'ai rassemblé, c'est parce que les constructeurs sont paramétrisés Set₀ et donc List A doit être dans Set₁).

En effet, les éléments suivants sont acceptés

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

Cependant, je ne suis plus en mesure d'utiliser {A : Set} → ... → List (List A) (ce qui est parfaitement compréhensible).

Donc ma question: quelle est la différence réelle entre List (A : Set) : Set et List : Set → Set?

Merci pour votre temps!