写一个不可满足的约束的好方法？

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 _ _ = ()