Simon Peyton-Jones
There is a little, ill-documented, sub-kind hierarchy in GHC. I'm trying
possible, and it is much less important than it used to be. It's always been
hard to get rid of it as much as 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