Promoting complex GADTs

216 views Asked by At

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!

0

There are 0 answers