Hello Cafe, I'm confused why I can't promote data family constructors, and what I should do instead. This message is a literate Haskell file.

{-# LANGUAGE DataKinds #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-}

I can promote constructors of normal data types nicely, here CT1 is promoted

data T = CT1 Char type PT1 = CT1 'x'

Suppose I want to promote constructors of a "non uniform" data definition, that is one where the structure of the type depends on a type argument, In Haskell that means a GADT, type family or data family. For my purposes a type family is unsuitable. I need to be able to reference it unsaturated. A GADT is also unsuitable because it introduces extra runtime tags that I don't want. But nor do data families work because their constructors can't be promoted.

data family DF a newtype instance DF Int = CDFInt1 Char data instance DF Bool = CDFBool1 | CDFBool2

-- • Data constructor ‘CDFInt1’ cannot be used here -- (it comes from a data family instance) -- type PDF = CDFInt1 'x'

The GHC users guide says Data family instance constructors cannot be promoted at the moment. GHC’s type theory just isn’t up to the task of promoting data families, which requires full dependent types. https://downloads.haskell.org/ghc/9.6.2/docs/users_guide/exts/data_kinds.htm... I'm puzzled about why I can't do that. I can do this

newtype DFInt = CDFInt1' Char data DFBool = CDFBool1' | CDFBool2' type family TF a type instance TF Int = DFInt type instance TF Bool = DFBool type PNF1 :: TF Int type PNF1 = CDFInt1' 'x'

which I said above is unsuitable because I can't refer to `TF` unsaturated. But I can apply a standard trick of wrapping a type family in a newtype:

newtype NF a = CNF (TF a) type PNF :: NF Int type PNF = CNF (CDFInt1' 'x')

Problem solved! But this goes all round the houses. What a mess! The data family version would be much neater if it worked. I have two questions: 1. Is this restriction *really* necessary? I'm surprised that GHC can't cope with promoting constructors of data families given that it is straightforward to simulate the desired behaviour with type families and a newtype. 2. Is my encoding the simplest that I can achieve? Note that the following GADT does *not* work because `GDFInt` has an unnecessary tag.

data GF a where GDFInt :: Char -> GF Int GDFBool1 :: GF Bool GDFBool2 :: GF Bool