[Agda] The sort of a datatype cannot depend on its indices

[Chris Casinghino]

Hi all,

I triggered the error in the subject line by trying to define a
datatype whose Sort depended on one of its indices.  I'm curious about
this restriction: is there a theoretic reason for it or was it just a
matter of convenience in the implementation.


The longer story, which you can safely ignore unless you're very
curious about how this came up:

I defined a universe to represent some of the Agda "kinds" at each
level and an interpretation function for these codes.  Here ⋆ is meant
to represent "Set l" for any Level l.

  data Kind : Level → Set where
    ⋆    : ∀ {l} → Kind l
    _⇒_  : ∀ {l1 l2} → Kind l1 -> Kind l2 -> Kind (l1 ⊔ l2)

  ⟦_⟧ : {l : Level} → Kind l → Set (suc l)


I made a type for lists of codes:

  Ctx : Set
  Ctx = List (Σ Level Kind)


Then I wanted to define a datatype which would hold an element of each
kind listed:

  maxlevel : Ctx → Level
  maxlevel [] = zero
  maxlevel ((l , _) ∷ c) = l ⊔ (maxlevel c)

  data Env : (c : Ctx) → Set (suc (maxlevel c)) where
    []   : Env []
    _∷_  : ∀ {l k G} → ⟦ k ⟧ → Env G
         → Env ((l , k) ∷ G)

But Agda gave the error:

  The sort of Env cannot depend on its indices

There are certainly ways to work around this.  For example, I can
define a type like Env with a function:

  Env : (c : Ctx) → Set (suc (maxlevel c))
  Env [] = Set  --unimportant
  Env ((l1 , k) ∷ c) = ⟦ k ⟧ × Env c

But I'm more interested in the general question of the restriction
than how best to deal with it.

Thanks!

--Chris Casinghino