[Agda] generic type recursion

[Serge D. Mechveliani]

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.

Please, how to fix this?

Thank you in advance for explanation,

------
Sergei