Promoting complex GADTs

Question

I've been toying around with -XDataKinds recently, and was wondering why Foo below won't be automatically promoted:

{-# LANGUAGE
    GADTs
  , DataKinds
  , KindSignatures #-}

import Data.HList

data Foo a where
  Foo :: Bar a =>
         a -> Foo a

data Baz where
  Baz :: (a ~ HList (l :: [Foo *])) =>
         a -> Baz

That is, Baz is a heterogenous list of Foo a's, where a is constrained by Bar.

Is there a way to manually create a promoted version of this data type? How would I go about doing so? Can kinds be declared? Could I make a dummy Haskell98 version of Foo, and separate it into a module or something? Ideally I'd like to keep the constraint context, but I don't think there's a Constraint sort. Any ideas would be very helpful!

Unbonnet

I'm wondering if I could just (somehow) declare a kind, then make Foo the only inhabitant of it. – Unbonnet

With some small changes I got this to work. Is that the kind of thing you're looking for? I can't explain why it works, but it does compile. – Berniecebernier

Ahh, you're very correct, this is exactly what I needed. The kind signature wasn't necessary! – Unbonnet

I also had to change it to '[] instead, but again I don't know enough about DataKinds to tell you why this version works in particular. – Berniecebernier

Foo is unpromotable, since GADTs in general are unpromotable (in this specific case, it is because of the constraint). If you try :kind! 'Foo in ghci, you will see this. Foo refers to the type constructor Foo, not the data constructor, when used in Baz. Although Baz is a very boring type because HList ('[Foo b]) is essentially just Foo b, and b is existentially quantified so Baz is equivalent to data Baz = forall a . Bar a => Baz a. I don't know if this is what you want, but somehow I doubt it. – Hedve

@Hedve You're right, I didn't realize '[Foo b] was a singleton. Crud. Back to the drawing board. – Unbonnet

@AthanClark If you need a heterogeneous list of types each of which satisfies some constraint, just have an HList and a class which recurses through the list and does whatever to each element. – Hedve

@Hedve Something that worked for me, actually was to put a kind signature on l, like in my question, but make it higher kinded, then supply a parameter b and bind it to FooLike a. Phew! @Berniecebernier Would you like to issue the answer? – Unbonnet