Specifying Kinds of Types

[Koen Claessen]

Ashley Yakeley wondered:

 | 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;
 |
 | Actually, I wanted p and q to both have kind '* -> *'.

The following workaround might be useful in this case:

  data CMap0 p q = MkCMap0
                 | DummyConstructor (p Int) (q Int)

But that doesn't help with the following example:

 |     type Composer c = forall x y z. (c y z) -> (c x y) -> (c x z);
 |
 | [..x..y..z..] But I wanted them to have kind '* -> *'.

Here, you might do the following trick:

  type HasKind_Help         x dummy = x
  type HasKind_Star_To_Star x       = HasKind_Help x (x Int)

  type C c x y = c (HasKind_Star_To_Star x)
                   (HasKind_Star_To_Star y)

  type Composer c =
    forall x y z . C c y z -> C c x y -> C c x z

(not tested!) There might be an easier workaround, too, but
you get the idea.

/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.