Idris: issue with Ord/Num

Question

I have a very simple example, as a demonstration of how to use case _ of that does not type check and I am not able to understand what the issue is:

data ZeroOrSign = Zero | Pos | Neg

sign : Ord elem => elem -> ZeroOrSign
sign x = case compare x 0 of
            LT => Neg
            EQ => Zero
            GT => Pos

The function compare is defined in Prelude, compare : Ord ty => ty -> ty -> Ordering where Ordering is just LT, EQ and GT. The error I get is the following:

When checking right hand side of sign with expected type
        ZeroOrSign

When checking an application of function Prelude.Interfaces.compare:
        Ord elem is not a numeric type

If I try to define sign : Num elem => elem -> ZeroOrSign then of course this creates issues as idris cannot find a function compare defined for Num types.

I am puzzled, any hint?

joel joel · Accepted Answer · 2020-05-23T22:13:16

compare's type requires x is of the same type* as 0, which you haven't specified. Try

sign : (Ord elem, Num elem) => elem -> ZeroOrSign

* or there are appropriate conversions. I don't quite understand how this works, but Num appears to suffice, perhaps due to fromInteger converting the 0 to be of type elem

Idris: issue with Ord/Num

1 Answers