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 <[email protected]> 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
