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't be injective even if Agda did have some notion of that, because the same type might have multiple orderings). I'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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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, \<= to <=, \:: to ::, \sqcup to max<br>
):<br>
<br>
data OrderedNatList? : List Nat -> Set<br>
where<br>
nil : OrderedNatList? []<br>
single : (x : Nat) -> OrderedNatList? (x :: [])<br>
cons : (x y : Nat) -> (xs : List Nat) -> x <= y -><br>
OrderedNatList? (y :: xs) -> 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' is type-checked.<br>
<br>
open DecTotalOrder<br>
<br>
data OrderedList? {c l1 l2 : Level} {ord : DecTotalOrder c l1 l2} :<br>
List (Carrier ord) -> Set (suc (max c (max l1 l2)))<br>
where<br>
nil : OrderedList? []<br>
single : (x : Carrier ord) -> OrderedList? (x :: [])<br>
cons : (x y : Carrier ord) -> (xs : List (Carrier ord)) -><br>
_<=_ ord x y -><br>
OrderedList? (y :: xs) -><br>
OrderedList? (x :: y :: xs)<br>
<br>
About `cons', the checker reports "Unsolved metas"<br>
-- which is only due to the line ``OrderedList? (y :: xs) ->''<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>