[Agda] `using (DecTotalOrder)'

[Serge D. Mechveliani]

On Tue, Oct 09, 2012 at 11:46:12AM +0200, Dominique Devriese wrote:
> 2012/10/9 Serge D. Mechveliani <mechvel at botik.ru>:
[..]
> > Question 2:
> > how to omit here the argument  ord  in  ``_<=_ ord x y''  ?
> > For it is said that  dep.records + hidden agruments  stands for type
> > classes.
> 
> Please refer to the following part of the manual on the wiki:
> 
>   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ModellingTypeClassesWithInstanceArguments



First, I write

----------------------------------------------------------
open import Level ...
open import Relation.Nullary using ( Dec; yes; no )
open import Relation.Binary  using ( DecTotalOrder; module DecTotalOrder )
...
open DecTotalOrder  -- **
data OrderedList? {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2) :
                  List $ Carrier ord -> Set $ L-suc $ max c $ max l1 l2
  where
  ...
  cons : let A = Carrier ord
         in
         (x y : A) -> (xs : List A) -> 
         _<=_ ord x y ->               -- **
         OrderedList? ord (y :: xs) -> OrderedList? ord (x :: y :: xs)
------------------------------------------------------------------------

(I rename for this letter  \<=  to  <= ). 
And it works.
Then I need to replace   _<=_ ord x y   with   x <= y.
I write

  open DecTotalOrder {{...}}  -- **
  data OrderedList? {c l1 l2 : Level} (ord : DecTotalOrder c l1 l2) :
                  List $ Carrier ord -> Set $ L-suc $ max c $ max l1 l2
    where
    ...
    cons : let A = Carrier ord
           in
           (x y : A) -> (xs : List A) -> x <= y ->   -- **
           OrderedList? ord (y :: xs) -> OrderedList? ord (x :: y :: xs)

And the type checker report is

  Panic:  Unbound name:  OrdList.OrderedList? [0,57]@197591509
  when checking that  ord  are valid arguments to a function of type
  ({{ : DecTotalOrder (_55 ord) (_56 ord) (_57 ord)}} Б├▓
   Set (_55 ord))
 
Probably I am missing something.
On the other hand, `panic' is discovered.

Thanks,
Sergei