I can agree that for a functional language, being able to apply any reasonable function to any reasonable matching argument has to be doable, but such a fundamental operation surely needs to be simple to describe?
But it is already rather simple conceptually, it's just that Haskell's kind signature syntax makes it look hairy. I mean, if you squint enough, this: ($) :: forall (r :: RuntimeRep) (a :: *) (b :: TYPE r). (a -> b) -> a -> b could be written like: ($) :: RuntimeRep r => (a :: TYPE Lifted) (b :: TYPE r). (a -> b) -> a -> b or like I've previously suggested (if * is the default kind and wildcards are allowed in kinds): ($) :: forall a (b :: TYPE _). (a -> b) -> a -> b I mean, perhaps the syntax could be improved, but the information that: * a is lifted and boxed * b can have any kind that has a runtime representation (so unlifted and unboxed types are ok, but data kinds are not) has to go somewhere if the ability to write levity-polymorphic functions is to be given to the user, rather than only available as a one-off hack in the compiler. Perhaps going fully dependently typed and giving up on the distinction between values and types would change that; I'm not sure how for example Idris would handle levity polymorphism. Best regards, Marcin Mrotek