Nel Gadt di AGDA, è "parametrizzato" e "indicizzato" diverso?

Question

So che hanno la differenza di scoping:

data a (n : Set) : Set where
    introA : a n

data b : Set -> Set where
    introB : {n : Set} -> b n

Quello è non di cosa mi prendo cura. Sono diversi semanticamente?