Agda Type-Checking Error

Question

I'm currently making an ordered vector datatype and I'm trying to create operations from the data type but I get an error:

(Set (.Agda.Primitive.lsuc ℓ)) != Set
when checking that the expression A has type Set ℓ

This is the datatype

module ordered-vector (A : Set) (_<A_ : A → A → ????) where

data ordered-???? : {A : Set}→ A  →  ℕ → Set where
      [] : {a : A} →  ordered-???? a 0
      _::_  : (head : A) {min : A} → {n : ℕ} → (tail : ordered-???? min n) → true (min <A head) → ordered-???? head (suc n)

And this is the operation:

[_]o???? : ∀ {ℓ} {A : Set ℓ} →  A  →   ordered-???? A 1
[ x ]o???? = x :: []

I believe the following code is more correct for the datatype. How do I retain the correctness of the cons part of the definition?

data ordered-???? {ℓ} (A : Set ℓ) : ℕ →  Set ℓ where
  [] :  ordered-???? A 0
  _::_  : (head : A) {min : A} → {n : ℕ} →  ordered-???? min n → true (min <A head) → ordered-???? head (suc n)

This is the nat module

http://lpaste.net/147233

Answer 1

First of all, the type of [_]o𝕍 doesn't make much sense, because you are passing the type of the argument (the type of x) as the index to ordered-𝕍; I believe you are trying to do

[_]o𝕍 : ∀ {ℓ} {A : Set ℓ} → (a : A) → ordered-𝕍 a 1

instead.

If you change the type of [_]o𝕍 accordingly, you will still get the error message

(Set ℓ) != Set 
when checking that the expression a has type A

and that is because your definition of [_]o𝕍 tries to be level-polymorphic, but your definition of ordered-𝕍 isn't.

You can either make [_]o𝕍 "dumber":

[_]o : ∀ {A : Set} → (a : A) → ordered a 1
[ x ]o = x ∷ []

or make ordered-𝕍 "smarter":

data ordered-𝕍 {ℓ} {A : Set ℓ} : A → ℕ → Set ℓ where
  [] : {a : A} →  ordered-𝕍 a 0
  _∷_  : (head : A) {min : A} → {n : ℕ} → (tail : ordered-𝕍 min n) → true (min <A head) → ordered-𝕍 head (suc n)

However, if you want A and _<A_ to be parameters to your module, I think this is altogether the wrong approach, and ordered-𝕍 should simply not be parametric in the choice of A at all:

module ordered-vector (A : Set) (_<A_ : A → A → 𝔹) where
  data ordered-𝕍 : A → ℕ → Set where
    [] : {a : A} →  ordered-𝕍 a 0
    _∷_  : (head : A) {min : A} → {n : ℕ} → (tail : ordered-𝕍 min n) → true (min <A head) → ordered-𝕍 head (suc n)