Can a type correct function be inapplicable? (Haskell)

Question

I have a function foo = \f x -> let c = \y -> x in f c which I have type inferenced to find :

\forall a,b,r. ((b -> a) -> r) -> a -> r.

GHCI confirms this type: foo :: ((p1 -> p2) -> t) -> p2 -> t

However, I am unable to find an applicable function that meets these parameters such that foo evaluates.

I have tried the following functions with no success:

bu :: Num a => ([Char] -> a) -> a
bu x = (x "hello") * 2 

ba :: (Fractional a1, Foldable t) => t a2 -> a1
ba x = (fromIntegral (length x) ) / 2

Another attempt was choosing the following functions:

bu :: Num a => ([Char] -> a) -> a -> a
bu x = (+ ((x "hello") * 2))

ba :: (Fractional a1, Foldable t) => t a2 -> a1
ba x = (fromIntegral (length x) ) / 2

Now I can call (bu ba) 4and get a correct result.

I understand why those don't work. The issue seems to be that in the first arguement (p1 -> p2) -> t), t would need to be a function that takes the argument p2. However, as soon as we do that the type of that function changes to something like (a -> a) and can no longer be correctly consumed by foo.

This exercise has lead me to the question; can a function with a correct type be inapplicable? My intuition leads me to believe that this is false and that an applicable input exists for any function with a valid type. Is there a proof for this?

Answer 1

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"