# [Agda] generic type recursion

Serge D. Mechveliani mechvel at botik.ru
Mon Oct 8 20:56:28 CEST 2012

```People,
I have a beginner question about a  generic ordered list  definition.

First, I write a special definition for  List Nat
(for this letter I rename the math symbols
\bn to Nat,  \<= to <=,  \:: to ::,  \sqcup to max
):

data OrderedNatList? : List Nat -> Set
where
nil    : OrderedNatList? []
single : (x : Nat) -> OrderedNatList? (x :: [])
cons   : (x y : Nat) -> (xs : List Nat) -> x <= y ->
OrderedNatList? (y :: xs) -> OrderedNatList? (x :: y :: xs)

This is a definition of what is an  ordered list of Nat elements.
I believe it looks natural. And it does work in my program.

Then, I try to generalize it from  Nat  to  DecTotalOrder
(this uses the  DecTotalOrder record  of  Standard Library).
After many attempts I have wrtitten the following code which part
before `cons' is type-checked.

open DecTotalOrder

data OrderedList? {c l1 l2 : Level} {ord : DecTotalOrder c l1 l2} :
List (Carrier ord) -> Set (suc (max c (max l1 l2)))
where
nil    : OrderedList? []
single : (x : Carrier ord) -> OrderedList? (x :: [])
cons   : (x y : Carrier ord) -> (xs : List (Carrier ord)) ->
_<=_ ord x y ->
OrderedList? (y :: xs) ->
OrderedList? (x :: y :: xs)

About `cons', the checker reports "Unsolved metas"
-- which is only due to the line  ``OrderedList? (y :: xs) ->''

(in  Agda-2.3.0.1 + MAlonzo + lib-0.6).

OrderedNatList?  uses recursion successfully,
and a generic  OrderedList?  fails to type-check.