[Haskell] Boxing (Day) Question

[Ashley Yakeley]

As I understand it, with unboxing switched on (->) actually has this 
kind:

  (->) :: ? -> ? -> *

Reading the Core specification, GHC has a particular kind of 
"polykindism" which introduces kind "?", and defines specialisation such 
that "?" may be replaced by "*" or "#" inside any kind. Accordingly, 
(->) may be specialised:

  (->) :: * -> * -> *
  (->) :: # -> * -> *
  (->) :: * -> # -> *
  (->) :: # -> # -> *

Examples:

  module Boxing where
  import GHC.Exts

  fooSS :: (->) Int Int
  fooSS 3 = 5
  fooSS _ = 2

  fooHS :: (->) Int# Int
  fooHS 3# = 5
  fooHS _ = 2

  fooSH :: (->) Int Int#
  fooSH 3 = 5#
  fooSH _ = 2#

  fooHH :: (->) Int# Int#
  fooHH 3# = 5#
  fooHH _ = 2#

  type Fun = (->)

  fooHH' :: Fun Int# Int#
  fooHH' 3# = 5#
  fooHH' _ = 2#

Do any other type constructors or symbols have a kind with "?" in it?

I like the "kind" approach to unboxed types. It automatically rules out 
"[Int#]" by kind mismatch, for instance. But I was disappointed I 
couldn't do this with GHC 6.4.1:

  data MyC s = MkMyC (s Int# Int)

or

  class C s where
      c :: s Int# Int

(in either case: "Kind error: Expecting kind `k_a19o', but `Int#' has 
kind `#' In the class declaration for `C'")

There's no kind mismatch here, merely a restriction that the kinds of 
arguments to classes be #-free. I can't do this, either:

  newtype MyD (u :: #) = MkMyD (u -> Bool)

GHC actually complains about parsing the kind signature.

Would Bad Things Happen if this restriction were lifted? I don't have a 
pressing need for it actually, though this might be useful:

  class Boxed (b :: *) (u :: #) | b -> u, u -> b where
      box :: u -> b
      unbox :: b -> u

In case you're worried, lifting the restriction would NOT allow 
uncompilable things such as

  newtype MyE (u :: #) = MkMyE u

...simply because there's already a straightforward restriction that 
values in type constructors have types of kind "*". It is merely the 
notion of "#-freeness" that seems unnecessary. It would, however, allow 
this:

  newtype Box (u :: #) = MkBox (() -> u)

...and quite possibly this:
 
  newtype Value (x :: ?) = MkValue (() -> x)  

I believe these can be compiled safely?

-- 
Ashley Yakeley, Seattle WA