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!