如何为类函数添加等式约束并使Haskell代码通过类型检查？

你的代码无法通过类型检查的核心问题是实例约束中包含未在实例头声明的自由类型变量，同时需要调整约束的表达逻辑。以下是修正后的代码和解释：

修正后的代码 #

class ProblemC c where
  data ProblemData c :: * -> *
  embedC :: (ProblemData c x ~ x) => x -> c x

data TestThing a f
  = TestA a
  | TestB f
  deriving Functor

instance ProblemC (TestThing a) where
  data ProblemData (TestThing a) b = TestData a
  embedC = TestA

关键修正点说明 #

1. 移除非法的实例约束
   原代码中instance (ProblemData (TestThing a) x ~ a) => ProblemC (TestThing a)的约束包含自由变量x，这违反了Haskell的实例规则：实例的约束只能引用实例头中明确声明的类型变量（此处只有a）。

2. 利用类约束自动推导类型等价性
   类定义中embedC的约束(ProblemData c x ~ x)会自动生效：对于TestThing a实例，ProblemData (TestThing a) x的类型是a，因此约束等价于x ~ a。这意味着只有当输入值的类型为a时，才能调用embedC，完全符合你的需求。

3. 构造器类型自动适配
   TestA的类型是a -> TestThing a f，由于约束推导得出x ~ a，f会被自动实例化为x（即a），最终TestA的类型适配为a -> TestThing a a，完美匹配embedC的类型签名x -> c x（c x即TestThing a x）。

内容的提问来源于stack exchange，提问作者sfultong