为什么我们不能定义封闭的数据族？

Question

以下所有工作：

{-# LANGUAGE TypeFamilies #-}

type family TF a
type instance TF Int = String
type instance TF Bool = Char

data family DF a
data instance DF Int = DFInt String
data instance DF Bool = DFBool Char

type family CTF a where
  CTF Int = String
  CTF Bool = Char
  CTF a = Double     -- Overlap OK!

...但这不是（从 GHC-8.2 开始）：

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

wtmpf-file24527.hs:16:19: error: parse error on input ‘where’
   |
16 | data family CDF a where
   |                   ^^^^^

只是没有人费心去实现它，还是有什么特殊原因导致关闭数据系列没有意义？我有一个数据系列，我希望保持注入性，但也有机会制作一个不相交的包罗万象的实例。现在，我认为完成这项工作的唯一方法是

newtype CDF' a = CDF' (CTF a)

Answer 1

（这里我只是猜测，但我想分享一下这个想法。）

假设我们可以写

data family CDF a where
  CDF Int = CDFInt String
  CDF Bool = CDFBool Char
  CDF a = CDFOther Double

现在，这个定义引入的值构造函数的类型是什么？我很想说：

CDFInt   :: String -> CDF Int
CDFBool  :: Char   -> CDF Bool
CDFOther :: Double -> CDF a

...但是最后一个感觉很不对劲，因为我们会得到

CDFOther @ Int :: Double -> CDF Int

这是不允许的，因为在一个封闭数据系列中，人们会期望CDF Int的（非底部）值必须以CDFInt构造函数开头。

也许合适的类型是

CDFOther :: (a /~ Int, a /~ Bool) => Double -> CDF a

涉及“不平等约束”，但这需要 GHC 中当前可用的更多打字机器。我不知道类型检查/推理是否可以通过这样的扩展来确定。

相比之下，type 系列不涉及值构造函数，因此不会出现此问题。