使用幻影类型时避免冗余约束

Question

这是一个简化的，也许是愚蠢的例子，说明我正在尝试编码什么(它更复杂，涉及列表长度的编译时编码)。

给定以下内容：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data D (a :: Bool) where
D :: Bool -> D a

我想要以下函数g:

g :: D a -> Bool
g (D x) = x == a

当然，这不会编译，因为a是一种类型，而不是一个值。

这里有一个可能的解决方案：

class C (a :: Bool) where
f :: D a -> Bool
instance C True where
f (D x) = x == True
instance C False where
f (D x) = x == False
g :: (C a) => D a -> Bool
g = f

但是，我必须向g添加一个约束，它看起来像a :: Bool一样是多余的，并且我已经获得了Bool的所有情况的实例。

有没有我可以写g，这样它就有签名：

g :: D a -> Bool 

即不需要额外的约束？

Answer 1

不，这是不可能的，因为我可以给您一个类型为D Any的非常好的值，其中Any定义为

type family Any :: k where {}

你能做的是编写一个更通用的类：

data SBool a where
SFalse :: SBool 'False
STrue :: SBool 'True
sBoolToBool :: SBool a -> Bool
sBoolToBool SFalse = False
sBoolToBool STrue = True
class KnownBool a where
knownBool :: SBool a
instance KnownBool 'False where
knownBool = SFalse
instance KnownBool 'True where
knownBool = STrue

当然，如果你不把这些类型用于其他任何事情，那么所有这些机器真的太夸张了。