Can a type correct function be inapplicable? (Haskell)

Here is a simple proof that a function can be inapplicable (disregarding bottoms)

data Never = Never Never

justTryIt :: Never -> ()
justTryIt _ = ()

However your function IS applicable

main = print $ foo (\c -> c ()) 3

So what is the type of that lambda?

g :: (() -> a) -> a
g = \c -> c ()

Point is you don't need a function of

g :: (a -> b) -> c

Which is uninhabited (iGnOrInG bOtToMs). The type signature is just saying you can take a function where all 3 of those type (forall a b c.) can vary. IE this works equally as well

g :: (Int -> String) -> Bool
g f = null $ f 3

main = print $ foo g "so concrete"

A function of type p1 -> p2 is impossible to write; that basically says "given any possible type, I can give you any other possible type". Good luck with that!

The type (p1 -> p2) -> t is impossible for a similar reason. However, (p1 -> p2) -> Bool is quite possible:

f :: (p1 -> p2) -> Bool
f x = True

You can write similar functions for various choices of type t. (What you can't do is write a function that can somehow return any possible t out of nothing.)

More generally, can every implementable function be successfully called? That's an interesting question. I'm not sure what the answer is. I'd love to know!

EDIT: Thinking about it... the type signature of every implementable function can be interpreted as a theorum (and the implementation of the function is in some sense a "proof" of that theorum). A function that takes another function as input is like "this theorum is true if this other theorum is true". So if you can come up with a proof that "X is true if Y is true", where Y is definitely false... then you have your implementable function that can never be called.

All of this cheerfully ignores that real Haskell has several ways to break the type system and get around these nice results. For example, the function error "banana" has type a (i.e., any possible type). So in this "cheating" sense, all Haskell functions are callable.