Hi Ashley, If you don't want to build ghc, or would rather use hugs, here's a (dirty) trick which John Hughes used in his "restricted data types" paper (I hope I recall correctly) to specify kinds. For your first example, you can write: data CMap0 p q = MkCMap0 | CMap0_Unused (p Int) (q Int) The idea is that you never use the CMap0_Unused branch, but it tells Haskell that p and q have kind * -> *. Your code would become less efficient if what you had was a newtype. For your second example, you have to turn it into a data declaration: data Composer c = Composer (forall x y z. (c y z) -> (c x y) -> (c x z)) | Composer_Unused (c [] []) Of course, you cannot insist on Composer being a type synonym any more. Is this solution acceptable to you? - Zhanyong Wan Simon Peyton-Jones wrote:
OK, it's done. In GHC you can specify kinds in [...]
And you can put kind signatures on arbitrary types, rather like you can put type signatures on arbitrary expressions.
No kind polymorphism though!
All this is in the HEAD. You'll need to build from source to get it until we make a release.
| I'd like to be able to declare the kinds of new types and synonyms, | because sometimes Haskell can't infer them. For instance: | | data CMap0 p q = MkCMap0; | | Without evidence, Haskell assumes that p and q have kind '*' | (as per sec. | 4.6), and therefore CMap0 has kind '* -> * -> *'. Actually, I | wanted p | and q to both have kind '* -> *', giving CMap0 kind '(* -> *) | -> (* -> *) | -> *'. | | Here's another example: | | type Composer c = forall x y z. (c y z) -> (c x y) -> (c x z); | | Haskell gives x, y and z all the kind '*'. But I wanted them | to have kind | '* -> *', giving c the kind '(* -> *) -> (* -> *) -> *' and | Composer the | kind '(* -> *) -> (* -> *) -> * -> *'.