[Haskell-cafe] Why can't I promote data family constructors, and what to do instead?

[Tom Ellis]

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.html

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