Kindness of strangers (or strangeness of Kinds)

[AntC]

Simon Peyton-Jones <simonpj <at> microsoft.com> writes:

> 
> There is a little, ill-documented, sub-kind hierarchy in GHC.  I'm trying 
hard to get rid of it as much as
> possible, and it is much less important than it used to be. It's always been 
there, and is nothing to do with polykinds.
> 
> I've extended the commentary a bit: see "Types" and "Kinds" here
> http://hackage.haskell.org/trac/ghc/wiki/Commentary/Compiler
> 
> The ArgKind thing has gone away following Max's recent unboxed-tuples patch, 
so we now only have OpenKind
> (described on the above pages).
> 

Thank you Simon, Richard, ~d, et al (so much kindness to a stranger!)

It's not that I have a specific problem (requirement) I'm trying to solve. 
It's more that I'm trying to understand how this ladder of 
Sorts/Kinds/Types/values hangs together.

With Phantom types, we've been familiar for many years with uninhabited types, 
so why are user-defined (promoted) Kinds/Types different?

The Singletons stuff shows there are use cases for mapping from uninhabited 
types to values -- but it seems to need a lot of machinery (all those shadow 
types and values). And indeed TypeRep maps from not-necessarily-inhabited 
types to values.

Is it that we really need to implement type application in the surface 
language to get it all to come together? Then we won't need functions applying 
to dummy arguments whose only purpose is to carry a Type::Kind.

To give a tight example:

    data MyNat = Z | S MyNat                -- to be promoted

    data ProxyNat (a :: MyNat) = ProxyNat   -- :k ProxyNat :: MyNat -> *

    proxyNat :: n -> ProxyNat n             -- rejected: Kind mis-match
    proxyNat _ = ProxyNat

The parallel of that with phantom types (and a class constraint for MyNat) 
seems unproblematic -- albeit with Kind *.

Could we have :k (->) :: OpenKind -> * -> *  -- why not?


AntC