Promotion of complex GADT

Question

I recently discussed with -XDataKinds, and I was wondering why the Foofollowing will not be automatically advertised:

{-# 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, it Bazis a heterogeneous list Foo awhere alimited Bar.

Is there a way to manually create an advanced version of this data type? How can i do this? Can species be declared? Can I make a dummy version of Haskell98 Fooand split it into a module or something else? Ideally, I would like to keep the context of the constraint, but I don't think there is a sort Constraint. Any ideas would be very helpful!