How to use `deriving` in Idris?

Question

I'm trying to deriving Show, Eq, Ord etc in Idris, but none of the following trials works:

trail #1:

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show)

got:

deriving.idr:5:15-18:
  |
5 |     deriving (Show)
  |               ~~~~
When checking type of Main.Add:
Type mismatch between
        Type -> Type (Type of Show)
and
        Type (Expected type)

trail #2:

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show _)

got:

*deriving> Lit 1
Lit 1 : Expr
*deriving> Add (Lit 1) (Lit 1)
(input):Can't infer argument ty to Add, Can't infer argument deriving to Add

trail #3:

data Expr =
      Lit Int
    | Neg Expr
    | Add Expr Expr
    deriving (Show Expr)

got:

*deriving> Lit 1
Lit 1 : Expr
*deriving> Add (Lit 1) (Lit 1)
(input):Can't infer argument deriving to Add

I have searched the keyword deriving on http://docs.idris-lang.org/ and google, and even in the idris-dev repo under test/ directory, but there is no demo for the usage of deriving in idris. Anyone can help?

Answer 1

You can use Stefan Hoeck's idris2-sop library to generate implementations with elaborator reflection.