为何Haskell实现带约束的类Functor时type family可行而typeclass编译失败

核心结论 #

你的代码逻辑没有问题，这个差异是类型类和类型族的设计本质区别导致的，不是语法编写错误。 #

问题a：为什么undefined的实现可以通过编译？ #

undefined在Haskell中的类型是forall a. a，可以匹配任意类型签名，不需要消费任何上下文约束。编译器此时只需要验证实例头符合类的定义，不需要检查实现的约束匹配，所以用undefined填充的时候自然能通过。 #

问题b：为什么WFT (Set a)无法匹配Eq a约束？ #

类型类和类型族的约束推导逻辑完全不同：

• 你使用的类型族版本是类型等价定义：type instance WFTF Set a = Eq a直接声明了两个约束是完全等价的，GHC可以双向互推，只要拿到WFTF Set a就能直接当Eq a使用。
• 你编写的类型类实例instance Eq a => WFT (Set a)是单向蕴含规则：只告诉GHC「如果当前上下文有Eq a，就可以推导出WFT (Set a)」，但GHC不会默认反向成立——因为Haskell的类型类是开放世界的，编译器无法假设你后续不会添加其他WFT (Set a)的实例（比如instance Ord a => WFT (Set a)），所以无法从WFT (Set a)反推出必然存在Eq a，自然无法满足fmapSet对Eq a的要求。

修复方案 #

如果要让类型类写法正常工作，可以选择两种方案：

1. 开启UndecidableInstances扩展，在实例声明时显式带上推导需要的约束：

{-# LANGUAGE UndecidableInstances #-}
instance (Eq a, Eq b) => WFTFunctor Set where
  wftfmap = fmapSet

因为Eq a可以正向推导出WFT (Set a)，符合类签名的约束要求，GHC会允许这个实例通过。
2. 改用封闭类型类（GHC 8.10+支持），明确告诉GHCWFT类只有你定义的这一组实例，允许编译器做反向推导。

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