Haskell能否表达否定类约束（如两种类型不相同）？

在Haskell里确实能实现类似(a !~ b)的类型不等约束，标准库虽没直接提供语法，但可以通过类型级编程技巧模拟出来，核心思路是在类型相等时触发编译错误，以此反向实现不等约束。

具体实现方式 #

借助TypeError（需要启用UndecidableInstances和TypeFamilies扩展），我们可以定义一个类型家族来实现这个约束：

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

import GHC.TypeError (TypeError, Text, ShowType, (:<>:))

type family a !~ b where
  a !~ a = TypeError ('Text "类型 " ':<>: 'ShowType a ':<>: 'Text " 不能等于 " ':<>: 'ShowType b)
  a !~ b = ()

这个类型家族的逻辑很直接：

• 当a和b类型相等时，触发TypeError，编译器会抛出明确的错误提示；
• 当a和b类型不等时，约束解析为()（空约束），不会影响编译。

使用示例 #

我们可以用这个约束写一个要求参数类型不等的函数：

foo :: (a !~ b) => a -> b -> String
foo _ _ = "两个参数类型不同"

测试场景：

• foo 1 "hello" 能正常编译，因为Int和String类型不等；
• foo 1 2 会编译报错，提示类型 Int 不能等于 Int。

注意事项 #

这种实现基于Haskell的编译时类型检查，依赖封闭世界假设——只要当前上下文能确定a和b类型相等，就会触发错误。但如果类型是多态且无法确定相等性的情况（比如完全多态的a和b），编译器不会报错，因为它无法排除未来可能的类型实例。

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