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

我发现自己在写这篇文章:

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的方法，或者这只是它的完成方式？

最佳答案

在最新版本的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 _ _ = ()