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