Nothing is constraining your recursive OrderedNatList? call to have the same DecTotalOrder as its implicit parameter, and the only part of that that appears explicitly is the Carrier (which couldn&#39;t be injective even if Agda did have some notion of that, because the same type might have multiple orderings). I&#39;d recommend making the DecTotalOrder argument explicit and then providing it for your recursive case in cons.<div>
<br></div><div>Hope this helps,</div><div>Dan<br><br><div class="gmail_quote">On Mon, Oct 8, 2012 at 2:56 PM, Serge D. Mechveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">People,<br>
I have a beginner question about a  generic ordered list  definition.<br>
<br>
First, I write a special definition for  List Nat<br>
(for this letter I rename the math symbols<br>
                 \bn to Nat,  \&lt;= to &lt;=,  \:: to ::,  \sqcup to max<br>
):<br>
<br>
  data OrderedNatList? : List Nat -&gt; Set<br>
    where<br>
    nil    : OrderedNatList? []<br>
    single : (x : Nat) -&gt; OrderedNatList? (x :: [])<br>
    cons   : (x y : Nat) -&gt; (xs : List Nat) -&gt; x &lt;= y -&gt;<br>
             OrderedNatList? (y :: xs) -&gt; OrderedNatList? (x :: y :: xs)<br>
<br>
This is a definition of what is an  ordered list of Nat elements.<br>
I believe it looks natural. And it does work in my program.<br>
<br>
Then, I try to generalize it from  Nat  to  DecTotalOrder<br>
(this uses the  DecTotalOrder record  of  Standard Library).<br>
After many attempts I have wrtitten the following code which part<br>
before `cons&#39; is type-checked.<br>
<br>
  open DecTotalOrder<br>
<br>
  data OrderedList? {c l1 l2 : Level} {ord : DecTotalOrder c l1 l2} :<br>
                    List (Carrier ord) -&gt; Set (suc (max c (max l1 l2)))<br>
       where<br>
       nil    : OrderedList? []<br>
       single : (x : Carrier ord) -&gt; OrderedList? (x :: [])<br>
       cons   : (x y : Carrier ord) -&gt; (xs : List (Carrier ord)) -&gt;<br>
                _&lt;=_ ord x y -&gt;<br>
                OrderedList? (y :: xs) -&gt;<br>
                OrderedList? (x :: y :: xs)<br>
<br>
About `cons&#39;, the checker reports &quot;Unsolved metas&quot;<br>
-- which is only due to the line  ``OrderedList? (y :: xs) -&gt;&#39;&#39;<br>
<br>
(in  Agda-2.3.0.1 + MAlonzo + lib-0.6).<br>
<br>
OrderedNatList?  uses recursion successfully,<br>
and a generic  OrderedList?  fails to type-check.<br>
<br>
Please, how to fix this?<br>
<br>
Thank you in advance for explanation,<br>
<br>
------<br>
Sergei<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>