### Re: Kind Demotion

Richard Eisenberg <eir <at> cis.upenn.edu>

2012-09-17 13:05:51 GMT

I see what you're getting at, but the problem is more fundamental than just the lack of a type *. GHC has no
notion of equality between kinds other than syntactic identity. If two kinds are other than
syntactically identical, they are considered distinct. This fact basically renders your approach
doomed to failure. Furthermore, a promoted datatype and the unpromoted datatype are distinct entities
with the same names, so you can't just use a variable both at the kind level and the type level (variable ka in
your final ConstructedT example). It is not hard to write a Demote type family that computes an unpromoted
datatype from its promoted kind, but that type family will interfere with type inference.
That's all the bad news. The good news is that some of us are working out how to extend GHC's rich notion of type
equality to the kind level, which would also allow intermingling of type- and kind-variables. We're
still a little ways out from starting to think about implementing these ideas, but there's a good chance
that what you want will be possible in the (not-so-terribly-long-term) future.
Richard
On Sep 17, 2012, at 12:41 AM, Ashley Yakeley wrote:
> TypeRep does indeed resemble * as a type.
>
> I'm working on a system for reification of types, building on my open-witness package (which is
essentially a cleaner, more Haskell-ish alternative to TypeRep).
>
> Firstly, there's a witness type to equality of types:
>
> data EqualType :: k -> k -> * where
> MkEqualType :: EqualType a a
>
> Then there's a class for matching witnesses to types:
>
> class SimpleWitness (w :: k -> *) where

(Continue reading)