haskell - 编写不可满足约束的好方法？

Question

我发现自己在写这个:

data T1
data T2

type Unsatisfiable = T1 ~ T2

所以我可以做这样的事情:

type family NEq t1 t2 :: Constraint where
  NEq t t = Unsatisfiable
  NEq _ _ = ()

type HasProxyT t = NEq t (ProxyT t)

然后我可以使用 HasProxyT 限制默认方法在代理类型与其自身相同时不循环(不会阻止两个实例循环到彼此的默认方法，但您可以做这种事一定很蠢)。

但是Unsatisfiable的定义看起来有点难看？有没有更好的方法来定义Unsatisfiable，或者这就是它的完成方式？

Answer 1

在最新版本的 GHC 上，您可以使用 TypeError :

import GHC.TypeLits 

type Unsatisfiable = TypeError ('Text "oops")

但是，我建议您直接在使用站点上使用 TypeError 并给出自定义错误消息:

type family NEq t1 t2 :: Constraint where
  NEq t t = TypeError ('Text "Expected a type distinct from " ':<>: 'ShowType t)
  NEq _ _ = ()