如何证明单射类型族（Injective Type Family）的类型参数等价？

问题解答 #

你写的这个unsafeCoerce用法是完全安全的，前提是你声明的类型族确实满足单射性（也就是你代码里写的| b -> a注解符合实际定义）。

原理说明 #

• GHC的类型检查器目前不会自动利用类型族的单射注解推导参数等价：哪怕你已经声明了MyTF a = b | b -> a，当你拿到MyTF a :~: MyTF b的证明时，GHC也不会自动得出a :~: b，这是现有类型系统实现的限制，而非逻辑上不成立。
• 单射类型族的定义本身就保证了：只要输出类型相等，输入类型必然相等，因此你用unsafeCoerce转换Refl的语义是完全合法的，不会引入运行时错误，也不会破坏类型一致性。

优化建议 #

• 你可以给这个函数加上INLINE编译指示，消除仅有的函数调用开销，毕竟这个转换是零成本的类型层面操作：

type family MyTF a = b | b -> a
...

coerceTypeFamily :: (MyTF a :~: MyTF b) -> (a :~: b)
coerceTypeFamily Refl = unsafeCoerce Refl
{-# INLINE coerceTypeFamily #-}

• 为了避免误用，建议不要把这个函数导出到模块外部，仅在模块内部作为基础工具使用，上层只导出你基于它封装的安全接口即可。如果后续GHC版本原生支持单射类型族的参数等价推导，你可以直接替换掉这部分实现，上层代码不需要做任何修改。

内容的提问来源于stack exchange，提问作者Josh.F