具有类型约束的 Haskell 类型族实例

我试图用类型族表示表达式，但我似乎无法弄清楚如何编写我想要的约束，并且我开始觉得这是不可能的。这是我的代码：

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Return n ~ Int) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

这一切都编译得很好，但它并没有准确表达我想要的。在约束条件下Negate的实例Evaluable，我说的是里面表达式的返回类型Negate必须是一个Int (with Return n ~ Int）这样我就可以对它调用否定，但这限制太大了。返回类型实际上只需要是一个实例Num类型类具有negate功能。那样Doubles, Integers，或任何其他实例Num也可以被否定，而不仅仅是Ints。但我不能只写

Return n ~ Num

相反，因为Num是一个类型类并且Return n是一种类型。我也不能放

Num (Return n)

相反，因为Return n是类型而不是类型变量。

我想要用 Haskell 做的事情是可能的吗？如果不是，应该是，还是我误解了它背后的一些理论？我觉得Java可以添加这样的约束。让我知道这个问题是否可以更清楚。

编辑：谢谢大家，你们的回复很有帮助，并且得到了我的怀疑。看来类型检查器无法在没有 UndecidableInstances 的情况下处理我想做的事情，所以我的问题是，我想表达的内容真的是不可判定的吗？它适用于 Haskell 编译器，但它是通用的吗？也就是说，是否存在一个约束，意味着“检查 Return n 是否是 Num 的一个实例”，这对于更高级的类型检查器来说是可判定的？

事实上，你完全可以按照你提到的做：

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}

class Evaluable c where
    type Return c :: *
    evaluate :: c -> Return c

data Negate n = Negate n

instance (Evaluable n, Num (Return n)) => Evaluable (Negate n) where
    type Return (Negate n) = Return n
    evaluate (Negate n) = negate (evaluate n)

Return n当然是一个类型，它可以是一个类的实例，就像Int能。您的困惑可能在于约束的参数是什么。答案是“任何类型正确的东西”。那种Int is *，就像是那种Return n. Num有善良* -> Constraint, so anything同类*可以作为它的论点。写是完全合法的（尽管是空洞的）Num Int作为约束，同样的方式Num (a :: *)是合法的。