Type of callcc (Programming Languages)

The monad of continuations defines

M α = (α → Answer) → Answer

and with this definition of M, I said that callcc has type

callcc :: ((α → M β) → M α) → M α

So expanding the definition of M, that becomes

callcc :: ((α → (β → Answer) → Answer) → (α → Answer) → Answer) → (α → Answer) → Answer

Its definition is

callcc g k = g h k where h x k' = k x

This function therefore does have the desirable property that its type is longer than its definition. To check that the type follows from the definition, we should first observe that (for fixed α and β), g and k have the types

g :: (α → (β → Answer) → Answer) → (α → Answer) → Answer
k :: α → Answer

So the local function h has the type α → γ → Answer for any type γ, because it ignores its argument k'. In particular, we can give it the type

h :: α → (β → Answer) → Answer.

Thus g h has type (α → Answer) → Answer, and g h k has type Answer as required.