title: List Set should be a sort, but it isn't
body: <p>I just start using Agda to work on some proof of concept.</p>
  <p>In this case, I want a data type with similar structure as <code>Relation</code> defined below.</p>
  <p>(for simplicity, the element of data type <code>A</code> and definition of function <code>relation-1</code> are omitted).</p>
  <p>When <code>Relation</code> is defined like this:</p>
  <pre><code>open import Data.Product using (_×_)
  open import Data.List using (List; _∷_; [])
  open import Data.Unit using (⊤)
  
  data A : Set where
  
  relation-1 : A → List A
  relation-1 = {!!} 
  
  map-1 : ∀{A : Set} → (A → Set) → List A → List Set
  map-1 _ [] = []
  map-1 p (a ∷ as) = p a ∷ (map-1 p as) 
  
  map-2 : ∀{A : Set} → (A → Set) → List A → Set
  map-2 p [] = ⊤
  map-2 p (a ∷ as) = p a × (map-2 p as)
  
  data Relation : A → Set where 
    refl : (a : A) → Relation a
    expand : (a : A) → map-1 Relation (relation-1 a) → Relation a 
  </code></pre>
  <p>The error message is :</p>
  <pre><code>List Set should be a sort, but it isn't
  when checking that the inferred type of an application
    List Set
  matches the expected type
    _43
  </code></pre>
  <p>However, after replacing map-1 with map-2</p>
  <pre><code>data Relation : A → Set where 
    refl : (a : A) → Relation a
    expand : (a : A) → map-2 Relation (relation-1 a) → Relation a 
  </code></pre>
  <p>there will be no type error.</p>
  <p>My question is why <code>List Set</code> is not a valid type when <code>map-1</code> is used in <code>Relation</code> ?</p>
  <p>It works well in the definition of <code>map-1</code> and in other cases such as in the heterogeneous list:</p>
  <pre><code>data HList : (List Set) → Set where
    [] : HList []
    _∷_ : {A : Set}{xs : List Set} → A → HList xs → HList (A ∷ xs)
  </code></pre>