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 typeclass IvoryType t whereivoryType :: 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 *) whereivoryArea :: 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 isdata 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 errorsrc/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 ‘AreaCould you please explain, how to express the ownership of ivoryArea function in Haskell properly ?EditSome links to the original declarations:https://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Type.hshttps://github.com/GaloisInc/ivory/blob/master/ivory/src/Ivory/Language/Area.hs

I've also tried rewriting AreaStorage as GADT with the same result

**1970年01月01日00分03秒**

I can't reproduce your result: f :: forall t . (IvoryArea t) => t get rejected by GHC for the same reason on my machine. Would you consider posting the implementation of it?

**2019年04月20日40分27秒**

Most likely your f actually has a type like forall t. (IvoryArea t) => Proxy t -> ....

**2019年04月20日40分27秒**

So... you write that you "want to store instances of IvoryArea". consider what an instance would be. In particular IvoryArea :: Area * -> GHC.Prim.Constraint. But what is a value level inhabitant of Area * ? Types that are of kinds created by DataKinds don't have inhabitants...

**2019年04月19日40分27秒**

"I mean I want to store datatypes which are instances of IvoryArea" - You can only "store" values. There seems to be some critical misunderstanding about what a "value" is. There are no values of type 'Stored Int, for example. Not even undefined, whose type is forall (a :: *) . a. Strictly speaking, values are not inhabitants of kind * - types of kind * are inhabitants of kind *. Values are inhabitants of types of kind *. You probably want to define a type indexed on Area (whose kind will be Area * -> *, perhaps, or maybe even Area k -> *).

**2019年04月20日40分27秒**

- Unusual Kinds and Data Constructors
- Type classes in Haskell data types
- Getting associated type synonyms with template Haskell
- Haskell Type vs Data Constructor
- Is it possible to get the Kind of a Type Constructor in Haskell?
- What exactly is the kind “*” in Haskell?
- Defining data types in Haskell
- Haskell cast higher kinded types
- Haskell Type Polymorphism — Mapping to String
- Haskell singletons: What do we gain with SNat
- Default values in Haskell data types

ADS