Haskell type-level-sets库Subset类型类的子集传递性如何实现？

方案1：用安全的unsafeCoerce注入传递性证明 #

你碰到的问题根源是type-level-sets库的Subset类型类只提供了基础的「逐个元素检查成员」的实例，没有内置代数性质推导，直接加全局传递性实例会和库的基础实例重叠，导致GHC实例搜索混乱。

由于子集传递性在逻辑上是必然成立的，你可以通过辅助函数手动给GHC补充这个证明，这种用法的unsafeCoerce是完全安全的，因为仅用来传递编译期约束，不会产生运行时代价：

{-# LANGUAGE ScopedTypeVariables #-}
import Unsafe.Coerce

-- 传入两个子集约束，导出传递后的子集约束
withSubsetTrans :: forall s t v r. (Subset s t, Subset t v) => (Subset s v => r) -> r
withSubsetTrans k = unsafeCoerce (\_ -> k) ()

你只需要在_clique的SendInt分支调用这个辅助函数即可：

_clique (SendInt l) = withSubsetTrans @recipients @clq @parties $ sendInt l

如果GHC无法自动推断类型参数，配合ScopedTypeVariables扩展显式标注即可。

方案2：封装自定义集合性质证明 #

如果你后续还需要更多集合性质（比如两个子集的并集仍是父集的子集），可以用同样的思路批量封装辅助函数：

import Data.Type.Set (Union)

withUnionSubset :: forall s t v r. (Subset s v, Subset t v) => (Subset (Union s t) v => r) -> r
withUnionSubset k = unsafeCoerce (\_ -> k) ()

所有这类函数的安全性都由你保证逻辑上的集合性质成立即可，不需要依赖GHC的实例搜索。

方案3：换用支持代数推导的类型级集合库 #

如果不想接触unsafeCoerce，可以换用singletons-base里的类型级集合实现，或者使用effectful生态下相关的类型级集合封装，这些库普遍内置了更多集合代数性质的内置推导，不需要手动补充证明。

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