You have made an invalid assumption that there exists a semantics for type-level reduction in Haskell. There doesn't. Without such a well-defined evaluation order, it's hard to talk about lifted kinds vs. unlifted kinds. Perhaps another way of slicing this exists, though. Does #7259 (https://ghc.haskell.org/trac/ghc/ticket/7259) solve your problem? I think so. Unfortunately, I've listed that as "Rocket Science" on my list of tickets that I'm interested in. Richard On Mar 18, 2016, at 5:25 PM, David Feuer wrote:

At present, currying and uncurrying at the type level doesn't seem to work terribly well. In particular, the kinds

(a, b) -> c

and

a -> b -> c

aren't really isomorphic, because (a, b) can be stuck. This makes some things (like expressing Atkey-style indexed functors in terms of McBride-style ones) rather awkward, and difficult or impossible to really get quite right. The thought came to me that maybe we could allow unlifted tuples to be promoted. Then something of the kind (# a, b #) would unconditionally unify with '(# a, b #). The restrictions on how values of unlifted tuple types can be used would presumably translate directly to restrictions on how types of unlifted tuple kind can be used.

David Feuer _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs