Idris - Eq for enumerated type

Question

Suppose I have an enumerated type like

data MyType
    = One
    | Two
    | Three
    ...
    | Ten

and I would like to implement the Eq interface for it. I could do it as follows

Eq MyType where
    One == One = True
    Two == Two = True
    ...
    Ten == Ten = True
    _ == _ = False

but this looks tedious.

Is there a better and more coincise way to do this in Idris?

Answer 1

You're looking for instance/implementation deriving for Idris.

There's a "Derive all the instances" project, which seems to have a working solution for Eq (see examples at the end of the file). However, it'll probably not be maintained in the future. There's a newer project in the works which also spans Eq, but still has to be completed.