Creating Haskell datatype accepting type of non-* kind in one of its constructors

Hello. I am playing with Ivory library which relies heavily on modern features of Haskell. Among others, it defines the typeclasses IvoryType accepting all types and IvoryArea accepting types of special kind Area. The definitions look like this:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}

-- | Proxy datatype with a phantom arbitrary-kinded type
-- and a single constructor 
data Proxy (a :: k) = Proxy

-- | The kind of memory-area types.
data Area k
  = Struct Symbol
  | Array Nat (Area k)
  | CArray (Area k)
  | Stored k
    -- ^ This is lifting for a *-kinded type

class IvoryType t where
  ivoryType :: Proxy t -> I.Type {- arguments are not important -}

-- | Guard the inhabitants of the Area type, as not all *s are Ivory *s.
class IvoryArea (a :: Area *) where
  ivoryArea :: Proxy a -> I.Type {- arguments are not important -}

OK. Now let's try to express the fact that we are going to store values with ivoryType function defined. Obviously, they are the memebers of IvoryType class, so the answer is

data TypeStorage = TypeStorage (forall t . IvoryType t => t)

So far so good. Now we want to store values which have ivoryArea function defined. Let's use the IvoryArea class as a filter condition, like in the prevoius case:

data AreaStorage = AreaStorage (forall t . IvoryArea t => t)

Surprisingly, the compiler (ghc version 7.8.4) outputs an error

src/IvoryLL/Types.hs:59:45:
    Expected a type, but ‘t’ has kind ‘Area *’
    In the type ‘forall t. IvoryArea t => t’
    In the definition of data constructor ‘AreaBase’
    In the data declaration for ‘Area

Could you please explain, how to express the ownership of ivoryArea function in Haskell properly ?

Edit Some links to the original declarations:

• https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Type.hs
• https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Area.hs

Now that we've established in the comments that you can't do what you want directly, which is create a special "subkind" of all types, we can use a bit more legwork to get what you want.

We just use a (closed) type family to interpret your Area * kind into something of kind * and then GADT, indexed by Area *, to hold such values. We can then wrap the whole shebang up in an existential to store arbitrary values of such a kind, if so desired.

Consider this cut down example:

data Area k
  = Stored k
  | List (Area k)

type family InterpIvoryArea a :: * where
    InterpIvoryArea (Stored k) = k
    InterpIvoryArea (List a) = [InterpIvoryArea a]

data AreaStorage a where
    AreaStorage :: InterpIvoryArea a -> AreaStorage a

data AreaStorageExistential where
    AreaStorageExistential :: AreaStorage a -> AreaStorageExistential

testValue :: AreaStorageExistential
testValue = AreaStorageExistential (AreaStorage [1,2,3] :: AreaStorage (List (Stored Int)))