Почему мы не можем определить закрытые семейства данных?

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. Я понятия не имею, если проверка типа / вывод будет оставаться разрешимым с таким расширением.

Семейства типов, напротив, не содержат конструкторов значений, поэтому эта проблема не возникает.