Polymorphic kinds

[Sebastien Carlier]

Hello,

I am experimenting with GHC to write low level code (e.g., device
drivers, interrupt handlers).  The ultimate goal is to write a
prototype operating system in Haskell, using the GHC RTS as a kind of
microkernel (this appears to be relatively easy by removing all the
dependencies on an operating system, and providing a block allocator
and interval timers).

I have added the necessary primitive operations to generate privileged
instructions for IA32 to GHC, and it seems to work fine, good quality
assembly code is generated.

Now, I would like to make use of do-notation to write cleaner code
(threading a State# RealWorld through computations is quite ugly).
I want to avoid allocating memory in parts of the code, so I would
like to be able to have monadic computations which return unboxed
values.  Sadly, GHC currently does not appear to allow that.

The following example illustrates the problem:

> {-# OPTIONS -fglasgow-exts #-}
> 
> import GHC.Prim
> 
> x :: IO Int#
> x =
>     return 1#

GHC (HEAD from 2003-08-01) reports:

T.lhs:5:
    Kind error: Expecting a lifted type, but `Int#' is unlifted
    When checking kinds in `IO Int#'
    In the type: IO Int#
    While checking the type signature for `x'

T.lhs:7:
    Couldn't match `*' against `#'
    When matching types `a' and `Int#'
        Expected type: a
        Inferred type: Int#
    In the first argument of `return', namely `1#'

After looking into the problem for a while, I realized that GHC does
not have polymorphic kinds - after checking a bunch of definitions, it
"zonks" all kind variables to (Type *) and all boxity variables to *.
So IO has kind (Type * -> Type *), and cannot be applied to an unboxed
value of kind (Type #).

GHC has had explicit kind annotations for a while:
<http://www.haskell.org/pipermail/haskell/2002-February/008906.html>
So I ought to be able define an IO# type for computations that return
unboxed values.
(By the way, is there already an unboxed unit value and type?)

Strangely, GHC did not recognizes # as the kind of unlifted types, so
I added that to the compiler, and hoped that things would work out.
Well, almost.

> {-# OPTIONS -fglasgow-exts #-}
>
> import GHC.Prim
> 
> newtype IO# (a :: # ) = IO# (State# RealWorld -> (# State# RealWorld, a #))
> 
> x :: IO# Int#
> x = IO# (\ s -> (# s, 1# #))

GHC reports:

T.lhs:8:
    Illegal unlifted type argument: Int#
    In the type: IO# Int#
    While checking the type signature for `x'

The example is accepted if "newtype" is replaced by "type" (and by
removing uses of the IO# value constructor), so I can proceed with my
experiment by not using do-notation (defining return#, then#, etc
appears to work fine).

Not being able to use do-notation is slightly inconvenient; is there a
reason why newtypes cannot be applied to unlifted type arguments?

I expect that I would eventually have been beaten anyway when trying
to make an instance of the Monad type class for the above IO# newtype,
since Monad is probably regarded as a predicate of kind (* -> *) -> P
(where P would be the hypothetical kind of propositions); application
to an operator of kind (# -> *) would fail.

What would need to be done to extend the compiler so that it allows IO
computations to be able to return unboxed values?  For some reason I
am worried that "just" having polymorphic kind may not be enough.
I also fail to understand all the implications of having polymorphic
kinds, so I would greatly appreciate if one of the GHC experts could
say something about that too.

-- 
Sebastien