Although I've never seen a function declaration like this, but I think I get it. Because f :: (a, c) -> (b, c) then then loop f :: ((a, c) -> (b, c)) -> (a -> b) which is the same as  ((a, c) -> (b, c)) -> a -> b.

However, I don't see where the c comes from in f (a,c). Is this a mistake or am I missing something? A friend of mine realized that this is just a recursive definition so f (a, c) == f (a, snd $ f (a, snd $ f (a, ...))). I don't really understand this definition. I can see how it compiles, but I don't see how it would ever produce a legitimate value. Do I have to assume that f never evaluates the second element in the pair and just passes it through?