<div dir="ltr">I finally resolved my confusion over how 'instances' are found but now I'm having another issue I can'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 -> t -> Bool</div><div>|</div><div>| record Ord {a : Set} (A : Eq a) : Set where<br>
</div><div>| field _<_ : A -> A -> Bool</div><div><br></div><div>fails with the error message:<br></div></div><div><br></div><div><div>Eq a !=< 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 'Eq (t : Set) : Set' to 'Eq (t:Set) : Set_2' and the error message becomes 'Eq a !=< Set'. Could anyone explain what's going on here?</div><div><br></div>
</div>