[Agda] I'm having an issue modeling type classes with records

[Chris Moline]

I finally resolved my confusion over how 'instances' are found but now I'm
having another issue I can't figure out. This code:

|  module TypeClassModeling where
|
|  data Bool : Set where
|    true false : Bool
|
|  record Eq (t : Set) : Set where
|    field equal : t -> t -> Bool
|
|  record Ord {a : Set} (A : Eq a) : Set where
|    field _<_ : A -> A -> Bool

fails with the error message:

Eq a !=< Set (_20 A) of type Set
when checking that the expression A has type Set (_20 A)

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130920/97f637da/attachment.html