Idris：Ord / Num问题

Question

我有一个非常简单的示例，作为如何使用case _ of的示例，该示例没有键入检查，并且我无法理解问题所在：

data ZeroOrSign = Zero | Pos | Neg

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

compare功能在序言compare : Ord ty => ty -> ty -> Ordering中定义，其中Ordering仅是LT，EQ和GT。我得到的错误如下：

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

[如果我尝试定义sign : Num elem => elem -> ZeroOrSign，则当然会创建问题，因为idris无法找到为compare类型定义的函数Num。

我很困惑，有任何提示吗？