A value of type forall a b. Either (a -> b) a is particularly dangerous because we can pick b to be uninhabited (Void) forall a. Either (a -> Void) a

A value of type forall a b. Either (a -> b) a is particularly dangerous because we can pick b to be uninhabited (Void) forall a. Either (a -> Void) a which is the law of excluded middle, for any type we either can immediately summon an example or prove that no example exists, as having a function (A -> Void) would allow us to create a value of the uninhabited type if we had a value of A. But forall r a. Cont r (Either (a -> r) a) is fine. Let's see what happens when we set c = Void and unwrap the Cont lem : forall r a. Cont r (Either (a -> r) a) runCont lem @Void : forall a. (Either (a -> Void) a -> Void) -> Void It turns into a weird statement, a double-negation, that there exists no proof that (Either (a -> Void) a), the true LEM type, is uninhabited. Not the same as actually having such a value. Consider the challenge of constructing (Either (A -> Void) A -> Void) for different types A. Let's say you have a positive capability of generating values of type A. This is constructive proof that (A -> Void) cannot exist so you know that any caller of your function will give you (Right value) if they are capable of calling you at all. That's not particularly helpful since you're on the hook to generate an uninhabited type Void, now. Alternatively, let's say you lack a method to construct values of A. Now either you (a) never get called, (b) get called with a parameter like (Right value), proving to you that values of A exist but asking you to use one to produce a value of type Void (impossible!), or (c) you get a value of type (Left fn), which constructively proves that no values of type A can be constructed. So in this double-negative formulation, allowing for the potential that you simply never get called, nothing about this LEM-like type is problematic. But it sure looks close to something dangerous. --- You can see how this construction works by stripping away the Cont wrapper. runCont (cont f) = f runCont (cont (\c -> (c . Left) (c . Right))) = \c -> (c . Left) (c . Right) \c -> (c . Left) (c . Right) lem :: forall a . (Either (a -> Void) Void -> Void) -> Void lem c = c (Left (\x -> c (Right x))) So we see that our callback, discussed above, is always called with a value of shape (Left fn), which appears to be a constructive proof that no values of type `a` exist. It works via a trick, though. If you were to attempt to disprove the statement of that function (a -> Void) by offering it a value of type `a`, that function will just use the value you constructed and hand it back to you as (Right value), forcing you to yourself prove (a -> Void). This is messy circular logic, but common in this kind of construction. The only way to "construct a value" of Void is to somehow pass the buck and force someone else to do it. And so this formulation of "LEM" does just what it says on the tin: shows that it's impossible to prove that LEM is impossible. Any such proof can be turned against itself.