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在Prelude，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找不到为Num类型定义的函数compare。

我很困惑，有什么提示吗？

Answer 1

compare的类型要求x与0的类型*相同，但您尚未指定。请尝试

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

*或者有适当的转换。我不太明白这是如何工作的，但是Num似乎就足够了，可能是因为fromInteger将0转换为elem类型