<div dir="ltr">I finally resolved my confusion over how &#39;instances&#39; are found but now I&#39;m having another issue I can&#39;t figure out. This code:<div><br></div><div><div>|  module TypeClassModeling where</div><div>
|</div><div>|  data Bool : Set where</div><div>|    true false : Bool</div><div>|</div><div>|  record Eq (t : Set) : Set where</div><div>|    field equal : t -&gt; t -&gt; Bool</div><div>|</div><div>|  record Ord {a : Set} (A : Eq a) : Set where<br>
</div><div>|    field _&lt;_ : A -&gt; A -&gt; Bool</div><div><br></div><div>fails with the error message:<br></div></div><div><br></div><div><div>Eq a !=&lt; Set (_20 A) of type Set</div><div>when checking that the expression A has type Set (_20 A)</div>
</div><div><br></div><div>I can change &#39;Eq (t : Set) : Set&#39; to &#39;Eq  (t:Set) : Set_2&#39; and the error message becomes &#39;Eq a !=&lt; Set&#39;. Could anyone explain what&#39;s going on here?</div><div><br></div>
</div>