You're misplacing your quantifiers.
(a -> Void) -> Void)
is not isomorphic to
forall r. (a -> r) -> r
but *is* isomorphic to
(a -> (forall r. r)) -> (forall r. r)
...which is because you could _define_ Void to be (forall r. r): {-# LANGUAGE Rank2Types #-} newtype Void = Void {absurd :: forall r. r} In practice, Void used to be implemented as data Void = Void Void before it became just data Void by means of EmptyDataDecls extension. The latter has the advantage that there is no constructor named 'Void'. In reality of course, Void does have an element, bottom, which it shares with all other types. Hence the 'absurd' function that returns the bottom in type r when given the bottom in type Void. But as you know the correspondence between types and theorems in intuitionistic logic explicitly regards only total values. Excersise: Prove that intuitionistically, it is absurd to deny the law of excluded middle: Not (Not (Either a (Not a))) There is a whole world to be discovered beneath the total values. Think about the type () as truth values and what universal quantification could be. Olaf