Hi all,<br><br>I notice that Nils has kindly made the changes to the standard library to make Relation.Unary and Induction.* universe-polymorphic! Thanks Nils! So now I have a bit of time, I'm moving ahead with my attempt to make Data.Graph.Acyclic universe-polymorphic too, and have mostly succeeded. However I encountered this strange behavior for the auxiliary function p in the preds function.<br>
<br>The original version is as follows:<div><span class="Apple-style-span" style="font-family: Times; font-size: medium; "><pre><a name="6032" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); background-color: rgb(180, 238, 180); ">preds</a><a name="6037" style="text-decoration: none; "> </a><a name="6038" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">:</a><a name="6039" style="text-decoration: none; "> </a><a name="6040" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">∀</a><a name="6041" style="text-decoration: none; "> </a><a name="6042" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">{</a><a name="6043" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6044" style="text-decoration: none; "> </a><a name="6045" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6045" class="Bound" style="text-decoration: none; color: black; ">N</a><a name="6046" style="text-decoration: none; "> </a><a name="6047" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6048" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">}</a><a name="6049" style="text-decoration: none; "> </a><a name="6050" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">→</a><a name="6051" style="text-decoration: none; "> </a><a name="6052" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1779" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">Graph</a><a name="6057" style="text-decoration: none; "> </a><a name="6058" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6045" class="Bound" style="text-decoration: none; color: black; ">N</a><a name="6059" style="text-decoration: none; "> </a><a name="6060" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6061" style="text-decoration: none; "> </a><a name="6062" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6063" style="text-decoration: none; "> </a><a name="6064" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">→</a><a name="6065" style="text-decoration: none; "> </a><a name="6066" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6067" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6067" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6068" style="text-decoration: none; "> </a><a name="6069" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">:</a><a name="6070" style="text-decoration: none; "> </a><a name="6071" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">Fin</a><a name="6074" style="text-decoration: none; "> </a><a name="6075" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6047" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6076" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6077" style="text-decoration: none; "> </a><a name="6078" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">→</a><a name="6079" style="text-decoration: none; "> </a><a name="6080" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#672" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">List</a><a name="6084" style="text-decoration: none; "> </a><a name="6085" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6086" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#967" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">Fin′</a><a name="6090" style="text-decoration: none; "> </a><a name="6091" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6067" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6092" style="text-decoration: none; "> </a><a name="6093" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">×</a><a name="6094" style="text-decoration: none; "> </a><a name="6095" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6043" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6096" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6097" style="text-decoration: none; ">
</a><a name="6098" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">preds</a><a name="6103" style="text-decoration: none; "> </a><a name="6104" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6104" class="Bound" style="text-decoration: none; color: black; ">g</a><a name="6105" style="text-decoration: none; "> </a><a name="6112" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#762" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">zero</a><a name="6116" style="text-decoration: none; "> </a><a name="6120" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">=</a><a name="6121" style="text-decoration: none; "> </a><a name="6122" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#709" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">[]</a><a name="6124" style="text-decoration: none; ">
</a><a name="6125" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">preds</a><a name="6130" style="text-decoration: none; "> </a><a name="6131" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6132" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6132" class="Bound" style="text-decoration: none; color: black; ">c</a><a name="6133" style="text-decoration: none; "> </a><a name="6134" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1847" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0); ">&</a><a name="6135" style="text-decoration: none; "> </a><a name="6136" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6136" class="Bound" style="text-decoration: none; color: black; ">g</a><a name="6137" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6138" style="text-decoration: none; "> </a><a name="6139" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6140" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#793" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">suc</a><a name="6143" style="text-decoration: none; "> </a><a name="6144" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6145" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6146" style="text-decoration: none; "> </a><a name="6147" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">=</a><a name="6148" style="text-decoration: none; ">
</a><a name="6151" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1009" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">List</a><a name="6155" style="text-decoration: none; ">.</a><a name="6156" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1009" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">_++_</a><a name="6160" style="text-decoration: none; "> </a><a name="6161" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6162" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#6139" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">List</a><a name="6166" style="text-decoration: none; ">.</a><a name="6167" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#6139" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">gfilter</a><a name="6174" style="text-decoration: none; "> </a><a name="6175" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6176" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">p</a><a name="6177" style="text-decoration: none; "> </a><a name="6178" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6179" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6180" style="text-decoration: none; "> </a><a name="6181" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1474" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">$</a><a name="6182" style="text-decoration: none; "> </a><a name="6183" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#1366" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">successors</a><a name="6193" style="text-decoration: none; "> </a><a name="6194" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6132" class="Bound" style="text-decoration: none; color: black; ">c</a><a name="6195" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6196" style="text-decoration: none; ">
</a><a name="6209" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6210" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1321" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">List</a><a name="6214" style="text-decoration: none; ">.</a><a name="6215" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.List.html#1321" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">map</a><a name="6218" style="text-decoration: none; "> </a><a name="6219" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6220" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#1699" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">Prod</a><a name="6224" style="text-decoration: none; ">.</a><a name="6225" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#1699" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">map</a><a name="6228" style="text-decoration: none; "> </a><a name="6229" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">suc</a><a name="6232" style="text-decoration: none; "> </a><a name="6233" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1007" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">id</a><a name="6235" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6236" style="text-decoration: none; "> </a><a name="6237" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Function.html#1474" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">$</a><a name="6238" style="text-decoration: none; "> </a><a name="6239" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6032" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">preds</a><a name="6244" style="text-decoration: none; "> </a><a name="6245" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6136" class="Bound" style="text-decoration: none; color: black; ">g</a><a name="6246" style="text-decoration: none; "> </a><a name="6247" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6144" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6248" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6249" style="text-decoration: none; ">
</a><a name="6252" class="Keyword" style="text-decoration: none; color: rgb(205, 102, 0); ">where</a><a name="6257" style="text-decoration: none; ">
</a><a name="6260" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">p</a><a name="6261" style="text-decoration: none; "> </a><a name="6262" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">:</a><a name="6263" style="text-decoration: none; "> </a><a name="6264" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">∀</a><a name="6265" style="text-decoration: none; "> </a><a name="6266" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">{</a><a name="6267" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6268" style="text-decoration: none; "> </a><a name="6269" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">:</a><a name="6270" style="text-decoration: none; "> </a><a name="6271" class="PrimitiveType" style="text-decoration: none; color: rgb(0, 0, 205); ">Set</a><a name="6274" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">}</a><a name="6275" style="text-decoration: none; "> </a><a name="6276" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">{</a><a name="6277" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6278" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">}</a><a name="6279" style="text-decoration: none; "> </a><a name="6280" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6281" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6281" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6282" style="text-decoration: none; "> </a><a name="6283" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">:</a><a name="6284" style="text-decoration: none; "> </a><a name="6285" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">Fin</a><a name="6288" style="text-decoration: none; "> </a><a name="6289" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6290" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6291" style="text-decoration: none; "> </a><a name="6292" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">→</a><a name="6293" style="text-decoration: none; "> </a><a name="6294" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6295" style="text-decoration: none; "> </a><a name="6296" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">×</a><a name="6297" style="text-decoration: none; "> </a><a name="6298" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#740" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">Fin</a><a name="6301" style="text-decoration: none; "> </a><a name="6302" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6277" class="Bound" style="text-decoration: none; color: black; ">n</a><a name="6303" style="text-decoration: none; "> </a><a name="6304" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">→</a><a name="6305" style="text-decoration: none; "> </a><a name="6306" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#323" class="Datatype" style="text-decoration: none; color: rgb(0, 0, 205); ">Maybe</a><a name="6311" style="text-decoration: none; "> </a><a name="6312" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6313" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#967" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">Fin′</a><a name="6317" style="text-decoration: none; "> </a><a name="6318" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6319" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.html#793" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">suc</a><a name="6322" style="text-decoration: none; "> </a><a name="6323" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6281" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6324" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6325" style="text-decoration: none; "> </a><a name="6326" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#792" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">×</a><a name="6327" style="text-decoration: none; "> </a><a name="6328" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6267" class="Bound" style="text-decoration: none; color: black; ">E</a><a name="6329" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6330" style="text-decoration: none; ">
</a><a name="6333" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">p</a><a name="6334" style="text-decoration: none; "> </a><a name="6335" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6335" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6336" style="text-decoration: none; "> </a><a name="6337" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6338" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6338" class="Bound" style="text-decoration: none; color: black; ">e</a><a name="6339" style="text-decoration: none; "> </a><a name="6340" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0); ">,</a><a name="6341" style="text-decoration: none; "> </a><a name="6342" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6342" class="Bound" style="text-decoration: none; color: black; ">j</a><a name="6343" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6344" style="text-decoration: none; "> </a><a name="6346" class="Keyword" style="text-decoration: none; color: rgb(205, 102, 0); ">with</a><a name="6350" style="text-decoration: none; "> </a><a name="6351" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6335" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6352" style="text-decoration: none; "> </a><a name="6353" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Fin.Props.html#2176" class="Function Operator" style="text-decoration: none; color: rgb(0, 0, 205); ">≟</a><a name="6354" style="text-decoration: none; "> </a><a name="6355" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6342" class="Bound" style="text-decoration: none; color: black; ">j</a><a name="6356" style="text-decoration: none; ">
</a><a name="6359" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">p</a><a name="6360" style="text-decoration: none; "> </a><a name="6361" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6361" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6362" style="text-decoration: none; "> </a><a name="6363" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6364" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6364" class="Bound" style="text-decoration: none; color: black; ">e</a><a name="6365" style="text-decoration: none; "> </a><a name="6366" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0); ">,</a><a name="6367" style="text-decoration: none; "> </a><a name="6368" class="DottedPattern Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">.</a><a name="6369" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6361" class="DottedPattern Bound" style="text-decoration: none; color: black; ">i</a><a name="6370" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6371" style="text-decoration: none; "> </a><a name="6372" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">|</a><a name="6373" style="text-decoration: none; "> </a><a name="6374" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#513" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">yes</a><a name="6377" style="text-decoration: none; "> </a><a name="6378" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Binary.Core.html#4468" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">refl</a><a name="6382" style="text-decoration: none; "> </a><a name="6383" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">=</a><a name="6384" style="text-decoration: none; "> </a><a name="6385" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#361" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">just</a><a name="6389" style="text-decoration: none; "> </a><a name="6390" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6391" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">zero</a><a name="6395" style="text-decoration: none; "> </a><a name="6396" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0); ">,</a><a name="6397" style="text-decoration: none; "> </a><a name="6398" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6364" class="Bound" style="text-decoration: none; color: black; ">e</a><a name="6399" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6400" style="text-decoration: none; ">
</a><a name="6403" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6260" class="Function" style="text-decoration: none; color: rgb(0, 0, 205); ">p</a><a name="6404" style="text-decoration: none; "> </a><a name="6405" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6405" class="Bound" style="text-decoration: none; color: black; ">i</a><a name="6406" style="text-decoration: none; "> </a><a name="6407" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">(</a><a name="6408" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6408" class="Bound" style="text-decoration: none; color: black; ">e</a><a name="6409" style="text-decoration: none; "> </a><a name="6410" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Product.html#509" class="InductiveConstructor Operator" style="text-decoration: none; color: rgb(0, 139, 0); ">,</a><a name="6411" style="text-decoration: none; "> </a><a name="6412" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Graph.Acyclic.html#6412" class="Bound" style="text-decoration: none; color: black; ">j</a><a name="6413" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">)</a><a name="6414" style="text-decoration: none; "> </a><a name="6416" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">|</a><a name="6417" style="text-decoration: none; "> </a><a name="6418" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Relation.Nullary.Core.html#540" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">no</a><a name="6420" style="text-decoration: none; "> </a><a name="6421" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">_</a><a name="6422" style="text-decoration: none; "> </a><a name="6427" class="Symbol" style="text-decoration: none; color: rgb(64, 64, 64); ">=</a><a name="6428" style="text-decoration: none; "> </a><a name="6429" href="http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Maybe.Core.html#391" class="InductiveConstructor" style="text-decoration: none; color: rgb(0, 139, 0); ">nothing</a></pre>
<pre><span class="Apple-style-span" style="font-family: arial; white-space: normal; font-size: small; ">So I modified it to put E and N in an arbitrary universe, and thus had to modify the p function to put E in the arbitrary universe too:</span></pre>
<pre><span class="Apple-style-span" style="font-family: sans-serif; white-space: normal; font-size: 14px; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px; "><pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; ">
<span id="li-14444-2"> <span class="n">p</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">:</span> <span class="err" style="color: rgb(48, 48, 48); ">∀</span> <span class="p">{</span><span class="n">e</span><span class="p">}</span> <span class="p">{</span><span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">E</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">:</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Set</span> <span class="n">e</span><span class="p">}</span> <span class="p">{</span><span class="n">n</span><span class="p">}</span> <span class="err" style="color: rgb(48, 48, 48); ">→</span> <span class="p">(</span><span class="n">i</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">:</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Fin</span> <span class="n">n</span><span class="p">)</span> <span class="err" style="color: rgb(48, 48, 48); ">→</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">E</span> <span class="err" style="color: rgb(48, 48, 48); ">×</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Fin</span> <span class="n">n</span> <span class="err" style="color: rgb(48, 48, 48); ">→</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Maybe</span> <span class="p">(</span><span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Fin</span><span class="err" style="color: rgb(48, 48, 48); ">′</span> <span class="p">(</span><span class="n">suc</span> <span class="n">i</span><span class="p">)</span> <span class="err" style="color: rgb(48, 48, 48); ">×</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">E</span><span class="p">)</span>
</span><span id="li-14444-3"> <span class="n">p</span> <span class="n">i</span> <span class="p">(</span><span class="n">e</span> <span class="p">,</span> <span class="n">j</span><span class="p">)</span> <span class="n">with</span> <span class="n">i</span> <span class="err" style="color: rgb(48, 48, 48); ">≟</span> <span class="n">j</span>
</span><span id="li-14444-4"> <span class="n">p</span> <span class="n">i</span> <span class="p">(</span><span class="n">e</span> <span class="p">,</span> <span class="o" style="color: rgb(48, 48, 48); ">.</span><span class="n">i</span><span class="p">)</span> <span class="o" style="color: rgb(48, 48, 48); ">|</span> <span class="n">yes</span> <span class="n">refl</span> <span class="ow" style="color: rgb(0, 0, 0); font-weight: bold; ">=</span> <span class="n">just</span> <span class="p">(</span><span class="n">zero</span> <span class="p">,</span> <span class="n">e</span><span class="p">)</span>
</span><span id="li-14444-5"> <span class="n">p</span> <span class="n">i</span> <span class="p">(</span><span class="n">e</span> <span class="p">,</span> <span class="n">j</span><span class="p">)</span> <span class="o" style="color: rgb(48, 48, 48); ">|</span> <span class="n">no</span> <span class="kr" style="color: rgb(0, 128, 0); font-weight: bold; ">_</span> <span class="ow" style="color: rgb(0, 0, 0); font-weight: bold; ">=</span> <span class="n">nothing </span>
</span></pre><div><span id="li-14444-5"><span class="n"><span class="Apple-style-span" style="font-family: arial; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small; ">y attemp which is identical to the original p, with an additional implicit argument for the level of E in its type. This fails with:</span></span></span></div>
<div><span id="li-14444-5"><span class="n"><pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; "><span id="li-14444-8"><span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Dec</span> <span class="p">(</span><span class="n">i'</span> <span class="err" style="color: rgb(48, 48, 48); ">≡</span> <span class="n">j</span><span class="p">)</span> <span class="o" style="color: rgb(48, 48, 48); ">!=<</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Level</span> <span class="kr" style="color: rgb(0, 128, 0); font-weight: bold; ">of</span> <span class="kr" style="color: rgb(0, 128, 0); font-weight: bold; ">type</span> <span class="kt" style="color: rgb(48, 48, 144); font-weight: bold; ">Set</span></span></pre>
<pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; "><font class="Apple-style-span" face="sans-serif"><span class="Apple-style-span" style="white-space: normal;">on the <span class="Apple-style-span" style="font-family: monospace; white-space: pre; "><span class="n">i</span> <span class="err" style="color: rgb(48, 48, 48); ">≟</span> <span class="n">j <span class="Apple-style-span" style="font-family: arial; white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small; ">line, supposedly in the `w' expression. I'm not really sure where `w' came from so I'm assuming it's from the desugaring of the with construct. As a workaround, if I manually make a q function that takes the Dec result of <span class="Apple-style-span" style="font-family: monospace; font-size: 14px; white-space: pre; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px; "><span class="n">i</span> <span class="err" style="color: rgb(48, 48, 48); ">≟</span> <span class="n">j <span class="Apple-style-span" style="font-family: arial; white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small; ">and matches on it, the whole thing works fine.</span></span></span></span></span></span></span></font></pre>
<pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; "><font class="Apple-style-span" face="sans-serif"><span class="Apple-style-span" style="white-space: normal;"><span class="Apple-style-span" style="font-family: monospace; white-space: pre; "><span class="n"><span class="Apple-style-span" style="font-family: arial; white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small; "><span class="Apple-style-span" style="font-family: monospace; font-size: 14px; white-space: pre; -webkit-border-horizontal-spacing: 2px; -webkit-border-vertical-spacing: 2px; "><span class="n"><span class="Apple-style-span" style="font-family: arial; white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small; ">Am I missing something?</span></span></span></span></span></span></span></font></pre>
<pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; "><font class="Apple-style-span" face="arial"><span class="Apple-style-span" style="white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small;">Thanks,</span></font></pre>
<pre style="overflow-x: auto; overflow-y: auto; padding-left: 5px; "><font class="Apple-style-span" face="arial"><span class="Apple-style-span" style="white-space: normal; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; font-size: small;">Dan</span></font></pre>
</span></span></div></span></pre></span></div>